TracialPropagationEndgame.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Propagation on the entire base Hilbert space. Polar decomposition is used only for the right support of the bounded vector qv; density handles all other base vectors. The full-column bound is derived from the cited cyclic inputs.

def OAI.KadisonSimilarity.TracialRightSupportInput line 20
Source documentation
The application-specific consequence of support projections and polar decomposition (Blackadar, I.5.2.1--3): the right support of qv has trace at most that of its containing left projection q.
```
def TracialRightSupportInput (τ : P → ℝ) (q : P) (A : StarSubalgebra ℂ P) : Prop :=
…
```

theorem OAI.KadisonSimilarity.TracialRepeatedWordRealization.propagation_on_base line 38

Source documentation

A supported full-column estimate on each bounded base vector propagates to every vector of the actual closed base space. The support may depend on v.

theorem propagation_on_base
    (R : TracialRepeatedWordRealization W z a Y B₀ Bₖ)
    (hτ : GD.trace 1 = 1) (ha : 0 < a)
    (htrace : GD.trace q = (a : ℂ)) (hhaar : HaarCornerMoments GD.trace z a)
    (τ : P → ℝ) (support : TracialRightSupportInput τ (ι q) A)
    (hsmall : ∀ v : A, R.small (G.baseVector A v) = G.vector (ι q * (v : P)))
    {η : ℝ}
    (hcolumn : ∀ r : P, IsStarProjection r → τ r ≤ τ (ι q) →
      ∃ b : P, r * b = b ∧
        ‖(Y - G.right b).comp (G.corner 1 r).toSubmodule.subtypeL‖ ≤ η)
    (v : G.baseSpace A) :
    ‖Bₖ (R.repeatVector v) - R.repeatVector (B₀ v)‖ ≤ 2 * η * ‖v‖ := by
…

Mentions: OAI.KadisonSimilarity.TracialRepeatedWordRealization, OAI.KadisonSimilarity.HaarCornerMoments, OAI.KadisonSimilarity.TracialRightSupportInput

theorem OAI.KadisonSimilarity.TracialRepeatedWordRealization.propagation_on_base_of_published_inputs line 63

Source documentation

All full-column assumptions are discharged using the actual matrix frame and published cyclic implementation and tracial commutation inputs.

theorem propagation_on_base_of_published_inputs
    (R : TracialRepeatedWordRealization W z a Y B₀ Bₖ)
    (hτ : GD.trace 1 = 1) (ha : 0 < a)
    (htrace : GD.trace q = (a : ℂ)) (hhaar : HaarCornerMoments GD.trace z a)
    (τ : P → ℝ) (support : TracialRightSupportInput τ (ι q) A)
    (hsmall : ∀ v : A, R.small (G.baseVector A v) = G.vector (ι q * (v : P)))
    (e : P) (he : IsStarProjection e) (hqe : τ (ι q) ≤ τ e)
    (hfaithful : Function.Injective G.vector)
    (comparison : FiniteFactorProjectionComparison τ)
    {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)
…

Mentions: OAI.KadisonSimilarity.TracialRepeatedWordRealization, OAI.KadisonSimilarity.HaarCornerMoments, OAI.KadisonSimilarity.TracialRightSupportInput, OAI.KadisonSimilarity.FiniteFactorProjectionComparison