WeightedBinomial.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.weighted_binomial_bound line 9

Source documentation

A weighted binomial bound, allowing a real cutoff on subset size.

theorem weighted_binomial_bound (L : ℕ) (t q : ℝ) (hq0 : 0 < q) (hq1 : q ≤ 1) :
    (∑ j ∈ (Finset.range (L + 1)).filter (fun j : ℕ => (j : ℝ) ≤ t),
      (Nat.choose L j : ℝ)) ≤ q ^ (-t) * (1 + q) ^ L := by
…

theorem OAI.Problem337.weighted_binomial_exp_bound line 39

Source documentation

Exponential form of the weighted subset count used in divisor estimates.

theorem weighted_binomial_exp_bound (L : ℕ) (t q : ℝ) (hq0 : 0 < q) (hq1 : q ≤ 1) :
    (∑ j ∈ (Finset.range (L + 1)).filter (fun j : ℕ => (j : ℝ) ≤ t),
      (Nat.choose L j : ℝ)) ≤ Real.exp (-t * Real.log q + (L : ℝ) * q) := by
…