Source indexedlemma · leanprover/lean4:v4.32.0

ZetaAppendix.integral_cpow_neg_eq_main

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3417 to 3430

Mathematical statement

Exact Lean statement

lemma integral_cpow_neg_eq_main {a b : ℝ} (ha : 0 < a) (hab : a < b)
    {s : ℂ} (hs1 : s ≠ 1) :
    (∫ x in a..b, (x : ℂ) ^ (-s)) =
      ((b : ℂ) ^ (1 - s) - (a : ℂ) ^ (1 - s)) / (1 - s)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma integral_cpow_neg_eq_main {a b : ℝ} (ha : 0 < a) (hab : a < b)    {s : ℂ} (hs1 : s ≠ 1) :    (∫ x in a..b, (x : ℂ) ^ (-s)) =      ((b : ℂ) ^ (1 - s) - (a : ℂ) ^ (1 - s)) / (1 - s) := by  convert integral_cpow (a := a) (b := b) (r := -s) ?_ using 1  · rw [(by ring : -s + 1 = 1 - s)]  · right    refine ⟨?_, ?_⟩    · intro hs      exact hs1 (neg_inj.mp hs)    · intro hx      have hx_pos : 0 < (0 : ℝ) := by        exact lt_of_lt_of_le ha ((Set.mem_uIcc.mp hx).elim (fun h ↦ h.1) (fun h ↦ le_trans hab.le h.1))      exact hx_pos.false