PowerSavings.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Power savings at the first-moment scale

A fixed power saving is smaller than X^(5/6) / log X. This is the analytic bookkeeping used for the short-range and truncation errors in the sharp-cutoff argument.

theorem OAI.CubicFirstMoment.powerSaving_isLittleO line 20
Source documentation
Any fixed positive power saving is negligible at the asserted scale.
```
theorem powerSaving_isLittleO {δ : ℝ} (hδ : 0 < δ) :
    (fun X : ℝ => X ^ (5 / 6 - δ : ℝ)) =o[atTop] firstMomentScale := by
…
```
Mentions: OAI.CubicFirstMoment.firstMomentScale
theorem OAI.CubicFirstMoment.isLittleO_of_powerSaving line 37
Source documentation
A bound with a fixed power saving implies the required little-oh bound for any normed target space.
```
theorem isLittleO_of_powerSaving {E : Type*} [NormedAddCommGroup E]
    {f : ℝ → E} {δ : ℝ} (hδ : 0 < δ)
    (hf : f =O[atTop] (fun X : ℝ => X ^ (5 / 6 - δ : ℝ))) :
    f =o[atTop] firstMomentScale :=
…
```
Mentions: OAI.CubicFirstMoment.firstMomentScale
theorem OAI.CubicFirstMoment.truncationError_le line 45
Source documentation
The Fourier truncation loss is controlled by a fixed power saving. The harmless 1 term is dominated by the interval-length term.
```
theorem truncationError_le {X ε ρ : ℝ} (hX : 1 ≤ X) (hρ : ρ ≤ 5 / 6) :
    X ^ ε * (1 + X / X ^ (1 / 6 + ρ : ℝ)) ≤
      2 * X ^ (5 / 6 - (ρ - ε) : ℝ) := by
…
```
theorem OAI.CubicFirstMoment.truncationError_isLittleO line 68
Source documentation
Choosing the norm-counting loss below the extra truncation height makes the entire Fourier endpoint error negligible.
```
theorem truncationError_isLittleO {ε ρ : ℝ} (hερ : ε < ρ) (hρ : ρ ≤ 5 / 6) :
    (fun X : ℝ => X ^ ε * (1 + X / X ^ (1 / 6 + ρ : ℝ)))
      =o[atTop] firstMomentScale := by
…
```
Mentions: OAI.CubicFirstMoment.firstMomentScale