OAI/NumberTheory/CubicMoment/Estimates/SieveTruncationScale.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The norm and cardinality costs of the logarithmic square-divisor truncation used in the positive variance term.

  1. lemma OAI.CubicFirstMoment.squarefreeDivisorTruncation_card_le line 14
  2. lemma OAI.CubicFirstMoment.squarefreeTruncation_join_norm line 22
  3. lemma OAI.CubicFirstMoment.eventually_logPower_le_rpow line 31