Source indexedlemma · leanprover/lean4:v4.32.0

BKLNW_app.integrable_η

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:879 to 893

Mathematical statement

Exact Lean statement

lemma integrable_η {c ε : ℝ} (hc : 0 < c) (hε : 0 < ε) :
    MeasureTheory.Integrable (η c ε)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma integrable_η {c ε : ℝ} (hc : 0 < c) (hε : 0 < ε) :    MeasureTheory.Integrable (η c ε) := by  have hsupp : Function.support (η c ε) ⊆ Set.Icc (-ε) ε := by    intro ξ hξ    rw [Set.mem_Icc, ← abs_le]    by_contra h    exact hξ (η_eq_zero_of_abs_gt (not_le.mp h))  rw [← MeasureTheory.integrableOn_iff_integrable_of_support_subset hsupp]  refine MeasureTheory.Measure.integrableOn_of_bounded    (M := c / (2 * ε * sinh c) * besselI0 c)    (by rw [Real.volume_Icc]; exact ENNReal.ofReal_ne_top)    ((measurable_η c ε).aestronglyMeasurable)    (MeasureTheory.ae_of_all _ fun ξ ↦ ?_)  rw [Real.norm_eq_abs, abs_of_nonneg (η_nonneg hc hε ξ)]  exact η_le hc hε ξ