OAI/NumberTheory/CubicMoment/Estimates/LowHeightLogIntegral.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The sharp height multiplier has logarithmic integral cost. This is needed when only a fixed power of logarithmic saving is available.

  1. lemma OAI.CubicFirstMoment.lowHeightWeight_norm_le_decay line 13
  2. lemma OAI.CubicFirstMoment.integral_reciprocal_one_add_abs line 33
  3. theorem OAI.CubicFirstMoment.lowHeightWeight_integral_log_bound line 59