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).

@[reducible, inline]

noncomputable abbrev bra (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : E →L⋆[𝕜] E →L[𝕜] 𝕜

Equations

• bra 𝕜 = innerSL 𝕜

@[simp]

theorem bra_apply_apply (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (w : E) : ((bra 𝕜) x) w = inner x w

@[simp]

theorem bra_toFun_toFun (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (w : E) : ((bra 𝕜) x) w = inner x w

@[simp]

theorem bra_toFun_apply (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (w : E) : ((bra 𝕜) x) w = inner x w

@[simp]

theorem bra_apply_toFun (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (w : E) : ((bra 𝕜) x) w = inner x w

noncomputable def ket (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : E →L[𝕜] 𝕜 →L[𝕜] E

Equations

• ket 𝕜 = { toFun := fun (x : E) => { toFun := fun (α : 𝕜) => α • x, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem ket_apply_apply (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (α : 𝕜) : ((ket 𝕜) x) α = α • x

@[simp]

theorem ket_toFun_apply (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (α : 𝕜) : ((ket 𝕜) x) α = α • x

@[simp]

theorem ket_apply_toFun (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (α : 𝕜) : ((ket 𝕜) x) α = α • x

@[simp]

theorem ket_toFun_toFun (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (α : 𝕜) : ((ket 𝕜) x) α = α • x

@[simp]

theorem ket_one_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) : ((ket 𝕜) x) 1 = x

theorem ket_RCLike {𝕜 : Type u_1} [RCLike 𝕜] (x : 𝕜) : (ket 𝕜) x = (ContinuousLinearMap.mul 𝕜 𝕜) x

theorem ContinuousLinearMap.mul_one_apply {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] : (ContinuousLinearMap.mul 𝕜 𝕜') 1 = 1

theorem ket_RCLike_one {𝕜 : Type u_1} [RCLike 𝕜] : (ket 𝕜) 1 = 1

theorem bra_RCLike {𝕜 : Type u_1} [RCLike 𝕜] (x : 𝕜) : (bra 𝕜) x = (ContinuousLinearMap.mul 𝕜 𝕜) ((starRingEnd 𝕜) x)

theorem bra_RCLike_one {𝕜 : Type u_1} [RCLike 𝕜] : (bra 𝕜) 1 = 1

theorem bra_adjoint_eq_ket {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (x : E) : ContinuousLinearMap.adjoint ((bra 𝕜) x) = (ket 𝕜) x

theorem ket_adjoint_eq_bra {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (x : E) : ContinuousLinearMap.adjoint ((ket 𝕜) x) = (bra 𝕜) x

theorem bra_ket_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : ((bra 𝕜) x).comp ((ket 𝕜) y) = (ket 𝕜) (inner x y)

theorem bra_ket_one_eq_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) (y : E) : (((bra 𝕜) x).comp ((ket 𝕜) y)) 1 = inner x y

theorem continuousLinearMap_comp_ket {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] (f : E₁ →L[𝕜] E₂) (x : E₁) : f.comp ((ket 𝕜) x) = (ket 𝕜) (f x)

theorem bra_comp_continuousLinearMap {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] [CompleteSpace E₁] [CompleteSpace E₂] (x : E₂) (f : E₁ →L[𝕜] E₂) : ((bra 𝕜) x).comp f = (bra 𝕜) ((ContinuousLinearMap.adjoint f) x)

def rankOne (𝕜 : Type u_1) {E₁ : Type u_2} {E₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] : E₁ →ₗ[𝕜] E₂ →ₗ⋆[𝕜] E₂ →L[𝕜] E₁

we define the rank one operator $| x \rangle\langle y |$ by $x \mapsto \langle y,z\rangle x$

@[simp]

theorem rankOne_apply_apply_apply (𝕜 : Type u_1) {E₁ : Type u_2} {E₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] (x : E₁) (y : E₂) (z : E₂) : (((rankOne 𝕜) x) y) z = inner y z • x

@[simp]

theorem rankOne_apply_apply_toFun (𝕜 : Type u_1) {E₁ : Type u_2} {E₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] (x : E₁) (y : E₂) (z : E₂) : (((rankOne 𝕜) x) y) z = inner y z • x

@[simp]

theorem rankOne_apply {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] {x : E₁} {y : E₂} (z : E₂) : (((rankOne 𝕜) x) y) z = inner y z • x

theorem ket_bra_eq_rankOne {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] {x : E₁} {y : E₂} : ((ket 𝕜) x).comp ((bra 𝕜) y) = ((rankOne 𝕜) x) y

theorem ket_eq_rankOne_one {𝕜 : Type u_1} {E₁ : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] (x : E₁) : (ket 𝕜) x = ((rankOne 𝕜) x) 1

theorem bra_eq_one_rankOne {𝕜 : Type u_1} {E₁ : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] (x : E₁) : (bra 𝕜) x = ((rankOne 𝕜) 1) x

@[simp]

theorem rankOne.smul_real_apply {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] {x : E₁} {y : E₂} {α : ℝ} : ((rankOne 𝕜) x) (↑α • y) = ↑α • ((rankOne 𝕜) x) y

@[simp]

theorem rankOne.apply_rankOne {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] {E₃ : Type u_4} [NormedAddCommGroup E₃] [InnerProductSpace 𝕜 E₃] (x : E₁) (y : E₂) (z : E₂) (w : E₃) : (((rankOne 𝕜) x) y).comp (((rankOne 𝕜) z) w) = inner y z • ((rankOne 𝕜) x) w

$| x \rangle\langle y | | z \rangle\langle w | = \langle y, z \rangle \cdot | x \rangle\langle w |$

theorem ContinuousLinearMap.comp_rankOne {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] {E₃ : Type u_4} [NormedAddCommGroup E₃] [InnerProductSpace 𝕜 E₃] (x : E₁) (y : E₂) (u : E₁ →L[𝕜] E₃) : u.comp (((rankOne 𝕜) x) y) = ((rankOne 𝕜) (u x)) y

$u \circ | x \rangle\langle y | = | u(x) \rangle\langle y |$

theorem ContinuousLinearMap.rankOne_comp {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] {E₃ : Type u_4} [NormedAddCommGroup E₃] [InnerProductSpace 𝕜 E₃] [CompleteSpace E₂] [CompleteSpace E₃] (x : E₁) (y : E₂) (u : E₃ →L[𝕜] E₂) : (((rankOne 𝕜) x) y).comp u = ((rankOne 𝕜) x) ((ContinuousLinearMap.adjoint u) y)

$| x \rangle\langle y | \circ u = | x \rangle\langle u^*(y) |$

theorem rankOne_self_isIdempotentElem_of_normOne {𝕜 : Type u_1} {E₁ : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] {x : E₁} (h : ‖x‖ = 1) : IsIdempotentElem (((rankOne 𝕜) x) x)

rank one operators given by norm one vectors are automatically idempotent

theorem rankOne_self_isSymmetric {𝕜 : Type u_1} {E₁ : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] {x : E₁} : (↑(((rankOne 𝕜) x) x)).IsSymmetric

@[simp]

theorem rankOne_self_isSelfAdjoint {𝕜 : Type u_1} {E₁ : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [CompleteSpace E₁] {x : E₁} : IsSelfAdjoint (((rankOne 𝕜) x) x)

rank one operators are automatically self-adjoint

theorem rankOne_adjoint {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] [CompleteSpace E₁] [CompleteSpace E₂] (x : E₁) (y : E₂) : ContinuousLinearMap.adjoint (((rankOne 𝕜) x) y) = ((rankOne 𝕜) y) x

$| x \rangle\langle y |^* = | y \rangle\langle x |$

theorem rankOne_inner_left {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] (x : E₁) (w : E₁) (y : E₂) (z : E₂) : inner ((((rankOne 𝕜) x) y) z) w = inner z y * inner x w

theorem rankOne_inner_right {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] (x : E₁) (y : E₁) (z : E₂) (w : E₂) : inner x ((((rankOne 𝕜) y) z) w) = inner z w * inner x y

theorem ContinuousLinearMap.commutes_with_all_iff {𝕜 : Type u_1} {E₁ : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [CompleteSpace E₁] {T : E₁ →L[𝕜] E₁} : (∀ (S : E₁ →L[𝕜] E₁), Commute S T) ↔ ∃ (α : 𝕜), T = α • 1

theorem ContinuousLinearMap.centralizer {𝕜 : Type u_1} {E₁ : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [CompleteSpace E₁] : Set.univ.centralizer = {x : E₁ →L[𝕜] E₁ | ∃ (α : 𝕜), x = α • 1}

theorem ContinuousLinearMap.scalar_centralizer {𝕜 : Type u_1} {E₁ : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] : {x : E₁ →L[𝕜] E₁ | ∃ (α : 𝕜), x = α • 1}.centralizer = Set.univ

theorem ContinuousLinearMap.centralizer_centralizer {𝕜 : Type u_1} {E₁ : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [CompleteSpace E₁] : Set.univ.centralizer.centralizer = Set.univ

theorem colinear_of_rankOne_self_eq_rankOne_self {𝕜 : Type u_1} {E₁ : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] (x : E₁) (y : E₁) (h : ((rankOne 𝕜) x) x = ((rankOne 𝕜) y) y) : ∃ (α : 𝕜ˣ), x = ↑α • y

theorem colinear_of_ne_zero_rankOne_eq_rankOne {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] [CompleteSpace E₂] [CompleteSpace E₁] {a : E₁} {c : E₁} {b : E₂} {d : E₂} (h : ((rankOne 𝕜) a) b = ((rankOne 𝕜) c) d) (ha : a ≠ 0) (hb : b ≠ 0) : ∃ (α : 𝕜ˣ) (β : 𝕜ˣ), a = ↑α • c ∧ b = (↑α * ↑β) • d

theorem ket_eq_ket_iff {𝕜 : Type u_1} {E₁ : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] {x : E₁} {y : E₁} : (ket 𝕜) x = (ket 𝕜) y ↔ x = y

theorem bra_eq_bra_iff {𝕜 : Type u_1} {E₁ : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] {x : E₁} {y : E₁} : (bra 𝕜) x = (bra 𝕜) y ↔ x = y

theorem ContinuousLinearMap.ext_inner_map {𝕜 : Type u_1} {E₁ : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] {F : Type u_4} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E₁ →L[𝕜] F) (S : E₁ →L[𝕜] F) : T = S ↔ ∀ (x : E₁) (y : F), inner (T x) y = inner (S x) y

theorem LinearMap.ext_inner_map {𝕜 : Type u_1} {E₁ : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] {F : Type u_4} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E₁ →ₗ[𝕜] F) (S : E₁ →ₗ[𝕜] F) : T = S ↔ ∀ (x : E₁) (y : F), inner (T x) y = inner (S x) y

theorem ContinuousLinearMap.exists_sum_rankOne {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] [FiniteDimensional 𝕜 E₁] [FiniteDimensional 𝕜 E₂] (T : E₁ →L[𝕜] E₂) : ∃ (x : Fin (Module.finrank 𝕜 E₁) × Fin (Module.finrank 𝕜 E₂) → E₂) (y : Fin (Module.finrank 𝕜 E₁) × Fin (Module.finrank 𝕜 E₂) → E₁), T = ∑ i : Fin (Module.finrank 𝕜 E₁) × Fin (Module.finrank 𝕜 E₂), ((rankOne 𝕜) (x i)) (y i)

theorem LinearMap.exists_sum_rankOne {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] [FiniteDimensional 𝕜 E₁] [FiniteDimensional 𝕜 E₂] (T : E₁ →ₗ[𝕜] E₂) : ∃ (x : Fin (Module.finrank 𝕜 E₁) × Fin (Module.finrank 𝕜 E₂) → E₂) (y : Fin (Module.finrank 𝕜 E₁) × Fin (Module.finrank 𝕜 E₂) → E₁), T = ∑ i : Fin (Module.finrank 𝕜 E₁) × Fin (Module.finrank 𝕜 E₂), ↑(((rankOne 𝕜) (x i)) (y i))

theorem rankOne.sum_orthonormalBasis_eq_id {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_6} [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) : ∑ i : ι, ((rankOne 𝕜) (b i)) (b i) = 1

theorem ContinuousLinearMap.ext_of_rankOne {𝕜 : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} {H' : Type u_4} [RCLike 𝕜] [NormedAddCommGroup H'] [Module 𝕜 H'] [NormedAddCommGroup H₁] [InnerProductSpace 𝕜 H₁] [NormedAddCommGroup H₂] [InnerProductSpace 𝕜 H₂] [FiniteDimensional 𝕜 H₁] [FiniteDimensional 𝕜 H₂] {x : (H₁ →L[𝕜] H₂) →L[𝕜] H'} {y : (H₁ →L[𝕜] H₂) →L[𝕜] H'} (h : ∀ (a : H₂) (b : H₁), x (((rankOne 𝕜) a) b) = y (((rankOne 𝕜) a) b)) : x = y

theorem LinearMap.ext_of_rankOne {𝕜 : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} {H' : Type u_4} [RCLike 𝕜] [AddCommMonoid H'] [Module 𝕜 H'] [NormedAddCommGroup H₁] [InnerProductSpace 𝕜 H₁] [NormedAddCommGroup H₂] [InnerProductSpace 𝕜 H₂] [FiniteDimensional 𝕜 H₁] [FiniteDimensional 𝕜 H₂] {x : (H₁ →L[𝕜] H₂) →ₗ[𝕜] H'} {y : (H₁ →L[𝕜] H₂) →ₗ[𝕜] H'} (h : ∀ (a : H₂) (b : H₁), x (((rankOne 𝕜) a) b) = y (((rankOne 𝕜) a) b)) : x = y

theorem AddMonoidHom.ext_of_rank_one' {𝕜 : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} {H' : Type u_4} [RCLike 𝕜] [AddCommMonoid H'] [Module 𝕜 H'] [NormedAddCommGroup H₁] [InnerProductSpace 𝕜 H₁] [NormedAddCommGroup H₂] [InnerProductSpace 𝕜 H₂] [FiniteDimensional 𝕜 H₁] [FiniteDimensional 𝕜 H₂] {x : (H₁ →ₗ[𝕜] H₂) →+ H'} {y : (H₁ →ₗ[𝕜] H₂) →+ H'} (h : ∀ (a : H₂) (b : H₁), x ↑(((rankOne 𝕜) a) b) = y ↑(((rankOne 𝕜) a) b)) : x = y

theorem LinearMap.ext_of_rank_one' {𝕜 : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} {H' : Type u_4} [RCLike 𝕜] [AddCommMonoid H'] [Module 𝕜 H'] [NormedAddCommGroup H₁] [InnerProductSpace 𝕜 H₁] [NormedAddCommGroup H₂] [InnerProductSpace 𝕜 H₂] [FiniteDimensional 𝕜 H₁] [FiniteDimensional 𝕜 H₂] {x : (H₁ →ₗ[𝕜] H₂) →ₗ[𝕜] H'} {y : (H₁ →ₗ[𝕜] H₂) →ₗ[𝕜] H'} (h : ∀ (a : H₂) (b : H₁), x ↑(((rankOne 𝕜) a) b) = y ↑(((rankOne 𝕜) a) b)) : x = y

theorem rankOne.sum_orthonormalBasis_eq_id_lm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) : ∑ i : ι, ↑(((rankOne 𝕜) (b i)) (b i)) = 1

theorem ContinuousLinearMap.coe_eq_zero {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₁] [InnerProductSpace 𝕜 E₂] (f : E₁ →L[𝕜] E₂) : ↑f = 0 ↔ f = 0

theorem rankOne.eq_zero_iff {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₁] [InnerProductSpace 𝕜 E₂] (x : E₁) (y : E₂) : ((rankOne 𝕜) x) y = 0 ↔ x = 0 ∨ y = 0

theorem LinearMap.rankOne_comp {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {E₃ : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [NormedAddCommGroup E₃] [InnerProductSpace 𝕜 E₁] [InnerProductSpace 𝕜 E₂] [InnerProductSpace 𝕜 E₃] [FiniteDimensional 𝕜 E₂] [FiniteDimensional 𝕜 E₃] (x : E₁) (y : E₂) (u : E₃ →ₗ[𝕜] E₂) : ↑(((rankOne 𝕜) x) y) ∘ₗ u = ↑(((rankOne 𝕜) x) ((LinearMap.adjoint u) y))

theorem LinearMap.rankOne_comp' {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {E₃ : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [NormedAddCommGroup E₃] [InnerProductSpace 𝕜 E₁] [InnerProductSpace 𝕜 E₂] [InnerProductSpace 𝕜 E₃] [FiniteDimensional 𝕜 E₂] [FiniteDimensional 𝕜 E₃] (x : E₁) (y : E₂) (u : E₂ →ₗ[𝕜] E₃) : ↑(((rankOne 𝕜) x) y) ∘ₗ LinearMap.adjoint u = ↑(((rankOne 𝕜) x) (u y))

theorem OrthonormalBasis.orthogonalProjection'_eq_sum_rankOne {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {U : Submodule 𝕜 E} [CompleteSpace ↥U] (b : OrthonormalBasis ι 𝕜 ↥U) : orthogonalProjection' U = ∑ i : ι, ((rankOne 𝕜) ↑(b i)) ↑(b i)

theorem LinearMap.comp_rankOne {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {E₃ : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [NormedAddCommGroup E₃] [InnerProductSpace 𝕜 E₁] [InnerProductSpace 𝕜 E₂] [InnerProductSpace 𝕜 E₃] (x : E₁) (y : E₂) (u : E₁ →ₗ[𝕜] E₃) : u ∘ₗ ↑(((rankOne 𝕜) x) y) = ↑(((rankOne 𝕜) (u x)) y)

theorem rankOne_smul_smul {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₁] [InnerProductSpace 𝕜 E₂] (x : E₁) (y : E₂) (r₁ : 𝕜) (r₂ : 𝕜) : ((rankOne 𝕜) (r₁ • x)) (star r₂ • y) = (r₁ * r₂) • ((rankOne 𝕜) x) y

theorem rankOne_lm_smul_smul {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₁] [InnerProductSpace 𝕜 E₂] (x : E₁) (y : E₂) (r₁ : 𝕜) (r₂ : 𝕜) : ↑(((rankOne 𝕜) (r₁ • x)) (star r₂ • y)) = (r₁ * r₂) • ↑(((rankOne 𝕜) x) y)

theorem rankOne_lm_sum_sum {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₁] [InnerProductSpace 𝕜 E₂] {ι₁ : Type u_4} {ι₂ : Type u_5} {k : Finset ι₁} {k₂ : Finset ι₂} (f : ι₁ → E₁) (g : ι₂ → E₂) : ↑(((rankOne 𝕜) (∑ i ∈ k, f i)) (∑ i ∈ k₂, g i)) = ∑ i ∈ k, ∑ j ∈ k₂, ↑(((rankOne 𝕜) (f i)) (g j))

theorem ContinuousLinearMap.linearMap_adjoint {𝕜 : Type u_1} {B : Type u_2} {C : Type u_3} [RCLike 𝕜] [NormedAddCommGroup B] [NormedAddCommGroup C] [InnerProductSpace 𝕜 B] [InnerProductSpace 𝕜 C] [FiniteDimensional 𝕜 B] [FiniteDimensional 𝕜 C] (x : B →L[𝕜] C) : LinearMap.adjoint ↑x = ↑(ContinuousLinearMap.adjoint x)

theorem LinearMap.toContinuousLinearMap_adjoint {𝕜 : Type u_1} {B : Type u_2} {C : Type u_3} [RCLike 𝕜] [NormedAddCommGroup B] [NormedAddCommGroup C] [InnerProductSpace 𝕜 B] [InnerProductSpace 𝕜 C] [FiniteDimensional 𝕜 B] [FiniteDimensional 𝕜 C] {x : B →ₗ[𝕜] C} : ContinuousLinearMap.adjoint (LinearMap.toContinuousLinearMap x) = LinearMap.toContinuousLinearMap (LinearMap.adjoint x)

theorem LinearMap.toContinuousLinearMap_adjoint' {𝕜 : Type u_1} {B : Type u_2} {C : Type u_3} [RCLike 𝕜] [NormedAddCommGroup B] [NormedAddCommGroup C] [InnerProductSpace 𝕜 B] [InnerProductSpace 𝕜 C] [FiniteDimensional 𝕜 B] [FiniteDimensional 𝕜 C] {x : B →ₗ[𝕜] C} : ↑(ContinuousLinearMap.adjoint (LinearMap.toContinuousLinearMap x)) = LinearMap.adjoint x

theorem OrthonormalBasis.repr_adjoint {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) : ContinuousLinearMap.adjoint ↑b.repr.toContinuousLinearEquiv = ↑b.repr.symm.toContinuousLinearEquiv

theorem OrthonormalBasis.repr_adjoint' {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) : LinearMap.adjoint ↑b.repr.toLinearEquiv = ↑b.repr.symm.toLinearEquiv

theorem rankOne_toMatrix_of_onb {ι₁ : Type u_1} {ι₂ : Type u_2} {𝕜 : Type u_3} {E₁ : Type u_4} {E₂ : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₁] [InnerProductSpace 𝕜 E₂] [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] [DecidableEq ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E₁) (b₂ : OrthonormalBasis ι₂ 𝕜 E₂) (x : E₁) (y : E₂) : (LinearMap.toMatrix b₂.toBasis b₁.toBasis) ↑(((rankOne 𝕜) x) y) = Matrix.col (Fin 1) (b₁.repr x) * (Matrix.col (Fin 1) (b₂.repr y)).conjTranspose