theorem CommutingRepetition.VN.Modular.two_apply_eq {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (ξ : K) : 2 ξ = ξ + ξ

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

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

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

theorem CommutingRepetition.VN.Modular.commute_two_sub_R_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 Ω)) : Commute x (2 - R M Ω)

An operator commuting with R commutes with 2 − R.

theorem CommutingRepetition.VN.Modular.inner_two_sub_R_apply {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 ℂ ((2 - R M Ω) (x Ω)) ((2 - R M Ω) ((star y) Ω)) = inner ℂ ((R M Ω * (2 - R M Ω)) (y Ω)) ((star x) Ω)

The bounded KMS-type identity: ⟪(2−R) xΩ, (2−R) y*Ω⟫ = ⟪R(2−R) yΩ, x*Ω⟫ for x, y ∈ M.

theorem CommutingRepetition.VN.Modular.inner_Ω_mul_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) (hxR : Commute x (R M Ω)) (hy : y ∈ M) : inner ℂ Ω ((x * y) Ω) = inner ℂ Ω ((y * x) Ω)

(M2): an element of M commuting with R is ψ-central: ψ(x y) = ψ(y x).

The centralizer

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

The centralizer of ψ: elements of M commuting with R (hence with every bounded Borel function of R; in particular fixed by the modular group).

Equations

• CommutingRepetition.VN.Modular.IsCentral M Ω x = (x ∈ M ∧ Commute x (CommutingRepetition.VN.Modular.R M Ω))

theorem CommutingRepetition.VN.Modular.IsCentral.mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {M : VonNeumannAlgebra K} {Ω : K} {x : K →L[ℂ] K} (h : IsCentral M Ω x) : x ∈ M

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

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

theorem CommutingRepetition.VN.Modular.IsCentral.one {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {M : VonNeumannAlgebra K} {Ω : K} : IsCentral M Ω 1

theorem CommutingRepetition.VN.Modular.IsCentral.star {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {M : VonNeumannAlgebra K} {Ω : K} {x : K →L[ℂ] K} (h : IsCentral M Ω x) : IsCentral M Ω (Star.star x)

theorem CommutingRepetition.VN.Modular.IsCentral.mul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {M : VonNeumannAlgebra K} {Ω : K} {x y : K →L[ℂ] K} (hx : IsCentral M Ω x) (hy : IsCentral M Ω y) : IsCentral M Ω (x * y)

theorem CommutingRepetition.VN.Modular.IsCentral.add {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {M : VonNeumannAlgebra K} {Ω : K} {x y : K →L[ℂ] K} (hx : IsCentral M Ω x) (hy : IsCentral M Ω y) : IsCentral M Ω (x + y)

theorem CommutingRepetition.VN.Modular.IsCentral.smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {M : VonNeumannAlgebra K} {Ω : K} (c : ℂ) {x : K →L[ℂ] K} (hx : IsCentral M Ω x) : IsCentral M Ω (c • x)

theorem CommutingRepetition.VN.Modular.IsCentral.cfc_real {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {M : VonNeumannAlgebra K} {Ω : K} {x : K →L[ℂ] K} (hx : IsCentral M Ω x) (f : ℝ → ℝ) : IsCentral M Ω (cfc f x)

Real continuous functions of a central element are central.

theorem CommutingRepetition.VN.Modular.IsCentral.tracial {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 : IsCentral M Ω x) (hy : y ∈ M) : inner ℂ Ω ((x * y) Ω) = inner ℂ Ω ((y * x) Ω)

(M2): ψ(x y) = ψ(y x) for central x and all y ∈ M.