SubsetCountBounds.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Counting the few omitted primes above an addition prefix

theorem OAI.JointDickman.subset_count_exp_sum line 12

Source documentation

The exponential generating function used for small omission sets.

theorem subset_count_exp_sum (P : Finset ℕ) (t : ℝ) :
    (∑ A ∈ P.powerset, Real.exp (-t*(A.card : ℝ))) = (1+Real.exp (-t))^P.card := by
…

theorem OAI.JointDickman.subset_count_exp_bound line 26

Source documentation

A real count threshold avoids floor errors in the regularity windows.

theorem subset_count_exp_bound (P : Finset ℕ) {t : ℝ} (ht : 0 ≤ t) (r : ℝ) :
    ((P.powerset.filter (fun A => (A.card : ℝ) ≤ r)).card : ℝ) ≤
      Real.exp (t*r)*(1+Real.exp (-t))^P.card := by
…