Joint continuity of x ↦ U x (ζ x) for uniformly bounded strongly continuous U

theorem CommutingRepetition.VN.Modular.continuousWithinAt_apply_of_bdd {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {X : Type u_2} [TopologicalSpace X] {U : X → K →L[ℂ] K} {ζ : X → K} {s : Set X} {x₀ : X} {C : ℝ} (hU : ∀ x ∈ s, ‖U x‖ ≤ C) (hUc : ∀ (v : K), ContinuousWithinAt (fun (x : X) => (U x) v) s x₀) (hζ : ContinuousWithinAt ζ s x₀) (hx₀ : x₀ ∈ s) : ContinuousWithinAt (fun (x : X) => (U x) (ζ x)) s x₀

theorem CommutingRepetition.VN.Modular.continuousOn_apply_of_bdd {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {X : Type u_2} [TopologicalSpace X] {U : X → K →L[ℂ] K} {ζ : X → K} {s : Set X} {C : ℝ} (hU : ∀ x ∈ s, ‖U x‖ ≤ C) (hUc : ∀ (v : K), ContinuousOn (fun (x : X) => (U x) v) s) (hζ : ContinuousOn ζ s) : ContinuousOn (fun (x : X) => (U x) (ζ x)) s

theorem CommutingRepetition.VN.Modular.continuous_apply_of_bdd {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {X : Type u_2} [TopologicalSpace X] {U : X → K →L[ℂ] K} {ζ : X → K} {C : ℝ} (hU : ∀ (x : X), ‖U x‖ ≤ C) (hUc : ∀ (v : K), Continuous fun (x : X) => (U x) v) (hζ : Continuous ζ) : Continuous fun (x : X) => (U x) (ζ x)

theorem CommutingRepetition.VN.Modular.continuous_Δit_comp {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {ζ : ℝ → K} (hζ : Continuous ζ) : Continuous fun (t : ℝ) => (Δit M Ω t) (ζ t)

The weak integral W = ∫ w_φ(t) Δ^{it} B Δ^{-it} dt

theorem CommutingRepetition.VN.Modular.integrable_w {φ : ℝ} (hφ : |φ| < Real.pi) : MeasureTheory.Integrable (StripCauchy.w φ) MeasureTheory.volume

theorem CommutingRepetition.VN.Modular.integrable_w_smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {φ : ℝ} (hφ : |φ| < Real.pi) {v : ℝ → K} (hv : Continuous v) {C : ℝ} (hC : ∀ (t : ℝ), ‖v t‖ ≤ C) : MeasureTheory.Integrable (fun (t : ℝ) => ↑(StripCauchy.w φ t) • v t) MeasureTheory.volume

Integrability of t ↦ w φ t • v t for bounded continuous v : ℝ → K.

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

The integrand t ↦ w φ t • Δ^{it} B Δ^{-it} ξ.

Equations

• CommutingRepetition.VN.Modular.Wint M Ω B φ ξ t = ↑(CommutingRepetition.StripCauchy.w φ t) • (CommutingRepetition.VN.Modular.Δit M Ω t) (B ((CommutingRepetition.VN.Modular.Δit M Ω (-t)) ξ))

theorem CommutingRepetition.VN.Modular.continuous_Wint {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (B : K →L[ℂ] K) (φ : ℝ) (ξ : K) : Continuous (Wint M Ω B φ ξ)

theorem CommutingRepetition.VN.Modular.norm_conj_apply_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (B : K →L[ℂ] K) (ξ : K) (t : ℝ) : ‖(Δit M Ω t) (B ((Δit M Ω (-t)) ξ))‖ ≤ ‖B‖ * ‖ξ‖

theorem CommutingRepetition.VN.Modular.integrable_Wint {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (B : K →L[ℂ] K) {φ : ℝ} (hφ : |φ| < Real.pi) (ξ : K) : MeasureTheory.Integrable (Wint M Ω B φ ξ) MeasureTheory.volume

noncomputable def CommutingRepetition.VN.Modular.Wop {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (B : K →L[ℂ] K) (φ : ℝ) (hφ : |φ| < Real.pi) : K →L[ℂ] K

The operator W.

Equations

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

theorem CommutingRepetition.VN.Modular.Wop_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (B : K →L[ℂ] K) (φ : ℝ) (hφ : |φ| < Real.pi) (ξ : K) : (Wop M Ω B φ hφ) ξ = ∫ (t : ℝ), ↑(StripCauchy.w φ t) • (Δit M Ω t) (B ((Δit M Ω (-t)) ξ))

theorem CommutingRepetition.VN.Modular.inner_Wop {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (B : K →L[ℂ] K) (φ : ℝ) (hφ : |φ| < Real.pi) (η ξ : K) : inner ℂ η ((Wop M Ω B φ hφ) ξ) = ∫ (t : ℝ), ↑(StripCauchy.w φ t) * inner ℂ η ((Δit M Ω t) (B ((Δit M Ω (-t)) ξ)))

theorem CommutingRepetition.VN.Modular.clm_Wop {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (B : K →L[ℂ] K) (φ : ℝ) (hφ : |φ| < Real.pi) (S : K →L[ℂ] K) (ξ : K) : S ((Wop M Ω B φ hφ) ξ) = ∫ (t : ℝ), ↑(StripCauchy.w φ t) • S ((Δit M Ω t) (B ((Δit M Ω (-t)) ξ)))

The bilinear form β(u, v) = ⟪J u, v⟫

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

β(u, v) = ⟪J u, v⟫, a continuous ℂ-bilinear form.

Equations

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

theorem CommutingRepetition.VN.Modular.βop_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω u v : K) : ((βop M Ω) u) v = inner ℂ ((Jm M Ω) u) v

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

RvD Lemma 4.7

theorem CommutingRepetition.VN.Modular.re_exp_half_pos {φ : ℝ} (hφ : |φ| < Real.pi) : 0 < (Complex.exp (Complex.I * ↑φ / 2)).re

theorem CommutingRepetition.VN.Modular.conj_exp_half (φ : ℝ) : (starRingEnd ℂ) (Complex.exp (Complex.I * ↑φ / 2)) = Complex.exp (-(Complex.I * ↑φ / 2))

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

Δ^{it} commutes with 2 − R.

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

The function f(z) = ⟪η, E(z) x E(−z) ξ⟫.

Equations

• CommutingRepetition.VN.Modular.fz M Ω x η ξ z = inner ℂ η ((CommutingRepetition.VN.Modular.Efam M Ω z) (x ((CommutingRepetition.VN.Modular.Efam M Ω (-z)) ξ)))

theorem CommutingRepetition.VN.Modular.neg_mem_strip {z : ℂ} (hz : z ∈ StripCauchy.strip) : -z ∈ StripCauchy.strip

theorem CommutingRepetition.VN.Modular.continuousOn_fz {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (x : K →L[ℂ] K) (η ξ : K) : ContinuousOn (fz M Ω x η ξ) StripCauchy.strip

theorem CommutingRepetition.VN.Modular.norm_fz_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (x : K →L[ℂ] K) (η ξ : K) {z : ℂ} (hz : z ∈ StripCauchy.strip) : ‖fz M Ω x η ξ z‖ ≤ ‖η‖ * (2 * (‖x‖ * (2 * ‖ξ‖)))

theorem CommutingRepetition.VN.Modular.fz_eq_βop {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (x : K →L[ℂ] K) (η ξ : K) {z : ℂ} (hz : z ∈ StripCauchy.strip) : fz M Ω x η ξ z = ((βop M Ω) ((Efam M Ω (-z)) ((Jm M Ω) η))) (x ((Efam M Ω (-z)) ξ))

On the strip, f(z) = β(E(−z) Jη, x E(−z) ξ).

theorem CommutingRepetition.VN.Modular.differentiableOn_fz {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (x : K →L[ℂ] K) (η ξ : K) : DifferentiableOn ℂ (fz M Ω x η ξ) StripCauchy.ostrip

theorem CommutingRepetition.VN.Modular.fz_zero {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (x : K →L[ℂ] K) (η ξ : K) : fz M Ω x η ξ 0 = inner ℂ η ((Tm M Ω) (x ((Tm M Ω) ξ)))

theorem CommutingRepetition.VN.Modular.fz_half_add {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (x : K →L[ℂ] K) (η ξ : K) (t : ℝ) : fz M Ω x η ξ (1 / 2 + ↑t * Complex.I) = inner ℂ η ((2 - R M Ω) ((Δit M Ω t) (x ((R M Ω) ((Δit M Ω (-t)) ξ)))))

theorem CommutingRepetition.VN.Modular.fz_neg_half_add {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (x : K →L[ℂ] K) (η ξ : K) (t : ℝ) : fz M Ω x η ξ (-1 / 2 + ↑t * Complex.I) = inner ℂ η ((R M Ω) ((Δit M Ω t) (x ((2 - R M Ω) ((Δit M Ω (-t)) ξ)))))

theorem CommutingRepetition.VN.Modular.sandwich_eq {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (x B : K →L[ℂ] K) (l : ℂ) (hB : Tm M Ω * B * Tm M Ω = l • ((2 - R M Ω) * x * R M Ω) + (starRingEnd ℂ) l • (R M Ω * x * (2 - R M Ω))) (t : ℝ) : l • ((2 - R M Ω) * Δit M Ω t * x * (R M Ω * Δit M Ω (-t))) + (starRingEnd ℂ) l • (R M Ω * Δit M Ω t * x * ((2 - R M Ω) * Δit M Ω (-t))) = Tm M Ω * (Δit M Ω t * B * Δit M Ω (-t)) * Tm M Ω

The operator identity behind λ f(1/2+it) + λ̄ f(-1/2+it) = ⟪η, T Δ^{it} B Δ^{-it} T ξ⟫.

theorem CommutingRepetition.VN.Modular.Tm_mul_eq_Tm_Wop {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') {φ : ℝ} (hφ : |φ| < Real.pi) {x : K →L[ℂ] K} (hB : Tm M Ω * conjJm M Ω x' * Tm M Ω = Complex.exp (Complex.I * ↑φ / 2) • ((2 - R M Ω) * x * R M Ω) + (starRingEnd ℂ) (Complex.exp (Complex.I * ↑φ / 2)) • (R M Ω * x * (2 - R M Ω))) : Tm M Ω * x * Tm M Ω = Tm M Ω * Wop M Ω (conjJm M Ω x') φ hφ * Tm M Ω

RvD Lemma 4.7: T x T = T W T for x as in Lemma 4.5 (with λ = e^{iφ/2}).

theorem CommutingRepetition.VN.Modular.eq_Wop_of_Tm_mul_eq {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {x S : K →L[ℂ] K} (h : Tm M Ω * x * Tm M Ω = Tm M Ω * S * Tm M Ω) : x = S

RvD Lemma 4.7 (operator form): x = ∫ w_φ(t) Δ^{it} (J x′ J) Δ^{-it} dt.

theorem CommutingRepetition.VN.Modular.Wop_conjJm_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.commutant) (hsa' : IsSelfAdjoint x') {φ : ℝ} (hφ : |φ| < Real.pi) : Wop M Ω (conjJm M Ω x') φ hφ ∈ M

For self-adjoint x′ ∈ M′ and |φ| < π, the weak integral W lies in M.

RvD Lemma 4.8: Δ^{it} (J x′ J) Δ^{-it} ∈ M

theorem CommutingRepetition.VN.Modular.integrable_clm_Wint {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (B : K →L[ℂ] K) {φ : ℝ} (hφ : |φ| < Real.pi) (S : K →L[ℂ] K) (ξ : K) : MeasureTheory.Integrable (fun (t : ℝ) => ↑(StripCauchy.w φ t) • S ((Δit M Ω t) (B ((Δit M Ω (-t)) ξ)))) MeasureTheory.volume

theorem CommutingRepetition.VN.Modular.integrable_w_mul_inner {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (B : K →L[ℂ] K) {φ : ℝ} (hφ : |φ| < Real.pi) (S : K →L[ℂ] K) (η ξ : K) : MeasureTheory.Integrable (fun (t : ℝ) => ↑(StripCauchy.w φ t) * inner ℂ η (S ((Δit M Ω t) (B ((Δit M Ω (-t)) ξ))))) MeasureTheory.volume

theorem CommutingRepetition.VN.Modular.inner_clm_Wop {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (B : K →L[ℂ] K) {φ : ℝ} (hφ : |φ| < Real.pi) (S : K →L[ℂ] K) (η ξ : K) : inner ℂ η (S ((Wop M Ω B φ hφ) ξ)) = ∫ (t : ℝ), ↑(StripCauchy.w φ t) * inner ℂ η (S ((Δit M Ω t) (B ((Δit M Ω (-t)) ξ))))

theorem CommutingRepetition.VN.Modular.exists_sa_decomp {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : VonNeumannAlgebra K) {x : K →L[ℂ] K} (hx : x ∈ N) : ∃ (a : K →L[ℂ] K) (b : K →L[ℂ] K), a ∈ N ∧ b ∈ N ∧ IsSelfAdjoint a ∧ IsSelfAdjoint b ∧ x = a + Complex.I • b

Every x ∈ N is a + i b with a, b ∈ N self-adjoint.

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

theorem CommutingRepetition.VN.Modular.conjJm_smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (c : ℂ) (G : K →L[ℂ] K) : conjJm M Ω (c • G) = (starRingEnd ℂ) c • conjJm M Ω G

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

theorem CommutingRepetition.VN.Modular.conjJm_mul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (G H : K →L[ℂ] K) : conjJm M Ω (G * H) = conjJm M Ω G * conjJm M Ω H

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

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

theorem CommutingRepetition.VN.Modular.star_conjJm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (G : K →L[ℂ] K) : star (conjJm M Ω G) = conjJm M Ω (star G)

theorem CommutingRepetition.VN.Modular.sa_Δit_conjJm_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.commutant) (hsa' : IsSelfAdjoint x') (t : ℝ) : Δit M Ω t * conjJm M Ω x' * Δit M Ω (-t) ∈ M

RvD Lemma 4.8 (self-adjoint case): Δ^{it} (J x′ J) Δ^{-it} ∈ M for self-adjoint x′ ∈ M′, by Laplace-transform uniqueness applied to the commutator with y′ ∈ M′.

theorem CommutingRepetition.VN.Modular.Δit_conjJm_Δit_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.commutant) (t : ℝ) : Δit M Ω t * conjJm M Ω x' * Δit M Ω (-t) ∈ M

RvD Lemma 4.8: Δ^{it} (J x′ J) Δ^{-it} ∈ M for every x′ ∈ M′.

theorem CommutingRepetition.VN.Modular.conjJm_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.commutant) : conjJm M Ω x' ∈ M

J M′ J ⊆ M.

RvD Lemma 4.9: J M J ⊆ M′

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

For ξ ∈ 𝒦, Q (J ξ) = 0.

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

For ξ, η ∈ 𝒦, ⟪J ξ, η⟫ is real.

theorem CommutingRepetition.VN.Modular.inner_conjJm_Ω_sa {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {x y : K →L[ℂ] K} (hx : x ∈ M) (hxs : IsSelfAdjoint x) (hy : y ∈ M) (hys : IsSelfAdjoint y) : inner ℂ Ω (y ((conjJm M Ω x) Ω)) = inner ℂ (x ((conjJm M Ω y) Ω)) Ω

Claim A (self-adjoint case): ⟪Ω, y J x Ω⟫ = ⟪x J y Ω, Ω⟫ for x, y ∈ M_s.

theorem CommutingRepetition.VN.Modular.inner_conjJm_Ω {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {x y : K →L[ℂ] K} (hx : x ∈ M) (hy : y ∈ M) : inner ℂ Ω (y ((conjJm M Ω x) Ω)) = inner ℂ (x ((conjJm M Ω y) Ω)) Ω

Claim A: ⟪Ω, y J x Ω⟫ = ⟪x J y Ω, Ω⟫ for x, y ∈ M.

theorem CommutingRepetition.VN.Modular.conjJm_apply_Ω_comm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {x y : K →L[ℂ] K} (hx : x ∈ M) (hy : y ∈ M) : (conjJm M Ω y) (x Ω) = x ((conjJm M Ω y) Ω)

Claim B: (J y J)(x Ω) = x (J y J Ω) for x, y ∈ M.

theorem CommutingRepetition.VN.Modular.conjJm_mem_commutant {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {y : K →L[ℂ] K} (hy : y ∈ M) : conjJm M Ω y ∈ M.commutant

RvD Lemma 4.9: J M J ⊆ M′.

RvD Theorem 4.2 and the modular automorphism group

theorem CommutingRepetition.VN.Modular.conjJm_mem_commutant_iff {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (x : K →L[ℂ] K) : conjJm M Ω x ∈ M.commutant ↔ x ∈ M

Tomita's theorem, part 1: J M J = M′.

theorem CommutingRepetition.VN.Modular.conjJm_mem_iff {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (x : K →L[ℂ] K) : conjJm M Ω x ∈ M ↔ x ∈ M.commutant

Tomita's theorem, part 1′: J M′ J = M.

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

The modular automorphism group σ_t(x) = Δ^{it} x Δ^{-it}.

Equations

• CommutingRepetition.VN.Modular.σ M Ω t x = CommutingRepetition.VN.Modular.Δit M Ω t * x * CommutingRepetition.VN.Modular.Δit M Ω (-t)

theorem CommutingRepetition.VN.Modular.σ_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (t : ℝ) (x : K →L[ℂ] K) (ξ : K) : (σ M Ω t x) ξ = (Δit M Ω t) (x ((Δit M Ω (-t)) ξ))

theorem CommutingRepetition.VN.Modular.σ_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) (t : ℝ) : σ M Ω t x ∈ M

Tomita's theorem, part 2: Δ^{it} M Δ^{-it} ⊆ M.

theorem CommutingRepetition.VN.Modular.conjJm_σ {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (t : ℝ) (x : K →L[ℂ] K) : conjJm M Ω (σ M Ω t x) = σ M Ω t (conjJm M Ω x)

theorem CommutingRepetition.VN.Modular.σ_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) (t : ℝ) : σ M Ω t x ∈ M.commutant

theorem CommutingRepetition.VN.Modular.σ_zero {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (x : K →L[ℂ] K) : σ M Ω 0 x = x

theorem CommutingRepetition.VN.Modular.σ_add {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (s t : ℝ) (x : K →L[ℂ] K) : σ M Ω (s + t) x = σ M Ω s (σ M Ω t x)

theorem CommutingRepetition.VN.Modular.σ_neg_σ {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (t : ℝ) (x : K →L[ℂ] K) : σ M Ω (-t) (σ M Ω t x) = x

theorem CommutingRepetition.VN.Modular.σ_σ_neg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (t : ℝ) (x : K →L[ℂ] K) : σ M Ω t (σ M Ω (-t) x) = x

theorem CommutingRepetition.VN.Modular.σ_mul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (t : ℝ) (x y : K →L[ℂ] K) : σ M Ω t (x * y) = σ M Ω t x * σ M Ω t y

theorem CommutingRepetition.VN.Modular.σ_add_op {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (t : ℝ) (x y : K →L[ℂ] K) : σ M Ω t (x + y) = σ M Ω t x + σ M Ω t y

theorem CommutingRepetition.VN.Modular.σ_smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (t : ℝ) (c : ℂ) (x : K →L[ℂ] K) : σ M Ω t (c • x) = c • σ M Ω t x

theorem CommutingRepetition.VN.Modular.σ_star {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (t : ℝ) (x : K →L[ℂ] K) : σ M Ω t (star x) = star (σ M Ω t x)

theorem CommutingRepetition.VN.Modular.σ_one {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (t : ℝ) : σ M Ω t 1 = 1

theorem CommutingRepetition.VN.Modular.σ_apply_Ω {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (t : ℝ) (x : K →L[ℂ] K) : (σ M Ω t x) Ω = (Δit M Ω t) (x Ω)

theorem CommutingRepetition.VN.Modular.inner_Ω_σ {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (t : ℝ) (x : K →L[ℂ] K) : inner ℂ Ω ((σ M Ω t x) Ω) = inner ℂ Ω (x Ω)

ψ ∘ σ_t = ψ for the vector state ψ = ⟪Ω, · Ω⟫.

theorem CommutingRepetition.VN.Modular.σ_eq_self_iff {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (t : ℝ) (x : K →L[ℂ] K) : σ M Ω t x = x ↔ Commute (Δit M Ω t) x

theorem CommutingRepetition.VN.Modular.σ_eq_self_of_commute_R {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {x : K →L[ℂ] K} (h : Commute x (R M Ω)) (t : ℝ) : σ M Ω t x = x

Elements commuting with R are fixed by the modular group.