OAI/NumberTheory/CubicMoment/Estimates/TypeILowIntegral.lean

GitHub source file

2 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. def OAI.CubicFirstMoment.lowTypeIIntegral line 13
  2. theorem OAI.CubicFirstMoment.typeI_low_integral_bound line 19