OAI/NumberTheory/CubicMoment/Estimates/LocalizedPowerScale.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The finite derivative cost of log-cell localization is absorbed at a fixed positive power scale, without a lower bound near A = Z².

  1. lemma OAI.CubicFirstMoment.thinCellExponent_le line 10
  2. lemma OAI.CubicFirstMoment.localized_height_ratio line 15
  3. lemma OAI.CubicFirstMoment.localized_remainder_scale line 26
  4. lemma OAI.CubicFirstMoment.localized_root_scale line 42
  5. lemma OAI.CubicFirstMoment.localized_height_power line 51