OAI/NumberTheory/TotientAsymptotic/PPTPreimageSplit.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The actual low/high factorization of a chosen preimage in the PPT construction. Large square factors have already been excluded; the high factor therefore has a strictly decreasing prime list. No conclusion about a mismatch with a second prime list is asserted here.

  1. lemma OAI.TotientAsymptotic.ppt_partAbove_eq_partBetween line 19
  2. lemma OAI.TotientAsymptotic.ppt_partAbove_pos line 28
  3. lemma OAI.TotientAsymptotic.ppt_partAbove_dvd line 32
  4. lemma OAI.TotientAsymptotic.ppt_partAbove_prime_gt line 36
  5. lemma OAI.TotientAsymptotic.ppt_partBelow_prime_le line 43
  6. lemma OAI.TotientAsymptotic.ppt_low_high_coprime line 49
  7. lemma OAI.TotientAsymptotic.ppt_low_totient_smooth line 56
  8. lemma OAI.TotientAsymptotic.ppt_high_squarefree line 66
  9. theorem OAI.TotientAsymptotic.ppt_preimage_prime_split_full line 74

    Source documentation

    The residual low totient and the ordered high primes give the exact equation used for unequal-list alignment. Normality is inherited from the actual preimage, and all high primes are strictly above the cutoff.

    theorem ppt_preimage_prime_split_full {n : ℕ} {S : ℝ} (hn : 0 < n) (hS : 1 ≤ S)
    (hsq : SquarefreeAbove n S)
    (hnormal : ∀ p : ℕ, p.Prime → p ∣ n → IsNormalPrime S p) :
    ∃ (h : ℕ) (p : Fin h → ℕ) (s : ℕ),
      0 < s ∧ n = s*∏ i, p i ∧ s.Coprime (∏ i, p i) ∧
      (largestPrimeFactor s.totient : ℝ) ≤ S ∧ StrictAnti p ∧
      (∀ i, IsNormalPrime S (p i) ∧ S < (p i : ℝ)) ∧
      n.totient = s.totient*shiftedProduct p ∧ s = partBelow n S := by
…

    Mentions: OAI.TotientAsymptotic.SquarefreeAbove, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.largestPrimeFactor, OAI.TotientAsymptotic.shiftedProduct, OAI.TotientAsymptotic.partBelow

  10. theorem OAI.TotientAsymptotic.ppt_preimage_prime_split line 134

    Source documentation

    Decomposition of a totient preimage for normality alignment.

    theorem ppt_preimage_prime_split {n : ℕ} {S : ℝ} (hn : 0 < n) (hS : 1 ≤ S)
    (hsq : SquarefreeAbove n S)
    (hnormal : ∀ p : ℕ, p.Prime → p ∣ n → IsNormalPrime S p) :
    ∃ (h : ℕ) (p : Fin h → ℕ) (s : ℕ),
      0 < s ∧ n = s*∏ i, p i ∧ s.Coprime (∏ i, p i) ∧
      (largestPrimeFactor s.totient : ℝ) ≤ S ∧ StrictAnti p ∧
      (∀ i, IsNormalPrime S (p i) ∧ S < (p i : ℝ)) ∧
      n.totient = s.totient*shiftedProduct p := by
…

    Mentions: OAI.TotientAsymptotic.SquarefreeAbove, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.largestPrimeFactor, OAI.TotientAsymptotic.shiftedProduct