Projections and their ranges

theorem Orthogonalization.Blocks.proj_apply_eq_self_of_mem_range {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {e : H →L[ℂ] H} (he : IsStarProjection e) {w : H} (hw : w ∈ (↑e).range) : e w = w

theorem Orthogonalization.Blocks.mul_eq_self_of_range_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {e f : H →L[ℂ] H} (he : IsStarProjection e) (h : (↑f).range ≤ (↑e).range) : e * f = f

theorem Orthogonalization.Blocks.range_le_of_mul_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {e f : H →L[ℂ] H} (h : e * f = f) : (↑f).range ≤ (↑e).range

theorem Orthogonalization.Blocks.starProjection_range_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {e : H →L[ℂ] H} (he : IsStarProjection e) : (↑e).range.starProjection = e

theorem Orthogonalization.Blocks.eq_of_range_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {e f : H →L[ℂ] H} (he : IsStarProjection e) (hf : IsStarProjection f) (h : (↑e).range = (↑f).range) : e = f

Two projections with the same range are equal.

theorem Orthogonalization.Blocks.eigenspace_starProjection_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] (M : VonNeumannAlgebra H) {x : H →L[ℂ] H} (hx : x ∈ M) (μ : ℂ) : (Module.End.eigenspace (↑x) μ).starProjection ∈ M

The projection onto an eigenspace of an element of M belongs to M: the eigenspace is invariant under the commutant.

Minimal projections

structure Orthogonalization.Blocks.IsMinimalProjIn {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] (M : VonNeumannAlgebra H) (z e : H →L[ℂ] H) : Prop

e is a minimal projection of M below the projection z: a nonzero projection of M with e ≤ z such that every projection of M below e is 0 or e.

• mem : e ∈ M
• isStarProjection : IsStarProjection e
• ne_zero : e ≠ 0
• mul_eq : e * z = e
• minimal (f : H →L[ℂ] H) : f ∈ M → IsStarProjection f → f * e = f → f = 0 ∨ f = e

theorem Orthogonalization.Blocks.exists_isMinimalProjIn {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] (M : VonNeumannAlgebra H) {z : H →L[ℂ] H} (hz : IsStarProjection z) (hzM : z ∈ M) (hz0 : z ≠ 0) : ∃ (e : H →L[ℂ] H), IsMinimalProjIn M z e

Below every nonzero projection of M there is a minimal projection of M (one of least rank).

theorem Orthogonalization.Blocks.exists_eq_smul_of_isMinimalProjIn {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] (M : VonNeumannAlgebra H) {z e : H →L[ℂ] H} (he : IsMinimalProjIn M z e) {x : H →L[ℂ] H} (hx : x ∈ M) (hxsa : IsSelfAdjoint x) (hex : e * x * e = x) : ∃ (c : ℝ), x = ↑c • e

e M e = ℂ e. A self-adjoint element of M supported in a minimal projection e (e x e = x) is a real multiple of e.

The central decomposition

structure Orthogonalization.Blocks.IsMinimalCentral {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] (M : VonNeumannAlgebra H) (z : H →L[ℂ] H) : Prop

A minimal central projection of M: a nonzero central projection such that every central projection below it is 0 or itself.

• isCentralProj : IsCentralProj M z
• ne_zero : z ≠ 0
• minimal (z' : H →L[ℂ] H) : IsCentralProj M z' → z' * z = z' → z' = 0 ∨ z' = z

theorem Orthogonalization.Blocks.IsCentralProj.sub {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {M : VonNeumannAlgebra H} {z z' : H →L[ℂ] H} (hz : IsCentralProj M z) (hz' : IsCentralProj M z') (hz'z : z' * z = z') : IsCentralProj M (z - z')

theorem Orthogonalization.Blocks.exists_minimal_central_decomposition_below {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] (M : VonNeumannAlgebra H) (n : ℕ) (z : H →L[ℂ] H) : IsCentralProj M z → Module.finrank ℂ ↥(↑z).range = n → ∃ (κ : Type) (x : Fintype κ) (w : κ → H →L[ℂ] H), (∀ (j : κ), IsMinimalCentral M (w j)) ∧ (∀ (j : κ), w j * z = w j) ∧ (∀ (j k : κ), j ≠ k → w j * w k = 0) ∧ ∑ j : κ, w j = z

Every central projection z of M is an orthogonal sum of minimal central projections below z (strong induction on the rank of z).

theorem Orthogonalization.Blocks.exists_minimal_central_decomposition {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] (M : VonNeumannAlgebra H) : ∃ (κ : Type) (x : Fintype κ) (z : κ → H →L[ℂ] H), (∀ (j : κ), IsMinimalCentral M (z j)) ∧ (∀ (j k : κ), j ≠ k → z j * z k = 0) ∧ ∑ j : κ, z j = 1

The central decomposition. 1 is an orthogonal sum of minimal central projections of M.