RandomizedPairing.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Extracting the scalar commutator from randomized rows

Finite Cauchy–Schwarz bounds the two row errors without a factor for the number of random choices. Together with the scalar commutator estimate this gives the constant 141 in the amplification argument.

theorem OAI.KadisonKastler.norm_limit_le_of_eventually_le_add line 24

Source documentation

A norm bound with arbitrarily small eventual error passes to any limit. No choice of a convergent subsequence is needed.

theorem norm_limit_le_of_eventually_le_add {J V : Type*} [NormedAddCommGroup V]
    {l : Filter J} [l.NeBot] {f : J → V} {z : V} {C : ℝ}
    (hf : Filter.Tendsto f l (𝓝 z))
    (hC : ∀ ε > 0, ∀ᶠ j in l, ‖f j‖ ≤ C + ε) : ‖z‖ ≤ C := by
…

def OAI.KadisonKastler.finiteRMS line 35
theorem OAI.KadisonKastler.finiteRMS_nonneg line 38
theorem OAI.KadisonKastler.expect_norm_mul_le_finiteRMS line 41
def OAI.KadisonKastler.meanPairing line 50
theorem OAI.KadisonKastler.norm_meanPairing_le line 55
Source documentation
The contraction between the two vectors does not increase the Cauchy–Schwarz bound for the average pairing.
```
theorem norm_meanPairing_le (x : Ω → H →L[ℂ] H) (hx : ∀ i, ‖x i‖ ≤ 1)
    (v w : Ω → H) : ‖meanPairing x v w‖ ≤ finiteRMS v * finiteRMS w := by
…
```
Mentions: OAI.KadisonKastler.meanPairing, OAI.KadisonKastler.finiteRMS
theorem OAI.KadisonKastler.norm_mean_operator_pairing_le line 68
Source documentation
An average of arbitrary operator-vector pairings satisfies the same bound when each operator acts with a uniform bound on the chosen vector.
```
theorem norm_mean_operator_pairing_le (x : Ω → H →L[ℂ] H)
    (v w : Ω → H) {δ : ℝ} (hδ : 0 ≤ δ)
    (hx : ∀ i, ‖x i (v i)‖ ≤ δ * ‖v i‖) :
    ‖meanPairing x v w‖ ≤ δ * (finiteRMS v * finiteRMS w) := by
…
```
Mentions: OAI.KadisonKastler.meanPairing, OAI.KadisonKastler.finiteRMS

theorem OAI.KadisonKastler.randomized_pairing_bound line 86

Source documentation

The two row errors and the original scalar commutator estimate give an explicit bound on the scalar pairing recovered by the rows.

theorem randomized_pairing_bound (h : H →L[ℂ] H) (hh : h.IsSymmetric)
    (x : Ω → H →L[ℂ] H) (hx : ∀ i, ‖x i‖ ≤ 1)
    (v w v₀ w₀ : Ω → H) {δ a b : ℝ} (hδ : 0 ≤ δ)
    (hcomm : ∀ i, ‖(h * x i - x i * h) (v i)‖ ≤ δ * ‖v i‖)
    (hv : finiteRMS v ≤ 1) (hw : finiteRMS w ≤ 1)
    (hforward : finiteRMS (fun i => h (v i) - v₀ i) ≤ a)
    (hbackward : finiteRMS (fun i => h (w i) - w₀ i) ≤ b) :
    ‖meanPairing x v w₀ - meanPairing x v₀ w‖ ≤ δ + a + b := by
…

Mentions: OAI.KadisonKastler.finiteRMS, OAI.KadisonKastler.meanPairing

theorem OAI.KadisonKastler.randomized_pairing_le_one_forty_one line 128

Source documentation

The constants used by the manuscript: two errors of size 70δ and one scalar commutator of size δ.

theorem randomized_pairing_le_one_forty_one (h : H →L[ℂ] H) (hh : h.IsSymmetric)
    (x : Ω → H →L[ℂ] H) (hx : ∀ i, ‖x i‖ ≤ 1)
    (v w v₀ w₀ : Ω → H) {δ : ℝ} (hδ : 0 ≤ δ)
    (hcomm : ∀ i, ‖(h * x i - x i * h) (v i)‖ ≤ δ * ‖v i‖)
    (hv : finiteRMS v ≤ 1) (hw : finiteRMS w ≤ 1)
    (hforward : finiteRMS (fun i => h (v i) - v₀ i) ≤ 70 * δ)
    (hbackward : finiteRMS (fun i => h (w i) - w₀ i) ≤ 70 * δ) :
    ‖meanPairing x v w₀ - meanPairing x v₀ w‖ ≤ 141 * δ := by
…

Mentions: OAI.KadisonKastler.finiteRMS, OAI.KadisonKastler.meanPairing

theorem OAI.KadisonKastler.randomized_pairing_limit_le line 141

Source documentation

The randomized pairing estimate needs only eventual row-error bounds, as supplied by the clipped-coefficient limits.

theorem randomized_pairing_limit_le {J : Type*} {l : Filter J} [l.NeBot]
    (h : H →L[ℂ] H) (hh : h.IsSymmetric)
    (x : J → Ω → H →L[ℂ] H) (hx : ∀ j i, ‖x j i‖ ≤ 1)
    (v w v₀ w₀ : J → Ω → H) {δ : ℝ} (hδ : 0 ≤ δ)
    (hcomm : ∀ j i, ‖(h * x j i - x j i * h) (v j i)‖ ≤ δ * ‖v j i‖)
    (hv : ∀ j, finiteRMS (v j) ≤ 1) (hw : ∀ j, finiteRMS (w j) ≤ 1)
    (hforward : ∀ ε > 0, ∀ᶠ j in l,
      finiteRMS (fun i => h (v j i) - v₀ j i) ≤ 70 * δ + ε)
    (hbackward : ∀ ε > 0, ∀ᶠ j in l,
      finiteRMS (fun i => h (w j i) - w₀ j i) ≤ 70 * δ + ε)
    {z : ℂ} (hz : Filter.Tendsto
      (fun j => meanPairing (x j) (v j) (w₀ j) - meanPairing (x j) (v₀ j) (w j)) l (𝓝 z)) :
…

Mentions: OAI.KadisonKastler.finiteRMS, OAI.KadisonKastler.meanPairing

theorem OAI.KadisonKastler.scalar_recovery_quadratic_bound line 163
Source documentation
The scalar lower bound in the recovery construction turns the complex pairing bound into the required real quadratic-form bound.
```
theorem scalar_recovery_quadratic_bound {c d δ : ℝ}
    (hc : 1 / 2 ≤ c) (hbound : ‖((c * d : ℝ) : ℂ)‖ ≤ 141 * δ) :
    |d| ≤ 282 * δ := by
…
```