Helpers on 𝒦, M_s Ω and M′ Ω

theorem CommutingRepetition.VN.Modular.inner_self_re' {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (ζ : K) : (inner ℂ ζ ζ).re = ‖ζ‖ ^ 2

theorem CommutingRepetition.VN.Modular.ofReal_smul' {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (r : ℝ) (v : K) : ↑r • v = r • v

theorem CommutingRepetition.VN.Modular.exists_sa_of_mem_saOrbit {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {v : K} (hv : v ∈ saOrbit M Ω) : ∃ h ∈ M, IsSelfAdjoint h ∧ h Ω = v

Elements of the real span of M_s Ω are of the form hΩ with h ∈ M_s.

theorem CommutingRepetition.VN.Modular.exists_sa_approx {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {v : K} (hv : v ∈ Kre M Ω) {ε : ℝ} (hε : 0 < ε) : ∃ h ∈ M, IsSelfAdjoint h ∧ ‖h Ω - v‖ < ε

Vectors of 𝒦 are approximated by hΩ, h ∈ M_s.

theorem CommutingRepetition.VN.Modular.eq_of_inner_sa_eq {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {u v : K} (hu : u ∈ Kre M Ω) (hv : v ∈ Kre M Ω) (h : ∀ y ∈ M, IsSelfAdjoint y → inner ℝ (y Ω) u = inner ℝ (y Ω) v) : u = v

Two vectors of 𝒦 with the same real inner products against M_s Ω are equal.

theorem CommutingRepetition.VN.Modular.Pre_eq_Pre_of_inner_sa {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {u v : K} (h : ∀ y ∈ M, IsSelfAdjoint y → inner ℝ (y Ω) u = inner ℝ (y Ω) v) : (Pre M Ω) u = (Pre M Ω) v

Pre of a vector is determined by real inner products against M_s Ω.

theorem CommutingRepetition.VN.Modular.Pre_conj_smul_Ω {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (l : ℂ) : (Pre M Ω) ((starRingEnd ℂ) l • Ω) = l.re • Ω

Pre (λ̄ • Ω) = Re λ • Ω (P Ω = Ω, P (iΩ) = i Q Ω = 0).

theorem CommutingRepetition.VN.Modular.exists_of_mem_orbit_vn {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : VonNeumannAlgebra K) {ξ v : K} (hv : v ∈ orbit (↑N) ξ) : ∃ y ∈ N, y ξ = v

Elements of the orbit of a von Neumann algebra are of the form y ξ, y ∈ N.

theorem CommutingRepetition.VN.Modular.dense_commutant_orbit {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) : Dense {v : K | ∃ y ∈ M.commutant, y Ω = v}

M′ Ω is dense (Ω separating for M).

theorem CommutingRepetition.VN.Modular.eq_of_inner_commutant {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) {u v : K} (h : ∀ z ∈ M.commutant, inner ℂ (z Ω) u = inner ℂ (z Ω) v) : u = v

Two vectors with the same inner products against the dense set M′ Ω are equal.

theorem CommutingRepetition.VN.Modular.ext_of_commutant_orbit {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) {S₁ S₂ : K →L[ℂ] K} (h : ∀ y ∈ M.commutant, ∀ z ∈ M.commutant, inner ℂ (z Ω) (S₁ (y Ω)) = inner ℂ (z Ω) (S₂ (y Ω))) : S₁ = S₂

Two operators with the same matrix coefficients on M′ Ω × M′ Ω are equal.

The self-adjoint unit ball and the set V

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

The self-adjoint unit ball of M.

Equations

• CommutingRepetition.VN.Modular.saBall M = {x : K →L[ℂ] K | x ∈ M ∧ IsSelfAdjoint x ∧ ‖x‖ ≤ 1}

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

V = {P(λ̄ • xΩ) : x ∈ M_s, ‖x‖ ≤ 1}.

Equations

• CommutingRepetition.VN.Modular.Vset M Ω l = (fun (x : K →L[ℂ] K) => (CommutingRepetition.VN.Modular.Pre M Ω) ((starRingEnd ℂ) l • x Ω)) '' CommutingRepetition.VN.Modular.saBall M

theorem CommutingRepetition.VN.Modular.convex_Vset {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (l : ℂ) : Convex ℝ (Vset M Ω l)

theorem CommutingRepetition.VN.Modular.isClosed_Vset {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (l : ℂ) : IsClosed (Vset M Ω l)

theorem CommutingRepetition.VN.Modular.bddAbove_Vset_norm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (l : ℂ) (v : K) : v ∈ Vset M Ω l → ‖v‖ ≤ ‖l‖ * ‖Ω‖

The sign trick: Re⟪hΩ, x′Ω⟫ ≤ Re⟪hΩ, sgn(h) Ω⟫ for 0 ≤ x′ ≤ 1 in M′

noncomputable def CommutingRepetition.VN.Modular.sgn (t : ℝ) : ℝ

sgn t = 1 for t ≥ 0 and -1 otherwise.

Equations

• CommutingRepetition.VN.Modular.sgn t = if 0 ≤ t then 1 else -1

theorem CommutingRepetition.VN.Modular.bdd_sgn : BorelCalc.Bdd sgn

theorem CommutingRepetition.VN.Modular.abs_sgn_le (t : ℝ) : |sgn t| ≤ 1

noncomputable def CommutingRepetition.VN.Modular.clamp (c t : ℝ) : ℝ

Truncation to [-c, c].

Equations

• CommutingRepetition.VN.Modular.clamp c t = max (-c) (min t c)

theorem CommutingRepetition.VN.Modular.continuous_clamp (c : ℝ) : Continuous (clamp c)

theorem CommutingRepetition.VN.Modular.abs_clamp_le {c : ℝ} (hc : 0 ≤ c) (t : ℝ) : |clamp c t| ≤ c

theorem CommutingRepetition.VN.Modular.bdd_clamp {c : ℝ} (hc : 0 ≤ c) : BorelCalc.Bdd (clamp c)

theorem CommutingRepetition.VN.Modular.bdd_abs_clamp {c : ℝ} (hc : 0 ≤ c) : BorelCalc.Bdd fun (t : ℝ) => |clamp c t|

theorem CommutingRepetition.VN.Modular.clamp_eq_of_abs_le {c t : ℝ} (h : |t| ≤ c) : clamp c t = t

theorem CommutingRepetition.VN.Modular.sgn_mul_clamp {c : ℝ} (hc : 0 ≤ c) (t : ℝ) : sgn t * clamp c t = |clamp c t|

theorem CommutingRepetition.VN.Modular.bfc_clamp_eq {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {h : K →L[ℂ] K} (hsa : IsSelfAdjoint h) : BorelCalc.bfc h hsa (clamp ‖h‖) = h

h = clamp(h) since the spectrum lies in [-‖h‖, ‖h‖].

noncomputable def CommutingRepetition.VN.Modular.sgnOp {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {h : K →L[ℂ] K} (hsa : IsSelfAdjoint h) : K →L[ℂ] K

The sign of h, sgn(h) = bfc h sgn.

Equations

• CommutingRepetition.VN.Modular.sgnOp hsa = CommutingRepetition.BorelCalc.bfc h hsa CommutingRepetition.VN.Modular.sgn

noncomputable def CommutingRepetition.VN.Modular.absOp {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {h : K →L[ℂ] K} (hsa : IsSelfAdjoint h) : K →L[ℂ] K

|h| = bfc h |clamp|.

Equations

• CommutingRepetition.VN.Modular.absOp hsa = CommutingRepetition.BorelCalc.bfc h hsa fun (t : ℝ) => |CommutingRepetition.VN.Modular.clamp ‖h‖ t|

theorem CommutingRepetition.VN.Modular.sgnOp_isSelfAdjoint {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {h : K →L[ℂ] K} (hsa : IsSelfAdjoint h) : IsSelfAdjoint (sgnOp hsa)

theorem CommutingRepetition.VN.Modular.norm_sgnOp_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {h : K →L[ℂ] K} (hsa : IsSelfAdjoint h) : ‖sgnOp hsa‖ ≤ 1

theorem CommutingRepetition.VN.Modular.sgnOp_mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) {h : K →L[ℂ] K} (hsa : IsSelfAdjoint h) (hh : h ∈ M) : sgnOp hsa ∈ M

theorem CommutingRepetition.VN.Modular.absOp_isSelfAdjoint {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {h : K →L[ℂ] K} (hsa : IsSelfAdjoint h) : IsSelfAdjoint (absOp hsa)

theorem CommutingRepetition.VN.Modular.absOp_mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) {h : K →L[ℂ] K} (hsa : IsSelfAdjoint h) (hh : h ∈ M) : absOp hsa ∈ M

theorem CommutingRepetition.VN.Modular.absOp_nonneg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {h : K →L[ℂ] K} (hsa : IsSelfAdjoint h) : 0 ≤ absOp hsa

theorem CommutingRepetition.VN.Modular.absOp_sub_nonneg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {h : K →L[ℂ] K} (hsa : IsSelfAdjoint h) : 0 ≤ absOp hsa - h

theorem CommutingRepetition.VN.Modular.sgnOp_mul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {h : K →L[ℂ] K} (hsa : IsSelfAdjoint h) : sgnOp hsa * h = absOp hsa

theorem CommutingRepetition.VN.Modular.mul_sgnOp {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {h : K →L[ℂ] K} (hsa : IsSelfAdjoint h) : h * sgnOp hsa = absOp hsa

theorem CommutingRepetition.VN.Modular.exists_sqrt_mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : VonNeumannAlgebra K) {A : K →L[ℂ] K} (hA : A ∈ N) (h0 : 0 ≤ A) : ∃ r ∈ N, IsSelfAdjoint r ∧ r * r = A

A nonnegative element of a von Neumann algebra has a self-adjoint square root in it.

theorem CommutingRepetition.VN.Modular.im_inner_apply_sa {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {A : K →L[ℂ] K} (hA : IsSelfAdjoint A) (ξ : K) : (inner ℂ ξ (A ξ)).im = 0

theorem CommutingRepetition.VN.Modular.re_inner_le_sgn {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {h : K →L[ℂ] K} (hh : h ∈ M) (hsa : IsSelfAdjoint h) {x' : K →L[ℂ] K} (hx' : x' ∈ M.commutant) (h0 : 0 ≤ x') (h1 : x' ≤ 1) : (inner ℂ (h Ω) (x' Ω)).re ≤ (inner ℂ (h Ω) ((sgnOp hsa) Ω)).re

RvD's computation (proof of Lemma 4.3): for h ∈ M_s and 0 ≤ x′ ≤ 1 in M′, Re⟪hΩ, x′Ω⟫ ≤ Re⟪hΩ, sgn(h) Ω⟫.

theorem CommutingRepetition.VN.Modular.im_inner_sgn {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (Ω : K) {h : K →L[ℂ] K} (hsa : IsSelfAdjoint h) : (inner ℂ (h Ω) ((sgnOp hsa) Ω)).im = 0

⟪hΩ, sgn(h) Ω⟫ is real.

RvD Lemma 4.3

theorem CommutingRepetition.VN.Modular.Pre_ofReal_smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (r : ℝ) (v : K) : (Pre M Ω) (↑r • v) = ↑r • (Pre M Ω) v

Real linearity of Pre for real scalars written as complex numbers.

theorem CommutingRepetition.VN.Modular.Pre_mem_Vset {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {x' : K →L[ℂ] K} (hx' : x' ∈ M.commutant) (h0 : 0 ≤ x') (h1 : x' ≤ 1) {l : ℂ} (hl : l.re = 1) : (Pre M Ω) (x' Ω) ∈ Vset M Ω l

The core case of Lemma 4.3: 0 ≤ x′ ≤ 1, Re λ = 1.

theorem CommutingRepetition.VN.Modular.exists_linearRN {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {x' : K →L[ℂ] K} (hx' : x' ∈ M.commutant) (hsa' : IsSelfAdjoint x') {l : ℂ} (hl : 0 < l.re) : ∃ x ∈ M, IsSelfAdjoint x ∧ (Pre M Ω) (x' Ω) = (Pre M Ω) ((starRingEnd ℂ) l • x Ω)

RvD Lemma 4.3 (existence): for self-adjoint x′ ∈ M′ and Re λ > 0 there is a self-adjoint x ∈ M with P(x′Ω) = P(λ̄ • xΩ).

RvD Corollary 4.4

theorem CommutingRepetition.VN.Modular.exists_Jm_Tm_eq_sa {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {x' : K →L[ℂ] K} (hx' : x' ∈ M.commutant) (hsa' : IsSelfAdjoint x') : ∃ x ∈ M, IsSelfAdjoint x ∧ (Jm M Ω) ((Tm M Ω) (x' Ω)) = x Ω

Corollary 4.4 for self-adjoint x′: J T x′Ω = xΩ with x ∈ M_s.

theorem CommutingRepetition.VN.Modular.exists_Jm_Tm_eq {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {x' : K →L[ℂ] K} (hx' : x' ∈ M.commutant) : ∃ x ∈ M, (Jm M Ω) ((Tm M Ω) (x' Ω)) = x Ω ∧ (Jm M Ω) ((Tm M Ω) ((star x') Ω)) = (star x) Ω

RvD Corollary 4.4: for x′ ∈ M′ there is x ∈ M with J T x′Ω = xΩ and J T x′*Ω = x*Ω.

RvD Lemma 4.5

theorem CommutingRepetition.VN.Modular.inner_Jm_right {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (ξ η : K) : inner ℂ ξ ((Jm M Ω) η) = inner ℂ η ((Jm M Ω) ξ)

⟪ξ, J η⟫ = ⟪η, J ξ⟫.

theorem CommutingRepetition.VN.Modular.inner_eq_of_Pre_eq {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {x' x : K →L[ℂ] K} (hx' : x' ∈ M.commutant) (hsa' : IsSelfAdjoint x') (hx : x ∈ M) (hxsa : IsSelfAdjoint x) {l : ℂ} (hP : (Pre M Ω) (x' Ω) = 2 • (Pre M Ω) ((starRingEnd ℂ) l • x Ω)) {y : K →L[ℂ] K} (hy : y ∈ M) : inner ℂ (y Ω) (x' Ω) = l * inner ℂ (x Ω) ((star y) Ω) + (starRingEnd ℂ) l * inner ℂ (y Ω) (x Ω)

The identity (E1): for all y ∈ M, ⟪yΩ, x′Ω⟫ = λ ⟪xΩ, y*Ω⟫ + λ̄ ⟪yΩ, xΩ⟫, given P(x′Ω) = 2 P(λ̄ • xΩ).

theorem CommutingRepetition.VN.Modular.exists_operator_eq {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {x' : K →L[ℂ] K} (hx' : x' ∈ M.commutant) (hsa' : IsSelfAdjoint x') {l : ℂ} (hl : 0 < l.re) : ∃ x ∈ M, IsSelfAdjoint x ∧ Tm M Ω * conjJm M Ω x' * Tm M Ω = l • ((2 - R M Ω) * x * R M Ω) + (starRingEnd ℂ) l • (R M Ω * x * (2 - R M Ω))

RvD Lemma 4.5: for self-adjoint x′ ∈ M′ and Re λ > 0 there is a self-adjoint x ∈ M with T (J x′ J) T = λ (2 − R) x R + λ̄ R x (2 − R).