Source indexedtheorem · leanprover/lean4:v4.32.0

Li2Bounds.pv_integral_eq_symmetric

PrimeNumberTheoremAnd.IEANTN.Li2Bounds · PrimeNumberTheoremAnd/IEANTN/Li2Bounds.lean:157 to 166

Source documentation

The principal value integral for li(2) equals ∫_ε^1 g(u) du.

Exact Lean statement

theorem pv_integral_eq_symmetric (ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1) :
    (∫ t in (0 : ℝ)..(1 - ε), 1 / log t) + ∫ t in (1 + ε)..(2 : ℝ), 1 / log t =
      ∫ u in ε..1, g u

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem pv_integral_eq_symmetric (ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1) :    (∫ t in (0 : ℝ)..(1 - ε), 1 / log t) + ∫ t in (1 + ε)..(2 : ℝ), 1 / log t =      ∫ u in ε..1, g u := by  rw [integral_sub_left ε hε hε1, integral_sub_right ε hε hε1,    ← intervalIntegral.integral_add (log_one_minus_integrable ε hε hε1)      (log_one_plus_integrable ε hε hε1)]  exact intervalIntegral.integral_congr fun u _ ↦ by    change 1 / log (1 - u) + 1 / log (1 + u) =      1 / log (1 + u) + 1 / log (1 - u)    exact add_comm _ _