OAI/NumberTheory/CubicMoment/Estimates/ShortOuterLow.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Sum all short outer norm dyads in the central corrected kernel. The dyad count costs one logarithm, and all weights and support are actual.

  1. def OAI.CubicFirstMoment.shortOuterCount line 14
  2. lemma OAI.CubicFirstMoment.shortOuterCount_covers line 16
  3. lemma OAI.CubicFirstMoment.shortOuterCount_scale line 23
  4. theorem OAI.CubicFirstMoment.shortOuterCount_log_bound line 30
  5. theorem OAI.CubicFirstMoment.short_outer_low_bound line 44