OAI/NumberTheory/CubicMoment/Estimates/FullPrimeFactorization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact independent-prime factorization, keeping the squarefree error and the coprimality exclusion of the actual structured sum.

  1. def OAI.CubicFirstMoment.primeExclusionCharacter line 14
  2. lemma OAI.CubicFirstMoment.primeExclusionCharacter_apply line 18
  3. def OAI.CubicFirstMoment.excludedPrimeWeight line 22
  4. lemma OAI.CubicFirstMoment.fullPrimeSupport_eq_prime_filter line 26
  5. lemma OAI.CubicFirstMoment.excluded_prime_factor_eq line 33
  6. lemma OAI.CubicFirstMoment.fullStructuredPrimeSum_eq_mixedSquarefree line 50
  7. lemma OAI.CubicFirstMoment.fullStructuredPrimeSum_factorization line 69