Source indexedlemma · leanprover/lean4:v4.32.0

integral_log_inv_pialt

PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:808 to 816

Mathematical statement

Exact Lean statement

lemma integral_log_inv_pialt (x : ℝ) (hx : 4 ≤ x) : ∫ (t : ℝ) in Set.Icc 2 x, 1 / log t =
    x / log x - 2 / log 2 + ∫ (t : ℝ) in Set.Icc 2 x, 1 / (log t) ^ 2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma integral_log_inv_pialt (x : ℝ) (hx : 4 ≤ x) : ∫ (t : ℝ) in Set.Icc 2 x, 1 / log t =    x / log x - 2 / log 2 + ∫ (t : ℝ) in Set.Icc 2 x, 1 / (log t) ^ 2 := by  have := integral_log_inv 2 x (by norm_num) (by linarith)  rw [MeasureTheory.integral_Icc_eq_integral_Ioc,    ← intervalIntegral.integral_of_le (by linarith [hx]),    MeasureTheory.integral_Icc_eq_integral_Ioc,      ← intervalIntegral.integral_of_le (by linarith [hx]),    ← mul_one_div, one_div, ← mul_one_div, one_div]  simp only [one_div, this, mul_comm]