EndpointKernel.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Summing the sharp-cutoff endpoint kernel

The Fourier truncation argument sums rapidly decaying endpoint errors over integer norms. These bounds supply the quantitative lattice step in eq:perron-error, uniformly in the location of the endpoint.

def OAI.CubicFirstMoment.endpointKernel line 18
lemma OAI.CubicFirstMoment.endpointKernel_nonneg line 20
lemma OAI.CubicFirstMoment.endpointKernel_nat_step line 23
lemma OAI.CubicFirstMoment.endpointKernel_tail_sum line 35
lemma OAI.CubicFirstMoment.endpointKernel_range_sum line 46
lemma OAI.CubicFirstMoment.endpointKernel_finite_nat_sum line 62
lemma OAI.CubicFirstMoment.endpointKernel_mono line 71
lemma OAI.CubicFirstMoment.endpointKernel_integer_left line 80
Source documentation
All integer norms to the left of an endpoint can be indexed by their distinct nonnegative integer distances from a fixed integer below it.
```
lemma endpointKernel_integer_left {h x : ℝ} (hh : 0 < h) (z : ℤ)
    (hz : (z : ℝ) ≤ x) (s : Finset ℤ) (hs : ∀ n ∈ s, n ≤ z) :
    (∑ n ∈ s, endpointKernel h ((n : ℝ) - x)) ≤ 1 + h := by
…
```
Mentions: OAI.CubicFirstMoment.endpointKernel
lemma OAI.CubicFirstMoment.endpointKernel_integer_right line 105
theorem OAI.CubicFirstMoment.endpointKernel_integer_sum line 132
Source documentation
Uniform in the real endpoint, including exact equality with an integer. This supplies the O(1+X/T) integer-norm sum in Fourier truncation.
```
theorem endpointKernel_integer_sum {h : ℝ} (hh : 0 < h) (x : ℝ) (s : Finset ℤ) :
    (∑ n ∈ s, endpointKernel h ((n : ℝ) - x)) ≤ 2 * (1 + h) := by
…
```
Mentions: OAI.CubicFirstMoment.endpointKernel

theorem OAI.CubicFirstMoment.weighted_endpoint_error line 148

Source documentation

Summing errors localized near the two endpoints, including endpoints that are integer norms. The coefficient bound is imposed after collecting equal norms, as required by the manuscript.

theorem weighted_endpoint_error {h C M : ℝ} (hh : 0 < h) (hC : 0 ≤ C) (hM : 0 ≤ M)
    (s : Finset ℤ) (x y : ℝ) (c error : ℤ → ℂ)
    (hc : ∀ n ∈ s, ‖c n‖ ≤ M)
    (he : ∀ n ∈ s, ‖error n‖ ≤ C *
      (endpointKernel h ((n : ℝ) - x) + endpointKernel h ((n : ℝ) - y))) :
    ‖∑ n ∈ s, c n * error n‖ ≤ 4 * C * M * (1 + h) := by
…

Mentions: OAI.CubicFirstMoment.endpointKernel

theorem OAI.CubicFirstMoment.endpoint_error_isLittleO line 176

Source documentation

The summed Fourier boundary error is negligible at the first-moment scale when the coefficient loss is smaller than the excess truncation height. This turns a pointwise kernel estimate into the sharp-cutoff summation error, rather than assuming that error as an input.

theorem endpoint_error_isLittleO {ε ρ C : ℝ} (hερ : ε < ρ) (hρ : ρ ≤ 5 / 6)
    (hC : 0 ≤ C) (s : ℝ → Finset ℤ) (c error : ℝ → ℤ → ℂ)
    (hc : ∀ X : ℝ, 1 ≤ X → ∀ n ∈ s X, ‖c X n‖ ≤ X ^ ε)
    (he : ∀ X : ℝ, 1 ≤ X → ∀ n ∈ s X, ‖error X n‖ ≤ C *
      (endpointKernel (X / X ^ (1 / 6 + ρ : ℝ)) ((n : ℝ) - X) +
        endpointKernel (X / X ^ (1 / 6 + ρ : ℝ)) ((n : ℝ) - 2 * X))) :
    (fun X : ℝ => ∑ n ∈ s X, c X n * error X n)
      =o[Filter.atTop] firstMomentScale := by
…

Mentions: OAI.CubicFirstMoment.endpointKernel, OAI.CubicFirstMoment.firstMomentScale