OAI/NumberTheory/CubicMoment/Estimates/SelectedPrimeGeometry.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact arithmetic after removing the selected largest prime. These identities retain the original squarefreeness, exclusion and norm range.

  1. lemma OAI.CubicFirstMoment.largestPrimeChoice_decomposition line 13
  2. lemma OAI.CubicFirstMoment.selectedPrime_product_conditions line 27
  3. lemma OAI.CubicFirstMoment.selectedPrime_norm_interval line 43
  4. lemma OAI.CubicFirstMoment.largestPrimePredicate_complement line 54