Source indexedtheorem · leanprover/lean4:v4.32.0

integral_Ioi_rpow_neg_re_sub_one

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.ImproperIntegrals · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean:58 to 69

Source documentation

∫_{1}^∞ u^{-re s - 1} = 1 / re s for 0 < re s.

Exact Lean statement

theorem integral_Ioi_rpow_neg_re_sub_one {s : ℂ} (hs : 0 < s.re) :
    ∫ u in Ioi (1 : ℝ), u ^ (-s.re - 1) = 1 / s.re

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem integral_Ioi_rpow_neg_re_sub_one {s : ℂ} (hs : 0 < s.re) :    ∫ u in Ioi (1 : ℝ), u ^ (-s.re - 1) = 1 / s.re := by  have ha : (-s.re - 1) < -1 := by linarith  have hc : 0 < (1 : ℝ) := zero_lt_one  have h := integral_Ioi_rpow_of_lt (a := (-s.re - 1)) ha (c := (1 : ℝ)) hc  have h' : ∫ u in Ioi (1 : ℝ), u ^ (-s.re - 1) = - (1 : ℝ) ^ (-s.re) / (-s.re) := by    simpa [sub_eq_add_neg, add_comm, add_left_comm, add_assoc] using h  calc    ∫ u in Ioi (1 : ℝ), u ^ (-s.re - 1)        = - (1 : ℝ) ^ (-s.re) / (-s.re) := h'    _ = - (1 : ℝ) / (-s.re) := by simp [Real.one_rpow]    _ = 1 / s.re := by simp