OAI/NumberTheory/CubicMoment/Estimates/SmallBVarianceRemainder.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The pure power saving for the original variance after subtraction of its exact, height-independent zero-frequency model.

  1. def OAI.CubicFirstMoment.varianceZeroMode line 12
  2. lemma OAI.CubicFirstMoment.commonGramZeroMode_height_eq line 16
  3. lemma OAI.CubicFirstMoment.variance_sub_zero_eq line 30
  4. theorem OAI.CubicFirstMoment.smallB_variance_remainder_height_power line 45