Source indexedtheorem · leanprover/lean4:v4.32.0

Li2Bounds.log_one_minus_integrable

PrimeNumberTheoremAnd.IEANTN.Li2Bounds · PrimeNumberTheoremAnd/IEANTN/Li2Bounds.lean:57 to 72

Source documentation

1/log(1-u) is integrable on [ε, 1) for ε > 0.

Exact Lean statement

theorem log_one_minus_integrable (ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1) :
    IntervalIntegrable (fun u => 1 / log (1 - u)) volume ε 1

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem log_one_minus_integrable (ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1) :    IntervalIntegrable (fun u => 1 / log (1 - u)) volume ε 1 := by  rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hε1.le]  refine Measure.integrableOn_of_bounded (M := 1 / ε) measure_Ioc_lt_top.ne    (Measurable.aestronglyMeasurable (by fun_prop)) ?_  filter_upwards [self_mem_ae_restrict (by measurability), Measure.ae_ne _ 1]    with u ⟨hε_lt_u, hu_le_one⟩ hu_ne_one  have h1mu_pos : 0 < 1 - u := by grind  have h1mu_lt1 : 1 - u < 1 := by linarith  have hlog_neg : log (1 - u) < 0 := log_neg h1mu_pos h1mu_lt1  rw [Real.norm_eq_abs, abs_one_div, abs_of_neg hlog_neg]  gcongr  have hlog_ub : log (1 - u) ≤ -u := by    have h := log_le_sub_one_of_pos h1mu_pos    linarith  linarith