Source indexedlemma · leanprover/lean4:v4.32.0

BKLNW_app.integrable_μ

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1009 to 1025

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 t ht    rw [Set.mem_Icc, ← abs_le]    by_contra h    rcases lt_abs.mp (not_le.mp h) with h1 | h1    · exact ht (μ_eq_zero_of_gt hε h1)    · exact ht (μ_eq_zero_of_lt_neg hε (by linarith))  rw [← MeasureTheory.integrableOn_iff_integrable_of_support_subset hsupp]  refine MeasureTheory.Measure.integrableOn_of_bounded    (M := c / sinh c * besselI0 c)    (by rw [Real.volume_Icc]; exact ENNReal.ofReal_ne_top)    ((measurable_μ hc hε).aestronglyMeasurable)    (MeasureTheory.ae_of_all _ fun t ↦ ?_)  rw [Real.norm_eq_abs]  exact μ_abs_le hc hε t