SchwartzLattice.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A Poisson proof of the lattice approximation needed by the cubic profile.

lemma OAI.CubicFirstMoment.traceLambda_normSq line 14

theorem OAI.CubicFirstMoment.schwartz_dual_lattice_tail line 19

Source documentation

Rapid decay gives a uniform bound for the nonzero dual lattice.

theorem schwartz_dual_lattice_tail (F : 𝓢(ℂ,ℂ)) :
    ∃ C : ℝ, 0 < C ∧ ∀ w : ℂ, w ≠ 0 →
      ‖∑' h : Eisenstein, if h = 0 then 0 else traceFourier F ((h:ℂ)/w)‖ ≤
        C*(Complex.normSq w)^2 := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.traceFourier

lemma OAI.CubicFirstMoment.traceFourier_zero line 64
theorem OAI.CubicFirstMoment.schwartz_lattice_approximation line 69
Source documentation
The area-normalized lattice sum differs from its integral by O(s²). This form is applied only to the fixed cubic Schwartz profile.
```
theorem schwartz_lattice_approximation (F : 𝓢(ℂ,ℂ)) :
    ∃ C : ℝ, 0 < C ∧ ∀ s : ℝ, 0 < s →
      ‖(∑' a : Eisenstein, F ((s:ℂ)*(a:ℂ))) -
        (2/(Real.sqrt 3*s^2):ℝ) • (∫ z : ℂ, F z)‖ ≤ C*s^2 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein