ComparisonClass.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The bound for one fixed class of actual tuple pairs, including both tails.

theorem OAI.TotientAsymptotic.actual_comparison_class_kernel line 16

Source documentation

Fix the surviving indices, the common and canceled primes, the grid and one residual integer. The published Ford estimate then bounds actual pairs, with both residual tuple factorizations included in the saving.

theorem actual_comparison_class_kernel (hford : FordLemma51Input) :
    ∃ C y₀ : ℝ, 0 < C ∧ 1 < y₀ ∧
    ∀ {x t y S h : ℝ} {H k K D r : ℕ} (I : Finset ℕ) (Y U : ℕ → ℝ),
      y₀ ≤ y → 1 ≤ Real.log y → 0 < B y → 5 ≤ h →
      ((R x H-k : ℕ) : ℝ) ≤ h → (I.card : ℝ) ≤ h →
      Real.log (B y) ≤ 26*h →
      (D.primeFactorsList.length : ℝ) ≤ 2*B y/h^8 → (K : ℝ) ≤ 2*B y/h^8 →
      1 < Y I.card → 0 ≤ B (Y I.card) → B (Y I.card) ≤ 2*B y/h^18 →
      FordComparisonParameters I.card y S D r Y U →
      (-2+(∑ j ∈ Finset.Icc 1 (I.card-1), a j*(B (Y j)/B y))+
        comparisonError I.card y S Y U ≤ -1-1/(2*h^4)) →
      L x H < m x → R x H < L x H → k < L x H →
…

Mentions: OAI.TotientAsymptotic.FordLemma51Input, OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.FordComparisonParameters, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.comparisonError, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.m