FordKernel.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Restoring both residual tuples still leaves an exponential collision saving.

lemma OAI.TotientAsymptotic.recovery_prefactor_bound line 13
lemma OAI.TotientAsymptotic.smooth_prefactor_bound line 36

theorem OAI.TotientAsymptotic.ford_recovered_kernel line 50

Source documentation

A single class of fixed canceled primes, residual integer and grid has this kernel after paying both missing-tuple and published Ford prefactors.

theorem ford_recovered_kernel {b n K D r : ℕ} {C y S h : ℝ} {Y U : ℕ → ℝ}
    (hC : 0 < C) (hy1 : 1 < y) (hy : 1 ≤ Real.log y) (hBy : 0 < B y)
    (hh : 5 ≤ h) (hn : (n : ℝ) ≤ h) (hb : (b : ℝ) ≤ h)
    (hlogB : Real.log (B y) ≤ 26*h)
    (hD : (D.primeFactorsList.length : ℝ) ≤ 2*B y/h^8)
    (hK : (K : ℝ) ≤ 2*B y/h^8)
    (hT : 1 < Y b) (hZ : 0 ≤ B (Y b)) (hZu : B (Y b) ≤ 2*B y/h^18)
    (hDr : 0 < D*r)
    (hE : -2+(∑ j ∈ Finset.Icc 1 (b-1), a j*(B (Y j)/B y))+comparisonError b y S Y U ≤
      -1-1/(2*h^4)) :
    (n+1 : ℝ)^(D.primeFactorsList.length+K)*fordComparisonBound C b y S D r Y U ≤
      y/(D*r)/Real.log y*Real.exp (6*(|Real.log C|+26)*h^2-B y/(4*h^4)) := by
…

Mentions: OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.comparisonError, OAI.TotientAsymptotic.fordComparisonBound