OAI/NumberTheory/CubicMoment/Estimates/LowHeightIntegral.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The low-height weight has a direct polynomial-logarithmic cost. This transfers the uniform corrected Type-I/II estimates to its integral.

  1. lemma OAI.CubicFirstMoment.cutoffHeightMultiplier_norm_le_log line 12
  2. def OAI.CubicFirstMoment.lowHeightWeight line 20
  3. lemma OAI.CubicFirstMoment.lowHeightWeight_norm_le line 23
  4. lemma OAI.CubicFirstMoment.lowHeightWeight_zero line 32
  5. theorem OAI.CubicFirstMoment.lowHeightWeight_integral_bound line 45