Source indexedlemma · leanprover/lean4:v4.32.0

Ramanujan.log_2_expansion_t

PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan · PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean:1446 to 1457

Mathematical statement

Exact Lean statement

lemma log_2_expansion_t (x : ℝ) (hx : 2 ≤ x) :
    ∫ t in Set.Icc 2 x, 1 / log t ^ 2 =
      x / log x ^ 2 + 2 * x / log x ^ 3 + 6 * x / log x ^ 4 + 24 * x / log x ^ 5 + 120 * x / log x ^ 6
      - 2 * (∑ k ∈ Finset.Icc 1 5, k.factorial / log 2 ^ (k + 1)) + 720 * ∫ t in Set.Icc 2 x, 1 / log t ^ 7

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma log_2_expansion_t (x : ℝ) (hx : 2 ≤ x) :    ∫ t in Set.Icc 2 x, 1 / log t ^ 2 =      x / log x ^ 2 + 2 * x / log x ^ 3 + 6 * x / log x ^ 4 + 24 * x / log x ^ 5 + 120 * x / log x ^ 6      - 2 * (∑ k ∈ Finset.Icc 1 5, k.factorial / log 2 ^ (k + 1)) + 720 * ∫ t in Set.Icc 2 x, 1 / log t ^ 7 := by  rw [log_2_IBP_t x hx, log_3_IBP_t x hx, log_4_IBP_t x hx, log_5_IBP_t x hx, log_6_IBP_t x hx]  have hsum :      (∑ k ∈ Finset.Icc 1 5, (k.factorial : ℝ) / log 2 ^ (k + 1)) =        (log 2)⁻¹ ^ 2 + (log 2)⁻¹ ^ 3 * 2 + (log 2)⁻¹ ^ 4 * 6 + (log 2)⁻¹ ^ 5 * 24 + (log 2)⁻¹ ^ 6 * 120 := by    norm_num [Finset.sum_Icc_succ_top, Nat.factorial]    ring_nf  rw [hsum]  ring_nf