Li2Bounds.g_intervalIntegrable_full

theorem g_intervalIntegrable_full : IntervalIntegrable g volume 0 1 := by  apply (intervalIntegrable_iff_integrableOn_Ioo_of_le (by linarith)).2  apply Measure.integrableOn_of_bounded measure_Ioo_lt_top.ne  · exact Measurable.aestronglyMeasurable (by      unfold g      change Measurable fun t : ℝ => 1 / log (1 + t) + 1 / log (1 - t)      fun_prop)  · filter_upwards [self_mem_ae_restrict (by measurability)] with t ht    have habs : |g t| = g t := abs_of_pos <|      LeanCert.CertifiedBounds.Li2.integrand_pos t ht.1 ht.2    simpa [Real.norm_eq_abs, habs] using!      LeanCert.CertifiedBounds.Li2.integrand_le_two t ht.1 ht.2