-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem Gamma_pos_of_pos {s : ℝ} (hs : 0 < s) : 0 < Gamma s

Proof state:
s : ℝ
hs : 0 < s
⊢ 0 < ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)

Tactic:
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'

Result:
s : ℝ
hs : 0 < s
this : (Function.support fun x => rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0
⊢ 0 < ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)

Proof state:
case hf
s : ℝ
hs : 0 < s
this : (Function.support fun x => rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0
⊢ ∀ x ∈ Ioi 0, 0 x ≤ (fun x => rexp (-x) * x ^ (s - 1)) x

Tactic:
exact fun x hx => (mul_pos (exp_pos _) (rpow_pos_of_pos hx _)).le

Result:
no goals

Proof state:
case hf
s : ℝ
hs : 0 < s
this : (Function.support fun x => rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0
⊢ 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] fun x => rexp (-x) * x ^ (s - 1)

Tactic:
refine eventually_of_mem (self_mem_ae_restrict measurableSet_Ioi) ?_

Result:
case hf
s : ℝ
hs : 0 < s
this : (Function.support fun x => rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0
⊢ ∀ x ∈ Ioi 0, 0 x ≤ (fun x => rexp (-x) * x ^ (s - 1)) x

Proof state:
s : ℝ
hs : 0 < s
⊢ Ioi 0 ⊆ Function.support fun x => rexp (-x) * x ^ (s - 1)

Tactic:
intro x hx

Result:
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Ioi 0
⊢ x ∈ Function.support fun x => rexp (-x) * x ^ (s - 1)

Proof state:
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Ioi 0
⊢ x ∈ Function.support fun x => rexp (-x) * x ^ (s - 1)

Tactic:
rw [Function.mem_support]

Result:
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Ioi 0
⊢ rexp (-x) * x ^ (s - 1) ≠ 0

Proof state:
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Ioi 0
⊢ rexp (-x) * x ^ (s - 1) ≠ 0

Tactic:
exact mul_ne_zero (exp_pos _).ne' (rpow_pos_of_pos hx _).ne'

Result:
no goals

Proof state:
s : ℝ
hs : 0 < s
this : (Function.support fun x => rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0
⊢ ENNReal.ofReal 0 < ⊤

Tactic:
exact ENNReal.ofReal_lt_top

Result:
no goals

Proof state:
case hfi
s : ℝ
hs : 0 < s
this : (Function.support fun x => rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0
⊢ IntegrableOn (fun x => rexp (-x) * x ^ (s - 1)) (Ioi 0) volume

Tactic:
exact GammaIntegral_convergent hs

Result:
no goals

Proof state:
s : ℝ
hs : 0 < s
this : (Function.support fun x => rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0
⊢ 0 < ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)

Tactic:
rw [setIntegral_pos_iff_support_of_nonneg_ae]

Result:
s : ℝ
hs : 0 < s
this : (Function.support fun x => rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0
⊢ 0 < volume ((Function.support fun x => rexp (-x) * x ^ (s - 1)) ∩ Ioi 0)

case hf
s : ℝ
hs : 0 < s
this : (Function.support fun x => rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0
⊢ 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] fun x => rexp (-x) * x ^ (s - 1)

case hfi
s : ℝ
hs : 0 < s
this : (Function.support fun x => rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0
⊢ IntegrableOn (fun x => rexp (-x) * x ^ (s - 1)) (Ioi 0) volume

Proof state:
s : ℝ
hs : 0 < s
this : (Function.support fun x => rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0
⊢ 0 < volume ((Function.support fun x => rexp (-x) * x ^ (s - 1)) ∩ Ioi 0)

Tactic:
rw [this, volume_Ioi, ← ENNReal.ofReal_zero]

Result:
s : ℝ
hs : 0 < s
this : (Function.support fun x => rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0
⊢ ENNReal.ofReal 0 < ⊤

Proof state:
s : ℝ
hs : 0 < s
⊢ (Function.support fun x => rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0

Tactic:
rw [inter_eq_right]

Result:
s : ℝ
hs : 0 < s
⊢ Ioi 0 ⊆ Function.support fun x => rexp (-x) * x ^ (s - 1)

Proof state:
s : ℝ
hs : 0 < s
⊢ 0 < Gamma s

Tactic:
rw [Gamma_eq_integral hs]

Result:
s : ℝ
hs : 0 < s
⊢ 0 < ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)