OAI/NumberTheory/CubicMoment/Estimates/SmallBCommonSum.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Sum the actual small-common-factor blocks with their joint divisor energy. The loss is smaller than the height saving.

  1. lemma OAI.CubicFirstMoment.continuous_commonGramBlock_height line 11
  2. theorem OAI.CubicFirstMoment.smallB_common_sum_height_power line 27