ClippedLimits.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Restoring clipped coefficient columns

These estimates separate the small errors on fixed vectors from the commutator of the moving unitary. In particular, a contractive discarded column costs only the commutator bound of that unitary.

theorem OAI.KadisonKastler.tendsto_column_norm_zero line 25

Source documentation

Finitely many strong errors vanish in column norm as well.

theorem tendsto_column_norm_zero (l : Filter J) (v : J → ω → H)
    (hv : ∀ w, Tendsto (fun j => ‖v j w‖) l (𝓝 0)) :
    Tendsto (fun j => ‖WithLp.toLp 2 (v j)‖) l (𝓝 0) := by
…

theorem OAI.KadisonKastler.column_commutator_error_le line 34

theorem OAI.KadisonKastler.column_commutator_moving_error_le line 45

Source documentation

Restoring a discarded column on a moving vector isolates the sole term which need not vanish on fixed vectors.

theorem column_commutator_moving_error_le (h s : H →L[ℂ] H)
    (E : ω → H →L[ℂ] H)
    (hE : ∀ z, ‖WithLp.toLp 2 (fun w => E w z)‖ ≤ ‖z‖) (y : H) :
    ‖WithLp.toLp 2 (fun w => (h * E w - E w * h) (s y))‖ ≤
      ‖h‖ * ‖WithLp.toLp 2 (fun w => E w (s y))‖ +
        ‖WithLp.toLp 2 (fun w => E w (s (h y)))‖ + ‖(h * s - s * h) y‖ := by
…

theorem OAI.KadisonKastler.column_restored_drift_le line 70

Source documentation

A pointwise error estimate for replacing a clipped column by the original column.

theorem column_restored_drift_le (h : H →L[ℂ] H)
    (K K' E : ω → H →L[ℂ] H) (hK : ∀ w, K w = K' w + E w)
    (x : H) {C : ℝ}
    (hC : ‖WithLp.toLp 2 (fun w => (h * K' w - K' w * h) x)‖ ≤ C) :
    ‖WithLp.toLp 2 (fun w => (h * K w - K w * h) x)‖ ≤ C +
      ‖h‖ * ‖WithLp.toLp 2 (fun w => E w x)‖ +
        ‖WithLp.toLp 2 (fun w => E w (h x))‖ := by
…

theorem OAI.KadisonKastler.column_restored_moving_drift_le line 91

Source documentation

The moving-vector version retains only the commutator of the moving operator besides the two strong errors.

theorem column_restored_moving_drift_le (h s : H →L[ℂ] H)
    (K K' E : ω → H →L[ℂ] H) (hK : ∀ w, K w = K' w + E w)
    (hE : ∀ z, ‖WithLp.toLp 2 (fun w => E w z)‖ ≤ ‖z‖)
    (y : H) {C : ℝ}
    (hC : ‖WithLp.toLp 2 (fun w => (h * K' w - K' w * h) (s y))‖ ≤ C) :
    ‖WithLp.toLp 2 (fun w => (h * K w - K w * h) (s y))‖ ≤ C +
      ‖h‖ * ‖WithLp.toLp 2 (fun w => E w (s y))‖ +
        ‖WithLp.toLp 2 (fun w => E w (s (h y)))‖ + ‖(h * s - s * h) y‖ := by
…

theorem OAI.KadisonKastler.eventually_column_restored_drift_le line 113

Source documentation

Vanishing discarded coefficients on two fixed vectors restore the original drift bound, with arbitrarily small error along the filter.

theorem eventually_column_restored_drift_le (l : Filter J) (h : H →L[ℂ] H)
    (K K' E : J → ω → H →L[ℂ] H) (hK : ∀ j w, K j w = K' j w + E j w)
    (x : H) {C : ℝ}
    (hC : ∀ j, ‖WithLp.toLp 2 (fun w => (h * K' j w - K' j w * h) x)‖ ≤ C)
    (hE : Tendsto (fun j => ‖WithLp.toLp 2 (fun w => E j w x)‖) l (𝓝 0))
    (hEh : Tendsto (fun j => ‖WithLp.toLp 2 (fun w => E j w (h x))‖) l (𝓝 0)) :
    ∀ ε > 0, ∀ᶠ j in l,
      ‖WithLp.toLp 2 (fun w => (h * K j w - K j w * h) x)‖ ≤ C + ε := by
…

theorem OAI.KadisonKastler.eventually_column_restored_moving_drift_le line 131

Source documentation

The moving-vector restoration costs the prescribed commutator bound D, without a factor depending on the number of coefficients.

theorem eventually_column_restored_moving_drift_le (l : Filter J)
    (h : H →L[ℂ] H) (s : J → H →L[ℂ] H)
    (K K' E : J → ω → H →L[ℂ] H) (hK : ∀ j w, K j w = K' j w + E j w)
    (hEcontract : ∀ j z, ‖WithLp.toLp 2 (fun w => E j w z)‖ ≤ ‖z‖)
    (y : H) {C D : ℝ}
    (hC : ∀ j, ‖WithLp.toLp 2 (fun w => (h * K' j w - K' j w * h) (s j y))‖ ≤ C)
    (hD : ∀ j, ‖(h * s j - s j * h) y‖ ≤ D)
    (hEs : Tendsto (fun j => ‖WithLp.toLp 2 (fun w => E j w (s j y))‖) l (𝓝 0))
    (hEsh : Tendsto (fun j => ‖WithLp.toLp 2 (fun w => E j w (s j (h y)))‖) l (𝓝 0)) :
    ∀ ε > 0, ∀ᶠ j in l,
      ‖WithLp.toLp 2 (fun w => (h * K j w - K j w * h) (s j y))‖ ≤ C + D + ε := by
…