OAI/NumberTheory/CubicMoment/Estimates/LowCoreHeightSaving.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Above a fixed logarithmic height, the actual ordinary mean supplies every logarithmic saving on the small-core frequency set.

  1. lemma OAI.CubicFirstMoment.logarithmic_height_factor line 13
  2. theorem OAI.CubicFirstMoment.low_core_height_log_saving line 26