OAI/NumberTheory/CubicMoment/Estimates/AllFrequencyOuterSieve.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Add the explicit cube frequencies to the proved outer sieve. The cube count is a lattice count, not an additional analytic hypothesis.

  1. lemma OAI.CubicFirstMoment.cube_frequency_card_le line 14
  2. lemma OAI.CubicFirstMoment.cubic_character_row_sq line 30
  3. theorem OAI.CubicFirstMoment.all_frequency_outer_sieve line 43
  4. lemma OAI.CubicFirstMoment.all_frequency_cubic_operator_bound line 90