Source indexedlemma · leanprover/lean4:v4.32.0

Ramanujan.Li_eq_sub_add_integral

PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations · PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:354 to 366

Source documentation

Integration by parts formula for Li(x).

Exact Lean statement

lemma Li_eq_sub_add_integral (x : ℝ) (hx : 2 ≤ x) :
    Li x = x / log x - 2 / log 2 + ∫ t in Icc 2 x, 1 / log t ^ 2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma Li_eq_sub_add_integral (x : ℝ) (hx : 2 ≤ x) :    Li x = x / log x - 2 / log 2 + ∫ t in Icc 2 x, 1 / log t ^ 2 := by  rw [MeasureTheory.integral_Icc_eq_integral_Ioc, ← intervalIntegral.integral_of_le (by linarith),    Li, intervalIntegral.integral_eq_sub_of_hasDerivAt]  rotate_right  · use fun t ↦ t / log t + ∫ u in (2 : ℝ)..t, 1 / log u ^ 2  · norm_num; ring  · intro t ht    exact hasDerivAt_li_antideriv (by norm_num) (by cases Set.mem_uIcc.mp ht <;> linarith)  · exact ContinuousOn.intervalIntegrable (continuousOn_of_forall_continuousAt fun t ht ↦      ContinuousAt.div continuousAt_const (continuousAt_log        (by linarith [Set.mem_Icc.mp (by simpa [hx] using ht)]))          (ne_of_gt (log_pos (by linarith [Set.mem_Icc.mp (by simpa [hx] using ht)]))))