RestoreCommonPrefix.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Restoring all common prefixes after counting distinct suffix pairs.

def OAI.TotientAsymptotic.collisionInnerPrefixes line 16
lemma OAI.TotientAsymptotic.first_collision_prefix_sum line 19
theorem OAI.TotientAsymptotic.collision_inner_prefix_mass line 50
Source documentation
The common-prefix mass is bounded uniformly in the suffix and index.
```
theorem collision_inner_prefix_mass (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput) :
    ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
    ∀ i : ℕ, 1 ≤ i → i ≤ R x H → ∀ t : ℝ,
    (∑ p ∈ collisionInnerPrefixes x H t i, reciprocalShiftWeight p) ≤ G x (m x) := by
…
```
Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.collisionInnerPrefixes, OAI.TotientAsymptotic.reciprocalShiftWeight, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m
theorem OAI.TotientAsymptotic.actual_positive_collision_count line 79
Source documentation
Count all original pairs at a positive first-difference index: both suffix choices and all their common prefixes are now included.
```
theorem actual_positive_collision_count (hford : FordLemma51Input) (hmertens : MertensProductInput)
    (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput) :
    ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
    ∀ i : ℕ, 1 ≤ i → i ≤ R x H → ∀ t ≤ x,
    ((firstCollisionPairs x H t i).card : ℝ) ≤
      (160/Real.log 2)*(x/Real.log x)*G x (m x)*((m x-i : ℕ) : ℝ)^4*
        Real.exp (-fordBandScale x i/(16*((m x-i : ℕ) : ℝ)^4)) := by
…
```
Mentions: OAI.TotientAsymptotic.FordLemma51Input, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.firstCollisionPairs, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.fordBandScale