OAI/NumberTheory/CubicMoment/Estimates/LowNormScale.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic normalization at an integral norm cutoff and at a small common-factor residual length.

  1. lemma OAI.CubicFirstMoment.log_floor_norm_comparison line 10
  2. lemma OAI.CubicFirstMoment.log_floor_power_comparison line 28
  3. lemma OAI.CubicFirstMoment.residual_log_comparison line 40