OAI/NumberTheory/CubicMoment/Estimates/SmallBLogScale.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Explicit outer-length and logarithmic losses for the small-B variance. Only positive real powers and the proved logarithm bound occur.

  1. lemma OAI.CubicFirstMoment.smallB_outer_log_root line 11
  2. lemma OAI.CubicFirstMoment.smallB_diagonal_log_scale line 24
  3. lemma OAI.CubicFirstMoment.smallB_nondiagonal_log_scale line 43