OAI/NumberTheory/CubicMoment/Estimates/BalancedErrorMoment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The repeated-prime discrepancy is negligible in the balanced exceptional family. Both its fourth moment and the number of rows are derived from the actual finite supports.

  1. lemma OAI.CubicFirstMoment.balanced_pair_card line 13
  2. lemma OAI.CubicFirstMoment.balanced_error_power_step line 28
  3. theorem OAI.CubicFirstMoment.repeatedPrime_balanced_second_moment line 70