Gamma_pos_of_pos — Mathlib

English

If s > 0, then Γ(s) > 0.

Русский

Если s > 0, то Γ(s) > 0.

LaTeX

$$$s>0 \Rightarrow \Gamma(s) > 0$$$

Lean4

theorem Gamma_pos_of_pos {s : ℝ} (hs : 0 < s) : 0 < Gamma s :=
  by
  rw [Gamma_eq_integral hs]
  have : (Function.support fun x : ℝ => exp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0 :=
    by
    rw [inter_eq_right]
    intro x hx
    rw [Function.mem_support]
    exact mul_ne_zero (exp_pos _).ne' (rpow_pos_of_pos hx _).ne'
  rw [setIntegral_pos_iff_support_of_nonneg_ae]
  · rw [this, volume_Ioi, ← ENNReal.ofReal_zero]
    exact ENNReal.ofReal_lt_top
  · refine eventually_of_mem (self_mem_ae_restrict measurableSet_Ioi) ?_
    exact fun x hx => (mul_pos (exp_pos _) (rpow_pos_of_pos hx _)).le
  · exact GammaIntegral_convergent hs

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