Self-adjoint decompositions

theorem CommutingRepetition.VN.Modular.isSelfAdjoint_half_add_star {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (y : K →L[ℂ] K) : IsSelfAdjoint ((1 / 2) • (y + star y))

theorem CommutingRepetition.VN.Modular.isSelfAdjoint_half_I_sub_star {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (y : K →L[ℂ] K) : IsSelfAdjoint ((-(1 / 2) * Complex.I) • (y - star y))

theorem CommutingRepetition.VN.Modular.eq_sa_add_I_smul_sa {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (y : K →L[ℂ] K) : y = (1 / 2) • (y + star y) + Complex.I • (-(1 / 2) * Complex.I) • (y - star y)

y = a + i b with a = (y + y*)/2, b = -(i/2)(y − y*) self-adjoint.

theorem CommutingRepetition.VN.Modular.inner_eq_zero_of_sa {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : VonNeumannAlgebra K) (Ω x : K) (h : ∀ a ∈ N, IsSelfAdjoint a → inner ℂ x (a Ω) = 0) {y : K →L[ℂ] K} (hy : y ∈ N) : inner ℂ x (y Ω) = 0

A vector orthogonal to a Ω for every self-adjoint a in a von Neumann algebra N is orthogonal to N Ω.

theorem CommutingRepetition.VN.Modular.inner_eq_zero_of_sa' {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : VonNeumannAlgebra K) (Ω x : K) (h : ∀ a ∈ N, IsSelfAdjoint a → inner ℂ (a Ω) x = 0) {y : K →L[ℂ] K} (hy : y ∈ N) : inner ℂ (y Ω) x = 0

theorem CommutingRepetition.VN.Modular.eq_zero_of_inner_orbit {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : VonNeumannAlgebra K) {Ω : K} (hd : Dense ↑(orbit (↑N) Ω)) {x : K} (h : ∀ y ∈ N, inner ℂ x (y Ω) = 0) : x = 0

A vector orthogonal to N Ω for a von Neumann algebra N with N Ω dense is zero.

The real subspace 𝒦 = closure (M_s Ω)

def CommutingRepetition.VN.Modular.saOrbitSet {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : Set K

{a Ω | a ∈ M self-adjoint}.

Equations

• CommutingRepetition.VN.Modular.saOrbitSet M Ω = {v : K | ∃ a ∈ M, IsSelfAdjoint a ∧ a Ω = v}

noncomputable def CommutingRepetition.VN.Modular.saOrbit {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : Submodule ℝ K

The real span of M_s Ω (already a real subspace, taken as a span for convenience).

Equations

• CommutingRepetition.VN.Modular.saOrbit M Ω = Submodule.span ℝ (CommutingRepetition.VN.Modular.saOrbitSet M Ω)

noncomputable def CommutingRepetition.VN.Modular.Kre {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : ClosedSubmodule ℝ K

The closed real subspace 𝒦 = closure (M_s Ω).

Equations

• CommutingRepetition.VN.Modular.Kre M Ω = (CommutingRepetition.VN.Modular.saOrbit M Ω).closure

theorem CommutingRepetition.VN.Modular.mem_saOrbitSet {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {a : K →L[ℂ] K} (ha : a ∈ M) (hsa : IsSelfAdjoint a) : a Ω ∈ saOrbitSet M Ω

theorem CommutingRepetition.VN.Modular.saOrbit_le_Kre {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : saOrbit M Ω ≤ ↑(Kre M Ω)

theorem CommutingRepetition.VN.Modular.mem_Kre_of_sa {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {a : K →L[ℂ] K} (ha : a ∈ M) (hsa : IsSelfAdjoint a) : a Ω ∈ Kre M Ω

theorem CommutingRepetition.VN.Modular.Ω_mem_Kre {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : Ω ∈ Kre M Ω

theorem CommutingRepetition.VN.Modular.mem_Kre_iff {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {x : K} : x ∈ Kre M Ω ↔ x ∈ closure ↑(saOrbit M Ω)

theorem CommutingRepetition.VN.Modular.Kre_induction {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {p : K → Prop} (hp : IsClosed {x : K | p x}) (h0 : p 0) (hadd : ∀ (x y : K), p x → p y → p (x + y)) (hsmul : ∀ (c : ℝ) (x : K), p x → p (c • x)) (hgen : ∀ a ∈ M, IsSelfAdjoint a → p (a Ω)) {x : K} (hx : x ∈ Kre M Ω) : p x

Induction principle for 𝒦: a closed property holding on M_s Ω and stable under real linear combinations holds on 𝒦.

theorem CommutingRepetition.VN.Modular.im_inner_commutant_sa {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {x : K} (hx : x ∈ Kre M Ω) {a' : K →L[ℂ] K} (ha' : a' ∈ M.commutant) (hsa' : IsSelfAdjoint a') : (inner ℂ x (a' Ω)).im = 0

⟪x, a′ Ω⟫ is real for x ∈ 𝒦 and self-adjoint a′ ∈ M′ (RvD Prop. 4.1).

theorem CommutingRepetition.VN.Modular.commutant_sa_mem_symplComp {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {a' : K →L[ℂ] K} (ha' : a' ∈ M.commutant) (hsa' : IsSelfAdjoint a') : a' Ω ∈ (Kre M Ω).symplComp

M′_s Ω ⊆ (i𝒦)^⊥: the self-adjoint commutant orbit lies in the symplectic complement.

theorem CommutingRepetition.VN.Modular.Ω_mem_symplComp {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : Ω ∈ (Kre M Ω).symplComp

theorem CommutingRepetition.VN.Modular.mem_mulI_Kre_iff {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {x : K} : x ∈ (Kre M Ω).mulI ↔ -Complex.I • x ∈ Kre M Ω

theorem CommutingRepetition.VN.Modular.I_smul_mem_mulI_Kre {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {x : K} (hx : x ∈ Kre M Ω) : Complex.I • x ∈ (Kre M Ω).mulI

The standard subspace (RvD Prop. 4.1)

theorem CommutingRepetition.VN.Modular.Kre_inf_mulI {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) : Kre M Ω ⊓ (Kre M Ω).mulI = ⊥

𝒦 ∩ i𝒦 = 0: a vector in both is orthogonal to M′ Ω, which is dense since Ω is separating for M.

theorem CommutingRepetition.VN.Modular.Kre_sup_mulI {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hc : IsCyclic (↑M) Ω) : Kre M Ω ⊔ (Kre M Ω).mulI = ⊤

𝒦 + i𝒦 is dense: a vector real-orthogonal to both is orthogonal to M Ω.

noncomputable def CommutingRepetition.VN.Modular.standardSubspace {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) : StandardSubspace K

The standard subspace 𝒦 = closure (M_s Ω) of a cyclic separating vector.

Equations

• CommutingRepetition.VN.Modular.standardSubspace M Ω hs hc = { toClosedSubmodule := CommutingRepetition.VN.Modular.Kre M Ω, IsSeparating := ⋯, IsCyclic := ⋯ }

theorem CommutingRepetition.VN.Modular.standardSubspace_toClosedSubmodule {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) : (standardSubspace M Ω hs hc).toClosedSubmodule = Kre M Ω