CollisionDyadicCount.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

From counts in dyadic suffix intervals to their reciprocal mass.

theorem OAI.TotientAsymptotic.collision_dyadic_reciprocal_bound line 14

Source documentation

The dyadic count has the exact normalization C*y/log(y) times its strict-slack saving. Weighting each suffix by its reciprocal cancels y.

theorem collision_dyadic_reciprocal_bound {α : Type*} (Q : Finset α)
    (idx : α → ℕ) (v : α → ℝ) {N : ℕ} (hN : 1 ≤ N) {C σ B : ℝ}
    (hC : 0 ≤ C) (hσ : 0 < σ) (hB : Real.exp B ≤ (N : ℝ)*Real.log 2)
    (hlo : ∀ a ∈ Q, (2 : ℝ)^(idx a+N+1)/2 < v a)
    (hcount : ∀ k : ℕ, ((Q.filter (fun a => idx a=k)).card : ℝ) ≤
      C*(2 : ℝ)^(k+N+1)*dyadicSuffixWeight σ (k+N+1)) :
    (∑ a ∈ Q, (v a)⁻¹) ≤ (2*C)/(σ*Real.log 2)*Real.exp (-σ*B) := by
…

Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.dyadicSuffixWeight