OAI/NumberTheory/CubicMoment/Estimates/AllShortNeighborhoods.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The conductor-neighborhood savings for the literal short factors, with cardinality and amplitude bounds derived from their finite supports.

  1. lemma OAI.CubicFirstMoment.short_neighborhood_length line 13
  2. lemma OAI.CubicFirstMoment.neighborhood_cubic_card line 18
  3. lemma OAI.CubicFirstMoment.neighborhood_balanced_card line 31
  4. theorem OAI.CubicFirstMoment.all_short_cubic_neighborhood line 45
  5. theorem OAI.CubicFirstMoment.all_short_mixed_neighborhood line 89