OAI/NumberTheory/CubicMoment/Estimates/LargeTupleLogScale.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic height and saving normalization for an ordinary group whose scale is at least X^(1/3).

  1. lemma OAI.CubicFirstMoment.largeTuple_log_comparison line 11
  2. lemma OAI.CubicFirstMoment.eventually_largeTuple_height_comparison line 19
  3. lemma OAI.CubicFirstMoment.largeTuple_bilinear_scale line 43