PPTTailParameters.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The factor-count cost of fixing the small left tail in the PPT application of Ford's comparison lemma. Normality bounds the count through the terminal cutoff, rather than through the much larger size of the tail.

theorem OAI.TotientAsymptotic.ppt_small_tail_totient_omega line 17

theorem OAI.TotientAsymptotic.ppt_small_tail_seed_omega line 31

Source documentation

The seed contribution stays fixed; the tail contributes only through its number of primes and the double logarithm of the terminal cutoff.

theorem ppt_small_tail_seed_omega {h d : ℕ} (p : Fin h → ℕ) {S V : ℝ}
    (hd : 0 < d) (hp : ∀ i, IsNormalPrime S (p i)) (hinj : Function.Injective p)
    (hS : 1 < S) (hBS : 0 ≤ B S) (hSV : S ≤ V)
    (hsmall : ∀ i, (largestPrimeFactor (p i-1) : ℝ) ≤ V) :
    ((d*(∏ i, p i).totient).primeFactorsList.length : ℝ) ≤
      d.primeFactorsList.length + 4*(h : ℝ)*B V := by
…

Mentions: OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.largestPrimeFactor

theorem OAI.TotientAsymptotic.ppt_small_tail_comparison_cost line 45

Source documentation

Explicit additional cost of using D=d*φ(a) in the l=0 specialization of the comparison estimate.

theorem ppt_small_tail_comparison_cost {h d : ℕ} (b : ℕ) (p : Fin h → ℕ) {S V : ℝ}
    (hd : 0 < d) (hp : ∀ i, IsNormalPrime S (p i)) (hinj : Function.Injective p)
    (hS : 1 < S) (hBS : 0 ≤ B S) (hSV : S ≤ V)
    (hsmall : ∀ i, (largestPrimeFactor (p i-1) : ℝ) ≤ V) :
    (b+1 : ℝ)^((d*(∏ i, p i).totient).primeFactorsList.length) ≤
      (b+1 : ℝ)^d.primeFactorsList.length *
        Real.exp (4*(h : ℝ)*B V*Real.log (b+1)) := by
…

Mentions: OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.largestPrimeFactor