GammaAux_recurrence2 — Mathlib

English

For n ∈ ℕ, Γ(-n) = 0.

Русский

Для натурального n, Γ(-n) = 0.

LaTeX

$$$$ \Gamma(-n) = 0, \quad n \in \mathbb{N}. $$$$

Lean4

theorem GammaAux_recurrence2 (s : ℂ) (n : ℕ) (h1 : -s.re < ↑n) : GammaAux n s = GammaAux (n + 1) s :=
  by
  rcases n with - | n
  · simp only [CharP.cast_eq_zero, Left.neg_neg_iff] at h1
    dsimp only [GammaAux]
    rw [GammaIntegral_add_one h1, mul_div_cancel_left₀]
    rintro rfl
    rw [zero_re] at h1
    exact h1.false
  · dsimp only [GammaAux]
    have : GammaAux n (s + 1 + 1) / (s + 1) = GammaAux n (s + 1) :=
      by
      have hh1 : -(s + 1).re < n := by
        rw [Nat.cast_add, Nat.cast_one] at h1
        rw [add_re, one_re]; linarith
      rw [GammaAux_recurrence1 (s + 1) n hh1]
    rw [this]

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