OAI/NumberTheory/CubicMoment/Estimates/TypeIHeightIntegral.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The literal Type-I height integral is bounded by the published-input mean estimates, with the outer norm phase and interval endpoint retained.

  1. def OAI.CubicFirstMoment.typeIHeightIntegral line 14
  2. lemma OAI.CubicFirstMoment.typeIHeightIntegral_le_mean line 20
  3. lemma OAI.CubicFirstMoment.metaplecticAngularSmoothSum_zero_mode line 45
  4. theorem OAI.CubicFirstMoment.radial_typeI_height_integral line 53
  5. theorem OAI.CubicFirstMoment.angular_typeI_height_integral line 79