Source indexedlemma · leanprover/lean4:v4.32.0

ZetaSum_aux1_2

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:793 to 803

Mathematical statement

Exact Lean statement

lemma ZetaSum_aux1_2 {a b : ℝ} {c : ℝ} (apos : 0 < a) (a_lt_b : a < b)
    (h : c ≠ 0 ∧ 0 ∉ [[a, b]]) :
    ∫ (x : ℝ) in a..b, 1 / x ^ (c+1) = (a ^ (-c) - b ^ (-c)) / c

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma ZetaSum_aux1_2 {a b : ℝ} {c : ℝ} (apos : 0 < a) (a_lt_b : a < b)    (h : c ≠ 0 ∧ 0 ∉ [[a, b]]) :    ∫ (x : ℝ) in a..b, 1 / x ^ (c+1) = (a ^ (-c) - b ^ (-c)) / c := by  rw [(by ring : (a ^ (-c) - b ^ (-c)) / c = (b ^ (-c) - a ^ (-c)) / (-c))]  have := integral_rpow (a := a) (b := b) (r := -c-1) (Or.inr ⟨by simp [h.1], h.2⟩)  simp only [sub_add_cancel] at this  rw [← this]  apply intervalIntegral.integral_congr  intro x hx  have : 0 ≤ x := (ZetaSum_aux1_1 apos a_lt_b hx).le  simp [div_rpow_eq_rpow_neg _ _ _ this, sub_eq_add_neg, add_comm]