RieszConstant.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The exact numerical constant in the cubic Riesz integral.

lemma OAI.CubicFirstMoment.Gamma_third_mul_two_thirds line 11
lemma OAI.CubicFirstMoment.cStar_sq line 19
theorem OAI.CubicFirstMoment.cubic_riesz_constant line 28
Source documentation
Includes the cubing multiplicity, trace-pairing dilation, and the covolume-normalized planar measure.
```
theorem cubic_riesz_constant :
    (1/3:ℝ)*(2/Real.sqrt 3)*Real.pi*(2*Real.pi)^(-(2/3:ℝ))*
      Real.Gamma (1/3:ℝ)/Real.Gamma (2/3:ℝ) = cStar^2 := by
…
```
Mentions: OAI.CubicFirstMoment.cStar
lemma OAI.CubicFirstMoment.cubic_riesz_gaussian_constant line 47