rank one operators #
This defines the rank one operator $| x \rangle\!\langle y |$ for continuous linear maps
(see rank_one) and linear maps (see rank_one_lm).
def
rank_one
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
(x y : E) :
we define the rank one operator $| x \rangle\!\langle y |$ by $x \mapsto \langle y, z \rangle \cdot x$
@[simp]
theorem
rank_one_apply
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
{x y : E}
(z : E) :
β(rank_one x y) z = has_inner.inner y z β’ x
@[simp]
theorem
rank_one.smul_apply
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
{x y : E}
{Ξ± : π} :
$| x \rangle\!\langle \alpha\cdot y | = \bar{\alpha} \cdot | x \rangle\!\langle y |$
@[simp]
theorem
rank_one.apply_smul
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
{x y : E}
{Ξ± : π} :
$| \alpha \cdot x \rangle\!\langle y | = \alpha \cdot | x \rangle\!\langle y |$
@[simp]
theorem
rank_one.smul_real_apply
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
{x y : E}
{Ξ± : β} :
@[simp]
theorem
rank_one.apply_rank_one
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
(x y z w : E) :
$| x \rangle\!\langle y | | z \rangle\!\langle w | = \langle y, z \rangle \cdot | x \rangle\!\langle w |$
theorem
continuous_linear_map.comp_rank_one
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
(x y : E)
(u : E βL[π] E) :
$u \circ | x \rangle\!\langle y | = | u(x) \rangle\!\langle y |$
theorem
continuous_linear_map.rank_one_comp
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
[complete_space E]
(x y : E)
(u : E βL[π] E) :
$| x \rangle\!\langle y | \circ u = | x \rangle\!\langle u^*(y) |$
@[simp]
theorem
rank_one.is_idempotent_elem
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
(x : E)
(h : βxβ = 1) :
is_idempotent_elem (rank_one x x)
rank one operators given by norm one vectors are automatically idempotent
theorem
rank_one.is_symmetric
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
(x : E) :
β(rank_one x x).is_symmetric
@[simp]
theorem
rank_one.is_self_adjoint
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
[complete_space E]
(x : E) :
is_self_adjoint (rank_one x x)
rank one operators are automatically self-adjoint
theorem
rank_one.adjoint
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
[complete_space E]
(x y : E) :
βcontinuous_linear_map.adjoint (rank_one x y) = rank_one y x
$| x \rangle\!\langle y |^* = | y \rangle\!\langle x |$
theorem
rank_one_inner_left
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
(x y z w : E) :
has_inner.inner (β(rank_one x y) z) w = has_inner.inner z y * has_inner.inner x w
theorem
rank_one_inner_right
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
(x y z w : E) :
has_inner.inner x (β(rank_one y z) w) = has_inner.inner z w * has_inner.inner x y
theorem
continuous_linear_map.commutes_with_all_iff
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
[complete_space E]
(T : E βL[π] E) :
theorem
continuous_linear_map.centralizer
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
[complete_space E] :
theorem
continuous_linear_map.scalar_centralizer
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E] :
theorem
continuous_linear_map.centralizer_centralizer
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
[complete_space E] :
theorem
rank_one.zero_left
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
(x : E) :
theorem
rank_one.zero_right
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
(x : E) :
theorem
continuous_linear_map.ext_inner_map
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
{F : Type u_3}
[normed_add_comm_group F]
[inner_product_space π F]
(T S : E βL[π] F) :
T = S β β (x : E) (y : F), has_inner.inner (βT x) y = has_inner.inner (βS x) y
theorem
continuous_linear_map.exists_sum_rank_one
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
[finite_dimensional π E]
(T : E βL[π] E) :
β (x y : fin (finite_dimensional.finrank π E) Γ fin (finite_dimensional.finrank π E) β E), T = finset.univ.sum (Ξ» (i : fin (finite_dimensional.finrank π E) Γ fin (finite_dimensional.finrank π E)), rank_one (x i) (y i))
theorem
linear_map.exists_sum_rank_one
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
[finite_dimensional π E]
(T : E ββ[π] E) :
β (x y : fin (finite_dimensional.finrank π E) Γ fin (finite_dimensional.finrank π E) β E), T = finset.univ.sum (Ξ» (i : fin (finite_dimensional.finrank π E) Γ fin (finite_dimensional.finrank π E)), β(rank_one (x i) (y i)))
theorem
rank_one.sum_orthonormal_basis_eq_id
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
{ΞΉ : Type u_3}
[fintype ΞΉ]
(b : orthonormal_basis ΞΉ π E) :
def
rank_one_lm
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
(x y : E) :
same as rank_one, but as a linear map
Equations
- rank_one_lm x y = (rank_one x y).to_linear_map
@[simp]
theorem
rank_one_lm_apply
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
(x y z : E) :
β(rank_one_lm x y) z = has_inner.inner y z β’ x
theorem
rank_one_lm_comp_rank_one_lm
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
(x y z w : E) :
(rank_one_lm x y).comp (rank_one_lm z w) = has_inner.inner y z β’ rank_one_lm x w
theorem
rank_one_lm_apply_rank_one
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
(x y z w v : E) :
β(rank_one_lm x y) (β(rank_one_lm z w) v) = (has_inner.inner y z * has_inner.inner w v) β’ x
theorem
rank_one_lm_adjoint
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
[finite_dimensional π E]
(x y : E) :
βlinear_map.adjoint (rank_one_lm x y) = rank_one_lm y x
theorem
sum_rank_one
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
{n : Type u_3}
[fintype n]
(x : n β E)
(y : E) :
rank_one (finset.univ.sum (Ξ» (i : n), x i)) y = finset.univ.sum (Ξ» (i : n), rank_one (x i) y)
theorem
rank_one_sum
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
{n : Type u_3}
[fintype n]
(x : E)
(y : n β E) :
rank_one x (finset.univ.sum (Ξ» (i : n), y i)) = finset.univ.sum (Ξ» (i : n), rank_one x (y i))
theorem
sum_rank_one_lm
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
{n : Type u_3}
[fintype n]
(x : n β E)
(y : E) :
rank_one_lm (finset.univ.sum (Ξ» (i : n), x i)) y = finset.univ.sum (Ξ» (i : n), rank_one_lm (x i) y)
theorem
rank_one_lm_sum
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
{n : Type u_3}
[fintype n]
(x : E)
(y : n β E) :
rank_one_lm x (finset.univ.sum (Ξ» (i : n), y i)) = finset.univ.sum (Ξ» (i : n), rank_one_lm x (y i))
theorem
linear_map.ext_of_rank_one
{π : Type u_1}
{H : Type u_2}
{H' : Type u_3}
[is_R_or_C π]
[add_comm_monoid H']
[module π H']
[normed_add_comm_group H]
[inner_product_space π H]
[finite_dimensional π H]
{x y : (H βL[π] H) ββ[π] H'}
(h : β (a b : H), βx (rank_one a b) = βy (rank_one a b)) :
x = y
theorem
linear_map.ext_of_rank_one'
{π : Type u_1}
{H : Type u_2}
{H' : Type u_3}
[is_R_or_C π]
[add_comm_monoid H']
[module π H']
[normed_add_comm_group H]
[inner_product_space π H]
[finite_dimensional π H]
{x y : (H ββ[π] H) ββ[π] H'}
(h : β (a b : H), βx β(rank_one a b) = βy β(rank_one a b)) :
x = y
theorem
rank_one.sum_orthonormal_basis_eq_id_lm
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
{ΞΉ : Type u_3}
[fintype ΞΉ]
(b : orthonormal_basis ΞΉ π E) :
theorem
continuous_linear_map.coe_eq_zero
{π : Type u_1}
{Eβ : Type u_2}
{Eβ : Type u_3}
[is_R_or_C π]
[normed_add_comm_group Eβ]
[normed_add_comm_group Eβ]
[inner_product_space π Eβ]
[inner_product_space π Eβ]
(f : Eβ βL[π] Eβ) :
theorem
rank_one.eq_zero_iff
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
(x y : E) :
theorem
rank_one.left_add
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
(x y z : E) :
theorem
rank_one.right_add
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
(x y z : E) :
theorem
rank_one.left_sub
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
(x y z : E) :
theorem
rank_one.right_sub
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
(x y z : E) :
theorem
linear_map.rank_one_comp
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
[finite_dimensional π E]
(x y : E)
(u : E ββ[π] E) :
theorem
linear_map.rank_one_comp'
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
[finite_dimensional π E]
(x y : E)
(u : E ββ[π] E) :
theorem
orthonormal_basis.orthogonal_projection'_eq_sum_rank_one
{ΞΉ : Type u_1}
{π : Type u_2}
[is_R_or_C π]
{E : Type u_3}
[normed_add_comm_group E]
[inner_product_space π E]
[fintype ΞΉ]
{U : submodule π E}
[complete_space β₯U]
(b : orthonormal_basis ΞΉ π β₯U) :
orthogonal_projection' U = finset.univ.sum (Ξ» (i : ΞΉ), rank_one β(βb i) β(βb i))