AngularLatticeCoset.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform-in-translate Poisson estimates. A smooth plane function with zero area has a small sum on every scaled Eisenstein coset.

theorem OAI.CubicFirstMoment.schwartz_dual_lattice_weighted_tail line 13
theorem OAI.CubicFirstMoment.schwartz_zero_area_coset_bound line 66
Source documentation
No arithmetic cancellation is assumed: the zero frequency vanishes by the actual area identity, and the rest is Schwartz Fourier decay.
```
theorem schwartz_zero_area_coset_bound (F : 𝓢(ℂ,ℂ))
    (hF : (∫ z : ℂ, F z) = 0) :
    ∃ K : ℝ, 0 < K ∧ ∀ q : ℂ, q ≠ 0 → ∀ z : ℂ,
      ‖∑' a : Eisenstein, F (z+q*(a:ℂ))‖ ≤ K*Complex.normSq q := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein