OAI/NumberTheory/CubicMoment/Decomposition/StoppedDivisorLogScale.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic choices for the two nonempty-divisor error terms.

  1. lemma OAI.CubicFirstMoment.rough_cutoff_log_saving line 9
  2. lemma OAI.CubicFirstMoment.stopped_hybrid_weighted_scale line 23