CubeAsymptotic.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The integral main term of the principal cube lattice.

def OAI.CubicFirstMoment.cubeProfileIntegral line 16
Source documentation
The normalized planar integral; the measure of an Eisenstein fundamental parallelogram is one.
```
def cubeProfileIntegral (W : ℝ → ℂ) : ℂ :=
…
```
lemma OAI.CubicFirstMoment.cubeProfileIntegral_eq line 19
theorem OAI.CubicFirstMoment.radial_cube_lattice_asymptotic line 32
Source documentation
The nonzero cube lattice has its integral main term with a bounded error for q ≤ 1. This is stronger than the radius-size error needed in the low-height dispersion application.
```
theorem radial_cube_lattice_asymptotic (W : ℝ → ℂ)
    (hW : HasCompactSupport W) (hW' : ContDiff ℝ ∞ W) :
    ∃ C : ℝ, 0 < C ∧ ∀ q : ℝ, 0 < q → q ≤ 1 →
      ‖(∑' j : Eisenstein, if j = 0 then (0:ℂ) else
          radialDualProfile W (q^3*(norm j)^3)) -
        (q⁻¹:ℝ) • cubeProfileIntegral W‖ ≤ C := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.radialDualProfile, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.cubeProfileIntegral