SuffixClassKernel.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_injective line 16

Source documentation

Fix the surviving indices, canceled primes, grid and residual integer. The common prefix may vary when the comparison encoding remains injective. The published Ford estimate then bounds actual pairs, with both residual tuple factorizations included in the saving.

theorem actual_comparison_class_kernel_injective (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