OAI/NumberTheory/CubicMoment/Estimates/NoncubeCutoffPowers.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Numerical margins for the three actual noncube conductor regions.

  1. lemma OAI.CubicFirstMoment.low_core_log_threshold line 11
  2. lemma OAI.CubicFirstMoment.low_height_power_threshold line 24
  3. lemma OAI.CubicFirstMoment.small_core_ordinary_window line 36