GammaAux_recurrence1 — Mathlib

English

For s ∈ ℂ and n ∈ ℕ with -Re(s) < n, ΓAux(n,s) = ΓAux(n+1,s).

Русский

При -Re(s) < n выполняется ΓAux(n,s) = ΓAux(n+1,s).

LaTeX

$$$$ \GammaAux(n,s) = \GammaAux(n+1, s), \quad -\operatorname{Re}(s) < n. $$$$

Lean4

theorem GammaAux_recurrence1 (s : ℂ) (n : ℕ) (h1 : -s.re < ↑n) : GammaAux n s = GammaAux n (s + 1) / s := by
  induction n generalizing s with
  | zero =>
    simp only [CharP.cast_eq_zero, Left.neg_neg_iff] at h1
    dsimp only [GammaAux]; rw [GammaIntegral_add_one h1]
    rw [mul_comm, mul_div_cancel_right₀]; contrapose! h1; rw [h1]
    simp
  | succ n hn =>
    dsimp only [GammaAux]
    have hh1 : -(s + 1).re < n := by
      rw [Nat.cast_add, Nat.cast_one] at h1
      rw [add_re, one_re]; linarith
    rw [← hn (s + 1) hh1]

Похожие утверждения