Intertwining the continuous functional calculus

theorem CommutingRepetition.VN.Modular.pow_intertwine {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {A : K →L[ℝ] K} {S S' : K →L[ℂ] K} (h : ∀ (x : K), A (S x) = S' (A x)) (n : ℕ) (x : K) : A ((S ^ n) x) = (S' ^ n) (A x)

theorem CommutingRepetition.VN.Modular.aeval_intertwine {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {A : K →L[ℝ] K} {S S' : K →L[ℂ] K} (h : ∀ (x : K), A (S x) = S' (A x)) (p : Polynomial ℝ) (x : K) : A (((Polynomial.aeval S) p) x) = ((Polynomial.aeval S') p) (A x)

theorem CommutingRepetition.VN.Modular.spectrum_subset_Icc_norm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : K →L[ℂ] K) : spectrum ℝ S ⊆ Set.Icc (-‖S‖) ‖S‖

theorem CommutingRepetition.VN.Modular.cfc_intertwine {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {A : K →L[ℝ] K} {S S' : K →L[ℂ] K} (hS : IsSelfAdjoint S) (hS' : IsSelfAdjoint S') (h : ∀ (x : K), A (S x) = S' (A x)) {f : ℝ → ℝ} (hf : Continuous f) (x : K) : A ((cfc f S) x) = (cfc f S') (A x)

A real-linear operator intertwining two self-adjoint operators intertwines their continuous functional calculi (Weierstrass approximation).

T = |P − Q| = (R(2−R))^{1/2} and A = P − Q

noncomputable def CommutingRepetition.VN.Modular.gT (l : ℝ) : ℝ

√(λ(2−λ)), bounded by 1.

Equations

• CommutingRepetition.VN.Modular.gT l = √(l * (2 - l))

theorem CommutingRepetition.VN.Modular.gT_nonneg (l : ℝ) : 0 ≤ gT l

theorem CommutingRepetition.VN.Modular.gT_le_one (l : ℝ) : gT l ≤ 1

theorem CommutingRepetition.VN.Modular.continuous_gT : Continuous gT

theorem CommutingRepetition.VN.Modular.bdd_gT : BorelCalc.Bdd gT

theorem CommutingRepetition.VN.Modular.gT_one : gT 1 = 1

theorem CommutingRepetition.VN.Modular.gT_two_sub (l : ℝ) : gT (2 - l) = gT l

theorem CommutingRepetition.VN.Modular.norm_R_le_two {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : ‖R M Ω‖ ≤ 2

theorem CommutingRepetition.VN.Modular.spectrum_R_subset {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : spectrum ℝ (R M Ω) ⊆ Set.Icc 0 2

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

T := (R(2−R))^{1/2} (RvD's T, the modulus of P − Q).

Equations

• CommutingRepetition.VN.Modular.Tm M Ω = cfc CommutingRepetition.VN.Modular.gT (CommutingRepetition.VN.Modular.R M Ω)

theorem CommutingRepetition.VN.Modular.Tm_isSelfAdjoint {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : IsSelfAdjoint (Tm M Ω)

theorem CommutingRepetition.VN.Modular.Tm_eq_bfc {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : Tm M Ω = BorelCalc.bfc (R M Ω) ⋯ gT

theorem CommutingRepetition.VN.Modular.cfc_two_sub {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : cfc (fun (l : ℝ) => 2 - l) (R M Ω) = 2 - R M Ω

theorem CommutingRepetition.VN.Modular.Tm_mul_Tm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : Tm M Ω * Tm M Ω = R M Ω * (2 - R M Ω)

T² = R(2−R) (RvD Prop. 2.2(2)).

theorem CommutingRepetition.VN.Modular.Tm_Ω {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : (Tm M Ω) Ω = Ω

theorem CommutingRepetition.VN.Modular.norm_Tm_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : ‖Tm M Ω‖ ≤ 1

theorem CommutingRepetition.VN.Modular.R_commute_Tm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : Commute (R M Ω) (Tm M Ω)

theorem CommutingRepetition.VN.Modular.Δit_commute_Tm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (t : ℝ) : Commute (Δit M Ω t) (Tm M Ω)

theorem CommutingRepetition.VN.Modular.Tm_eq_zero_iff {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {x : K} : (Tm M Ω) x = 0 ↔ x = 0

theorem CommutingRepetition.VN.Modular.denseRange_Tm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) : DenseRange ⇑(Tm M Ω)

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

A := P − Q (conjugate-linear).

Equations

• CommutingRepetition.VN.Modular.Am M Ω = CommutingRepetition.VN.Modular.Pre M Ω - CommutingRepetition.VN.Modular.Qre M Ω

theorem CommutingRepetition.VN.Modular.Am_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x : K) : (Am M Ω) x = (Pre M Ω) x - (Qre M Ω) x

theorem CommutingRepetition.VN.Modular.Am_I_smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x : K) : (Am M Ω) (Complex.I • x) = -Complex.I • (Am M Ω) x

theorem CommutingRepetition.VN.Modular.inner_Am_left {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x y : K) : inner ℝ ((Am M Ω) x) y = inner ℝ x ((Am M Ω) y)

theorem CommutingRepetition.VN.Modular.Am_Am {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x : K) : (Am M Ω) ((Am M Ω) x) = (R M Ω * (2 - R M Ω)) x

A² = R(2−R) (RvD Prop. 2.2(2)).

theorem CommutingRepetition.VN.Modular.Am_R {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x : K) : (Am M Ω) ((R M Ω) x) = (2 - R M Ω) ((Am M Ω) x)

A R = (2 − R) A (RvD Prop. 2.2(5) via the polar decomposition).

theorem CommutingRepetition.VN.Modular.inner_sa_real {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {S : K →L[ℂ] K} (hS : IsSelfAdjoint S) (x y : K) : inner ℝ (S x) y = inner ℝ x (S y)

theorem CommutingRepetition.VN.Modular.Am_Tm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x : K) : (Am M Ω) ((Tm M Ω) x) = (Tm M Ω) ((Am M Ω) x)

A T = T A (RvD Prop. 2.2(4)).

theorem CommutingRepetition.VN.Modular.norm_Am_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x : K) : ‖(Am M Ω) x‖ = ‖(Tm M Ω) x‖

theorem CommutingRepetition.VN.Modular.Am_Ω {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : (Am M Ω) Ω = Ω

The antiunitary J: J (T x) = A x

@[reducible, inline]

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

The range of T as a (dense) subspace.

Equations

• CommutingRepetition.VN.Modular.TmRange M Ω = (↑(CommutingRepetition.VN.Modular.Tm M Ω)).range

theorem CommutingRepetition.VN.Modular.exists_rep_Tm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (v : ↥(TmRange M Ω)) : ∃ (x : K), (Tm M Ω) x = ↑v

noncomputable def CommutingRepetition.VN.Modular.repT {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (v : ↥(TmRange M Ω)) : K

A preimage under T.

Equations

• CommutingRepetition.VN.Modular.repT M Ω v = ⋯.choose

theorem CommutingRepetition.VN.Modular.Tm_repT {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (v : ↥(TmRange M Ω)) : (Tm M Ω) (repT M Ω v) = ↑v

theorem CommutingRepetition.VN.Modular.repT_Tm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (x : K) : repT M Ω ⟨(Tm M Ω) x, ⋯⟩ = x

theorem CommutingRepetition.VN.Modular.Am_eq_of_Tm_eq {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {x y : K} (h : (Tm M Ω) x = (Tm M Ω) y) : (Am M Ω) x = (Am M Ω) y

noncomputable def CommutingRepetition.VN.Modular.J₀ {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : ↥(TmRange M Ω) →L⋆[ℂ] K

J₀ : T x ↦ A x on the range of T, conjugate-linear and isometric.

Equations

• One or more equations did not get rendered due to their size.

theorem CommutingRepetition.VN.Modular.J₀_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (v : ↥(TmRange M Ω)) : (J₀ M Ω) v = (Am M Ω) (repT M Ω v)

theorem CommutingRepetition.VN.Modular.denseRange_subtypeL_TmRange {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) : DenseRange ⇑(TmRange M Ω).subtypeL

theorem CommutingRepetition.VN.Modular.isUniformInducing_subtypeL_TmRange {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : IsUniformInducing ⇑(TmRange M Ω).subtypeL

noncomputable def CommutingRepetition.VN.Modular.Jm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : K →L⋆[ℂ] K

The antiunitary J, the continuous extension of T x ↦ A x (RvD §2, the partial isometry of the polar decomposition P − Q = JT).

Equations

• CommutingRepetition.VN.Modular.Jm M Ω = (CommutingRepetition.VN.Modular.J₀ M Ω).extend (CommutingRepetition.VN.Modular.TmRange M Ω).subtypeL

theorem CommutingRepetition.VN.Modular.Jm_Tm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (x : K) : (Jm M Ω) ((Tm M Ω) x) = (Am M Ω) x

theorem CommutingRepetition.VN.Modular.Jm_smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (c : ℂ) (ξ : K) : (Jm M Ω) (c • ξ) = (starRingEnd ℂ) c • (Jm M Ω) ξ

theorem CommutingRepetition.VN.Modular.ext_of_Tm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] {f g : K → Y} (hf : Continuous f) (hg : Continuous g) (h : ∀ (x : K), f ((Tm M Ω) x) = g ((Tm M Ω) x)) : f = g

Two continuous maps agreeing on the range of T agree everywhere.

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

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

T J = A (J commutes with T, RvD Prop. 2.2(4)).

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

theorem CommutingRepetition.VN.Modular.inner_Jm_left_real {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 Ω) η)

Real symmetry Re⟪Jξ, η⟫ = Re⟪ξ, Jη⟫.

theorem CommutingRepetition.VN.Modular.inner_Jm_left {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η, ξ⟫ (RvD Prop. 3.1).

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

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

J² = 1 (RvD Prop. 2.2(3)).

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

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

J R = (2 − R) J (RvD Prop. 2.2(5)).

J and the functional calculus of R

J R = (2 − R) J transports the spectral data of R under λ ↦ 2 − λ: J g(R) = g(2 − R) J for every bounded Borel g.

theorem CommutingRepetition.VN.Modular.two_sub_R_isSelfAdjoint {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : IsSelfAdjoint (2 - R M Ω)

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

J as a real-linear operator.

Equations

• CommutingRepetition.VN.Modular.JmR M Ω = { toFun := ⇑(CommutingRepetition.VN.Modular.Jm M Ω), map_add' := ⋯, map_smul' := ⋯ }.mkContinuous ‖CommutingRepetition.VN.Modular.Jm M Ω‖ ⋯

theorem CommutingRepetition.VN.Modular.JmR_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω x : K) : (JmR M Ω) x = (Jm M Ω) x

theorem CommutingRepetition.VN.Modular.Jm_cfc {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {f : ℝ → ℝ} (hf : Continuous f) (x : K) : (Jm M Ω) ((cfc f (R M Ω)) x) = (cfc (fun (l : ℝ) => f (2 - l)) (R M Ω)) ((Jm M Ω) x)

J f(R) = f(2 − R) J = (f ∘ (2 − ·))(R) J for continuous f.

theorem CommutingRepetition.VN.Modular.ν_Jm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (ξ : K) : BorelCalc.ν (R M Ω) ⋯ ((Jm M Ω) ξ) = MeasureTheory.Measure.map (fun (l : ℝ) => 2 - l) (BorelCalc.ν (R M Ω) ⋯ ξ)

The spectral measure of R at J ξ is the push-forward of the one at ξ under λ ↦ 2 − λ.

theorem CommutingRepetition.BorelCalc.Bdd.comp_two_sub {g : ℝ → ℝ} (hg : Bdd g) : Bdd fun (l : ℝ) => g (2 - l)

noncomputable def CommutingRepetition.VN.Modular.conjJm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (G : K →L[ℂ] K) : K →L[ℂ] K

Conjugation G ↦ J G J by the antiunitary J, a (complex-linear) operator.

Equations

• CommutingRepetition.VN.Modular.conjJm M Ω G = CommutingRepetition.VN.Modular.Jm M Ω ∘SL G ∘SL CommutingRepetition.VN.Modular.Jm M Ω

theorem CommutingRepetition.VN.Modular.conjJm_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (G : K →L[ℂ] K) (ξ : K) : (conjJm M Ω G) ξ = (Jm M Ω) (G ((Jm M Ω) ξ))

theorem CommutingRepetition.VN.Modular.Jm_bfc {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (g : ℝ → ℝ) (ξ : K) : (Jm M Ω) ((BorelCalc.bfc (R M Ω) ⋯ g) ξ) = (BorelCalc.bfc (R M Ω) ⋯ fun (l : ℝ) => g (2 - l)) ((Jm M Ω) ξ)

J g(R) = (g ∘ (2 − ·))(R) J for bounded Borel g.

theorem CommutingRepetition.VN.Modular.Jm_cbfc {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {G : ℝ → ℂ} (hG : BorelCalc.CBdd G) (ξ : K) : (Jm M Ω) ((BorelCalc.cbfc (R M Ω) ⋯ G) ξ) = (BorelCalc.cbfc (R M Ω) ⋯ fun (l : ℝ) => (starRingEnd ℂ) (G (2 - l))) ((Jm M Ω) ξ)

theorem CommutingRepetition.VN.Modular.θ_two_sub (l : ℝ) : θ (2 - l) = -θ l

θ(2 − l) = −θ l.

theorem CommutingRepetition.VN.Modular.gDel_two_sub (t l : ℝ) : gDel t (2 - l) = (starRingEnd ℂ) (gDel t l)

theorem CommutingRepetition.VN.Modular.Jm_Δit {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (t : ℝ) (ξ : K) : (Jm M Ω) ((Δit M Ω t) ξ) = (Δit M Ω t) ((Jm M Ω) ξ)

J Δ^{it} = Δ^{it} J (RvD Prop. 3.3).

theorem CommutingRepetition.VN.Modular.Δit_Kre {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (t : ℝ) {x : K} (hx : x ∈ Kre M Ω) : (Δit M Ω t) x ∈ Kre M Ω

Δ^{it} preserves 𝒦 (RvD Prop. 3.3): P = (R + A)/2 commutes with Δ^{it}.

The bounded identities T J (x Ω) = (2 − R)(x* Ω), T J (x' Ω) = R (x'* Ω) (RvD Lemma 4.5)

theorem CommutingRepetition.VN.Modular.Qre_commutant_sa {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') : (Qre M Ω) (a' Ω) = 0

For self-adjoint a' ∈ M', Q (a' Ω) = 0: a' Ω ⊥ i𝒦.

theorem CommutingRepetition.VN.Modular.Am_sa_mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {a : K →L[ℂ] K} (ha : a ∈ M) (hsa : IsSelfAdjoint a) : (Am M Ω) (a Ω) = (2 - R M Ω) (a Ω)

For self-adjoint a ∈ M, T J (a Ω) = (2 − R)(a Ω).

theorem CommutingRepetition.VN.Modular.Am_commutant_sa {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') : (Am M Ω) (a' Ω) = (R M Ω) (a' Ω)

For self-adjoint a' ∈ M', A (a' Ω) = R (a' Ω).

theorem CommutingRepetition.VN.Modular.Am_add_I_smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω u v : K) : (Am M Ω) (u + Complex.I • v) = (Am M Ω) u - Complex.I • (Am M Ω) v

Conjugate-linearity of A in the form used for the decomposition x = a + i b.

theorem CommutingRepetition.VN.Modular.Tm_Jm_apply_mem {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) : (Tm M Ω) ((Jm M Ω) (x Ω)) = (2 - R M Ω) ((star x) Ω)

RvD Lemma 4.5 (first identity): T J (x Ω) = (2 − R)(x* Ω) for x ∈ M.

theorem CommutingRepetition.VN.Modular.Tm_Jm_apply_mem_commutant {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) : (Tm M Ω) ((Jm M Ω) (x' Ω)) = (R M Ω) ((star x') Ω)

RvD Lemma 4.5 (second identity): T J (x' Ω) = R (x'* Ω) for x' ∈ M'.