FourthMomentClipping.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Fourth-moment control of the clipping error

The continuous cutoff already used for quotient lifts also supplies the tracial tail estimate needed to test bimodular operators on bounded balls.

theorem OAI.KadisonKastler.discardedFunction_square_le_fourth line 19
theorem OAI.KadisonKastler.spectralClip_discard_fourth_bound line 38
Source documentation
The discarded square is bounded by the fourth power divided by the square of the cutoff, in the C*-algebra order.
```
theorem spectralClip_discard_fourth_bound {β : ℝ} (hβ : 0 < β) (x : A) :
    star (x - spectralClip β x) * (x - spectralClip β x) ≤
      (β ^ 2)⁻¹ • (star x * x) ^ 2 := by
…
```
Mentions: OAI.KadisonKastler.spectralClip
theorem OAI.KadisonKastler.FaithfulTracialState.re_mono line 66
Source documentation
A positive trace is monotone on selfadjoint elements.
```
theorem FaithfulTracialState.re_mono (τ : FaithfulTracialState A) {x y : A}
    (hxy : x ≤ y) : (τ.toLinearMap x).re ≤ (τ.toLinearMap y).re := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
theorem OAI.KadisonKastler.traceTwoNorm_spectralClip_discard_sq_le line 74
Source documentation
Fourth moments control the squared tracial norm lost to clipping.
```
theorem traceTwoNorm_spectralClip_discard_sq_le
    (τ : FaithfulTracialState A) {β : ℝ} (hβ : 0 < β) (x : A) :
    traceTwoNorm τ (x - spectralClip β x) ^ 2 ≤
      (τ.toLinearMap ((star x * x) ^ 2)).re / β ^ 2 := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.spectralClip
theorem OAI.KadisonKastler.traceTwoNorm_spectralClip_le line 83

theorem OAI.KadisonKastler.expect_traceTwoNorm_spectralClip_discard_sq_le line 91

Source documentation

A uniform fourth-moment bound gives the averaged squared tail bound.

theorem expect_traceTwoNorm_spectralClip_discard_sq_le
    {ι : Type*} [Fintype ι] (τ : FaithfulTracialState A) (x : ι → A)
    {β C : ℝ} (hβ : 0 < β)
    (hfour : (𝔼 i, (τ.toLinearMap ((star (x i) * x i) ^ 2)).re) ≤ C) :
    (𝔼 i, traceTwoNorm τ (x i - spectralClip β (x i)) ^ 2) ≤ C / β ^ 2 := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.spectralClip