MIPRE.Background.Repetition.CommutingRepetition.VN.Modular.Perturb

The scalar functions #

source

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

ℝ

Clamp to [0,2].

Equations

CommutingRepetition.VN.Modular.clR l = max 0 (min l 2)

Instances For

source

theorem CommutingRepetition.VN.Modular.continuous_clR :

Continuous clR

source

theorem CommutingRepetition.VN.Modular.clR_nonneg (l : ℝ) :

0 ≤ clR l

source

theorem CommutingRepetition.VN.Modular.clR_le_two (l : ℝ) :

clR l ≤ 2

source

theorem CommutingRepetition.VN.Modular.bdd_clR :

BorelCalc.Bdd clR

source

theorem CommutingRepetition.VN.Modular.clR_eq_self {l : ℝ} (h : l ∈ Set.Icc 0 2) :

clR l = l

source

noncomputable def CommutingRepetition.VN.Modular.dfn (C m : ℝ) :

ℝ

e^{clamp C m}.

Equations

CommutingRepetition.VN.Modular.dfn C m = Real.exp (CommutingRepetition.VN.Modular.clamp C m)

Instances For

source

theorem CommutingRepetition.VN.Modular.continuous_dfn (C : ℝ) :

Continuous (dfn C)

source

theorem CommutingRepetition.VN.Modular.dfn_pos (C m : ℝ) :

0 < dfn C m

source

theorem CommutingRepetition.VN.Modular.dfn_ge {C : ℝ} (hC : 0 ≤ C) (m : ℝ) :

Real.exp (-C) ≤ dfn C m

source

theorem CommutingRepetition.VN.Modular.bdd_dfn {C : ℝ} (hC : 0 ≤ C) :

BorelCalc.Bdd (dfn C)

source

noncomputable def CommutingRepetition.VN.Modular.den (C : ℝ) (p : ℝ × ℝ) :

ℝ

The denominator l + e^m(2 − l) (with the clamps).

Equations

CommutingRepetition.VN.Modular.den C p = CommutingRepetition.VN.Modular.clR p.1 + CommutingRepetition.VN.Modular.dfn C p.2 * (2 - CommutingRepetition.VN.Modular.clR p.1)

Instances For

source

noncomputable def CommutingRepetition.VN.Modular.denLB (C : ℝ) :

ℝ

The lower bound for the denominator.

Equations

CommutingRepetition.VN.Modular.denLB C = 2 * min 1 (Real.exp (-C))

Instances For

source

theorem CommutingRepetition.VN.Modular.denLB_pos (C : ℝ) :

0 < denLB C

source

theorem CommutingRepetition.VN.Modular.den_ge {C : ℝ} (hC : 0 ≤ C) (p : ℝ × ℝ) :

denLB C ≤ den C p

source

theorem CommutingRepetition.VN.Modular.den_pos {C : ℝ} (hC : 0 ≤ C) (p : ℝ × ℝ) :

0 < den C p

source

theorem CommutingRepetition.VN.Modular.den_ne_zero {C : ℝ} (hC : 0 ≤ C) (p : ℝ × ℝ) :

den C p ≠ 0

source

theorem CommutingRepetition.VN.Modular.continuous_den (C : ℝ) :

Continuous (den C)

source

theorem CommutingRepetition.VN.Modular.den_le {C : ℝ} (hC : 0 ≤ C) (p : ℝ × ℝ) :

den C p ≤ 2 + 2 * Real.exp C

source

theorem CommutingRepetition.VN.Modular.bdd2_den {C : ℝ} (hC : 0 ≤ C) :

BorelCalc.Bdd2 (den C)

source

noncomputable def CommutingRepetition.VN.Modular.fN (C : ℝ) (p : ℝ × ℝ) :

ℝ

1/den: the symbol of the inverse (R + e^B(2−R))⁻¹.

Equations

CommutingRepetition.VN.Modular.fN C p = 1 / CommutingRepetition.VN.Modular.den C p

Instances For

source

noncomputable def CommutingRepetition.VN.Modular.fR (C : ℝ) (p : ℝ × ℝ) :

ℝ

2l/den: the symbol of the perturbed modular operator.

Equations

CommutingRepetition.VN.Modular.fR C p = 2 * CommutingRepetition.VN.Modular.clR p.1 / CommutingRepetition.VN.Modular.den C p

Instances For

source

theorem CommutingRepetition.VN.Modular.continuous_fN {C : ℝ} (hC : 0 ≤ C) :

Continuous (fN C)

source

theorem CommutingRepetition.VN.Modular.continuous_fR {C : ℝ} (hC : 0 ≤ C) :

Continuous (fR C)

source

theorem CommutingRepetition.VN.Modular.fN_nonneg {C : ℝ} (hC : 0 ≤ C) (p : ℝ × ℝ) :

0 ≤ fN C p

source

theorem CommutingRepetition.VN.Modular.fN_le {C : ℝ} (hC : 0 ≤ C) (p : ℝ × ℝ) :

fN C p ≤ 1 / denLB C

source

theorem CommutingRepetition.VN.Modular.bdd2_fN {C : ℝ} (hC : 0 ≤ C) :

BorelCalc.Bdd2 (fN C)

source

theorem CommutingRepetition.VN.Modular.fR_nonneg {C : ℝ} (hC : 0 ≤ C) (p : ℝ × ℝ) :

0 ≤ fR C p

source

theorem CommutingRepetition.VN.Modular.fR_le_two {C : ℝ} (hC : 0 ≤ C) (p : ℝ × ℝ) :

fR C p ≤ 2

source

theorem CommutingRepetition.VN.Modular.bdd2_fR {C : ℝ} (hC : 0 ≤ C) :

BorelCalc.Bdd2 (fR C)

source

theorem CommutingRepetition.VN.Modular.fN_mul_den {C : ℝ} (hC : 0 ≤ C) (p : ℝ × ℝ) :

fN C p * den C p = 1

source

theorem CommutingRepetition.VN.Modular.fR_eq (C : ℝ) (p : ℝ × ℝ) :

fR C p = 2 * (clR p.1 * fN C p)

The Fourier symbol: `θ(fR) = clamp C m + θ(l)` on `(0,2)` #

source

theorem CommutingRepetition.VN.Modular.fR_mem_Ioo {C : ℝ} (hC : 0 ≤ C) {p : ℝ × ℝ} (hp : p.1 ∈ Set.Ioo 0 2) :

fR C p ∈ Set.Ioo 0 2

source

theorem CommutingRepetition.VN.Modular.θ_fR {C : ℝ} (hC : 0 ≤ C) {p : ℝ × ℝ} (hp : p.1 ∈ Set.Ioo 0 2) :

θ (fR C p) = clamp C p.2 + θ p.1

source

theorem CommutingRepetition.VN.Modular.gDel_fR {C : ℝ} (hC : 0 ≤ C) (t : ℝ) {p : ℝ × ℝ} (hp : p.1 ∈ Set.Ioo 0 2) :

gDel t (fR C p) = eitf t (clamp C p.2) * gDel t p.1

The Fourier symbol of the perturbed modular operator on (0,2).

The operators for a commuting pair `(E, B)` #

source

theorem CommutingRepetition.VN.Modular.bdd2_clR_fst :

BorelCalc.Bdd2 fun (p : ℝ × ℝ) => clR p.1

source

theorem CommutingRepetition.VN.Modular.bdd2_two_sub_clR :

BorelCalc.Bdd2 fun (p : ℝ × ℝ) => 2 - clR p.1

source

theorem CommutingRepetition.VN.Modular.bdd2_dfn_snd {C : ℝ} (hC : 0 ≤ C) :

BorelCalc.Bdd2 fun (p : ℝ × ℝ) => dfn C p.2

source

theorem CommutingRepetition.VN.Modular.bfc_clR {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ ] K} (hE : IsSelfAdjoint E) (hsp : spectrum ℝ E ⊆ Set.Icc 0 2) :

BorelCalc.bfc E hE clR = E

clR is the identity on the spectrum of E when spectrum E ⊆ [0,2].

source

theorem CommutingRepetition.VN.Modular.bfc_dfn {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {B : K →L[ℂ ] K} (hB : IsSelfAdjoint B) :

BorelCalc.bfc B hB (dfn ‖B‖) = expA B 1

source

theorem CommutingRepetition.VN.Modular.jbfc_clR_fst {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E B : K →L[ℂ ] K} (hE : IsSelfAdjoint E) (hB : IsSelfAdjoint B) (hcm : Commute E B) (hsp : spectrum ℝ E ⊆ Set.Icc 0 2) :

(BorelCalc.jbfc E B hE hB hcm fun (p : ℝ × ℝ) => clR p.1) = E

source

theorem CommutingRepetition.VN.Modular.jbfc_dfn_snd {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E B : K →L[ℂ ] K} (hE : IsSelfAdjoint E) (hB : IsSelfAdjoint B) (hcm : Commute E B) :

(BorelCalc.jbfc E B hE hB hcm fun (p : ℝ × ℝ) => dfn ‖B‖ p.2) = expA B 1

source

theorem CommutingRepetition.VN.Modular.jbfc_two_sub_clR {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E B : K →L[ℂ ] K} (hE : IsSelfAdjoint E) (hB : IsSelfAdjoint B) (hcm : Commute E B) (hsp : spectrum ℝ E ⊆ Set.Icc 0 2) :

(BorelCalc.jbfc E B hE hB hcm fun (p : ℝ × ℝ) => 2 - clR p.1) = 2 - E

source

theorem CommutingRepetition.VN.Modular.jbfc_den {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E B : K →L[ℂ ] K} (hE : IsSelfAdjoint E) (hB : IsSelfAdjoint B) (hcm : Commute E B) (hsp : spectrum ℝ E ⊆ Set.Icc 0 2) :

BorelCalc.jbfc E B hE hB hcm (den ‖B‖) = E + expA B 1 * (2 - E)

E + e^B(2 − E) is the jbfc of the denominator.

source

theorem CommutingRepetition.VN.Modular.jbfc_fN_mul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E B : K →L[ℂ ] K} (hE : IsSelfAdjoint E) (hB : IsSelfAdjoint B) (hcm : Commute E B) (hsp : spectrum ℝ E ⊆ Set.Icc 0 2) :

BorelCalc.jbfc E B hE hB hcm (fN ‖B‖) * (E + expA B 1 * (2 - E)) = 1

The inverse relation: (E + e^B(2−E))⁻¹ (E + e^B(2−E)) = 1.

source

theorem CommutingRepetition.VN.Modular.jbfc_fR_eq {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E B : K →L[ℂ ] K} (hE : IsSelfAdjoint E) (hB : IsSelfAdjoint B) (hcm : Commute E B) (hsp : spectrum ℝ E ⊆ Set.Icc 0 2) :

BorelCalc.jbfc E B hE hB hcm (fR ‖B‖) = ↑2 • (E * BorelCalc.jbfc E B hE hB hcm (fN ‖B‖))

2E(E + e^B(2−E))⁻¹ is the jbfc of fR.

source

theorem CommutingRepetition.VN.Modular.commute_jbfc_fN {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E B : K →L[ℂ ] K} (hE : IsSelfAdjoint E) (hB : IsSelfAdjoint B) (hcm : Commute E B) {T : K →L[ℂ ] K} (h1 : Commute E T) (h2 : Commute B T) :

Commute (BorelCalc.jbfc E B hE hB hcm (fN ‖B‖)) T

The modular group of the perturbed operator #

source

theorem CommutingRepetition.VN.Modular.ae_fst_mem_Ioo {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E B : K →L[ℂ ] K} (hE : IsSelfAdjoint E) (hB : IsSelfAdjoint B) (hcm : Commute E B) (hν : ∀ (ζ : K), (BorelCalc.ν E hE ζ) (Set.Ioo 0 2)ᶜ = 0) (ζ : K) :

∀ᵐ (p : ℝ × ℝ) ∂BorelCalc.νP E B hE hB hcm ζ, p.1 ∈ Set.Ioo 0 2

source

theorem CommutingRepetition.VN.Modular.cbfc_jbfc_fR_gDel {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E B : K →L[ℂ ] K} (hE : IsSelfAdjoint E) (hB : IsSelfAdjoint B) (hcm : Commute E B) (hν : ∀ (ζ : K), (BorelCalc.ν E hE ζ) (Set.Ioo 0 2)ᶜ = 0) (t : ℝ) :

BorelCalc.cbfc (BorelCalc.jbfc E B hE hB hcm (fR ‖B‖)) ⋯ (gDel t) = eit B hB t * BorelCalc.cbfc E hE (gDel t)

The modular group of the perturbed operator: (fR)(E,B)^{it} = e^{itB} E^{it} in the sense of the Fourier symbols gDel.

(M3): the modular data of `ξ = e^{-a/2}Ω` #

source

theorem CommutingRepetition.VN.Modular.commute_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {x y : K →L[ℂ ] K} (h : Commute x y) (ζ : K) :

x (y ζ) = y (x ζ)

source

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

K →L[ℂ ] K

B = a′ − a, with a′ = J a J.

Equations

CommutingRepetition.VN.Modular.Bp M Ω a = CommutingRepetition.VN.Modular.conjJm M Ω a - a

Instances For

source

theorem CommutingRepetition.VN.Modular.isSelfAdjoint_Bp {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (hsa : IsSelfAdjoint a) :

IsSelfAdjoint (Bp M Ω a)

source

theorem CommutingRepetition.VN.Modular.commute_R_Bp {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (haR : Commute a (R M Ω)) :

Commute (R M Ω) (Bp M Ω a)

source

theorem CommutingRepetition.VN.Modular.commute_a_conjJm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (ha : a ∈ M) :

Commute a (conjJm M Ω a)

source

theorem CommutingRepetition.VN.Modular.commute_Bp_expA_a {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (ha : a ∈ M) (r : ℝ) :

Commute (Bp M Ω a) (expA a r)

source

theorem CommutingRepetition.VN.Modular.commute_Bp_expA_conjJm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (ha : a ∈ M) (r : ℝ) :

Commute (Bp M Ω a) (expA (conjJm M Ω a) r)

source

noncomputable def CommutingRepetition.VN.Modular.Nop {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (hsa : IsSelfAdjoint a) (haR : Commute a (R M Ω)) :

K →L[ℂ ] K

The inverse (R + e^B(2−R))⁻¹.

Equations

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

Instances For

source

noncomputable def CommutingRepetition.VN.Modular.Rpert {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (hsa : IsSelfAdjoint a) (haR : Commute a (R M Ω)) :

K →L[ℂ ] K

The perturbed modular operator 2R(R + e^B(2−R))⁻¹.

Equations

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

Instances For

source

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

K →L[ℂ ] K

e^{-a/2}e^{a′/2}.

Equations

CommutingRepetition.VN.Modular.Emul M Ω a = CommutingRepetition.VN.Modular.expA a (-(1 / 2)) * CommutingRepetition.VN.Modular.expA (CommutingRepetition.VN.Modular.conjJm M Ω a) (1 / 2)

Instances For

source

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

K →L[ℂ ] K

e^{a/2}e^{-a′/2}, the inverse of Emul.

Equations

CommutingRepetition.VN.Modular.Einv M Ω a = CommutingRepetition.VN.Modular.expA a (1 / 2) * CommutingRepetition.VN.Modular.expA (CommutingRepetition.VN.Modular.conjJm M Ω a) (-(1 / 2))

Instances For

source

theorem CommutingRepetition.VN.Modular.Emul_mul_Einv {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (ha : a ∈ M) (hsa : IsSelfAdjoint a) :

Emul M Ω a * Einv M Ω a = 1

source

theorem CommutingRepetition.VN.Modular.Emul_mul_Emul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (ha : a ∈ M) (hsa : IsSelfAdjoint a) :

Emul M Ω a * Emul M Ω a = expA (Bp M Ω a) 1

source

theorem CommutingRepetition.VN.Modular.commute_Nop {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (hsa : IsSelfAdjoint a) (haR : Commute a (R M Ω)) {T : K →L[ℂ ] K} (h1 : Commute (R M Ω) T) (h2 : Commute (Bp M Ω a) T) :

Commute (Nop M Ω hs hc a hsa haR) T

source

theorem CommutingRepetition.VN.Modular.commute_Nop_R {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (hsa : IsSelfAdjoint a) (haR : Commute a (R M Ω)) :

Commute (Nop M Ω hs hc a hsa haR) (R M Ω)

source

theorem CommutingRepetition.VN.Modular.commute_Nop_expA_a {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (ha : a ∈ M) (hsa : IsSelfAdjoint a) (haR : Commute a (R M Ω)) (r : ℝ) :

Commute (Nop M Ω hs hc a hsa haR) (expA a r)

source

theorem CommutingRepetition.VN.Modular.commute_Nop_expA_conjJm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (ha : a ∈ M) (hsa : IsSelfAdjoint a) (haR : Commute a (R M Ω)) (r : ℝ) :

Commute (Nop M Ω hs hc a hsa haR) (expA (conjJm M Ω a) r)

source

theorem CommutingRepetition.VN.Modular.commute_Nop_Emul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (ha : a ∈ M) (hsa : IsSelfAdjoint a) (haR : Commute a (R M Ω)) :

Commute (Nop M Ω hs hc a hsa haR) (Emul M Ω a)

source

theorem CommutingRepetition.VN.Modular.commute_Nop_Einv {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (ha : a ∈ M) (hsa : IsSelfAdjoint a) (haR : Commute a (R M Ω)) :

Commute (Nop M Ω hs hc a hsa haR) (Einv M Ω a)

source

theorem CommutingRepetition.VN.Modular.Nop_mul_den {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (hsa : IsSelfAdjoint a) (haR : Commute a (R M Ω)) :

Nop M Ω hs hc a hsa haR * (R M Ω + expA (Bp M Ω a) 1 * (2 - R M Ω)) = 1

source

theorem CommutingRepetition.VN.Modular.Rpert_eq {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (hsa : IsSelfAdjoint a) (haR : Commute a (R M Ω)) :

Rpert M Ω hs hc a hsa haR = ↑2 • (R M Ω * Nop M Ω hs hc a hsa haR)

The candidate conjugate-linear part #

source

noncomputable def CommutingRepetition.VN.Modular.Xpert {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (hsa : IsSelfAdjoint a) (haR : Commute a (R M Ω)) :

K →L[ℂ ] K

The complex-linear factor of A_ξ.

Equations

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

Instances For

source

noncomputable def CommutingRepetition.VN.Modular.Apert {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (hsa : IsSelfAdjoint a) (haR : Commute a (R M Ω)) :

K →L⋆[ℂ ] K

The candidate for T_ξ J_ξ.

Equations

CommutingRepetition.VN.Modular.Apert M Ω hs hc a hsa haR = CommutingRepetition.VN.Modular.Xpert M Ω hs hc a hsa haR ∘SL CommutingRepetition.VN.Modular.Jm M Ω

Instances For

source

theorem CommutingRepetition.VN.Modular.Apert_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (hsa : IsSelfAdjoint a) (haR : Commute a (R M Ω)) (ζ : K) :

(Apert M Ω hs hc a hsa haR) ζ = ↑2 • (Emul M Ω a) ((Nop M Ω hs hc a hsa haR) ((Tm M Ω) ((Jm M Ω) ζ)))

source

theorem CommutingRepetition.VN.Modular.Tm_Jm_expA_conjJm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (hsa : IsSelfAdjoint a) (haR : Commute a (R M Ω)) (r : ℝ) (ζ : K) :

(Tm M Ω) ((Jm M Ω) ((expA (conjJm M Ω a) r) ζ)) = (expA a r) ((Tm M Ω) ((Jm M Ω) ζ))

The transport of T J past e^{ra′}.

The projection identities #

source

theorem CommutingRepetition.VN.Modular.hfix_pert {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (ha : a ∈ M) (hsa : IsSelfAdjoint a) (haR : Commute a (R M Ω)) {k : K} (hk : k ∈ Kre M (pvec Ω a)) :

(Rpert M Ω hs hc a hsa haR) k + (Apert M Ω hs hc a hsa haR) k = 2 • k

source

theorem CommutingRepetition.VN.Modular.hker_pert {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (ha : a ∈ M) (hsa : IsSelfAdjoint a) (haR : Commute a (R M Ω)) {η : K} (hη : η ∈ (↑(Kre M (pvec Ω a)))ᗮ) :

(Rpert M Ω hs hc a hsa haR) η + (Apert M Ω hs hc a hsa haR) η = 0

(M3) #

source

theorem CommutingRepetition.VN.Modular.R_pvec {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (ha : a ∈ M) (hsa : IsSelfAdjoint a) (haR : Commute a (R M Ω)) :

R M (pvec Ω a) = Rpert M Ω hs hc a hsa haR

(M3), the modular operator: R(M, ξ) = 2R(R + e^{a′−a}(2 − R))⁻¹ for ξ = e^{-a/2}Ω.

source

theorem CommutingRepetition.VN.Modular.Δit_pvec {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (ha : a ∈ M) (hsa : IsSelfAdjoint a) (haR : Commute a (R M Ω)) (t : ℝ) :

Δit M (pvec Ω a) t = eit (Bp M Ω a) ⋯ t * Δit M Ω t

(M3), the modular group: Δ_ξ^{it} = e^{it(a′−a)}Δ^{it}.

source

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

IsSeparating (↑M) (pvec Ω a)

ξ = e^{-a/2}Ω is cyclic and separating, so the whole modular package applies to it.

source

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

IsCyclic (↑M) (pvec Ω a)

source

theorem CommutingRepetition.VN.Modular.isCentral_pvec_of_σ_eq_self {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (a : K →L[ℂ ] K) (ha : a ∈ M) (hsa : IsSelfAdjoint a) {x : K →L[ℂ ] K} (hx : x ∈ M) (h : ∀ (t : ℝ), σ M (pvec Ω a) t x = x) :

IsCentral M (pvec Ω a) x

A fixed point of the perturbed modular group is in the perturbed centralizer, hence ψ_ξ-tracial (IsCentral.tracial).

The scalar functions #

The Fourier symbol: θ(fR) = clamp C m + θ(l) on (0,2) #

The operators for a commuting pair (E, B) #

The modular group of the perturbed operator #

(M3): the modular data of ξ = e^{-a/2}Ω #

The candidate conjugate-linear part #

The projection identities #

(M3) #

The Fourier symbol: `θ(fR) = clamp C m + θ(l)` on `(0,2)` #

The operators for a commuting pair `(E, B)` #

(M3): the modular data of `ξ = e^{-a/2}Ω` #