ActualSuffixMass.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual reciprocal mass of distinct colliding suffix pairs.

def OAI.TotientAsymptotic.suffixDyadicIndex line 15
lemma OAI.TotientAsymptotic.firstCollisionSuffixes_denominator_gt_one line 18
theorem OAI.TotientAsymptotic.actual_suffix_mass line 40
Source documentation
All distinct suffix pairs, with no fixed prefix, have exponentially small reciprocal mass. Constants and the cutoff are uniform in the phase.
```
theorem actual_suffix_mass (hford : FordLemma51Input) (hmertens : MertensProductInput) :
    ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
    ∀ i : ℕ, 1 ≤ i → i ≤ R x H → L x H < m x → R x H < L x H → ∀ t : ℝ,
    (∑ s ∈ firstCollisionSuffixes x H t i, (prefixDenominator s.1 : ℝ)⁻¹) ≤
      (16/Real.log 2)*((m x-i : ℕ) : ℝ)^4*
        Real.exp (-fordBandScale x i/(16*((m x-i : ℕ) : ℝ)^4)) := by
…
```
Mentions: OAI.TotientAsymptotic.FordLemma51Input, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.firstCollisionSuffixes, OAI.TotientAsymptotic.prefixDenominator, OAI.TotientAsymptotic.fordBandScale