TracialPropagation.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Propagation through actual left multipliers on a tracial Hilbert space. The full-column approximation is derived from the concrete corner theorem; the remaining hypotheses describe the repeated words and their tensor geometry.

theorem OAI.KadisonSimilarity.RepeatedLetterWords.tracial_support_commutes line 33
Source documentation
A word support represented by left multiplication commutes with every right multiplier, directly from the tracial representation.
```
theorem tracial_support_commutes (q : P) (hsupport : D.support = G.left q) (b : P) :
    D.support.comp (G.right b) = (G.right b).comp D.support := by
…
```

theorem OAI.KadisonSimilarity.RepeatedLetterWords.tracial_letter_commutes line 40

Source documentation

The tracial left/right action law gives the letter commutation needed by propagation.

theorem tracial_letter_commutes (x : ℕ → P)
    (hletter : ∀ n, D.letter n = G.left (x n)) (b : P) (n : ℕ) :
    (G.right b).comp (D.letter n) = (D.letter n).comp (G.right b) := by
…

theorem OAI.KadisonSimilarity.RepeatedLetterWords.tracial_prefix_commutes line 47

Source documentation

Prefix multiplication obeys the same left/right action law.

theorem tracial_prefix_commutes (a : ℕ → P)
    (hprefix : ∀ n, D.wordPrefix n = G.left (a n)) (b : P) (n : ℕ) :
    (G.right b).comp (D.wordPrefix n) = (D.wordPrefix n).comp (G.right b) := by
…

theorem OAI.KadisonSimilarity.RepeatedLetterWords.tracial_letter_mem line 54

Source documentation

An actual left letter preserves the complete right-supported column.

theorem tracial_letter_mem (r : P) (x : ℕ → P)
    (hletter : ∀ n, D.letter n = G.left (x n)) (n : ℕ) (z : H)
    (hz : z ∈ (G.corner 1 r).toSubmodule) :
    D.letter n z ∈ (G.corner 1 r).toSubmodule := by
…

theorem OAI.KadisonSimilarity.RepeatedLetterWords.tracial_prefix_mem line 62

Source documentation

An actual left prefix preserves the same column.

theorem tracial_prefix_mem (r : P) (a : ℕ → P)
    (hprefix : ∀ n, D.wordPrefix n = G.left (a n)) (n : ℕ) (z : H)
    (hz : z ∈ (G.corner 1 r).toSubmodule) :
    D.wordPrefix n z ∈ (G.corner 1 r).toSubmodule := by
…

theorem OAI.KadisonSimilarity.RepeatedLetterWords.small_mem_tracial_column line 72
Source documentation
An algebraic right support gives membership in the completed right column. This allows the support projection to be chosen for each bounded input vector separately.
```
theorem small_mem_tracial_column (r z : P) (v : B)
    (hsmall : D.small v = G.vector z) (hz : z * r = z) :
    D.small v ∈ (G.corner 1 r).toSubmodule := by
…
```

theorem OAI.KadisonSimilarity.RepeatedLetterWords.propagation_of_tracial_column line 81

Source documentation

The concrete tracial action discharges all multiplier commutation and column-preservation hypotheses in the abstract propagation theorem.

theorem propagation_of_tracial_column (ht : 0 < t)
    (q r : P) (x a : ℕ → P)
    (hsupport : D.support = G.left q)
    (hletter : ∀ n, D.letter n = G.left (x n))
    (hprefix : ∀ n, D.wordPrefix n = G.left (a n))
    (b : P) {η : ℝ}
    (hcolumn : ‖(Y - G.right b).comp (G.corner 1 r).toSubmodule.subtypeL‖ ≤ η)
    (v : B) (hv : D.small v ∈ (G.corner 1 r).toSubmodule) :
    ‖Bₖ (D.repeatVector v) - D.repeatVector (B₀ v)‖ ≤ 2 * η * ‖v‖ := by
…

theorem OAI.KadisonSimilarity.RepeatedLetterWords.propagation_of_tracial_full_column line 99

Source documentation

Supply a concrete supported full-column multiplier; no commutation or invariance assumptions about that multiplier remain.

theorem propagation_of_tracial_full_column (ht : 0 < t)
    (q r : P) (x a : ℕ → P)
    (hsupport : D.support = G.left q)
    (hletter : ∀ n, D.letter n = G.left (x n))
    (hprefix : ∀ n, D.wordPrefix n = G.left (a n))
    {η : ℝ} (fullColumn : ∃ b : P, r * b = b ∧
      ‖(Y - G.right b).comp (G.corner 1 r).toSubmodule.subtypeL‖ ≤ η)
    (v : B) (hv : D.small v ∈ (G.corner 1 r).toSubmodule) :
    ‖Bₖ (D.repeatVector v) - D.repeatVector (B₀ v)‖ ≤ 2 * η * ‖v‖ := by
…

theorem OAI.KadisonSimilarity.TracialCornerGeometry.repeated_propagation_of_full_column line 120

Source documentation

Concrete tracial propagation with the manuscript constant. The column estimate is proved by full_column from projection comparison and the cited cyclic inputs, and is not an additional input.

theorem repeated_propagation_of_full_column
    (e : P) (he : IsStarProjection e) (r : P)
    (hfaithful : Function.Injective G.vector)
    (τ : P → ℝ) (comparison : FiniteFactorProjectionComparison τ)
    (hr : IsStarProjection r) (hτ : τ r ≤ τ e)
    {n : ℕ} (hn : 0 < n) (frame : Fin n → P)
    (hframe : ∀ i j, star (frame i) * frame j = if i = j then e else 0)
    (hsum : ∑ i, frame i * star (frame i) = 1)
    (hYe : Y.comp (G.left e) = (G.left e).comp Y)
    (hYframe : ∀ i, Y.comp (G.left (frame i)) = (G.left (frame i)).comp Y)
    {ε : ℝ} (hε : 0 ≤ ε)
    (hY : ∀ a : CStarCorner e he, ‖commutator Y (G.left (a : P))‖ ≤ ε * ‖a‖)
…

Mentions: OAI.KadisonSimilarity.FiniteFactorProjectionComparison, OAI.KadisonSimilarity.CStarCorner, OAI.KadisonSimilarity.commutator