PropagationTheorem.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Propagation from a full column through repeated reduced words

Only raw word identities and the elementary tracial operator relations are supplied below. The error vector, its scaling, the vanishing exceptional coefficient, and the propagation bound are all derived.

theorem OAI.KadisonSimilarity.column_error_apply_le line 24

Source documentation

Evaluate the full-column operator norm bound on a vector in that column.

theorem column_error_apply_le (G S : H →L[ℂ] H) (M : Submodule ℂ H)
    {η : ℝ} (hcolumn : ‖(G - S).comp M.subtypeL‖ ≤ η) (x : H) (hx : x ∈ M) :
    ‖G x - S x‖ ≤ η * ‖x‖ := by
…

theorem OAI.KadisonSimilarity.norm_apply_of_scaled_support line 32

Source documentation

The relation X*X = a⁻¹Q gives the exact tracial scaling on the range fixed by Q; no smallness assumption on ‖X‖ is used.

theorem norm_apply_of_scaled_support (X Q : H →L[ℂ] H) {a : ℝ} (ha : 0 < a)
    (hX : X.adjoint.comp X = ((a⁻¹ : ℝ) : ℂ) • Q) (y : H) (hy : Q y = y) :
    ‖X y‖ = (Real.sqrt a)⁻¹ * ‖y‖ := by
…

structure OAI.KadisonSimilarity.RepeatedLetterWords line 60
Source documentation
Local tracial-word data for one fixed positive word level. The fields are operator identities, word isometries, and the tensor-coordinate formula for the exceptional projection. There is no approximation or propagation bound among the fields.
```
structure RepeatedLetterWords (G : H →L[ℂ] H) (B₀ : B →L[ℂ] B) (Bₖ : V →L[ℂ] V)
    (P : Submodule ℂ H) [P.HasOrthogonalProjection] (a : ℝ) where
…
```
theorem OAI.KadisonSimilarity.RepeatedLetterWords.vacuum_projection_tendsto_zero line 91
Source documentation
The exceptional first-coordinate coefficient vanishes on each fixed error vector. This is a consequence of orthonormality and tensor completion.
```
theorem vacuum_projection_tendsto_zero
    (D : RepeatedLetterWords (E := E) (F := F) G B₀ Bₖ P a) (y : H) :
…
```
Mentions: OAI.KadisonSimilarity.RepeatedLetterWords
theorem OAI.KadisonSimilarity.RepeatedLetterWords.propagation_of_column line 101
Source documentation
The repeated-letter estimate for a vector supported in the full column. The multiplier commutation hypotheses are the raw left/right action laws.
```
theorem propagation_of_column
    (D : RepeatedLetterWords (E := E) (F := F) G B₀ Bₖ P a) (ha : 0 < a)
…
```
Mentions: OAI.KadisonSimilarity.RepeatedLetterWords
theorem OAI.KadisonSimilarity.RepeatedLetterWords.propagation_of_full_column line 164
Source documentation
Feed a supported right multiplier obtained by the full-column theorem into propagation. The support equality is retained in the supplied conclusion; only the column error and left/right commutation enter the limit estimate.
```
theorem propagation_of_full_column
    {A : Type*} [CStarAlgebra A]
    (D : RepeatedLetterWords (E := E) (F := F) G B₀ Bₖ P a) (ha : 0 < a)
…
```
Mentions: OAI.KadisonSimilarity.RepeatedLetterWords

theorem OAI.KadisonSimilarity.norm_repeated_error_le_of_dense line 184

Source documentation

The bounded-vector argument extends to every vector by density and continuity, yielding the operator norm formulation of propagation.

theorem norm_repeated_error_le_of_dense
    {I : Type*} (f : I → B) (hf : DenseRange f)
    (B₀ : B →L[ℂ] B) (Bₖ : V →L[ℂ] V) (repeatVector : B →ₗᵢ[ℂ] V)
    {η : ℝ} (hη : 0 ≤ η)
    (hbound : ∀ i, ‖Bₖ (repeatVector (f i)) - repeatVector (B₀ (f i))‖ ≤ 2 * η * ‖f i‖) :
    ‖Bₖ.comp repeatVector.toContinuousLinearMap - repeatVector.toContinuousLinearMap.comp B₀‖ ≤ 2 * η := by
…