awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
x : ℝ
e_a : (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ)) = cexp (↑(-x) : ℂ) * (↑x : ℂ) ^ (a - 1)
e_a₁ : (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ)) = cexp (-(↑x : ℂ)) * (↑x : ℂ) ^ (a - 1)
e_a₂ e_a₃ : cexp (-(↑x : ℂ)) * (↑x : ℂ) ^ (a - 1) = cexp (-(↑x : ℂ)) * (↑x : ℂ) ^ (a - 1)
⊢ (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ)) = (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (a - 1)

Tactic:
rw [ofReal_exp, ofReal_neg, mul_comm]

Premises used: Complex.ofReal_neg, Complex.ofReal_exp, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
_ :
  Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ))))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑t : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ))))
_₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑t : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ)))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
_₂ :
  (1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))) =
    1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
_₃ :
  (1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))) =
    (1 / (↑r : ℂ)) ^ a * Gamma a
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ)))) =
    (1 / (↑r : ℂ)) ^ a * Gamma a

Tactic:
calc
    _ = ∫ (t : ℝ) in Ioi 0, (1 / r) ^ (a - 1) * (r * t) ^ (a - 1) * exp (-(r * t)) := by
      refine MeasureTheory.setIntegral_congr_fun measurableSet_Ioi (fun x hx ↦ ?_)
      rw [mem_Ioi] at hx
      rw [mul_cpow_ofReal_nonneg hr.le hx.le, ← mul_assoc, one_div, ← ofReal_inv,
        ← mul_cpow_ofReal_nonneg (inv_pos.mpr hr).le hr.le, ← ofReal_mul r⁻¹,
        inv_mul_cancel₀ hr.ne', ofReal_one, one_cpow, one_mul]
    _ = 1 / r * ∫ (t : ℝ) in Ioi 0, (1 / r) ^ (a - 1) * t ^ (a - 1) * exp (-t) := by
      simp_rw [← ofReal_mul]
      rw [integral_comp_mul_left_Ioi (fun x ↦ _ * x ^ (a - 1) * exp (-x)) _ hr, mul_zero,
        real_smul, ← one_div, ofReal_div, ofReal_one]
    _ = 1 / r * (1 / r : ℂ) ^ (a - 1) * (∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * exp (-t)) := by
      simp_rw [← MeasureTheory.integral_const_mul, mul_assoc]
    _ = (1 / r) ^ a * Gamma a := by
      rw [aux, Gamma_eq_integral ha]
      congr 2 with x
      rw [ofReal_exp, ofReal_neg, mul_comm]

Premises used: Set.Ioi, HMul.hMul, HSub.hSub, MeasureTheory.Measure.restrict, Complex.Gamma, HDiv.hDiv, Complex.ofReal, HPow.hPow, MeasureTheory.MeasureSpace.volume, MeasureTheory.integral, Complex.exp, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : 0 < s
rw :
  (Complex.Gamma (↑s : ℂ)).re =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ (s - 1)
rw₁ :
  (↑s : ℂ).GammaIntegral.re =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ (s - 1)
rw₂ :
  (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
            rexp (-x) * x ^ (s - 1)) :
        ℂ).re =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ (s - 1)
rw₃ rw₄ :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ (s - 1))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ (s - 1))
⊢ Gamma s =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ (s - 1)

Tactic:
rw [Gamma, Complex.Gamma_eq_integral (RCLike.ofReal_pos.mp hs), Complex.GammaIntegral_ofReal,
    Complex.ofReal_re]

Premises used: Complex.GammaIntegral_ofReal, Real.Gamma, RCLike.ofReal_pos, Iff.mp, Complex.ofReal_re, Complex.Gamma_eq_integral
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : s ≠ 0
h2 : (↑s : ℂ) ≠ 0
⊢ (Complex.Gamma (↑(s + 1) : ℂ)).re = s * (Complex.Gamma (↑s : ℂ)).re

Tactic:
rw [Complex.ofReal_add, Complex.ofReal_one, Complex.Gamma_add_one, Complex.re_ofReal_mul]

Premises used: Complex.Gamma_add_one, Complex.ofReal_add, Complex.ofReal_one, Complex.re_ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs h2 h2₁ h2₂ h2₃ : s ≠ 0
⊢ (↑s : ℂ) ≠ 0

Tactic:
rwa [Complex.ofReal_ne_zero]

Premises used: Complex.ofReal_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
rw : (Complex.Gamma (↑1 : ℂ)).re = 1
rw₁ : (Complex.Gamma 1).re = 1
rw₂ : Complex.re 1 = 1
rw₃ rw₄ : Eq (α := ℝ) 1 1
⊢ Gamma 1 = 1

Tactic:
rw [Gamma, Complex.ofReal_one, Complex.Gamma_one, Complex.one_re]

Premises used: Complex.Gamma_one, Complex.ofReal_one, Real.Gamma, Complex.one_re
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
rw : Complex.Gamma (↑s : ℂ) = (↑(Complex.Gamma (↑s : ℂ)).re : ℂ)
rw₁ : (↑(Complex.Gamma (↑s : ℂ)).re : ℂ) = Complex.Gamma (↑s : ℂ)
rw₂ : (starRingEnd ℂ : (a : ℂ) → ℂ) (Complex.Gamma (↑s : ℂ)) = Complex.Gamma (↑s : ℂ)
rw₃ : Complex.Gamma ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑s : ℂ)) = Complex.Gamma (↑s : ℂ)
rw₄ rw₅ : Complex.Gamma (↑s : ℂ) = Complex.Gamma (↑s : ℂ)
⊢ Complex.Gamma (↑s : ℂ) = (↑(Gamma s) : ℂ)

Tactic:
rw [Gamma, eq_comm, ← Complex.conj_eq_iff_re, ← Complex.Gamma_conj, Complex.conj_ofReal]

Premises used: Complex.Gamma_conj, Complex.conj_eq_iff_re, eq_comm, Real.Gamma, Complex.conj_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
rw : (Complex.Gamma (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ)).re = (↑n ! : ℝ)
rw₁ : (Complex.Gamma ((↑(↑n : ℝ) : ℂ) + (↑1 : ℂ))).re = (↑n ! : ℝ)
rw₂ : (Complex.Gamma ((↑n : ℂ) + (↑1 : ℂ))).re = (↑n ! : ℝ)
rw₃ : (Complex.Gamma (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)).re = (↑n ! : ℝ)
rw₄ : Complex.re (↑n ! : ℂ) = (↑n ! : ℝ)
rw₅ : (↑(↑n ! : ℝ) : ℂ).re = (↑n ! : ℝ)
rw₆ rw₇ : Eq (α := ℝ) (↑n ! : ℝ) (↑n ! : ℝ)
⊢ Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ)

Tactic:
rw [Gamma, Complex.ofReal_add, Complex.ofReal_natCast, Complex.ofReal_one,
    Complex.Gamma_nat_eq_factorial, ← Complex.ofReal_natCast, Complex.ofReal_re]

Premises used: Complex.Gamma_nat_eq_factorial, Complex.ofReal_add, Complex.ofReal_one, Real.Gamma, Complex.ofReal_natCast, Complex.ofReal_re
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
inst : (n + 1).AtLeastTwo
⊢ Gamma (OfNat.ofNat (n + 1)) = (↑n ! : ℝ)

Tactic:
mod_cast Gamma_nat_eq_factorial (n : ℕ)

Premises used: congrArg, Nat.cast_add._simp_1, cast, Nat.cast, HAdd.hAdd, Nat.factorial, Real.Gamma, congrFun', OfNat.ofNat, Eq.symm, Real.Gamma_nat_eq_factorial, Eq, Nat.cast_one, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
⊢ Gamma 0 = 0

Tactic:
simpa only [← Complex.ofReal_zero, Complex.Gamma_ofReal, Complex.ofReal_inj] using
    Complex.Gamma_zero

Premises used: Complex.ofReal_zero, Complex.ofReal_inj, Complex.Gamma_zero, Complex.Gamma_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
⊢ Gamma (-(↑n : ℝ)) = 0

Tactic:
simpa only [← Complex.ofReal_natCast, ← Complex.ofReal_neg, Complex.Gamma_ofReal,
    Complex.ofReal_eq_zero] using Complex.Gamma_neg_nat_eq_zero n

Premises used: Complex.Gamma_neg_nat_eq_zero, Complex.ofReal_neg, Complex.ofReal_eq_zero, Complex.ofReal_natCast, Complex.Gamma_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : 0 < s
rw :
  LT.lt (α := ℝ) 0
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ (s - 1))
⊢ 0 < Gamma s

Tactic:
rw [Gamma_eq_integral hs]

Premises used: Real.Gamma_eq_integral
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : 0 < s
rw : Subset (α := Set ℝ) (Ioi 0) (Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1))
⊢ Eq (α := Set ℝ) ((Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0) (Ioi 0)

Tactic:
rw [inter_eq_right]

Premises used: Set.inter_eq_right
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : 0 < s
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ rexp (-x) * x ^ (s - 1) ≠ 0

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

Premises used: Real.rpow_pos_of_pos, LT.lt.ne', mul_ne_zero, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : 0 < s
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ rexp (-x) * x ^ (s - 1) ≠ 0

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

Premises used: Real.rpow_pos_of_pos, LT.lt.ne', mul_ne_zero, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : 0 < s
⊢ Eq (α := Set ℝ) ((Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0) (Ioi 0)

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'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : 0 < s
this : Eq (α := Set ℝ) ((Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0) (Ioi 0)
rw :
  LT.lt (α := ENNReal) (0 : ENNReal)
    ((volume : (a : Set ℝ) → ENNReal) ((Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0) :
      ENNReal)
hf :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)
hfi :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Ioi 0) volume
⊢ LT.lt (α := ℝ) 0
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ (s - 1))

Tactic:
rw [setIntegral_pos_iff_support_of_nonneg_ae]

Premises used: MeasureTheory.setIntegral_pos_iff_support_of_nonneg_ae
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : 0 < s
this : Eq (α := Set ℝ) ((Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0) (Ioi 0)
rw : ENNReal.ofReal 0 < ⊤
⊢ LT.lt (α := ENNReal) (0 : ENNReal)
    ((volume : (a : Set ℝ) → ENNReal) ((Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0) :
      ENNReal)

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

Premises used: ENNReal.ofReal_zero, Real.volume_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : 0 < s
this : Eq (α := Set ℝ) ((Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0) (Ioi 0)
⊢ ENNReal.ofReal 0 < ⊤

Tactic:
ENNReal.ofReal_lt_top

Premises used: ENNReal.ofReal_lt_top
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : 0 < s
this : Eq (α := Set ℝ) ((Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0) (Ioi 0)
⊢ ENNReal.ofReal 0 < ⊤

Tactic:
exact ENNReal.ofReal_lt_top

Premises used: ENNReal.ofReal_lt_top
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : 0 < s
this : Eq (α := Set ℝ) ((Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0) (Ioi 0)
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)

Tactic:
eventually_of_mem (self_mem_ae_restrict measurableSet_Ioi) ?_

Premises used: measurableSet_Ioi, Filter.eventually_of_mem, Filter.EventuallyLE, MeasureTheory.self_mem_ae_restrict
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : 0 < s
this : Eq (α := Set ℝ) ((Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0) (Ioi 0)
hf : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → LE.le (α := ℝ) (0 x) ((fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) x)
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)

Tactic:
refine eventually_of_mem (self_mem_ae_restrict measurableSet_Ioi) ?_

Premises used: measurableSet_Ioi, Filter.eventually_of_mem, MeasureTheory.self_mem_ae_restrict
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : 0 < s
this : Eq (α := Set ℝ) ((Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0) (Ioi 0)
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → LE.le (α := ℝ) (0 x) ((fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) x)

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

Premises used: Real.rpow_pos_of_pos, HSub.hSub, LT.lt.le, mul_pos, OfNat.ofNat, Neg.neg, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : 0 < s
this : Eq (α := Set ℝ) ((Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0) (Ioi 0)
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → LE.le (α := ℝ) (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

Premises used: Real.rpow_pos_of_pos, LT.lt.le, mul_pos, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : 0 < s
this : Eq (α := Set ℝ) ((Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0) (Ioi 0)
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Ioi 0) volume

Tactic:
GammaIntegral_convergent hs

Premises used: Real.GammaIntegral_convergent
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : 0 < s
this : Eq (α := Set ℝ) ((Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0) (Ioi 0)
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Ioi 0) volume

Tactic:
exact GammaIntegral_convergent hs

Premises used: Real.GammaIntegral_convergent
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : 0 ≤ s
inl : ∀ (hs : LE.le (α := ℝ) 0 0), 0 ≤ Gamma 0
inr : ∀ (h : 0 < s), 0 ≤ Gamma s
⊢ 0 ≤ Gamma s

Tactic:
obtain rfl | h := eq_or_lt_of_le hs

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
hs inl inl₁ : LE.le (α := ℝ) 0 0
⊢ 0 ≤ Gamma 0

Tactic:
rw [Gamma_zero]

Premises used: Real.Gamma_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : 0 ≤ s
h : 0 < s
⊢ 0 ≤ Gamma s

Tactic:
(Gamma_pos_of_pos h).le

Premises used: Real.Gamma_pos_of_pos, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : 0 ≤ s
h : 0 < s
⊢ 0 ≤ Gamma s

Tactic:
exact (Gamma_pos_of_pos h).le

Premises used: Real.Gamma_pos_of_pos, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ 0 ≤ 1 / r

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
rw :
  (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          t ^ (a - 1) * rexp (-(r * t))) :
      ℂ) =
    ((↑1 : ℂ) / (↑r : ℂ)) ^ (↑a : ℂ) * Complex.Gamma (↑a : ℂ)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (a - 1) * rexp (-(r * t))) =
    (1 / r) ^ a * Gamma a

Tactic:
rw [← ofReal_inj, ofReal_mul, ← Gamma_ofReal, ofReal_cpow (by positivity), ofReal_div]

Premises used: Complex.ofReal_cpow, Complex.ofReal_div, Complex.ofReal_inj, Complex.Gamma_ofReal, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
rwa rwa₁ rwa₂ rwa₃ : 0 < a
⊢ 0 < (↑a : ℂ).re

Tactic:
rwa [ofReal_re]

Premises used: Complex.ofReal_re
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
h :
  (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          t ^ (a - 1) * rexp (-(r * t))) :
      ℂ) =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ ((↑a : ℂ) - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ)))
⊢ (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          t ^ (a - 1) * rexp (-(r * t))) :
      ℂ) =
    ((↑1 : ℂ) / (↑r : ℂ)) ^ (↑a : ℂ) * Complex.Gamma (↑a : ℂ)

Tactic:
convert! integral_cpow_mul_exp_neg_mul_Ioi (by rwa [ofReal_re] : 0 < (a : ℂ).re) hr

Premises used: Complex.integral_cpow_mul_exp_neg_mul_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          t ^ (a - 1) * rexp (-(r * t))) :
      ℂ) =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ ((↑a : ℂ) - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ)))

Tactic:
integral_ofReal.symm.trans <| setIntegral_congr_fun measurableSet_Ioi (fun t ht ↦ ?_)

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun, integral_ofReal, Eq.symm, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
h :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
    (↑(t ^ (a - 1) * rexp (-(r * t))) : ℂ) = (↑t : ℂ) ^ ((↑a : ℂ) - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ)))
⊢ (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          t ^ (a - 1) * rexp (-(r * t))) :
      ℂ) =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ ((↑a : ℂ) - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ)))

Tactic:
refine integral_ofReal.symm.trans <| setIntegral_congr_fun measurableSet_Ioi (fun t ht ↦ ?_)

Premises used: intervalIntegral.integral_ofReal, measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun, Eq.symm, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
h : (↑(t ^ (a - 1) * rexp (-(r * t))) : ℂ) = (↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑(rexp (-(r * t))) : ℂ)
⊢ (↑(t ^ (a - 1) * rexp (-(r * t))) : ℂ) = (↑t : ℂ) ^ ((↑a : ℂ) - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ)))

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
h : (↑(t ^ (a - 1) * rexp (-(r * t))) : ℂ) = (↑(t ^ (a - 1)) : ℂ) * (↑(rexp (-(r * t))) : ℂ)
h₁ : HMul.hMul (α := ℂ) (↑(t ^ (a - 1)) : ℂ) (↑(rexp (-(r * t))) : ℂ) = (↑(t ^ (a - 1)) : ℂ) * (↑(rexp (-(r * t))) : ℂ)
⊢ (↑(t ^ (a - 1) * rexp (-(r * t))) : ℂ) = (↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑(rexp (-(r * t))) : ℂ)

Tactic:
simp_rw [← ofReal_cpow ht.le, RCLike.ofReal_mul, coe_algebraMap]

Premises used: Complex.ofReal_cpow, RCLike.ofReal_mul, LT.lt.le, Complex.coe_algebraMap
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
this : ∀ {n : ℕ}, -(↑n : ℝ) < s → Gamma s ≠ 0
a : -(↑(⌊-s⌋₊ + 1) : ℝ) < s
n : ℕ
⊢ Gamma s ≠ 0

Tactic:
apply this
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
this : ∀ {n : ℕ}, -(↑n : ℝ) < s → Gamma s ≠ 0
⊢ ℕ

Tactic:
exact ⌊-s⌋₊ + 1
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
this : ∀ {n : ℕ}, -(↑n : ℝ) < s → Gamma s ≠ 0
a : -s < HAdd.hAdd (α := ℝ) (↑⌊-s⌋₊ : ℝ) 1
⊢ -(↑(⌊-s⌋₊ + 1) : ℝ) < s

Tactic:
rw [neg_lt, Nat.cast_add, Nat.cast_one]

Premises used: Nat.cast_add, neg_lt, Nat.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
this : ∀ {n : ℕ}, -(↑n : ℝ) < s → Gamma s ≠ 0
⊢ -s < HAdd.hAdd (α := ℝ) (↑⌊-s⌋₊ : ℝ) 1

Tactic:
Nat.lt_floor_add_one _

Premises used: Nat.lt_floor_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
this : ∀ {n : ℕ}, -(↑n : ℝ) < s → Gamma s ≠ 0
⊢ -s < HAdd.hAdd (α := ℝ) (↑⌊-s⌋₊ : ℝ) 1

Tactic:
exact Nat.lt_floor_add_one _

Premises used: Nat.lt_floor_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
suffices : ∀ {n : ℕ}, -(↑n : ℝ) < s → Gamma s ≠ 0
⊢ Gamma s ≠ 0

Tactic:
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 _
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs_1 : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
hs : -(↑0 : ℝ) < s
⊢ Gamma s ≠ 0

Tactic:
(Gamma_pos_of_pos ?_).ne'

Premises used: Real.Gamma_pos_of_pos, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs_1 : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
hs : -(↑0 : ℝ) < s
zero : 0 < s
⊢ Gamma s ≠ 0

Tactic:
refine (Gamma_pos_of_pos ?_).ne'

Premises used: Real.Gamma_pos_of_pos, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
hs_1 : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
hs : -(↑0 : ℝ) < s
zero : ∀ (hs : -0 < s), 0 < s
zero₁ zero₂ zero₃ zero₄ : ∀ (hs : 0 < s), 0 < s
⊢ 0 < s

Tactic:
rwa [Nat.cast_zero, neg_zero] at hs

Premises used: Nat.cast_zero, neg_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
hs' : -(↑(n + 1) : ℝ) < s
hs₁ : ∀ (m : ℕ), s + 1 ≠ -(↑m : ℝ)
a : -(↑n : ℝ) < s + 1
⊢ Gamma (s + 1) ≠ 0

Tactic:
apply n_ih
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
hs' : -(↑(n + 1) : ℝ) < s
m : ℕ
⊢ s ≠ -(↑(1 + m) : ℝ)

Tactic:
specialize hs (1 + m)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0
s : ℝ
hs' : -(↑(n + 1) : ℝ) < s
m : ℕ
hs : s ≠ -(↑(1 + m) : ℝ)
hs₁ : ∀ (hs : s + 1 = -(↑m : ℝ)), s = -(↑(1 + m) : ℝ)
⊢ s + 1 ≠ -(↑m : ℝ)

Tactic:
contrapose hs
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0
s : ℝ
hs' : -(↑(n + 1) : ℝ) < s
m : ℕ
hs : s + 1 = -(↑m : ℝ)
⊢ s = HSub.hSub (α := ℝ) (-(↑m : ℝ)) 1

Tactic:
rw [← eq_sub_iff_add_eq] at hs

Premises used: eq_sub_iff_add_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0
s : ℝ
hs' : -(↑(n + 1) : ℝ) < s
m : ℕ
hs : s = HSub.hSub (α := ℝ) (-(↑m : ℝ)) 1
hs₁ : HSub.hSub (α := ℝ) (-(↑m : ℝ)) 1 = -(↑(1 + m) : ℝ)
⊢ s = -(↑(1 + m) : ℝ)

Tactic:
rw [hs]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0
s : ℝ
hs' : -(↑(n + 1) : ℝ) < s
m : ℕ
hs : s = HSub.hSub (α := ℝ) (-(↑m : ℝ)) 1
hs₁ : HSub.hSub (α := ℝ) (-(↑m : ℝ)) 1 = -HAdd.hAdd (α := ℝ) 1 (↑m : ℝ)
⊢ HSub.hSub (α := ℝ) (-(↑m : ℝ)) 1 = -(↑(1 + m) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0
s : ℝ
hs' : -(↑(n + 1) : ℝ) < s
m : ℕ
hs : s = HSub.hSub (α := ℝ) (-(↑m : ℝ)) 1
⊢ HSub.hSub (α := ℝ) (-(↑m : ℝ)) 1 = -HAdd.hAdd (α := ℝ) 1 (↑m : ℝ)

Tactic:
ring