English
Further simplifications about gamma non-vanishing compatibility with real-casted expressions.
Русский
Дополнительные упрощения о несовпадении нуля гаммы с вещественным приводом.
LaTeX
$$Γ(s) ≠ 0 for generic s with conditions, reducing to basic cases$$
Lean4
/-- The Gamma function does not vanish on `ℝ` (except at non-positive integers, where the function
is mathematically undefined and we set it to `0` by convention). -/
theorem Gamma_ne_zero {s : ℝ} (hs : ∀ m : ℕ, s ≠ -m) : Gamma s ≠ 0 :=
by
suffices ∀ {n : ℕ}, -(n : ℝ) < s → Gamma s ≠ 0 by
apply this
swap
· exact ⌊-s⌋₊ + 1
rw [neg_lt, Nat.cast_add, Nat.cast_one]
exact Nat.lt_floor_add_one _
intro n
induction n generalizing s with
| zero =>
intro hs
refine (Gamma_pos_of_pos ?_).ne'
rwa [Nat.cast_zero, neg_zero] at hs
| succ _ n_ih =>
intro hs'
have : Gamma (s + 1) ≠ 0 := by
apply n_ih
· intro m
specialize hs (1 + m)
contrapose! hs
rw [← eq_sub_iff_add_eq] at hs
rw [hs]
push_cast
ring
· rw [Nat.cast_add, Nat.cast_one, neg_add] at hs'
linarith
rw [Gamma_add_one, mul_ne_zero_iff] at this
· exact this.2
· simpa using hs 0
