OAI/NumberTheory/CubicMoment/Estimates/SmallBCommonScale.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The small-B scale remains valid after the exact common-factor and Möbius changes of variables.

  1. lemma OAI.CubicFirstMoment.smallB_common_outer_scale line 10
  2. lemma OAI.CubicFirstMoment.smallB_common_height_scale line 22
  3. lemma OAI.CubicFirstMoment.smallB_common_bound_scale line 27