OAI/NumberTheory/CubicMoment/Estimates/ScaleFirstStoppedAggregation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The exact finite stopping sums cost only a fixed power of log X.

  1. lemma OAI.CubicFirstMoment.norm_double_sum_le_card_sq line 12
  2. theorem OAI.CubicFirstMoment.distinguishedScaleStoppedRow_bound line 25
  3. theorem OAI.CubicFirstMoment.distinguishedScaleStopped_bound line 64