OAI/NumberTheory/CubicMoment/Theta/CubicThetaTypeIMixedLow.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Type I with the precise radial factor in the mixed term of the corrected square. The squarefree product model, including common zeros, is preserved on the right.

  1. theorem OAI.CubicFirstMoment.cubicTheta_typeI_mixed_low line 13