English
The Gamma function does not vanish on ℝ except at non-positive integers; at those points it is conventionally 0.
Русский
Гамма-функция не обращается в ноль на ℝ, за исключением не-положительных целых, где она по соглашению равна 0.
LaTeX
$$Γ(s) ≠ 0 unless s = -m with m ∈ ℕ; Γ(-m) = 0 in that case$$
Lean4
/-- The `positivity` extension which identifies expressions of the form `Gamma a`. -/
@[positivity Gamma (_ : ℝ)]
def _root_.Mathlib.Meta.Positivity.evalGamma : PositivityExt where
eval {u α} _zα _pα
e := do
match u, α, e with
| 0, ~q(ℝ), ~q(Gamma $a) =>
match ← core q(inferInstance) q(inferInstance) a with
| .positive pa =>
assertInstancesCommute
pure (.positive q(Gamma_pos_of_pos $pa))
| .nonnegative pa =>
assertInstancesCommute
pure (.nonnegative q(Gamma_nonneg_of_nonneg $pa))
| _ =>
pure .none
| _, _, _ =>
throwError"failed to match on Gamma application"
