OAI/NumberTheory/CubicMoment/Theta/CubicThetaCentralTypeILowIntegral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integrating the proved low Type-I estimate against the actual central height weight. Outer-level and interval phases have modulus one.

  1. theorem OAI.CubicFirstMoment.typeI_low_integral_bound_actual line 14