OAI/NumberTheory/CubicMoment/Theta/CubicThetaRadialDyadic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The radial dyadic height estimate in the polynomial range used by the prime decomposition. No metaplectic mean-square input is required.

  1. theorem OAI.CubicFirstMoment.UniformLogWeights.cubicTheta_radial_dyadic_mean line 13