OAI/NumberTheory/Ostmann/ZeroDensity/FiniteLaplaceDensity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.finite_exp_density_square_sum line 12
2. theorem OAI.Ostmann.finite_reciprocal_square_sum_le_two line 57
3. theorem OAI.Ostmann.finite_laplace_density_bound line 74

   Source documentation

   An exponential counting bound and a zero-free gap give exponential decay for the whole finite zero sum. Squaring the counting constant is harmless for the subsequent exp(-D L) estimates.

   theorem finite_laplace_density_bound {ι : Type*} (S : Finset ι)
       (y : ι → ℝ) (A B M u : ℝ) (hA : 0 ≤ A) (hB : 0 ≤ B)
       (hM : 4 * A ≤ M) (hu : 0 ≤ u) (hy : ∀ i ∈ S, u ≤ y i)
       (hc : ∀ t : ℝ, 0 ≤ t →
         ((S.filter (fun i => y i ≤ t)).card : ℝ) ≤ B * Real.exp (A * t)) :
       (∑ i ∈ S, Real.exp (-M * y i)) ≤
         2 * B ^ 2 * Real.exp (-(M * u) / 2) := by
   …