SuffixRepresentatives.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Selecting one actual witness pair for each distinct suffix pair.

lemma OAI.TotientAsymptotic.finite_image_representatives line 14

theorem OAI.TotientAsymptotic.actual_suffix_block_count line 43

Source documentation

The full exponential saving counts distinct suffix pairs independently of how many common prefixes or full witnesses represent each suffix.

theorem actual_suffix_block_count (hford : FordLemma51Input) (hmertens : MertensProductInput) :
    ∃ y₀ : ℝ, 1 < y₀ ∧ ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
    ∀ i : ℕ, i ≤ R x H → L x H < m x → R x H < L x H → ∀ t y : ℝ,
    y₀ ≤ y → 0 < B y → (87/100 : ℝ)*fordBandScale x i ≤ B y → B y ≤ 2*fordBandScale x i →
    ∀ Q : Finset (TotientTuple (R x H) × TotientTuple (R x H)),
    (∀ q ∈ Q, GoodCollisionBlock x t H i y q) →
    ((Q.image (fun q => pairSuffix q i)).card : ℝ) ≤
      y/Real.log y*Real.exp (-B y/(8*((m x-i : ℕ) : ℝ)^4)) := by
…

Mentions: OAI.TotientAsymptotic.FordLemma51Input, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.fordBandScale, OAI.TotientAsymptotic.TotientTuple, OAI.TotientAsymptotic.GoodCollisionBlock, OAI.TotientAsymptotic.pairSuffix