CubeLattice.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The convergent cube lattice in dispersion

Rapid decay of the actual radial Fourier profile justifies the cube regrouping. The factor one third is proved from the arithmetic fibers.

lemma OAI.CubicFirstMoment.eisenstein_norm_pow line 20
Distinct definitions of this name: OAI/NumberTheory/CubicGram/CubeEstimates.lean:139 (different declaration text). Qualify references as OAI.CubicFirstMoment.eisenstein_norm_pow@path.
theorem OAI.CubicFirstMoment.summable_radial_cube_lattice line 27
Source documentation
Decay of the Fourier profile makes the cube lattice absolutely summable for every positive scale.
```
theorem summable_radial_cube_lattice (W : ℝ → ℂ) (hW : HasCompactSupport W)
    (hW' : ContDiff ℝ ∞ W) {c : ℝ} (hc : 0 < c) :
    Summable (fun j : Eisenstein => radialDualProfile W (c*(norm j)^3)) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.radialDualProfile, OAI.CubicFirstMoment.norm

theorem OAI.CubicFirstMoment.radial_cube_lattice_sum line 46

Source documentation

The exact normalized cube-frequency sum, with the origin removed.

theorem radial_cube_lattice_sum (W : ℝ → ℂ) (hW : HasCompactSupport W)
    (hW' : ContDiff ℝ ∞ W) {c : ℝ} (hc : 0 < c) :
    (∑' h : Eisenstein, if h ≠ 0 ∧ (∃ j : Eisenstein, j^3 = h) then
      radialDualProfile W (c*norm h) else 0) =
      (1/3:ℂ)*(∑' j : Eisenstein, if j = 0 then 0 else
        radialDualProfile W (c*(norm j)^3)) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.radialDualProfile, OAI.CubicFirstMoment.norm