OAI/NumberTheory/Ostmann/ZeroDensity/FiniteInverseSquareDensity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.finite_exp_three_halves_sum line 12

   Source documentation

   Sorting by height converts the counting bound into a convergent 4/3-series.

   theorem finite_exp_three_halves_sum {ι : Type*} (S : Finset ι)
       (y : ι → ℝ) (B : ℝ) (hB : 0 ≤ B)
       (hy : ∀ i ∈ S, 0 ≤ y i)
       (hc : ∀ t : ℝ, 0 ≤ t →
         ((S.filter (fun i => y i ≤ t)).card : ℝ) ≤ B * Real.exp ((3 / 2) * t)) :
       (∑ i ∈ S, Real.exp (-2 * y i)) ≤ B ^ (4 / 3 : ℝ) *
         ∑ j ∈ Finset.range S.card, ((j + 1 : ℕ) : ℝ) ^ (-4 / 3 : ℝ) := by
   …