OAI/NumberTheory/CubicMoment/Estimates/LargestPrimeSelection.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Exact selection of a largest prime, with a fixed injective tie code. This is an unordered selection: inserting it into a finite sum introduces no factor depending on the number of primes.

  1. def OAI.CubicFirstMoment.primeTieCode line 13
  2. lemma OAI.CubicFirstMoment.primeTieCode_injective line 16
  3. lemma OAI.CubicFirstMoment.exists_largestPrime line 28
  4. lemma OAI.CubicFirstMoment.largestPrime_unique line 44
  5. def OAI.CubicFirstMoment.selectedLargestPrime line 55
  6. lemma OAI.CubicFirstMoment.selectedLargestPrime_spec line 58
  7. lemma OAI.CubicFirstMoment.selectedLargestPrime_norm line 63
  8. lemma OAI.CubicFirstMoment.selectedLargestPrime_large line 73
  9. lemma OAI.CubicFirstMoment.selectedLargestPrime_product_split line 80
  10. theorem OAI.CubicFirstMoment.primary_largest_prime_split line 88

    Source documentation

    The actual largest prime of a squarefree primary element can be removed once, leaving a primary squarefree factor coprime to it.

    theorem primary_largest_prime_split {n : Eisenstein} (hn : primary n)
    (hs : Squarefree n) (hne : (primaryPrimeFactors n).Nonempty) :
    ∃ p c : Eisenstein, primaryPrime p ∧ primary c ∧ Squarefree c ∧
      ¬p ∣ c ∧ p*c = n ∧
      largestPrimePredicate primeTieCode (primaryPrimeFactors c) p ∧
      normNat p = (primaryPrimeFactors n).sup normNat := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.primaryPrimeFactors, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.largestPrimePredicate, OAI.CubicFirstMoment.primeTieCode, OAI.CubicFirstMoment.normNat

  11. lemma OAI.CubicFirstMoment.largestPrimePredicate_erase line 115
  12. theorem OAI.CubicFirstMoment.sum_largestPrime_selected line 127