Pairs in the block space H ⊕ H

noncomputable def CommutingRepetition.GraphMod.pair (M : StdTracialAlgebra) (v v' : M.H) : Block.BH M (Fin 2)

The pair (v, v') in H².

Equations

• CommutingRepetition.GraphMod.pair M v v' = (CommutingRepetition.Block.embed M (Fin 2) 0) v + (CommutingRepetition.Block.embed M (Fin 2) 1) v'

theorem CommutingRepetition.GraphMod.pair_apply_zero (M : StdTracialAlgebra) (v v' : M.H) : (pair M v v').ofLp 0 = v

theorem CommutingRepetition.GraphMod.pair_apply_one (M : StdTracialAlgebra) (v v' : M.H) : (pair M v v').ofLp 1 = v'

theorem CommutingRepetition.GraphMod.pair_zero_left (M : StdTracialAlgebra) (v' : M.H) : pair M 0 v' = (Block.embed M (Fin 2) 1) v'

theorem CommutingRepetition.GraphMod.decomp (M : StdTracialAlgebra) (w : Block.BH M (Fin 2)) : w = pair M (w.ofLp 0) (w.ofLp 1)

theorem CommutingRepetition.GraphMod.inner_pair_left (M : StdTracialAlgebra) (v v' : M.H) (w : Block.BH M (Fin 2)) : inner ℂ (pair M v v') w = inner ℂ v (w.ofLp 0) + inner ℂ v' (w.ofLp 1)

theorem CommutingRepetition.GraphMod.inner_pair (M : StdTracialAlgebra) (v v' w w' : M.H) : inner ℂ (pair M v v') (pair M w w') = inner ℂ v w + inner ℂ v' w'

theorem CommutingRepetition.GraphMod.norm_pair_sq (M : StdTracialAlgebra) (v v' : M.H) : ‖pair M v v'‖ ^ 2 = ‖v‖ ^ 2 + ‖v'‖ ^ 2

theorem CommutingRepetition.GraphMod.apply_pair (M : StdTracialAlgebra) (T : Block.BH M (Fin 2) →L[ℂ] Block.BH M (Fin 2)) (v v' : M.H) : T (pair M v v') = pair M ((Block.entry M (Fin 2) T 0 0) v + (Block.entry M (Fin 2) T 0 1) v') ((Block.entry M (Fin 2) T 1 0) v + (Block.entry M (Fin 2) T 1 1) v')

A block operator on a pair, through its four entries.

theorem CommutingRepetition.GraphMod.Rop_Rop (M : StdTracialAlgebra) (a b : M.A) (v : M.H) : (M.Rop b) ((M.Rop a) v) = (M.Rop (a * b)) v

theorem CommutingRepetition.GraphMod.Rt_pair (M : StdTracialAlgebra) (b : M.A) (v v' : M.H) : (Block.Rt M (Fin 2) b) (pair M v v') = pair M ((M.Rop b) v) ((M.Rop b) v')

The graph of left multiplication by x

noncomputable def CommutingRepetition.GraphMod.gen (M : StdTracialAlgebra) (x : M.H) (a : M.A) : Block.BH M (Fin 2)

The generator (ι a, x·a) of the graph.

Equations

• CommutingRepetition.GraphMod.gen M x a = CommutingRepetition.GraphMod.pair M (M.ι a) ((M.Rop a) x)

noncomputable def CommutingRepetition.GraphMod.Γ (M : StdTracialAlgebra) (x : M.H) : Submodule ℂ (Block.BH M (Fin 2))

The closed graph Γₓ.

Equations

• CommutingRepetition.GraphMod.Γ M x = (Submodule.span ℂ (Set.range (CommutingRepetition.GraphMod.gen M x))).topologicalClosure

theorem CommutingRepetition.GraphMod.gen_mem (M : StdTracialAlgebra) (x : M.H) (a : M.A) : gen M x a ∈ Γ M x

theorem CommutingRepetition.GraphMod.isClosed_Γ (M : StdTracialAlgebra) (x : M.H) : IsClosed ↑(Γ M x)

theorem CommutingRepetition.GraphMod.Γ_le (M : StdTracialAlgebra) (x : M.H) {N : Submodule ℂ (Block.BH M (Fin 2))} (hN : IsClosed ↑N) (h : ∀ (a : M.A), gen M x a ∈ N) : Γ M x ≤ N

instance CommutingRepetition.GraphMod.instCompleteSpaceSubtypeBHFinOfNatNatMemSubmoduleComplexΓ (M : StdTracialAlgebra) (x : M.H) : CompleteSpace ↥(Γ M x)

instance CommutingRepetition.GraphMod.instHasOrthogonalProjectionComplexBHFinOfNatNatΓ (M : StdTracialAlgebra) (x : M.H) : (Γ M x).HasOrthogonalProjection

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

The orthogonal projection onto the graph.

Equations

• CommutingRepetition.GraphMod.P M x = (CommutingRepetition.GraphMod.Γ M x).starProjection

theorem CommutingRepetition.GraphMod.P_sa (M : StdTracialAlgebra) (x : M.H) : IsSelfAdjoint (P M x)

theorem CommutingRepetition.GraphMod.P_idem (M : StdTracialAlgebra) (x : M.H) : P M x * P M x = P M x

theorem CommutingRepetition.GraphMod.P_eq_self (M : StdTracialAlgebra) (x : M.H) {w : Block.BH M (Fin 2)} (hw : w ∈ Γ M x) : (P M x) w = w

theorem CommutingRepetition.GraphMod.mem_of_P_eq (M : StdTracialAlgebra) (x : M.H) {w : Block.BH M (Fin 2)} (hw : (P M x) w = w) : w ∈ Γ M x

theorem CommutingRepetition.GraphMod.P_gen (M : StdTracialAlgebra) (x : M.H) (a : M.A) : (P M x) (gen M x a) = gen M x a

Closability

theorem CommutingRepetition.GraphMod.inner_gen_key (M : StdTracialAlgebra) (x : M.H) (a b : M.A) : inner ℂ ((M.Rop a) x) (M.ι b) = inner ℂ (M.ι a) ((M.Rop b) (M.J x))

The adjoint identity on generators: ⟪x·a, ι b⟫ = ⟪ι a, (Jx)·b⟫.

noncomputable def CommutingRepetition.GraphMod.orthGen (M : StdTracialAlgebra) (x : M.H) (b : M.A) : Block.BH M (Fin 2)

The vectors (−(Jx)·b, ι b) are orthogonal to the graph.

Equations

• CommutingRepetition.GraphMod.orthGen M x b = CommutingRepetition.GraphMod.pair M (-(M.Rop b) (M.J x)) (M.ι b)

theorem CommutingRepetition.GraphMod.inner_gen_orthGen (M : StdTracialAlgebra) (x : M.H) (a b : M.A) : inner ℂ (gen M x a) (orthGen M x b) = 0

theorem CommutingRepetition.GraphMod.orthGen_mem (M : StdTracialAlgebra) (x : M.H) (b : M.A) : orthGen M x b ∈ (Γ M x)ᗮ

theorem CommutingRepetition.GraphMod.closable (M : StdTracialAlgebra) (x : M.H) {η : M.H} (h : (Block.embed M (Fin 2) 1) η ∈ Γ M x) : η = 0

Closability: the graph closure is a graph.

Right-action invariance and the entries of P

theorem CommutingRepetition.GraphMod.Rt_gen (M : StdTracialAlgebra) (x : M.H) (b a : M.A) : (Block.Rt M (Fin 2) b) (gen M x a) = gen M x (a * b)

theorem CommutingRepetition.GraphMod.Γ_invariant (M : StdTracialAlgebra) (x : M.H) (b : M.A) {w : Block.BH M (Fin 2)} (hw : w ∈ Γ M x) : (Block.Rt M (Fin 2) b) w ∈ Γ M x

theorem CommutingRepetition.GraphMod.starProjection_comm (M : StdTracialAlgebra) {K : Submodule ℂ (Block.BH M (Fin 2))} [K.HasOrthogonalProjection] {A : Block.BH M (Fin 2) →L[ℂ] Block.BH M (Fin 2)} (hA : ∀ w ∈ K, A w ∈ K) (hA' : ∀ w ∈ K, (star A) w ∈ K) : A * K.starProjection = K.starProjection * A

An operator leaving a closed subspace and its orthogonal complement invariant commutes with the orthogonal projection.

theorem CommutingRepetition.GraphMod.P_comm_Rt (M : StdTracialAlgebra) (x : M.H) (b : M.A) : Block.Rt M (Fin 2) b * P M x = P M x * Block.Rt M (Fin 2) b

theorem CommutingRepetition.GraphMod.P_mem_blockAlg (M : StdTracialAlgebra) (x : M.H) : P M x ∈ Block.blockAlg M (Fin 2)

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

E = P₁₁ = TT*(1+TT*)⁻¹.

Equations

• CommutingRepetition.GraphMod.Eop M x = CommutingRepetition.Block.entry M (Fin 2) (CommutingRepetition.GraphMod.P M x) 1 1

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

C = P₀₁ = T*(1+TT*)⁻¹.

Equations

• CommutingRepetition.GraphMod.Cop M x = CommutingRepetition.Block.entry M (Fin 2) (CommutingRepetition.GraphMod.P M x) 0 1

theorem CommutingRepetition.GraphMod.Eop_mem (M : StdTracialAlgebra) (x : M.H) : Eop M x ∈ M.vnAlg

theorem CommutingRepetition.GraphMod.Cop_mem (M : StdTracialAlgebra) (x : M.H) : Cop M x ∈ M.vnAlg

theorem CommutingRepetition.GraphMod.star_Cop_mem (M : StdTracialAlgebra) (x : M.H) : star (Cop M x) ∈ M.vnAlg

theorem CommutingRepetition.GraphMod.entry_P_one_zero (M : StdTracialAlgebra) (x : M.H) : Block.entry M (Fin 2) (P M x) 1 0 = star (Cop M x)

theorem CommutingRepetition.GraphMod.Eop_sa (M : StdTracialAlgebra) (x : M.H) : IsSelfAdjoint (Eop M x)

theorem CommutingRepetition.GraphMod.P_embed_one (M : StdTracialAlgebra) (x η : M.H) : (P M x) ((Block.embed M (Fin 2) 1) η) = pair M ((Cop M x) η) ((Eop M x) η)

The graph relations

theorem CommutingRepetition.GraphMod.norm_Cop_sq_add (M : StdTracialAlgebra) (x η : M.H) : ‖(Cop M x) η‖ ^ 2 + ‖(Eop M x) η‖ ^ 2 = (inner ℂ η ((Eop M x) η)).re

(R1) ‖Cη‖² + ‖Eη‖² = ⟪η, Eη⟫.

theorem CommutingRepetition.GraphMod.star_Cop_ι (M : StdTracialAlgebra) (x : M.H) (a : M.A) : (star (Cop M x)) (M.ι a) = (1 - Eop M x) ((M.Rop a) x)

(R2) C*(ι a) = (1 − E)(x·a).

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

(R3) C*C = E(1 − E).

theorem CommutingRepetition.GraphMod.norm_Cop_apply_sq (M : StdTracialAlgebra) (x η : M.H) : ‖(Cop M x) η‖ ^ 2 = (inner ℂ η ((Eop M x * (1 - Eop M x)) η)).re

theorem CommutingRepetition.GraphMod.eq_zero_of_Eop_eq (M : StdTracialAlgebra) (x : M.H) {ζ : M.H} (h : (Eop M x) ζ = ζ) : ζ = 0

Injectivity of 1 − E.

theorem CommutingRepetition.GraphMod.Eop_nonneg (M : StdTracialAlgebra) (x : M.H) : 0 ≤ Eop M x

theorem CommutingRepetition.GraphMod.norm_Eop_apply_le (M : StdTracialAlgebra) (x ζ : M.H) : ‖(Eop M x) ζ‖ ≤ ‖ζ‖

theorem CommutingRepetition.GraphMod.Eop_le_one (M : StdTracialAlgebra) (x : M.H) : Eop M x ≤ 1

theorem CommutingRepetition.GraphMod.norm_Eop_le_one (M : StdTracialAlgebra) (x : M.H) : ‖Eop M x‖ ≤ 1

theorem CommutingRepetition.GraphMod.spectrum_Eop_subset (M : StdTracialAlgebra) (x : M.H) : spectrum ℝ (Eop M x) ⊆ Set.Icc 0 1

The spectrum of E lies in [0, 1].

The Borel calculus of E

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

t ↦ max 0 (min 1 t): a bounded continuous function equal to the identity on [0, 1].

Equations

• CommutingRepetition.GraphMod.clamp t = max 0 (min 1 t)

theorem CommutingRepetition.GraphMod.clamp_continuous : Continuous clamp

theorem CommutingRepetition.GraphMod.clamp_nonneg (t : ℝ) : 0 ≤ clamp t

theorem CommutingRepetition.GraphMod.clamp_le_one (t : ℝ) : clamp t ≤ 1

theorem CommutingRepetition.GraphMod.clamp_bdd : BorelCalc.Bdd clamp

theorem CommutingRepetition.GraphMod.one_sub_clamp_bdd : BorelCalc.Bdd fun (t : ℝ) => 1 - clamp t

theorem CommutingRepetition.GraphMod.clamp_of_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) : clamp t = t

theorem CommutingRepetition.GraphMod.clamp_zero : clamp 0 = 0

theorem CommutingRepetition.GraphMod.clamp_one : clamp 1 = 1

theorem CommutingRepetition.GraphMod.vnAlg_strong_closed (M : StdTracialAlgebra) (T : ℕ → M.H →L[ℂ] M.H) (L : M.H →L[ℂ] M.H) : (∀ (n : ℕ), T n ∈ M.vnAlg) → (∀ (ξ : M.H), Filter.Tendsto (fun (n : ℕ) => (T n) ξ) Filter.atTop (nhds (L ξ))) → L ∈ M.vnAlg

theorem CommutingRepetition.GraphMod.bE_mem (M : StdTracialAlgebra) (x : M.H) {g : ℝ → ℝ} (hg : BorelCalc.Bdd g) : BorelCalc.bfc (Eop M x) ⋯ g ∈ M.vnAlg

theorem CommutingRepetition.GraphMod.PE_mem (M : StdTracialAlgebra) (x : M.H) (I : Set ℝ) : BorelCalc.P (Eop M x) ⋯ I ∈ M.vnAlg

theorem CommutingRepetition.GraphMod.bE_clamp (M : StdTracialAlgebra) (x : M.H) : BorelCalc.bfc (Eop M x) ⋯ clamp = Eop M x

E = clamp(E).

theorem CommutingRepetition.GraphMod.one_sub_Eop_sa (M : StdTracialAlgebra) (x : M.H) : IsSelfAdjoint (1 - Eop M x)

theorem CommutingRepetition.GraphMod.one_sub_Eop_eq (M : StdTracialAlgebra) (x : M.H) : 1 - Eop M x = BorelCalc.bfc (Eop M x) ⋯ fun (t : ℝ) => 1 - clamp t

theorem CommutingRepetition.GraphMod.Eop_mul_bE (M : StdTracialAlgebra) (x : M.H) {g : ℝ → ℝ} (hg : BorelCalc.Bdd g) : Eop M x * BorelCalc.bfc (Eop M x) ⋯ g = BorelCalc.bfc (Eop M x) ⋯ fun (t : ℝ) => clamp t * g t

theorem CommutingRepetition.GraphMod.bE_mul_Eop (M : StdTracialAlgebra) (x : M.H) {g : ℝ → ℝ} (hg : BorelCalc.Bdd g) : BorelCalc.bfc (Eop M x) ⋯ g * Eop M x = BorelCalc.bfc (Eop M x) ⋯ fun (t : ℝ) => g t * clamp t

theorem CommutingRepetition.GraphMod.one_sub_Eop_mul_bE (M : StdTracialAlgebra) (x : M.H) {g : ℝ → ℝ} (hg : BorelCalc.Bdd g) : (1 - Eop M x) * BorelCalc.bfc (Eop M x) ⋯ g = BorelCalc.bfc (Eop M x) ⋯ fun (t : ℝ) => (1 - clamp t) * g t

theorem CommutingRepetition.GraphMod.bE_mul_one_sub_Eop (M : StdTracialAlgebra) (x : M.H) {g : ℝ → ℝ} (hg : BorelCalc.Bdd g) : BorelCalc.bfc (Eop M x) ⋯ g * (1 - Eop M x) = BorelCalc.bfc (Eop M x) ⋯ fun (t : ℝ) => g t * (1 - clamp t)

theorem CommutingRepetition.GraphMod.PE_singleton_one (M : StdTracialAlgebra) (x : M.H) : BorelCalc.P (Eop M x) ⋯ {1} = 0

The spectral projection at {1} vanishes (1 − E is injective).

theorem CommutingRepetition.GraphMod.Cop_bfc_traceVector (M : StdTracialAlgebra) (x : M.H) {g : ℝ → ℝ} (hg : BorelCalc.Bdd g) : (Cop M x) ((BorelCalc.bfc (Eop M x) ⋯ g) M.traceVector) = M.J ((BorelCalc.bfc (Eop M x) ⋯ fun (t : ℝ) => (1 - clamp t) * g t) x)

The key formula: C g(E) Ω = J ((1 − t) g)(E) x for bounded Borel g.

theorem CommutingRepetition.GraphMod.PE_singleton_zero_apply (M : StdTracialAlgebra) (x : M.H) : (BorelCalc.P (Eop M x) ⋯ {0}) x = 0

x has no mass at {0} (it lies in the closure of the range of T).