Source indexedlemma · leanprover/lean4:v4.32.0

Complex.exp_logGammaSeq

PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.DigammaSeries · PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Gamma/DigammaSeries.lean:331 to 346

Source documentation

On the right half-plane, exp (logGammaSeq z n) = GammaSeq z n for n ≠ 0.

Exact Lean statement

lemma exp_logGammaSeq {z : ℂ} (hz : 0 < z.re) {n : ℕ} (hn : n ≠ 0) :
    exp (logGammaSeq z n) = GammaSeq z n

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma exp_logGammaSeq {z : ℂ} (hz : 0 < z.re) {n : ℕ} (hn : n ≠ 0) :    exp (logGammaSeq z n) = GammaSeq z n := by  have hne : ∀ m : ℕ, z + (m : ℂ) ≠ 0 := by    intro m h    have hpos : 0 < (z + (m : ℂ)).re := by      rw [add_re, natCast_re]      have : (0 : ℝ) ≤ m := Nat.cast_nonneg m      linarith    simp [h] at hpos  unfold logGammaSeq GammaSeq  rw [exp_sub, exp_add, exp_sum]  congr 1  · congr 1    · rw [natCast_log, cpow_def_of_ne_zero (Nat.cast_ne_zero.mpr hn), mul_comm z (log (n : ℂ))]    · rw [natCast_log, exp_log (by exact_mod_cast n.factorial_ne_zero)]  · exact Finset.prod_congr rfl fun m _ => exp_log (hne m)