The ‖·‖_ψ toolkit

theorem CommutingRepetition.VN.Haagerup.norm_apply_Ω_sq {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (Ω : K) (y : K →L[ℂ] K) : ‖y Ω‖ ^ 2 = (inner ℂ Ω ((star y * y) Ω)).re

theorem CommutingRepetition.VN.Haagerup.norm_mul_apply_Ω_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (Ω : K) (x y : K →L[ℂ] K) : ‖(x * y) Ω‖ ≤ ‖x‖ * ‖y Ω‖

The trivial half: ‖x y Ω‖ ≤ ‖x‖ ‖y Ω‖.

theorem CommutingRepetition.VN.Haagerup.norm_eq_of_sq_eq {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (h : a ^ 2 = b ^ 2) : a = b

theorem CommutingRepetition.VN.Haagerup.conjJm_apply_Ω_of_isCentral {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {w : K →L[ℂ] K} (hw : Modular.IsCentral M Ω w) (hwsa : IsSelfAdjoint w) : (Modular.conjJm M Ω w) Ω = w Ω

A self-adjoint central element acts on Ω through the commutant: w Ω = (J w J) Ω for w ∈ M self-adjoint and commuting with R.

theorem CommutingRepetition.VN.Haagerup.norm_mul_right_apply_Ω_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {w y : K →L[ℂ] K} (hw : Modular.IsCentral M Ω w) (hwsa : IsSelfAdjoint w) (hy : y ∈ M) : ‖(y * w) Ω‖ ≤ ‖w‖ * ‖y Ω‖

HJX Lemma 2.5(ii): ‖y w Ω‖ ≤ ‖w‖ ‖y Ω‖ for w self-adjoint in the centralizer.

theorem CommutingRepetition.VN.Haagerup.norm_conj_unitary_apply_Ω {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {u y : K →L[ℂ] K} (hu : Modular.IsCentral M Ω u) (hu1 : star u * u = 1) (hy : y ∈ M) : ‖(u * y * star u) Ω‖ = ‖y Ω‖

Conjugation by a unitary of the centralizer is ‖·‖_ψ-isometric.

theorem CommutingRepetition.VN.Haagerup.norm_mul_unitary_apply_Ω {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {u y : K →L[ℂ] K} (hu : Modular.IsCentral M Ω u) (hu2 : u * star u = 1) (hy : y ∈ M) : ‖(y * u) Ω‖ = ‖y Ω‖

Multiplying on the right by a unitary of the centralizer is ‖·‖_ψ-isometric.

theorem CommutingRepetition.VN.Haagerup.norm_commutator_central_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {w y : K →L[ℂ] K} (hw : Modular.IsCentral M Ω w) (hwsa : IsSelfAdjoint w) (hy : y ∈ M) : ‖(w * y - y * w) Ω‖ ≤ 2 * ‖w‖ * ‖y Ω‖

‖[w, y]Ω‖ ≤ 2‖w‖‖yΩ‖ for w self-adjoint in the centralizer.

theorem CommutingRepetition.VN.Haagerup.isCentral_pow {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {w : K →L[ℂ] K} (hw : Modular.IsCentral M Ω w) (k : ℕ) : Modular.IsCentral M Ω (w ^ k)

theorem CommutingRepetition.VN.Haagerup.norm_commutator_pow_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {w y : K →L[ℂ] K} (hw : Modular.IsCentral M Ω w) (hwsa : IsSelfAdjoint w) (hy : y ∈ M) (k : ℕ) : ‖(w ^ (k + 1) * y - y * w ^ (k + 1)) Ω‖ ≤ (↑k + 1) * ‖w‖ ^ k * ‖(w * y - y * w) Ω‖

‖[w^{k+1}, y]Ω‖ ≤ (k+1)‖w‖^k‖[w,y]Ω‖ for w self-adjoint in the centralizer.

theorem CommutingRepetition.VN.Haagerup.norm_commutator_eit_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {w y : K →L[ℂ] K} (hw : Modular.IsCentral M Ω w) (hwsa : IsSelfAdjoint w) (hy : y ∈ M) (t : ℝ) : ‖(Modular.eit w hwsa t * y - y * Modular.eit w hwsa t) Ω‖ ≤ |t| * Real.exp (|t| * ‖w‖) * ‖(w * y - y * w) Ω‖

HJX Lemma 2.6(ii): ‖[e^{itw}, y]Ω‖ ≤ |t| e^{|t|‖w‖}‖[w,y]Ω‖.

Left-bounded elements

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

x is left bounded with constant c: ψ(x* y x) ≤ c ψ(y) for 0 ≤ y ∈ M (HJX Lemma 2.5).

Equations

• CommutingRepetition.VN.Haagerup.LeftBounded M Ω x c = ∀ y ∈ M, 0 ≤ y → (inner ℂ Ω ((star x * y * x) Ω)).re ≤ c * (inner ℂ Ω (y Ω)).re

theorem CommutingRepetition.VN.Haagerup.norm_mul_apply_Ω_le_of_leftBounded {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {x : K →L[ℂ] K} {c : ℝ} (hc0 : 0 ≤ c) (hx : LeftBounded M Ω x c) {y : K →L[ℂ] K} (hy : y ∈ M) : ‖(y * x) Ω‖ ≤ √c * ‖y Ω‖

‖y x Ω‖ ≤ √c ‖y Ω‖ for a left-bounded x.

theorem CommutingRepetition.VN.Haagerup.norm_commutator_apply_Ω_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {x : K →L[ℂ] K} {c : ℝ} (hc0 : 0 ≤ c) (hx : LeftBounded M Ω x c) {y : K →L[ℂ] K} (hy : y ∈ M) : ‖(y * x - x * y) Ω‖ ≤ (√c + ‖x‖) * ‖y Ω‖

The commutator estimate: ‖[y, x] Ω‖ ≤ (√c + ‖x‖) ‖y Ω‖ for a left-bounded x.

theorem CommutingRepetition.VN.Haagerup.leftBounded_xk {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {k : ℝ} (hk : 0 < k) {x : K →L[ℂ] K} (hx : x ∈ M) : LeftBounded M Ω (Modular.xk M Ω k hk x) (‖Modular.xkFlat M Ω k hk x‖ ^ 2)

The Gaussian-smeared elements are left bounded (E4.5, HJX Lemma 2.5(i)).

The bounded logarithms b_n = 2^{-n} a_n

theorem CommutingRepetition.VN.Haagerup.norm_ulog_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {u : K →L[ℂ] K} (hu1 : star u * u = 1) (hu2 : u * star u = 1) : ‖Modular.ulog u hu1 hu2‖ ≤ 2 * Real.pi

theorem CommutingRepetition.VN.Haagerup.spectrum_ulog {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {u : K →L[ℂ] K} (hu1 : star u * u = 1) (hu2 : u * star u = 1) : spectrum ℝ (Modular.ulog u hu1 hu2) ⊆ Set.Icc 0 (2 * Real.pi)

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

b_n = −i Log λ(2^{-n}), so that a_n = 2^n b_n.

Equations

• CommutingRepetition.VN.Haagerup.bn n = CommutingRepetition.VN.Modular.ulog (CommutingRepetition.VN.Haagerup.un n) ⋯ ⋯

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

theorem CommutingRepetition.VN.Haagerup.norm_bn_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (n : ℕ) : ‖bn n‖ ≤ 2 * Real.pi

theorem CommutingRepetition.VN.Haagerup.spectrum_bn {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (n : ℕ) : spectrum ℝ (bn n) ⊆ Set.Icc 0 (2 * Real.pi)

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

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

theorem CommutingRepetition.VN.Haagerup.commute_bn_R {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (n : ℕ) : Commute (bn n) (Modular.R (Crossed.crossed M Ω) (Crossed.Ωh Ω))

theorem CommutingRepetition.VN.Haagerup.isCentral_bn {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (n : ℕ) : Modular.IsCentral (Crossed.crossed M Ω) (Crossed.Ωh Ω) (bn n)

theorem CommutingRepetition.VN.Haagerup.eit_bn_int {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (n : ℕ) (k : ℤ) : Modular.eit (bn n) ⋯ ↑k = Crossed.shift (↑k * qn n)

e^{ikb_n} = λ(k2^{-n}) for every integer k.

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

HJX Lemma 2.2 in this model: Ω̂ is Haar distributed for b_n, because the vectors λ(k2^{-n})Ω̂ = δ_{k2^{-n}} ⊗ Ω are pairwise orthogonal.

HJX Lemma 2.6(i): ‖[b_n, x]Ω̂‖ → 0

theorem CommutingRepetition.VN.Haagerup.norm_commutator_shift {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (q : ℚ) {x : Crossed.L2Q K →L[ℂ] Crossed.L2Q K} (hx : x ∈ Crossed.crossed M Ω) : ‖(Crossed.shift q * x - x * Crossed.shift q) (Crossed.Ωh Ω)‖ = ‖x (Crossed.Ωh Ω) - (Modular.Δit (Crossed.crossed M Ω) (Crossed.Ωh Ω) ↑(-q)) (x (Crossed.Ωh Ω))‖

‖[λ(q), x]Ω̂‖ = ‖xΩ̂ − Δ̂^{-iq}(xΩ̂)‖, because λ(q) is unitary and λ(-q)xλ(q) = σ̂_{-q}(x).

theorem CommutingRepetition.VN.Haagerup.tendsto_qn_mul (k : ℤ) : Filter.Tendsto (fun (n : ℕ) => ↑(-(↑k * qn n))) Filter.atTop (nhds 0)

theorem CommutingRepetition.VN.Haagerup.tendsto_commutator_shift {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {x : Crossed.L2Q K →L[ℂ] Crossed.L2Q K} (hx : x ∈ Crossed.crossed M Ω) (k : ℤ) : Filter.Tendsto (fun (n : ℕ) => ‖(Crossed.shift (↑k * qn n) * x - x * Crossed.shift (↑k * qn n)) (Crossed.Ωh Ω)‖) Filter.atTop (nhds 0)

theorem CommutingRepetition.VN.Haagerup.tendsto_commutator_bn {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {x : Crossed.L2Q K →L[ℂ] Crossed.L2Q K} (hx : x ∈ Crossed.crossed M Ω) : Filter.Tendsto (fun (n : ℕ) => ‖(bn n * x - x * bn n) (Crossed.Ωh Ω)‖) Filter.atTop (nhds 0)

HJX Lemma 2.6(i): ‖[b_n, x] Ω̂‖ → 0 for every x ∈ ℛ.

HJX Lemma 2.6(iii) and the density theorem

theorem CommutingRepetition.VN.Haagerup.isCentral_eit_an {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (n : ℕ) (t : ℝ) : Modular.IsCentral (Crossed.crossed M Ω) (Crossed.Ωh Ω) (Modular.eit (an n) ⋯ t)

theorem CommutingRepetition.VN.Haagerup.norm_σ_xin_sub_le {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) (Crossed.Ωh Ω) - x (Crossed.Ωh Ω)‖ ≤ ‖(Modular.Δit (Crossed.crossed M Ω) (Crossed.Ωh Ω) t) (x (Crossed.Ωh Ω)) - x (Crossed.Ωh Ω)‖ + ‖(Modular.eit (an n) ⋯ t * x - x * Modular.eit (an n) ⋯ t) (Crossed.Ωh Ω)‖

HJX Lemma 2.6(iii), pointwise in t: on ℛ, ‖σ^{ξ_n}_t(x)Ω̂ − xΩ̂‖ ≤ ‖Δ̂^{it}(xΩ̂) − xΩ̂‖ + ‖[e^{ita_n}, x]Ω̂‖.

theorem CommutingRepetition.VN.Haagerup.norm_Phi_sub_le {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} {C : ℝ} (h : ∀ t ∈ Set.Ioc 0 (Tn n), ‖(Modular.σ (Crossed.crossed M Ω) (xin Ω n) t x) (Crossed.Ωh Ω) - x (Crossed.Ωh Ω)‖ ≤ C) : ‖(Phi M Ω n x) (Crossed.Ωh Ω) - x (Crossed.Ωh Ω)‖ ≤ C

The averaging bound: a uniform bound on [0, 2^{-n}] bounds ‖(Φ_n x − x)Ω̂‖.

theorem CommutingRepetition.VN.Haagerup.tendsto_Phi_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {x : Crossed.L2Q K →L[ℂ] Crossed.L2Q K} (hx : x ∈ Crossed.crossed M Ω) : Filter.Tendsto (fun (n : ℕ) => (Phi M Ω n x) (Crossed.Ωh Ω)) Filter.atTop (nhds (x (Crossed.Ωh Ω)))

Haagerup's density theorem (the final lemma of HJX §2): Φ_n(x)Ω̂ → xΩ̂ for every x ∈ ℛ. Since Φ_n(x) ∈ ℛ_n (E6.4), the union ⋃_n ℛ_n is ‖·‖_{ψ̂}-dense in ℛ.

theorem CommutingRepetition.VN.Haagerup.exists_mem_Rn_approx {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {x : Crossed.L2Q K →L[ℂ] Crossed.L2Q K} (hx : x ∈ Crossed.crossed M Ω) {ε : ℝ} (hε : 0 < ε) : ∃ (n : ℕ), ∃ y ∈ Rn M Ω n, ‖y (Crossed.Ωh Ω) - x (Crossed.Ωh Ω)‖ < ε

⋃_n ℛ_n is ‖·‖_{ψ̂}-dense in ℛ: every x ∈ ℛ is ‖·‖_{ψ̂}-approximated by Φ_n(x) ∈ ℛ_n.