SharpCutoff.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The sharp-cutoff error at integer norms

The smoothing constructed from the fixed Fourier kernel has a summable endpoint error.

def OAI.CubicFirstMoment.smoothLogInterval line 18
def OAI.CubicFirstMoment.sharpIntervalError line 21
theorem OAI.CubicFirstMoment.intervalStep_log line 24
theorem OAI.CubicFirstMoment.intervalStep_div line 32
theorem OAI.CubicFirstMoment.kernelMoment_nonneg line 36
theorem OAI.CubicFirstMoment.sharpIntervalError_bound line 40
Source documentation
The concrete error has the two summable endpoint majorants.
```
theorem sharpIntervalError_bound {X T n : ℝ}
    (hX : 0 < X) (hT : 0 < T) (hn : 0 < n) (hn4 : n ≤ 4*X) :
    ‖sharpIntervalError X T n‖ ≤ 16 * kernelMoment truncationKernel 1 *
      (endpointKernel (X/T) (n-X) + endpointKernel (X/T) (n-2*X)) := by
…
```
Mentions: OAI.CubicFirstMoment.sharpIntervalError, OAI.CubicFirstMoment.kernelMoment, OAI.CubicFirstMoment.truncationKernel, OAI.CubicFirstMoment.endpointKernel

theorem OAI.CubicFirstMoment.sharp_interval_sum_error line 63

Source documentation

Collected integer coefficients incur exactly the permitted truncation cost.

theorem sharp_interval_sum_error {X T M : ℝ} (hX : 0 < X) (hT : 0 < T)
    (hM : 0 ≤ M) (s : Finset ℤ) (c : ℤ → ℂ)
    (hs : ∀ n ∈ s, 0 < (n : ℝ) ∧ (n : ℝ) ≤ 4*X)
    (hc : ∀ n ∈ s, ‖c n‖ ≤ M) :
    ‖∑ n ∈ s, c n * sharpIntervalError X T n‖ ≤
      64 * kernelMoment truncationKernel 1 * M * (1 + X/T) := by
…

Mentions: OAI.CubicFirstMoment.sharpIntervalError, OAI.CubicFirstMoment.kernelMoment, OAI.CubicFirstMoment.truncationKernel

theorem OAI.CubicFirstMoment.sharp_interval_error_isLittleO line 78

Source documentation

At the chosen height, the actual Fourier-smoothing error is little-oh of the Patterson first-moment scale.

theorem sharp_interval_error_isLittleO {ε ρ : ℝ} (hερ : ε < ρ) (hρ : ρ ≤ 5/6)
    (s : ℝ → Finset ℤ) (c : ℝ → ℤ → ℂ)
    (hs : ∀ X : ℝ, 1 ≤ X → ∀ n ∈ s X, 0 < (n : ℝ) ∧ (n : ℝ) ≤ 4*X)
    (hc : ∀ X : ℝ, 1 ≤ X → ∀ n ∈ s X, ‖c X n‖ ≤ X^ε) :
    (fun X : ℝ => ∑ n ∈ s X, c X n *
      sharpIntervalError X (X^(1/6+ρ : ℝ)) n)
      =o[Filter.atTop] firstMomentScale := by
…

Mentions: OAI.CubicFirstMoment.sharpIntervalError, OAI.CubicFirstMoment.firstMomentScale