OAI/NumberTheory/TotientAsymptotic/DyadicCollisionMass.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TotientAsymptotic.dyadic_nat_bounds line 13
2. lemma OAI.TotientAsymptotic.dyadic_endpoint_log line 29
3. lemma OAI.TotientAsymptotic.dyadic_endpoint_B line 32
4. theorem OAI.TotientAsymptotic.finite_dyadic_collision_mass line 38

   Source documentation

   The dyadic count can be integrated using only a lower bound at the occupied slices. Empty slices require no separate counting hypothesis.

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

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

5. lemma OAI.TotientAsymptotic.dyadic_band_start line 84