theorem Orthogonalization.Blocks.inner_apply_of_isSelfAdjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] {e : H →L[ℂ] H} (he : IsSelfAdjoint e) (x w : H) : inner ℂ x (e w) = inner ℂ (e x) w

noncomputable def Orthogonalization.Blocks.orbitSubmodule {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] (M : VonNeumannAlgebra H) (ξ : H) : Submodule ℂ H

The orbit M ξ of a vector under M, as a submodule.

Equations

• Orthogonalization.Blocks.orbitSubmodule M ξ = Submodule.map (↑((ContinuousLinearMap.apply ℂ H) ξ)) (Subalgebra.toSubmodule M.toSubalgebra)

theorem Orthogonalization.Blocks.mem_orbitSubmodule {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] (M : VonNeumannAlgebra H) {ξ v : H} : v ∈ orbitSubmodule M ξ ↔ ∃ x ∈ M, x ξ = v

theorem Orthogonalization.Blocks.orthAt_of_isMinimalCentral {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [FiniteDimensional ℂ H] (M : VonNeumannAlgebra H) {z : H →L[ℂ] H} (hz : IsMinimalCentral M z) (ι : Type u_2) [Fintype ι] : OrthAt M z ι

The block of a minimal central projection is a full matrix algebra, in the form consumed by the transport theorem: Theorem 1.2 holds at every minimal central projection.