OAI/NumberTheory/JointDickman/Arithmetic/PrimeCountChernoff.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.bernoulliSubsetMass_restricted_count_exp line 13

   Source documentation

   The exact generating function for the count in Q.

   theorem bernoulliSubsetMass_restricted_count_exp (P Q : Finset ℕ) (q : ℕ → ℝ) (s : ℝ) :
       (∑ S ∈ P.powerset, bernoulliSubsetMass P q S * Real.exp (s * (S ∩ Q).card)) =
         ∏ p ∈ P ∩ Q, (1 - q p + q p * Real.exp s) := by
   …

   Mentions: OAI.JointDickman.bernoulliSubsetMass

2. theorem OAI.JointDickman.bernoulliSubsetMass_restricted_count_exp_bound line 34
3. theorem OAI.JointDickman.bernoulliSubsetMass_restricted_count_tail line 53

   Source documentation

   Both upper and lower tails are covered by the signed threshold s*r ≤ s*count; no asymptotic or distributional premise is hidden here.

   theorem bernoulliSubsetMass_restricted_count_tail (P Q : Finset ℕ)
       (q : ℕ → ℝ) (s r : ℝ) (hq : ∀ p ∈ P, 0 ≤ q p ∧ q p ≤ 1) :
       (∑ S ∈ P.powerset, if s * r ≤ s * (S ∩ Q).card then bernoulliSubsetMass P q S else 0) ≤
         Real.exp (-s * r + (Real.exp s - 1) * ∑ p ∈ P ∩ Q, q p) := by
   …

   Mentions: OAI.JointDickman.bernoulliSubsetMass