Cutoff parameters

noncomputable def CommutingRepetition.GraphMod.aN (n : ℕ) : ℝ

aₙ = 1 − 1/(n+1).

Equations

• CommutingRepetition.GraphMod.aN n = 1 - 1 / (↑n + 1)

noncomputable def CommutingRepetition.GraphMod.bN (n : ℕ) : ℝ

bₙ = 1/(n+1).

Equations

• CommutingRepetition.GraphMod.bN n = 1 / (↑n + 1)

theorem CommutingRepetition.GraphMod.bN_pos (n : ℕ) : 0 < bN n

theorem CommutingRepetition.GraphMod.bN_le_one (n : ℕ) : bN n ≤ 1

theorem CommutingRepetition.GraphMod.aN_eq (n : ℕ) : aN n = 1 - bN n

theorem CommutingRepetition.GraphMod.aN_lt_one (n : ℕ) : aN n < 1

theorem CommutingRepetition.GraphMod.aN_nonneg (n : ℕ) : 0 ≤ aN n

theorem CommutingRepetition.GraphMod.bN_anti : Antitone bN

theorem CommutingRepetition.GraphMod.aN_mono : Monotone aN

theorem CommutingRepetition.GraphMod.exists_le_aN {t : ℝ} (ht : t < 1) : ∃ (n : ℕ), t ≤ aN n

theorem CommutingRepetition.GraphMod.exists_bN_le {t : ℝ} (ht : 0 < t) : ∃ (n : ℕ), bN n ≤ t

theorem CommutingRepetition.GraphMod.iUnion_Icc_aN : ⋃ (n : ℕ), Set.Icc 0 (aN n) = Set.Ico 0 1

theorem CommutingRepetition.GraphMod.iUnion_Icc_bN_aN : ⋃ (n : ℕ), Set.Icc (bN n) (aN n) = Set.Ioo 0 1

theorem CommutingRepetition.GraphMod.iUnion_Icc_bN_const (n : ℕ) : ⋃ (k : ℕ), Set.Icc (bN k) (aN n) = Set.Ioc 0 (aN n)

theorem CommutingRepetition.GraphMod.iUnion_Ioc_aN : ⋃ (n : ℕ), Set.Ioc 0 (aN n) = Set.Ioo 0 1

theorem CommutingRepetition.GraphMod.monotone_Icc_aN : Monotone fun (n : ℕ) => Set.Icc 0 (aN n)

theorem CommutingRepetition.GraphMod.monotone_Icc_bN_aN : Monotone fun (n : ℕ) => Set.Icc (bN n) (aN n)

theorem CommutingRepetition.GraphMod.monotone_Icc_bN_const (n : ℕ) : Monotone fun (k : ℕ) => Set.Icc (bN k) (aN n)

theorem CommutingRepetition.GraphMod.monotone_Ioc_aN : Monotone fun (n : ℕ) => Set.Ioc 0 (aN n)

The modulus function and its truncations

noncomputable def CommutingRepetition.GraphMod.ψ (t : ℝ) : ℝ

ψ(t) = √(t/(1−t)) on (0,1), 0 elsewhere.

Equations

• CommutingRepetition.GraphMod.ψ t = if 0 < t ∧ t < 1 then √(t / (1 - t)) else 0

theorem CommutingRepetition.GraphMod.ψ_nonneg (t : ℝ) : 0 ≤ ψ t

theorem CommutingRepetition.GraphMod.ψ_measurable : Measurable ψ

theorem CommutingRepetition.GraphMod.ψ_of_not {t : ℝ} (h : ¬(0 < t ∧ t < 1)) : ψ t = 0

theorem CommutingRepetition.GraphMod.ψ_of_mem {t : ℝ} (h : 0 < t ∧ t < 1) : ψ t = √(t / (1 - t))

theorem CommutingRepetition.GraphMod.ψ_pos_iff (t : ℝ) : 0 < ψ t ↔ 0 < t ∧ t < 1

theorem CommutingRepetition.GraphMod.ψ_sq {t : ℝ} (h0 : 0 ≤ t) (h1 : t < 1) : ψ t ^ 2 = t / (1 - t)

theorem CommutingRepetition.GraphMod.ψ_sq_le {n : ℕ} {t : ℝ} (ht : t ∈ Set.Icc 0 (aN n)) : ψ t ^ 2 ≤ ↑n + 1

noncomputable def CommutingRepetition.GraphMod.ψn (n : ℕ) : ℝ → ℝ

The truncated modulus function ψₙ = 1_{[0,aₙ]} ψ.

Equations

• CommutingRepetition.GraphMod.ψn n = (Set.Icc 0 (CommutingRepetition.GraphMod.aN n)).indicator CommutingRepetition.GraphMod.ψ

theorem CommutingRepetition.GraphMod.ψn_bdd (n : ℕ) : BorelCalc.Bdd (ψn n)

theorem CommutingRepetition.GraphMod.ψn_nonneg (n : ℕ) (t : ℝ) : 0 ≤ ψn n t

noncomputable def CommutingRepetition.GraphMod.gn (n : ℕ) : ℝ → ℝ

gₙ = 1_{[0,aₙ]} / (1 − t).

Equations

• CommutingRepetition.GraphMod.gn n = (Set.Icc 0 (CommutingRepetition.GraphMod.aN n)).indicator fun (t : ℝ) => 1 / (1 - t)

theorem CommutingRepetition.GraphMod.gn_bdd (n : ℕ) : BorelCalc.Bdd (gn n)

noncomputable def CommutingRepetition.GraphMod.mn (n : ℕ) : ℝ → ℝ

mₙ = 1_{[bₙ,aₙ]} / √(t(1−t)).

Equations

• CommutingRepetition.GraphMod.mn n = (Set.Icc (CommutingRepetition.GraphMod.bN n) (CommutingRepetition.GraphMod.aN n)).indicator fun (t : ℝ) => 1 / √(t * (1 - t))

theorem CommutingRepetition.GraphMod.mem_Icc_bN_aN {n : ℕ} {t : ℝ} (ht : t ∈ Set.Icc (bN n) (aN n)) : bN n ≤ t ∧ bN n ≤ 1 - t

theorem CommutingRepetition.GraphMod.mn_bdd (n : ℕ) : BorelCalc.Bdd (mn n)

Pointwise identities

theorem CommutingRepetition.GraphMod.mem_Icc_aN_lt {n : ℕ} {t : ℝ} (ht : t ∈ Set.Icc 0 (aN n)) : t < 1

theorem CommutingRepetition.GraphMod.ψn_mul_ψn (n : ℕ) : ψn n * ψn n = fun (t : ℝ) => gn n t * (clamp t * ((1 - clamp t) * gn n t))

(F1) ψₙ² = gₙ · t(1−t) · gₙ.

theorem CommutingRepetition.GraphMod.one_sub_clamp_mul_gn (n : ℕ) : (fun (t : ℝ) => (1 - clamp t) * gn n t) = (Set.Icc 0 (aN n)).indicator 1

(F2) (1−t) gₙ = 1_{[0,aₙ]}.

theorem CommutingRepetition.GraphMod.mn_mul_mn {m n : ℕ} (hmn : m ≤ n) : (fun (t : ℝ) => mn n t * (clamp t * ((1 - clamp t) * mn m t))) = (Set.Icc (bN m) (aN m)).indicator 1

(F3) mₙ · t(1−t) · mₘ = 1_{[bₘ,aₘ]} for m ≤ n.

theorem CommutingRepetition.GraphMod.one_sub_clamp_mul_mn_mul_ψn {n k : ℕ} (hnk : n ≤ k) : (fun (t : ℝ) => (1 - clamp t) * (mn k t * ψn n t)) = (Set.Icc (bN k) (aN n)).indicator 1

(F4) (1−t) mₖ ψₙ = 1_{[bₖ,aₙ]} for k ≥ n.

theorem CommutingRepetition.GraphMod.ψn_mul_ψn_of_le {m n : ℕ} (hmn : m ≤ n) : ψn n * ψn m = ψn m * ψn m

(F5) ψₙ ψₘ = ψₘ² for m ≤ n.

theorem CommutingRepetition.GraphMod.indicator_Ioo_mul_ψn (n : ℕ) : (Set.Ioo 0 1).indicator 1 * ψn n = ψn n

(F6) 1_{(0,1)} ψₙ = ψₙ.

The graph data of x

theorem CommutingRepetition.GraphMod.PE_Icc_zero_one (M : StdTracialAlgebra) (x : M.H) : BorelCalc.P (Eop M x) ⋯ (Set.Icc 0 1) = 1

theorem CommutingRepetition.GraphMod.PE_Ico (M : StdTracialAlgebra) (x : M.H) : BorelCalc.P (Eop M x) ⋯ (Set.Ico 0 1) = 1

theorem CommutingRepetition.GraphMod.PE_Ioo_apply (M : StdTracialAlgebra) (x : M.H) : (BorelCalc.P (Eop M x) ⋯ (Set.Ioo 0 1)) x = x

theorem CommutingRepetition.GraphMod.inner_bE_traceVector (M : StdTracialAlgebra) (x : M.H) {g : ℝ → ℝ} (hg : BorelCalc.Bdd g) : inner ℂ M.traceVector ((BorelCalc.bfc (Eop M x) ⋯ g) M.traceVector) = ↑(∫ (t : ℝ), g t ∂BorelCalc.ν (Eop M x) ⋯ M.traceVector)

⟪Ω, g(E) Ω⟫ = ∫ g dν_Ω.

theorem CommutingRepetition.GraphMod.inner_bE_bE (M : StdTracialAlgebra) (x : M.H) {f g : ℝ → ℝ} (hf : BorelCalc.Bdd f) (hg : BorelCalc.Bdd g) (ξ η : M.H) : inner ℂ ((BorelCalc.bfc (Eop M x) ⋯ f) ξ) ((BorelCalc.bfc (Eop M x) ⋯ g) η) = inner ℂ ξ ((BorelCalc.bfc (Eop M x) ⋯ (f * g)) η)

theorem CommutingRepetition.GraphMod.norm_ψn_traceVector_sq (M : StdTracialAlgebra) (x : M.H) (n : ℕ) : ‖(BorelCalc.bfc (Eop M x) ⋯ (ψn n)) M.traceVector‖ ^ 2 = ‖(BorelCalc.P (Eop M x) ⋯ (Set.Icc 0 (aN n))) x‖ ^ 2

The norm of a truncated modulus vector: ‖ψₙ(E)Ω‖² = ‖P[0,aₙ] x‖².

theorem CommutingRepetition.GraphMod.norm_PE_Icc_aN_le (M : StdTracialAlgebra) (x : M.H) (n : ℕ) : ‖(BorelCalc.P (Eop M x) ⋯ (Set.Icc 0 (aN n))) x‖ ≤ ‖x‖

theorem CommutingRepetition.GraphMod.tendsto_norm_PE_Icc_aN (M : StdTracialAlgebra) (x : M.H) : Filter.Tendsto (fun (n : ℕ) => ‖(BorelCalc.P (Eop M x) ⋯ (Set.Icc 0 (aN n))) x‖ ^ 2) Filter.atTop (nhds (‖x‖ ^ 2))

theorem CommutingRepetition.GraphMod.inner_ψn_traceVector (M : StdTracialAlgebra) (x : M.H) {m n : ℕ} (hmn : m ≤ n) : (inner ℂ ((BorelCalc.bfc (Eop M x) ⋯ (ψn n)) M.traceVector) ((BorelCalc.bfc (Eop M x) ⋯ (ψn m)) M.traceVector)).re = ‖(BorelCalc.bfc (Eop M x) ⋯ (ψn m)) M.traceVector‖ ^ 2

The polarized norms: ⟪ψₙ(E)Ω, ψₘ(E)Ω⟫ = ‖ψₘ(E)Ω‖² for m ≤ n.

An abstract Cauchy criterion

theorem CommutingRepetition.GraphMod.cauchySeq_of_inner_min {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] (u : ℕ → 𝓗) (c : ℕ → ℝ) (hin : ∀ (m n : ℕ), m ≤ n → (inner ℂ (u n) (u m)).re = c m) (hc : ∀ (n : ℕ), ‖u n‖ ^ 2 = c n) {l : ℝ} (hconv : Filter.Tendsto c Filter.atTop (nhds l)) : CauchySeq u

A sequence whose Gram matrix is ⟪u n, u m⟫ = c (min m n) with c convergent is Cauchy.

The modulus vector hvec

theorem CommutingRepetition.GraphMod.exists_hvec (M : StdTracialAlgebra) (x : M.H) : ∃ (h : M.H), Filter.Tendsto (fun (n : ℕ) => (BorelCalc.bfc (Eop M x) ⋯ (ψn n)) M.traceVector) Filter.atTop (nhds h)

noncomputable def CommutingRepetition.GraphMod.hvec (M : StdTracialAlgebra) (x : M.H) : M.H

The left modulus vector hvec = |T*| Ω = lim ψₙ(E) Ω.

Equations

• CommutingRepetition.GraphMod.hvec M x = ⋯.choose

theorem CommutingRepetition.GraphMod.hvec_tendsto (M : StdTracialAlgebra) (x : M.H) : Filter.Tendsto (fun (n : ℕ) => (BorelCalc.bfc (Eop M x) ⋯ (ψn n)) M.traceVector) Filter.atTop (nhds (hvec M x))

theorem CommutingRepetition.GraphMod.norm_hvec (M : StdTracialAlgebra) (x : M.H) : ‖hvec M x‖ = ‖x‖

theorem CommutingRepetition.GraphMod.J_bE_traceVector (M : StdTracialAlgebra) (x : M.H) {g : ℝ → ℝ} (hg : BorelCalc.Bdd g) : M.J ((BorelCalc.bfc (Eop M x) ⋯ g) M.traceVector) = (BorelCalc.bfc (Eop M x) ⋯ g) M.traceVector

theorem CommutingRepetition.GraphMod.J_hvec (M : StdTracialAlgebra) (x : M.H) : M.J (hvec M x) = hvec M x

theorem CommutingRepetition.GraphMod.PE_Ioo_hvec (M : StdTracialAlgebra) (x : M.H) : (BorelCalc.P (Eop M x) ⋯ (Set.Ioo 0 1)) (hvec M x) = hvec M x

The partial isometry W

noncomputable def CommutingRepetition.GraphMod.Wn (M : StdTracialAlgebra) (x : M.H) (n : ℕ) : M.H →L[ℂ] M.H

Wₙ = C mₙ(E).

Equations

• CommutingRepetition.GraphMod.Wn M x n = CommutingRepetition.GraphMod.Cop M x * CommutingRepetition.BorelCalc.bfc (CommutingRepetition.GraphMod.Eop M x) ⋯ (CommutingRepetition.GraphMod.mn n)

theorem CommutingRepetition.GraphMod.Wn_mem (M : StdTracialAlgebra) (x : M.H) (n : ℕ) : Wn M x n ∈ M.vnAlg

theorem CommutingRepetition.GraphMod.inner_Wn (M : StdTracialAlgebra) (x : M.H) {m n : ℕ} (hmn : m ≤ n) (ζ ζ' : M.H) : inner ℂ ((Wn M x n) ζ) ((Wn M x m) ζ') = inner ℂ ζ ((BorelCalc.P (Eop M x) ⋯ (Set.Icc (bN m) (aN m))) ζ')

The Gram matrix of the Wₙ: ⟪Wₙ ζ, Wₘ ζ'⟫ = ⟪ζ, P[bₘ,aₘ] ζ'⟫ for m ≤ n.

theorem CommutingRepetition.GraphMod.norm_Wn_apply_sq (M : StdTracialAlgebra) (x : M.H) (n : ℕ) (ζ : M.H) : ‖(Wn M x n) ζ‖ ^ 2 = ‖(BorelCalc.P (Eop M x) ⋯ (Set.Icc (bN n) (aN n))) ζ‖ ^ 2

theorem CommutingRepetition.GraphMod.norm_Wn_apply_le (M : StdTracialAlgebra) (x : M.H) (n : ℕ) (ζ : M.H) : ‖(Wn M x n) ζ‖ ≤ ‖ζ‖

theorem CommutingRepetition.GraphMod.norm_Wn_le (M : StdTracialAlgebra) (x : M.H) (n : ℕ) : ‖Wn M x n‖ ≤ 1

theorem CommutingRepetition.GraphMod.tendsto_norm_PE_Icc_bN_aN (M : StdTracialAlgebra) (x ζ : M.H) : Filter.Tendsto (fun (n : ℕ) => ‖(BorelCalc.P (Eop M x) ⋯ (Set.Icc (bN n) (aN n))) ζ‖ ^ 2) Filter.atTop (nhds (‖(BorelCalc.P (Eop M x) ⋯ (Set.Ioo 0 1)) ζ‖ ^ 2))

theorem CommutingRepetition.GraphMod.exists_Wn_tendsto (M : StdTracialAlgebra) (x ζ : M.H) : ∃ (l : M.H), Filter.Tendsto (fun (n : ℕ) => (Wn M x n) ζ) Filter.atTop (nhds l)

noncomputable def CommutingRepetition.GraphMod.W (M : StdTracialAlgebra) (x : M.H) : M.H →L[ℂ] M.H

The polar partial isometry W = lim C mₙ(E), the strong limit.

Equations

• CommutingRepetition.GraphMod.W M x = CommutingRepetition.StrongLimit.pointwiseLimit (CommutingRepetition.GraphMod.Wn M x) 1 ⋯ ⋯

theorem CommutingRepetition.GraphMod.W_tendsto (M : StdTracialAlgebra) (x ζ : M.H) : Filter.Tendsto (fun (n : ℕ) => (Wn M x n) ζ) Filter.atTop (nhds ((W M x) ζ))

theorem CommutingRepetition.GraphMod.W_mem (M : StdTracialAlgebra) (x : M.H) : W M x ∈ M.vnAlg

theorem CommutingRepetition.GraphMod.star_W_mul_W (M : StdTracialAlgebra) (x : M.H) : star (W M x) * W M x = BorelCalc.P (Eop M x) ⋯ (Set.Ioo 0 1)

W*W = P(0,1).

theorem CommutingRepetition.GraphMod.Wn_ψn (M : StdTracialAlgebra) (x : M.H) {n k : ℕ} (hnk : n ≤ k) : (Wn M x k) ((BorelCalc.bfc (Eop M x) ⋯ (ψn n)) M.traceVector) = M.J ((BorelCalc.P (Eop M x) ⋯ (Set.Icc (bN k) (aN n))) x)

Wₖ ψₙ(E) Ω = J (P[bₖ,aₙ] x) for k ≥ n.

theorem CommutingRepetition.GraphMod.W_ψn (M : StdTracialAlgebra) (x : M.H) (n : ℕ) : (W M x) ((BorelCalc.bfc (Eop M x) ⋯ (ψn n)) M.traceVector) = M.J ((BorelCalc.P (Eop M x) ⋯ (Set.Ioc 0 (aN n))) x)

theorem CommutingRepetition.GraphMod.W_hvec (M : StdTracialAlgebra) (x : M.H) : (W M x) (hvec M x) = M.J x

W hvec = J x.

The polar element

noncomputable def CommutingRepetition.GraphMod.vEl (M : StdTracialAlgebra) (x : M.H) : ↥M.vnAlg

v = W* as an element of the von Neumann algebra.

Equations

• CommutingRepetition.GraphMod.vEl M x = ⟨star (CommutingRepetition.GraphMod.W M x), ⋯⟩

theorem CommutingRepetition.GraphMod.vnModel_Rop_vEl_hvec (M : StdTracialAlgebra) (x : M.H) : (M.vnModel.Rop (vEl M x)) (hvec M x) = x

theorem CommutingRepetition.GraphMod.vnModel_Rop_vEl_mul_star_hvec (M : StdTracialAlgebra) (x : M.H) : (M.vnModel.Rop (vEl M x * star (vEl M x))) (hvec M x) = hvec M x

theorem CommutingRepetition.GraphMod.vEl_mul_star_vEl_val (M : StdTracialAlgebra) (x : M.H) : ↑(vEl M x * star (vEl M x)) = BorelCalc.P (Eop M x) ⋯ (Set.Ioo 0 1)