Propagation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The fixed-prefix limit in propagation from a small corner

On the centered-word subspace the prefix acts isometrically. On the remaining subspace its norm may be large, but is fixed while the tensor slice tends to zero. The estimates below carry out that limit without a rate assumption.

theorem OAI.KadisonSimilarity.norm_prefix_le line 25

Source documentation

Split a prefix into its isometric centered-word action and the exceptional projection. The latter incurs only the fixed operator norm.

theorem norm_prefix_le (P : Submodule ℂ H) [P.HasOrthogonalProjection]
    (A : H →L[ℂ] H)
    (hisometry : ∀ z ∈ Pᗮ, ‖A z‖ = ‖z‖) (z : H) :
    ‖A z‖ ≤ ‖z‖ + ‖A‖ * ‖P.starProjection z‖ := by
…

theorem OAI.KadisonSimilarity.propagation_bound_of_vanishing_projection line 43

Source documentation

A uniform prefix bound need not be small. It vanishes from the resulting estimate because it multiplies a sequence converging to zero.

theorem propagation_bound_of_vanishing_projection
    (P : Submodule ℂ H) [P.HasOrthogonalProjection]
    (A : ℕ → H →L[ℂ] H) (z : ℕ → H)
    (hisometry : ∀ n, ∀ v ∈ Pᗮ, ‖A n v‖ = ‖v‖)
    (L : ℝ) (hL : ∀ n, ‖A n‖ ≤ L)
    (error target : ℝ) (hz : ∀ n, ‖z n‖ ≤ error)
    (hvanish : Tendsto (fun n => P.starProjection (z n)) atTop (𝓝 0))
    (htest : ∀ n, target ≤ error + ‖A n (z n)‖) :
    target ≤ 2 * error := by
…

theorem OAI.KadisonSimilarity.corner_scaled_error_le line 63
Source documentation
The scaling identity in the small corner removes its trace from the propagation error.
```
theorem corner_scaled_error_le {a c ε v y : ℝ} (ha : 0 < a)
    (hy : y ≤ c * ε * Real.sqrt a * v) :
    (Real.sqrt a)⁻¹ * y ≤ c * ε * v := by
…
```