MIPRE.Background.Repetition.CommutingRepetition.VN.Haagerup.Reduction

The generating unitaries `λ(2^{-n})` #

source

noncomputable def CommutingRepetition.VN.Haagerup.qn (n : ℕ) :

ℚ

The rational 2^{-n}.

Equations

CommutingRepetition.VN.Haagerup.qn n = 1 / 2 ^ n

Instances For

source

theorem CommutingRepetition.VN.Haagerup.qn_cast (n : ℕ) :

↑(qn n) = 1 / 2 ^ n

source

theorem CommutingRepetition.VN.Haagerup.qn_pos (n : ℕ) :

0 < qn n

source

noncomputable def CommutingRepetition.VN.Haagerup.un {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (n : ℕ) :

Crossed.L2Q K →L[ℂ ] Crossed.L2Q K

u_n = λ(2^{-n}).

Equations

CommutingRepetition.VN.Haagerup.un n = CommutingRepetition.VN.Crossed.shift (CommutingRepetition.VN.Haagerup.qn n)

Instances For

source

theorem CommutingRepetition.VN.Haagerup.star_un {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (n : ℕ) :

star (un n) = Crossed.shift (-qn n)

source

theorem CommutingRepetition.VN.Haagerup.star_un_mul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (n : ℕ) :

star (un n) * un n = 1

source

theorem CommutingRepetition.VN.Haagerup.un_mul_star {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (n : ℕ) :

un n * star (un n) = 1

source

theorem CommutingRepetition.VN.Haagerup.un_mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (n : ℕ) :

un n ∈ Crossed.crossed M Ω

source

theorem CommutingRepetition.VN.Haagerup.commute_un_amp {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (n : ℕ) (y : K →L[ℂ ] K) :

Commute (un n) (Crossed.amp y)

source

theorem CommutingRepetition.VN.Haagerup.commute_star_un_amp {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (n : ℕ) (y : K →L[ℂ ] K) :

Commute (star (un n)) (Crossed.amp y)

The logarithms `a_n` #

source

noncomputable def CommutingRepetition.VN.Haagerup.an {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (n : ℕ) :

Crossed.L2Q K →L[ℂ ] Crossed.L2Q K

a_n = 2^n·(−i log λ(2^{-n})): self-adjoint, in ℛ, and in the centralizer of ψ̂.

Equations

CommutingRepetition.VN.Haagerup.an n = ↑(2 ^ n) • CommutingRepetition.VN.Modular.ulog (CommutingRepetition.VN.Haagerup.un n) ⋯ ⋯

Instances For

source

theorem CommutingRepetition.VN.Haagerup.isSelfAdjoint_an {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (n : ℕ) :

IsSelfAdjoint (an n)

source

theorem CommutingRepetition.VN.Haagerup.an_mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (n : ℕ) :

an n ∈ Crossed.crossed M Ω

source

theorem CommutingRepetition.VN.Haagerup.commute_an_amp {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (n : ℕ) (y : K →L[ℂ ] K) :

Commute (an n) (Crossed.amp y)

source

theorem CommutingRepetition.VN.Haagerup.commute_an_R {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (n : ℕ) :

Commute (an n) (Modular.R (Crossed.crossed M Ω) (Crossed.Ωh Ω))

The exponentials of `a_n` #

source

theorem CommutingRepetition.VN.Haagerup.eit_an {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (n : ℕ) (t : ℝ) :

Modular.eit (an n) ⋯ t = Modular.eit (Modular.ulog (un n) ⋯ ⋯) ⋯ (t * 2 ^ n)

source

theorem CommutingRepetition.VN.Haagerup.eit_an_qn {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (n : ℕ) :

Modular.eit (an n) ⋯ (1 / 2 ^ n) = un n

source

theorem CommutingRepetition.VN.Haagerup.eit_an_neg_qn {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (n : ℕ) :

Modular.eit (an n) ⋯ (-(1 / 2 ^ n)) = star (un n)

The perturbed vectors and their modular groups #

source

noncomputable def CommutingRepetition.VN.Haagerup.xin {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (Ω : K) (n : ℕ) :

Crossed.L2Q K

ξ_n = e^{−a_n/2}Ω̂.

Equations

CommutingRepetition.VN.Haagerup.xin Ω n = CommutingRepetition.VN.Modular.pvec (CommutingRepetition.VN.Crossed.Ωh Ω) (CommutingRepetition.VN.Haagerup.an n)

Instances For

source

theorem CommutingRepetition.VN.Haagerup.isSeparating_xin {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (n : ℕ) :

IsSeparating (↑(Crossed.crossed M Ω)) (xin Ω n)

source

theorem CommutingRepetition.VN.Haagerup.isCyclic_xin {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (n : ℕ) :

IsCyclic (↑(Crossed.crossed M Ω)) (xin Ω n)

source

theorem CommutingRepetition.VN.Haagerup.Δit_xin {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (n : ℕ) (t : ℝ) :

Modular.Δit (Crossed.crossed M Ω) (xin Ω n) t = Modular.eit (Modular.Bp (Crossed.crossed M Ω) (Crossed.Ωh Ω) (an n)) ⋯ t * Modular.Δit (Crossed.crossed M Ω) (Crossed.Ωh Ω) t

source

theorem CommutingRepetition.VN.Haagerup.σ_xin {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (n : ℕ) (t : ℝ) {x : Crossed.L2Q K →L[ℂ ] Crossed.L2Q K} (hx : x ∈ Crossed.crossed M Ω) :

Modular.σ (Crossed.crossed M Ω) (xin Ω n) t x = Modular.eit (an n) ⋯ (-t) * Modular.σ (Crossed.crossed M Ω) (Crossed.Ωh Ω) t x * Modular.eit (an n) ⋯ t

The modular group of ξ_n: σ^{ξ_n}_t = Ad(e^{−ita_n}) ∘ σ̂_t on ℛ.

source

theorem CommutingRepetition.VN.Haagerup.σ_xin_period {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (n : ℕ) {x : Crossed.L2Q K →L[ℂ ] Crossed.L2Q K} (hx : x ∈ Crossed.crossed M Ω) :

Modular.σ (Crossed.crossed M Ω) (xin Ω n) (1 / 2 ^ n) x = x

Periodicity: σ^{ξ_n} is 2^{-n}-periodic on ℛ, i.e. trivial at t = 2^{-n}.

The centralizer algebra `ℛ_n` #

source

theorem CommutingRepetition.VN.Haagerup.isClosed_vn {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (N : VonNeumannAlgebra (Crossed.L2Q K)) :

IsClosed ↑N

source

theorem CommutingRepetition.VN.Haagerup.commute_star_of_isSelfAdjoint {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {A x : Crossed.L2Q K →L[ℂ ] Crossed.L2Q K} (hA : IsSelfAdjoint A) (h : Commute x A) :

Commute (star x) A

source

noncomputable def CommutingRepetition.VN.Haagerup.Rn {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (n : ℕ) :

StarSubalgebra ℂ (Crossed.L2Q K →L[ℂ ] Crossed.L2Q K)

The centralizer ℛ_n of the perturbed state: the elements of ℛ commuting with R(ℛ, ξ_n), equivalently the fixed points of σ^{ξ_n}.

Equations

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

Instances For

source

theorem CommutingRepetition.VN.Haagerup.mem_Rn_iff {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {n : ℕ} {x : Crossed.L2Q K →L[ℂ ] Crossed.L2Q K} :

x ∈ Rn M Ω n ↔ x ∈ Crossed.crossed M Ω ∧ Commute x (Modular.R (Crossed.crossed M Ω) (xin Ω n))

source

theorem CommutingRepetition.VN.Haagerup.isCentral_of_mem_Rn {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {n : ℕ} {x : Crossed.L2Q K →L[ℂ ] Crossed.L2Q K} (hx : x ∈ Rn M Ω n) :

Modular.IsCentral (Crossed.crossed M Ω) (xin Ω n) x

source

theorem CommutingRepetition.VN.Haagerup.mem_Rn_iff_σ {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {n : ℕ} {x : Crossed.L2Q K →L[ℂ ] Crossed.L2Q K} :

x ∈ Rn M Ω n ↔ x ∈ Crossed.crossed M Ω ∧ ∀ (t : ℝ), Modular.σ (Crossed.crossed M Ω) (xin Ω n) t x = x

ℛ_n is exactly the fixed-point algebra of σ^{ξ_n}.

source

theorem CommutingRepetition.VN.Haagerup.isClosed_Rn {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (n : ℕ) :

IsClosed ↑(Rn M Ω n)

Traciality and the Radon–Nikodym element #

source

theorem CommutingRepetition.VN.Haagerup.tracial_Rn {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (n : ℕ) {x y : Crossed.L2Q K →L[ℂ ] Crossed.L2Q K} (hx : x ∈ Rn M Ω n) (hy : y ∈ Crossed.crossed M Ω) :

inner ℂ (xin Ω n) ((x * y) (xin Ω n)) = inner ℂ (xin Ω n) ((y * x) (xin Ω n))

The perturbed state is tracial on ℛ_n (IsCentral.tracial).

source

noncomputable def CommutingRepetition.VN.Haagerup.dn {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (n : ℕ) :

Crossed.L2Q K →L[ℂ ] Crossed.L2Q K

d_n = e^{a_n}, the Radon–Nikodym derivative of ψ̂ with respect to ψ_{ξ_n}.

Equations

CommutingRepetition.VN.Haagerup.dn n = CommutingRepetition.VN.Modular.expA (CommutingRepetition.VN.Haagerup.an n) 1

Instances For

source

theorem CommutingRepetition.VN.Haagerup.dn_mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (n : ℕ) :

dn n ∈ Crossed.crossed M Ω

source

theorem CommutingRepetition.VN.Haagerup.isSelfAdjoint_dn {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (n : ℕ) :

IsSelfAdjoint (dn n)

source

theorem CommutingRepetition.VN.Haagerup.isCentral_expA_an {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (n : ℕ) (r : ℝ) :

Modular.IsCentral (Crossed.crossed M Ω) (Crossed.Ωh Ω) (Modular.expA (an n) r)

source

theorem CommutingRepetition.VN.Haagerup.inner_Ωh_eq_inner_xin_dn {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (n : ℕ) {x : Crossed.L2Q K →L[ℂ ] Crossed.L2Q K} (hx : x ∈ Crossed.crossed M Ω) :

inner ℂ (Crossed.Ωh Ω) (x (Crossed.Ωh Ω)) = inner ℂ (xin Ω n) ((dn n * x) (xin Ω n))

ψ̂ = ψ_{ξ_n}(d_n ·) on ℛ: the state of Ω̂ is the d_n-perturbation of the state of ξ_n.

The averaging weight `2^n·1_{(0,2^{-n}]}` #

source

noncomputable def CommutingRepetition.VN.Haagerup.Tn (n : ℕ) :

ℝ

The period T_n = 2^{-n} of σ^{ξ_n}.

Equations

CommutingRepetition.VN.Haagerup.Tn n = 1 / 2 ^ n

Instances For

source

theorem CommutingRepetition.VN.Haagerup.Tn_eq (n : ℕ) :

Tn n = 1 / 2 ^ n

source

theorem CommutingRepetition.VN.Haagerup.Tn_pos (n : ℕ) :

0 < Tn n

source

theorem CommutingRepetition.VN.Haagerup.two_pow_mul_Tn (n : ℕ) :

2 ^ n * Tn n = 1

source

noncomputable def CommutingRepetition.VN.Haagerup.wtR (n : ℕ) :

ℝ → ℝ

The real averaging weight 2^n·1_{(0,2^{-n}]}: a probability density.

Equations

CommutingRepetition.VN.Haagerup.wtR n = (Set.Ioc 0 (CommutingRepetition.VN.Haagerup.Tn n)).indicator fun (x : ℝ) => 2 ^ n

Instances For

source

noncomputable def CommutingRepetition.VN.Haagerup.wt (n : ℕ) (t : ℝ) :

ℂ

The averaging weight as a complex-valued function.

Equations

CommutingRepetition.VN.Haagerup.wt n t = ↑(CommutingRepetition.VN.Haagerup.wtR n t)

Instances For

source

theorem CommutingRepetition.VN.Haagerup.wtR_nonneg (n : ℕ) (t : ℝ) :

0 ≤ wtR n t

source

theorem CommutingRepetition.VN.Haagerup.wtR_of_mem {n : ℕ} {t : ℝ} (h : t ∈ Set.Ioc 0 (Tn n)) :

wtR n t = 2 ^ n

source

theorem CommutingRepetition.VN.Haagerup.wtR_of_notMem {n : ℕ} {t : ℝ} (h : t ∉ Set.Ioc 0 (Tn n)) :

wtR n t = 0

source

theorem CommutingRepetition.VN.Haagerup.conj_wt (n : ℕ) (t : ℝ) :

(starRingEnd ℂ) (wt n t) = wt n t

source

theorem CommutingRepetition.VN.Haagerup.norm_wt (n : ℕ) (t : ℝ) :

‖wt n t‖ = wtR n t

source

theorem CommutingRepetition.VN.Haagerup.wt_eq_indicator (n : ℕ) :

wt n = (Set.Ioc 0 (Tn n)).indicator fun (x : ℝ) => ↑(2 ^ n)

source

theorem CommutingRepetition.VN.Haagerup.integrable_wtR (n : ℕ) :

MeasureTheory.Integrable (wtR n) MeasureTheory.volume

source

theorem CommutingRepetition.VN.Haagerup.integrable_wt (n : ℕ) :

MeasureTheory.Integrable (wt n) MeasureTheory.volume

source

theorem CommutingRepetition.VN.Haagerup.integral_wtR (n : ℕ) :

∫ (t : ℝ), wtR n t = 1

source

theorem CommutingRepetition.VN.Haagerup.integral_wt (n : ℕ) :

∫ (t : ℝ), wt n t = 1

source

theorem CommutingRepetition.VN.Haagerup.integral_norm_wt (n : ℕ) :

∫ (t : ℝ), ‖wt n t‖ = 1

source

theorem CommutingRepetition.VN.Haagerup.integral_wt_smul {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] (n : ℕ) (g : ℝ → E) :

∫ (t : ℝ), wt n t • g t = ↑(2 ^ n) • ∫ (t : ℝ) in 0..Tn n, g t

Integrating against wt n is averaging over one period.

source

theorem CommutingRepetition.VN.Haagerup.integrable_wt_mul {n : ℕ} {g : ℝ → ℂ} (hg : Continuous g) :

MeasureTheory.Integrable (fun (t : ℝ) => wt n t * g t) MeasureTheory.volume

The conditional expectation `Φ_n` #

source

noncomputable def CommutingRepetition.VN.Haagerup.Phi {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (n : ℕ) (x : Crossed.L2Q K →L[ℂ ] Crossed.L2Q K) :

Crossed.L2Q K →L[ℂ ] Crossed.L2Q K

Haagerup's conditional expectation Φ_n(x) = 2^n ∫_0^{2^{-n}} σ^{ξ_n}_t(x) dt, realized as a weak (vectorwise) integral.

Equations

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

Instances For

source

theorem CommutingRepetition.VN.Haagerup.intervalIntegrable_σ {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (n : ℕ) (x : Crossed.L2Q K →L[ℂ ] Crossed.L2Q K) (ζ : Crossed.L2Q K) (a b : ℝ) :

IntervalIntegrable (fun (t : ℝ) => (Modular.σ (Crossed.crossed M Ω) (xin Ω n) t x) ζ) MeasureTheory.volume a b

source

theorem CommutingRepetition.VN.Haagerup.Phi_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (n : ℕ) (x : Crossed.L2Q K →L[ℂ ] Crossed.L2Q K) (ζ : Crossed.L2Q K) :

(Phi M Ω n x) ζ = ↑(2 ^ n) • ∫ (t : ℝ) in 0..Tn n, (Modular.σ (Crossed.crossed M Ω) (xin Ω n) t x) ζ

source

theorem CommutingRepetition.VN.Haagerup.norm_Phi_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (n : ℕ) (x : Crossed.L2Q K →L[ℂ ] Crossed.L2Q K) :

‖Phi M Ω n x‖ ≤ ‖x‖

source

theorem CommutingRepetition.VN.Haagerup.Phi_mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (n : ℕ) {x : Crossed.L2Q K →L[ℂ ] Crossed.L2Q K} (hx : x ∈ Crossed.crossed M Ω) :

Phi M Ω n x ∈ Crossed.crossed M Ω

Φ_n maps ℛ into ℛ.

source

theorem CommutingRepetition.VN.Haagerup.Phi_one {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (n : ℕ) :

Phi M Ω n 1 = 1

Φ_n is unital.

source

theorem CommutingRepetition.VN.Haagerup.Phi_add {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (n : ℕ) (x y : Crossed.L2Q K →L[ℂ ] Crossed.L2Q K) :

Phi M Ω n (x + y) = Phi M Ω n x + Phi M Ω n y

source

theorem CommutingRepetition.VN.Haagerup.Phi_smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (n : ℕ) (c : ℂ) (x : Crossed.L2Q K →L[ℂ ] Crossed.L2Q K) :

Phi M Ω n (c • x) = c • Phi M Ω n x

`Φ_n` lands in `ℛ_n` #

source

theorem CommutingRepetition.VN.Haagerup.periodic_σ_xin {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (n : ℕ) {x : Crossed.L2Q K →L[ℂ ] Crossed.L2Q K} (hx : x ∈ Crossed.crossed M Ω) (ζ : Crossed.L2Q K) :

Function.Periodic (fun (t : ℝ) => (Modular.σ (Crossed.crossed M Ω) (xin Ω n) t x) ζ) (Tn n)

source

theorem CommutingRepetition.VN.Haagerup.σ_Phi {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (n : ℕ) (s : ℝ) {x : Crossed.L2Q K →L[ℂ ] Crossed.L2Q K} (hx : x ∈ Crossed.crossed M Ω) :

Modular.σ (Crossed.crossed M Ω) (xin Ω n) s (Phi M Ω n x) = Phi M Ω n x

σ^{ξ_n} fixes the range of Φ_n: the average over one full period is invariant.

source

theorem CommutingRepetition.VN.Haagerup.Phi_mem_Rn {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (n : ℕ) {x : Crossed.L2Q K →L[ℂ ] Crossed.L2Q K} (hx : x ∈ Crossed.crossed M Ω) :

Phi M Ω n x ∈ Rn M Ω n

Φ_n maps ℛ into the centralizer ℛ_n.

source

theorem CommutingRepetition.VN.Haagerup.Phi_eq_self {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (n : ℕ) {x : Crossed.L2Q K →L[ℂ ] Crossed.L2Q K} (hx : x ∈ Rn M Ω n) :

Phi M Ω n x = x

Φ_n is the identity on ℛ_n, so it is a projection onto ℛ_n.

`Φ_n` preserves the state, positivity and self-adjointness #

source

theorem CommutingRepetition.VN.Haagerup.inner_xin_Phi {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (n : ℕ) (x : Crossed.L2Q K →L[ℂ ] Crossed.L2Q K) :

inner ℂ (xin Ω n) ((Phi M Ω n x) (xin Ω n)) = inner ℂ (xin Ω n) (x (xin Ω n))

ψ_{ξ_n} ∘ Φ_n = ψ_{ξ_n}.

source

theorem CommutingRepetition.VN.Haagerup.isSelfAdjoint_σ {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (n : ℕ) {x : Crossed.L2Q K →L[ℂ ] Crossed.L2Q K} (hx : IsSelfAdjoint x) (t : ℝ) :

IsSelfAdjoint (Modular.σ (Crossed.crossed M Ω) (xin Ω n) t x)

source

theorem CommutingRepetition.VN.Haagerup.isSelfAdjoint_Phi {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (n : ℕ) {x : Crossed.L2Q K →L[ℂ ] Crossed.L2Q K} (hx : IsSelfAdjoint x) :

IsSelfAdjoint (Phi M Ω n x)

source

theorem CommutingRepetition.VN.Haagerup.nonneg_σ {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (n : ℕ) {x : Crossed.L2Q K →L[ℂ ] Crossed.L2Q K} (hx : 0 ≤ x) (t : ℝ) :

0 ≤ Modular.σ (Crossed.crossed M Ω) (xin Ω n) t x

source

theorem CommutingRepetition.VN.Haagerup.Phi_nonneg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (n : ℕ) {x : Crossed.L2Q K →L[ℂ ] Crossed.L2Q K} (hx : 0 ≤ x) :

0 ≤ Phi M Ω n x

Φ_n is positive.

The generating unitaries λ(2^{-n}) #

The logarithms a_n #

The exponentials of a_n #

The perturbed vectors and their modular groups #

The centralizer algebra ℛ_n #

Traciality and the Radon–Nikodym element #

The averaging weight 2^n·1_{(0,2^{-n}]} #

The conditional expectation Φ_n #

Φ_n lands in ℛ_n #

Φ_n preserves the state, positivity and self-adjointness #

The generating unitaries `λ(2^{-n})` #

The logarithms `a_n` #

The exponentials of `a_n` #

The centralizer algebra `ℛ_n` #

The averaging weight `2^n·1_{(0,2^{-n}]}` #

The conditional expectation `Φ_n` #

`Φ_n` lands in `ℛ_n` #

`Φ_n` preserves the state, positivity and self-adjointness #