RowExtraction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Extracting the unitary quadratic bound from randomized rows

theorem OAI.KadisonKastler.row_scalar_quadratic_bound line 21

Source documentation

The two drift estimates and the scalar weak limit give the real quadratic estimate. The rows and contractions are the actual operators; no bound on the size of the finite random space occurs.

theorem row_scalar_quadratic_bound
    {l : Filter J} [l.NeBot]
    (h : H →L[ℂ] H) (hh : h.IsSymmetric)
    (T : K →L[ℂ] K) (hT : IsSelfAdjoint T)
    (u : unitary (K →L[ℂ] K)) (ξ : K)
    (F G : J → Ω → K →L[ℂ] H) (x : J → Ω → H →L[ℂ] H)
    {δ c : ℝ} (hδ : 0 ≤ δ) (hc : 1 / 2 ≤ c)
    (hx : ∀ j i, ‖x j i‖ ≤ 1)
    (hcomm : ∀ j i, ‖(h * x j i - x j i * h) (F j i ξ)‖ ≤ δ * ‖F j i ξ‖)
    (hF : ∀ j, finiteRMS (fun i => F j i ξ) ≤ 1)
    (hG : ∀ j, finiteRMS (fun i => G j i ξ) ≤ 1)
    (hforward : ∀ ε > 0, ∀ᶠ j in l,
…

Mentions: OAI.KadisonKastler.finiteRMS