CubeRiesz.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Identification of the actual cube-lattice integral with the model term.

lemma OAI.CubicFirstMoment.normProfileFourier_cubing_integral line 14
theorem OAI.CubicFirstMoment.cubeProfileIntegral_eq_model line 31
Source documentation
The exact Riesz constant for the trace pairing and covolume-one Eisenstein measure. All Fourier and singular-integral steps are proved.
```
theorem cubeProfileIntegral_eq_model (W : ℝ → ℂ) (hW : HasCompactSupport W)
    (hW' : ContDiff ℝ ∞ W) :
    cubeProfileIntegral W = (cStar^2:ℝ) •
      ((2/Real.sqrt 3:ℝ) • (∫ z : ℂ, ((‖z‖^(-(2/3:ℝ)):ℝ):ℂ)*W (Complex.normSq z))) := by
…
```
Mentions: OAI.CubicFirstMoment.cubeProfileIntegral, OAI.CubicFirstMoment.cStar