The unnormalized trace on M₂(R(M)′)

noncomputable def CommutingRepetition.GraphMod.τ₂ (M : StdTracialAlgebra) (T : Block.BH M (Fin 2) →L[ℂ] Block.BH M (Fin 2)) : ℂ

τ₂ T = ∑ᵣ ⟪eᵣΩ, T eᵣΩ⟫.

Equations

• CommutingRepetition.GraphMod.τ₂ M T = ∑ r : Fin 2, inner ℂ ((CommutingRepetition.Block.embed M (Fin 2) r) M.traceVector) (T ((CommutingRepetition.Block.embed M (Fin 2) r) M.traceVector))

theorem CommutingRepetition.GraphMod.τ₂_eq (M : StdTracialAlgebra) (T : Block.BH M (Fin 2) →L[ℂ] Block.BH M (Fin 2)) : τ₂ M T = ∑ r : Fin 2, inner ℂ M.traceVector ((Block.entry M (Fin 2) T r r) M.traceVector)

theorem CommutingRepetition.GraphMod.τ₂_add (M : StdTracialAlgebra) (T T' : Block.BH M (Fin 2) →L[ℂ] Block.BH M (Fin 2)) : τ₂ M (T + T') = τ₂ M T + τ₂ M T'

theorem CommutingRepetition.GraphMod.τ₂_sub (M : StdTracialAlgebra) (T T' : Block.BH M (Fin 2) →L[ℂ] Block.BH M (Fin 2)) : τ₂ M (T - T') = τ₂ M T - τ₂ M T'

theorem CommutingRepetition.GraphMod.τ₂_re_nonneg (M : StdTracialAlgebra) {T : Block.BH M (Fin 2) →L[ℂ] Block.BH M (Fin 2)} (hT : 0 ≤ T) : 0 ≤ (τ₂ M T).re

theorem CommutingRepetition.GraphMod.re_τ₂_star_mul_self (M : StdTracialAlgebra) (T : Block.BH M (Fin 2) →L[ℂ] Block.BH M (Fin 2)) : (τ₂ M (star T * T)).re = ∑ r : Fin 2, ‖T ((Block.embed M (Fin 2) r) M.traceVector)‖ ^ 2

theorem CommutingRepetition.GraphMod.τ₂_mul_comm (M : StdTracialAlgebra) {T T' : Block.BH M (Fin 2) →L[ℂ] Block.BH M (Fin 2)} (hT : T ∈ Block.blockAlg M (Fin 2)) (hT' : T' ∈ Block.blockAlg M (Fin 2)) : τ₂ M (T * T') = τ₂ M (T' * T)

Traciality of τ₂ on the block algebra.

theorem CommutingRepetition.GraphMod.blockAlg_strong_closed (M : StdTracialAlgebra) (T : ℕ → Block.BH M (Fin 2) →L[ℂ] Block.BH M (Fin 2)) (L : Block.BH M (Fin 2) →L[ℂ] Block.BH M (Fin 2)) : (∀ (n : ℕ), T n ∈ Block.blockAlg M (Fin 2)) → (∀ (ξ : Block.BH M (Fin 2)), Filter.Tendsto (fun (n : ℕ) => (T n) ξ) Filter.atTop (nhds (L ξ))) → L ∈ Block.blockAlg M (Fin 2)

Square roots, positive and negative parts

noncomputable def CommutingRepetition.GraphMod.sqrtOp {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (A : 𝓗 →L[ℂ] 𝓗) : 𝓗 →L[ℂ] 𝓗

The positive square root √A = cfc √ A.

Equations

• CommutingRepetition.GraphMod.sqrtOp A = cfc Real.sqrt A

theorem CommutingRepetition.GraphMod.sqrtOp_nonneg {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (A : 𝓗 →L[ℂ] 𝓗) : 0 ≤ sqrtOp A

theorem CommutingRepetition.GraphMod.sqrtOp_sa {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (A : 𝓗 →L[ℂ] 𝓗) : IsSelfAdjoint (sqrtOp A)

theorem CommutingRepetition.GraphMod.sqrtOp_mul_self {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {A : 𝓗 →L[ℂ] 𝓗} (hA : 0 ≤ A) : sqrtOp A * sqrtOp A = A

theorem CommutingRepetition.GraphMod.sqrtOp_eq_of_mul_self {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {A D : 𝓗 →L[ℂ] 𝓗} (hD : 0 ≤ D) (h : D * D = A) : sqrtOp A = D

Uniqueness of the positive square root.

noncomputable def CommutingRepetition.GraphMod.posPart {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (S : 𝓗 →L[ℂ] 𝓗) : 𝓗 →L[ℂ] 𝓗

The positive part S₊ = max(S, 0).

Equations

• CommutingRepetition.GraphMod.posPart S = cfc (fun (t : ℝ) => max t 0) S

noncomputable def CommutingRepetition.GraphMod.negPart {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (S : 𝓗 →L[ℂ] 𝓗) : 𝓗 →L[ℂ] 𝓗

The negative part S₋ = max(−S, 0).

Equations

• CommutingRepetition.GraphMod.negPart S = cfc (fun (t : ℝ) => max (-t) 0) S

noncomputable def CommutingRepetition.GraphMod.absPart {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (S : 𝓗 →L[ℂ] 𝓗) : 𝓗 →L[ℂ] 𝓗

The absolute value |S|.

Equations

• CommutingRepetition.GraphMod.absPart S = cfc (fun (t : ℝ) => |t|) S

theorem CommutingRepetition.GraphMod.posPart_nonneg {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (S : 𝓗 →L[ℂ] 𝓗) : 0 ≤ posPart S

theorem CommutingRepetition.GraphMod.negPart_nonneg {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (S : 𝓗 →L[ℂ] 𝓗) : 0 ≤ negPart S

theorem CommutingRepetition.GraphMod.absPart_nonneg {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (S : 𝓗 →L[ℂ] 𝓗) : 0 ≤ absPart S

theorem CommutingRepetition.GraphMod.absPart_sa {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (S : 𝓗 →L[ℂ] 𝓗) : IsSelfAdjoint (absPart S)

theorem CommutingRepetition.GraphMod.posPart_sub_negPart {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {S : 𝓗 →L[ℂ] 𝓗} (hS : IsSelfAdjoint S) : posPart S - negPart S = S

theorem CommutingRepetition.GraphMod.absPart_eq {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {S : 𝓗 →L[ℂ] 𝓗} (hS : IsSelfAdjoint S) : absPart S = posPart S + negPart S

theorem CommutingRepetition.GraphMod.posPart_mul_negPart {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {S : 𝓗 →L[ℂ] 𝓗} (hS : IsSelfAdjoint S) : posPart S * negPart S = 0

theorem CommutingRepetition.GraphMod.negPart_mul_posPart {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {S : 𝓗 →L[ℂ] 𝓗} (hS : IsSelfAdjoint S) : negPart S * posPart S = 0

theorem CommutingRepetition.GraphMod.absPart_mul_self {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {S : 𝓗 →L[ℂ] 𝓗} (hS : IsSelfAdjoint S) : absPart S * absPart S = S * S

theorem CommutingRepetition.GraphMod.absPart_eq_sqrtOp {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {S : 𝓗 →L[ℂ] 𝓗} (hS : IsSelfAdjoint S) : absPart S = sqrtOp (S * S)

theorem CommutingRepetition.GraphMod.parts_identity {R : Type u_1} [Ring R] (P N P' N' : R) (h1 : P * N = 0) (h2 : N * P = 0) (h3 : P' * N' = 0) (h4 : N' * P' = 0) : (P - N - (P' - N')) * (P - N - (P' - N')) - (P + N - (P' + N')) * (P + N - (P' + N')) = 2 * (P * N' + N * P' + P' * N + N' * P)

The noncommutative ring identity behind the Lipschitz property.

The L²-Lipschitz property of the absolute value

theorem CommutingRepetition.GraphMod.re_τ₂_mul_nonneg (M : StdTracialAlgebra) {A B : Block.BH M (Fin 2) →L[ℂ] Block.BH M (Fin 2)} (hA : 0 ≤ A) (hB : 0 ≤ B) (hAm : A ∈ Block.blockAlg M (Fin 2)) (hBm : B ∈ Block.blockAlg M (Fin 2)) : 0 ≤ (τ₂ M (A * B)).re

theorem CommutingRepetition.GraphMod.posPart_mem (M : StdTracialAlgebra) {S : Block.BH M (Fin 2) →L[ℂ] Block.BH M (Fin 2)} (hS : IsSelfAdjoint S) (hSm : S ∈ Block.blockAlg M (Fin 2)) : posPart S ∈ Block.blockAlg M (Fin 2)

theorem CommutingRepetition.GraphMod.negPart_mem (M : StdTracialAlgebra) {S : Block.BH M (Fin 2) →L[ℂ] Block.BH M (Fin 2)} (hS : IsSelfAdjoint S) (hSm : S ∈ Block.blockAlg M (Fin 2)) : negPart S ∈ Block.blockAlg M (Fin 2)

theorem CommutingRepetition.GraphMod.re_τ₂_absPart_sub_le (M : StdTracialAlgebra) {S S' : Block.BH M (Fin 2) →L[ℂ] Block.BH M (Fin 2)} (hS : IsSelfAdjoint S) (hS' : IsSelfAdjoint S') (hSm : S ∈ Block.blockAlg M (Fin 2)) (hS'm : S' ∈ Block.blockAlg M (Fin 2)) : (τ₂ M ((absPart S - absPart S') * (absPart S - absPart S'))).re ≤ (τ₂ M ((S - S') * (S - S'))).re

L²-Lipschitz property of |·| on M₂(R(M)′): ‖|S| − |S'|‖₂² ≤ ‖S − S'‖₂².

The modulus of [[0, B], [B*, 0]]

noncomputable def CommutingRepetition.GraphMod.Xop (M : StdTracialAlgebra) (B : M.H →L[ℂ] M.H) : Block.BH M (Fin 2) →L[ℂ] Block.BH M (Fin 2)

X_B = [[0, B], [B*, 0]].

Equations

• CommutingRepetition.GraphMod.Xop M B = (CommutingRepetition.Block.place M (Fin 2) 0 1) B + (CommutingRepetition.Block.place M (Fin 2) 1 0) (star B)

theorem CommutingRepetition.GraphMod.Xop_mem (M : StdTracialAlgebra) {B : M.H →L[ℂ] M.H} (hB : B ∈ M.vnAlg) : Xop M B ∈ Block.blockAlg M (Fin 2)

theorem CommutingRepetition.GraphMod.Xop_sa (M : StdTracialAlgebra) (B : M.H →L[ℂ] M.H) : IsSelfAdjoint (Xop M B)

noncomputable def CommutingRepetition.GraphMod.diag (M : StdTracialAlgebra) (A A' : M.H →L[ℂ] M.H) : Block.BH M (Fin 2) →L[ℂ] Block.BH M (Fin 2)

The block-diagonal operator diag(A, A').

Equations

• CommutingRepetition.GraphMod.diag M A A' = (CommutingRepetition.Block.place M (Fin 2) 0 0) A + (CommutingRepetition.Block.place M (Fin 2) 1 1) A'

theorem CommutingRepetition.GraphMod.Xop_mul_Xop (M : StdTracialAlgebra) (B : M.H →L[ℂ] M.H) : Xop M B * Xop M B = diag M (B * star B) (star B * B)

theorem CommutingRepetition.GraphMod.diag_mul_diag (M : StdTracialAlgebra) (A A' C C' : M.H →L[ℂ] M.H) : diag M A A' * diag M C C' = diag M (A * C) (A' * C')

theorem CommutingRepetition.GraphMod.diag_sub (M : StdTracialAlgebra) (A A' C C' : M.H →L[ℂ] M.H) : diag M A A' - diag M C C' = diag M (A - C) (A' - C')

theorem CommutingRepetition.GraphMod.place_diag_nonneg (M : StdTracialAlgebra) (r : Fin 2) {A : M.H →L[ℂ] M.H} (hA : 0 ≤ A) : 0 ≤ (Block.place M (Fin 2) r r) A

theorem CommutingRepetition.GraphMod.diag_nonneg (M : StdTracialAlgebra) {A A' : M.H →L[ℂ] M.H} (hA : 0 ≤ A) (hA' : 0 ≤ A') : 0 ≤ diag M A A'

theorem CommutingRepetition.GraphMod.absPart_Xop (M : StdTracialAlgebra) (B : M.H →L[ℂ] M.H) : absPart (Xop M B) = diag M (sqrtOp (B * star B)) (sqrtOp (star B * B))

|X_B| = diag(|B*|, |B|).

theorem CommutingRepetition.GraphMod.diag_embed_zero (M : StdTracialAlgebra) (A A' : M.H →L[ℂ] M.H) (v : M.H) : (diag M A A') ((Block.embed M (Fin 2) 0) v) = (Block.embed M (Fin 2) 0) (A v)

theorem CommutingRepetition.GraphMod.diag_embed_one (M : StdTracialAlgebra) (A A' : M.H →L[ℂ] M.H) (v : M.H) : (diag M A A') ((Block.embed M (Fin 2) 1) v) = (Block.embed M (Fin 2) 1) (A' v)

theorem CommutingRepetition.GraphMod.Xop_embed_zero (M : StdTracialAlgebra) (B : M.H →L[ℂ] M.H) (v : M.H) : (Xop M B) ((Block.embed M (Fin 2) 0) v) = (Block.embed M (Fin 2) 1) ((star B) v)

theorem CommutingRepetition.GraphMod.Xop_embed_one (M : StdTracialAlgebra) (B : M.H →L[ℂ] M.H) (v : M.H) : (Xop M B) ((Block.embed M (Fin 2) 1) v) = (Block.embed M (Fin 2) 0) (B v)

theorem CommutingRepetition.GraphMod.norm_embed (M : StdTracialAlgebra) (r : Fin 2) (v : M.H) : ‖(Block.embed M (Fin 2) r) v‖ = ‖v‖

theorem CommutingRepetition.GraphMod.bounded_stability (M : StdTracialAlgebra) {B B' : M.H →L[ℂ] M.H} (hB : B ∈ M.vnAlg) (hB' : B' ∈ M.vnAlg) : ‖(sqrtOp (B * star B) - sqrtOp (B' * star B')) M.traceVector‖ ^ 2 ≤ 2 * ‖(B - B') M.traceVector‖ ^ 2

Bounded stability: ‖(|B*| − |B'*|)Ω‖² ≤ 2‖(B − B')Ω‖² for B, B' ∈ R(M)′.

Truncation and the stability of the left modulus

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

The bounded truncation Bₙ = gₙ(E) C* of left multiplication by x.

Equations

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

theorem CommutingRepetition.GraphMod.Bn_mem (M : StdTracialAlgebra) (x : M.H) (n : ℕ) : Bn M x n ∈ M.vnAlg

theorem CommutingRepetition.GraphMod.star_Cop_traceVector (M : StdTracialAlgebra) (x : M.H) : (star (Cop M x)) M.traceVector = (1 - Eop M x) x

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

theorem CommutingRepetition.GraphMod.Bn_traceVector (M : StdTracialAlgebra) (x : M.H) (n : ℕ) : (Bn M x n) M.traceVector = (BorelCalc.P (Eop M x) ⋯ (Set.Icc 0 (aN n))) x

BₙΩ = P[0,aₙ] x.

theorem CommutingRepetition.GraphMod.Bn_mul_star (M : StdTracialAlgebra) (x : M.H) (n : ℕ) : Bn M x n * star (Bn M x n) = BorelCalc.bfc (Eop M x) ⋯ (ψn n) * BorelCalc.bfc (Eop M x) ⋯ (ψn n)

Bₙ Bₙ* = ψₙ(E)².

theorem CommutingRepetition.GraphMod.sqrtOp_Bn (M : StdTracialAlgebra) (x : M.H) (n : ℕ) : sqrtOp (Bn M x n * star (Bn M x n)) = BorelCalc.bfc (Eop M x) ⋯ (ψn n)

|Bₙ*| = ψₙ(E).

theorem CommutingRepetition.GraphMod.stability (M : StdTracialAlgebra) (x y : M.H) : ‖hvec M x - hvec M y‖ ^ 2 ≤ 2 * ‖x - y‖ ^ 2

Stability of the left modulus (06_otqcs.tex, lem otqcs-modulus): ‖hvec x − hvec y‖² ≤ 2 ‖x − y‖².