awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
h : 0 < s
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Ioi 1) volume

Tactic:
integrable_of_isBigO_exp_neg one_half_pos ?_ (Gamma_integrand_isLittleO _).isBigO

Premises used: Asymptotics.IsLittleO.isBigO, one_half_pos, integrable_of_isBigO_exp_neg, Real.Gamma_integrand_isLittleO
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
h : 0 < s
right : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Ici 1)
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Ioi 1) volume

Tactic:
refine integrable_of_isBigO_exp_neg one_half_pos ?_ (Gamma_integrand_isLittleO _).isBigO

Premises used: Asymptotics.IsLittleO.isBigO, one_half_pos, integrable_of_isBigO_exp_neg, Real.Gamma_integrand_isLittleO
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
h : 0 < s
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ici 1) x → id x ≠ 0 ∨ 0 ≤ s - 1

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
h : 0 < s
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Ici 1)

Tactic:
exact continuousOn_id.neg.rexp.mul (continuousOn_id.rpow_const (by grind))

Premises used: ContinuousOn.neg, ContinuousOn.rpow_const, continuousOn_id, ContinuousOn.rexp, ContinuousOn.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
left :
  AEStronglyMeasurable (β := ℂ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) (Measure.restrict volume (Ioi 0))
right :
  @HasFiniteIntegral _ ℂ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
    (Measure.restrict volume (Ioi 0))
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
    (Ioi 0) volume

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) (Measure.restrict volume (Ioi 0))

Tactic:
ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioi

Premises used: ContinuousOn.aestronglyMeasurable, measurableSet_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
left : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) (Ioi 0)
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) (Measure.restrict volume (Ioi 0))

Tactic:
refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioi

Premises used: ContinuousOn.aestronglyMeasurable, measurableSet_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
left : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) (Ioi 0)
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) (Ioi 0)

Tactic:
apply (continuous_ofReal.comp continuous_neg.rexp).continuousOn.mul

Premises used: Continuous.rexp, Continuous.continuousOn, ContinuousNeg.continuous_neg, Continuous.comp, Complex.continuous_ofReal, ContinuousOn.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
left : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) x
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) (Ioi 0)

Tactic:
apply continuousOn_of_forall_continuousAt

Premises used: continuousOn_of_forall_continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ x ^ (s - 1)) (↑x : ℂ)

Tactic:
have : ContinuousAt (fun x : ℂ => x ^ (s - 1)) ↑x :=
      continuousAt_cpow_const <| ofReal_mem_slitPlane.2 hx
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
this : ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ x ^ (s - 1)) (↑x : ℂ)
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) x

Tactic:
ContinuousAt.comp this continuous_ofReal.continuousAt

Premises used: Continuous.continuousAt, Complex.continuous_ofReal, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
this : ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ x ^ (s - 1)) (↑x : ℂ)
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) x

Tactic:
exact ContinuousAt.comp this continuous_ofReal.continuousAt

Premises used: Continuous.continuousAt, Complex.continuous_ofReal, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
right :
  @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (a : ℝ) ↦ ‖(↑(rexp (-a)) : ℂ) * (↑a : ℂ) ^ (s - 1)‖)
    (Measure.restrict volume (Ioi 0))
⊢ @HasFiniteIntegral _ ℂ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
    (Measure.restrict volume (Ioi 0))

Tactic:
rw [← hasFiniteIntegral_norm_iff]

Premises used: MeasureTheory.hasFiniteIntegral_norm_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (a : ℝ) ↦ ‖(↑(rexp (-a)) : ℂ) * (↑a : ℂ) ^ (s - 1)‖)
    (Measure.restrict volume (Ioi 0))

Tactic:
HasFiniteIntegral.congr (Real.GammaIntegral_convergent hs).2 ?_

Premises used: Real.GammaIntegral_convergent, And.right, MeasureTheory.HasFiniteIntegral.congr
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
right :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ)
    (fun (x : ℝ) ↦ rexp (-x) * x ^ (s.re - 1)) fun (a : ℝ) ↦ ‖(↑(rexp (-a)) : ℂ) * (↑a : ℂ) ^ (s - 1)‖
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (a : ℝ) ↦ ‖(↑(rexp (-a)) : ℂ) * (↑a : ℂ) ^ (s - 1)‖)
    (Measure.restrict volume (Ioi 0))

Tactic:
refine HasFiniteIntegral.congr (Real.GammaIntegral_convergent hs).2 ?_

Premises used: Real.GammaIntegral_convergent, And.right, MeasureTheory.HasFiniteIntegral.congr
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
right :
  ∀ᵐ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Eq (α := ℝ) ((fun (x : ℝ) ↦ rexp (-x) * x ^ (s.re - 1)) x)
        ((fun (a : ℝ) ↦ ‖(↑(rexp (-a)) : ℂ) * (↑a : ℂ) ^ (s - 1)‖) x)
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ)
    (fun (x : ℝ) ↦ rexp (-x) * x ^ (s.re - 1)) fun (a : ℝ) ↦ ‖(↑(rexp (-a)) : ℂ) * (↑a : ℂ) ^ (s - 1)‖

Tactic:
apply (ae_restrict_iff' measurableSet_Ioi).mpr

Premises used: Iff.mpr, measurableSet_Ioi, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
right :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
    rexp (-x) * x ^ (s.re - 1) = ‖(↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)‖
⊢ ∀ᵐ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Eq (α := ℝ) ((fun (x : ℝ) ↦ rexp (-x) * x ^ (s.re - 1)) x)
        ((fun (a : ℝ) ↦ ‖(↑(rexp (-a)) : ℂ) * (↑a : ℂ) ^ (s - 1)‖) x)

Tactic:
filter_upwards with x hx
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
right : rexp (-x) * x ^ (s.re - 1) = rexp (-x) * x ^ (s - 1).re
⊢ rexp (-x) * x ^ (s.re - 1) = ‖(↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)‖

Tactic:
rw [norm_mul, Complex.norm_of_nonneg <| le_of_lt <| exp_pos <| -x,
      norm_cpow_eq_rpow_re_of_pos hx _]

Premises used: le_of_lt, norm_mul, Complex.norm_of_nonneg, Complex.norm_cpow_eq_rpow_re_of_pos, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ rexp (-x) * x ^ (s.re - 1) = rexp (-x) * x ^ (s - 1).re

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
rw :
  Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
⊢ GammaIntegral ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) s.GammaIntegral

Tactic:
rw [GammaIntegral, GammaIntegral, ← integral_conj]

Premises used: Complex.GammaIntegral, integral_conj
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))

Tactic:
setIntegral_congr_fun measurableSet_Ioi fun x hx => ?_

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
refine :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
    (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) =
      (starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi fun x hx => ?_

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
⊢ ∀ (r : ℝ), (↑r : ℂ) = (↑r : ℂ)

Tactic:
have : ∀ r : ℝ, Complex.ofReal r = @RCLike.ofReal ℂ _ r := fun r => rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
this : ∀ (r : ℝ), (↑r : ℂ) = (↑r : ℂ)
rw :
  @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)) :
    ℂ)

Tactic:
rw [this, ← _root_.integral_ofReal]

Premises used: integral_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
this : ∀ (r : ℝ), (↑r : ℂ) = (↑r : ℂ)
conv_rhs :
  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)) : ℂ))
⊢ (@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)) :
      ℂ)

Tactic:
conv_rhs => rw [this, ← _root_.integral_ofReal]

Premises used: integral_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
this : ∀ (r : ℝ), (↑r : ℂ) = (↑r : ℂ)
⊢ 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)) : ℂ))

Tactic:
setIntegral_congr_fun measurableSet_Ioi ?_

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
this : ∀ (r : ℝ), (↑r : ℂ) = (↑r : ℂ)
refine :
  EqOn (β := ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ ((↑s : ℂ) - 1))
    (fun (x : ℝ) ↦ (↑(rexp (-x) * x ^ (s - 1)) : ℂ)) (Ioi 0)
⊢ 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)) : ℂ))

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi ?_

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
this : ∀ (r : ℝ), (↑r : ℂ) = (↑r : ℂ)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw : (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ ((↑s : ℂ) - 1) = (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (↑(s - 1) : ℂ)
⊢ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ ((↑s : ℂ) - 1) = (↑(rexp (-x) * x ^ (s - 1)) : ℂ)

Tactic:
rw [ofReal_mul, ofReal_cpow (mem_Ioi.mp hx).le]

Premises used: Complex.ofReal_cpow, Set.mem_Ioi, LT.lt.le, Iff.mp, Complex.ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℝ
this : ∀ (r : ℝ), (↑r : ℂ) = (↑r : ℂ)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ ((↑s : ℂ) - 1) = (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (↑(s - 1) : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
⊢ GammaIntegral 1 = 1

Tactic:
simpa only [← ofReal_one, GammaIntegral_ofReal, ofReal_inj, sub_self, rpow_zero,
    mul_one] using integral_exp_neg_Ioi_zero

Premises used: sub_self, Complex.GammaIntegral_ofReal, Real.rpow_zero, Complex.ofReal_one, Complex.ofReal_inj, mul_one, integral_exp_neg_Ioi_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun (X : ℝ) ↦ s.partialGamma X) atTop (𝓝 s.GammaIntegral)

Tactic:
intervalIntegral_tendsto_integral_Ioi 0 (GammaIntegral_convergent hs) tendsto_id

Premises used: Filter.tendsto_id, Complex.GammaIntegral, MeasureTheory.intervalIntegral_tendsto_integral_Ioi, OfNat.ofNat, Complex.GammaIntegral_convergent, Complex.partialGamma
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
X : ℝ
hs : 0 < s.re
hX : 0 ≤ X
rw :
  IntegrableOn (ε := ℂ) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) (Ioc 0 X)
    volume
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) volume 0 X

Tactic:
rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hX]

Premises used: intervalIntegrable_iff_integrableOn_Ioc_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
X : ℝ
hs : 0 < s.re
hX : 0 ≤ X
⊢ IntegrableOn (ε := ℂ) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) (Ioc 0 X)
    volume

Tactic:
IntegrableOn.mono_set (GammaIntegral_convergent hs) Ioc_subset_Ioi_self

Premises used: Set.Ioc_subset_Ioi_self, MeasureTheory.IntegrableOn.mono_set, Complex.GammaIntegral_convergent
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
X : ℝ
hs : 0 < s.re
hX : 0 ≤ X
⊢ IntegrableOn (ε := ℂ) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) (Ioc 0 X)
    volume

Tactic:
exact IntegrableOn.mono_set (GammaIntegral_convergent hs) Ioc_subset_Ioi_self

Premises used: Set.Ioc_subset_Ioi_self, MeasureTheory.IntegrableOn.mono_set, Complex.GammaIntegral_convergent
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
⊢ IntervalIntegrable (ε := ℂ) (-fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s + 1 - 1)) volume 0 X

Tactic:
(Gamma_integrand_intervalIntegrable (s + 1) _ hX).neg

Premises used: IntervalIntegrable.neg, HAdd.hAdd, _private.0.Complex.Gamma_integrand_intervalIntegrable, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
h : ∀ (x : ℝ), -((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s) = (-fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s + 1 - 1)) x
convert! : 0 < (s + 1).re
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ -((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s)) volume 0 X

Tactic:
convert! (Gamma_integrand_intervalIntegrable (s + 1) _ hX).neg

Premises used: IntervalIntegrable.neg, HAdd.hAdd, _private.0.Complex.Gamma_integrand_intervalIntegrable, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x : ℝ
h : -(cexp (-(↑x : ℂ)) * (↑x : ℂ) ^ s) = (-fun (x : ℝ) ↦ cexp (-(↑x : ℂ)) * (↑x : ℂ) ^ s) x
⊢ -((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s) = (-fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s + 1 - 1)) x

Tactic:
simp only [ofReal_exp, ofReal_neg, add_sub_cancel_right]

Premises used: Complex.ofReal_neg, Complex.ofReal_exp, add_sub_cancel_right
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x : ℝ
⊢ -(cexp (-(↑x : ℂ)) * (↑x : ℂ) ^ s) = (-fun (x : ℝ) ↦ cexp (-(↑x : ℂ)) * (↑x : ℂ) ^ s) x

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
linarith : s.re + 1 ≤ 0 → -1 + (0 - s.re) + (s.re + 1 - 0) = 0
⊢ 0 < s.re + 1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
h : ∀ (x : ℝ), (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1)) = s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
⊢ Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))

Tactic:
ext1
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
x : ℝ
⊢ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1)) = s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
⊢ Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))

Tactic:
have : (fun x => (-x).exp * (s * x ^ (s - 1)) : ℝ → ℂ) =
      (fun x => s * ((-x).exp * x ^ (s - 1)) : ℝ → ℂ) := by ext1; ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this :
  Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
rw :
  IntegrableOn (ε := ℂ) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
    (Ioc 0 Y) volume
⊢ IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) volume 0 Y

Tactic:
rw [this, intervalIntegrable_iff_integrableOn_Ioc_of_le hY]

Premises used: intervalIntegrable_iff_integrableOn_Ioc_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this :
  Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
left :
  AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace)
    (fun (x : ℝ) ↦ s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))) (Measure.restrict volume (Ioc 0 Y))
right :
  @HasFiniteIntegral _ ℂ _ Real.measurableSpace (fun (x : ℝ) ↦ s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
    (Measure.restrict volume (Ioc 0 Y))
⊢ IntegrableOn (ε := ℂ) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
    (Ioc 0 Y) volume

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this :
  Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace)
    (fun (x : ℝ) ↦ s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))) (Measure.restrict volume (Ioc 0 Y))

Tactic:
(continuousOn_const.mul ?_).aestronglyMeasurable measurableSet_Ioc

Premises used: continuousOn_const, ContinuousOn.aestronglyMeasurable, measurableSet_Ioc, ContinuousOn.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this :
  Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
left : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) (Ioc 0 Y)
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace)
    (fun (x : ℝ) ↦ s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))) (Measure.restrict volume (Ioc 0 Y))

Tactic:
refine (continuousOn_const.mul ?_).aestronglyMeasurable measurableSet_Ioc

Premises used: continuousOn_const, ContinuousOn.aestronglyMeasurable, measurableSet_Ioc, ContinuousOn.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this :
  Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
left : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) (Ioc 0 Y)
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) (Ioc 0 Y)

Tactic:
apply (continuous_ofReal.comp continuous_neg.rexp).continuousOn.mul

Premises used: Continuous.rexp, Continuous.continuousOn, ContinuousNeg.continuous_neg, Continuous.comp, Complex.continuous_ofReal, ContinuousOn.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this :
  Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
left : ∀ x ∈ Ioc 0 Y, ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) x
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) (Ioc 0 Y)

Tactic:
apply continuousOn_of_forall_continuousAt

Premises used: continuousOn_of_forall_continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this :
  Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
x : ℝ
hx : x ∈ Ioc 0 Y
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) x

Tactic:
(?_ : ContinuousAt (fun x : ℂ => x ^ (s - 1)) _).comp continuous_ofReal.continuousAt

Premises used: Continuous.continuousAt, Complex.continuous_ofReal, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this :
  Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
x : ℝ
hx : x ∈ Ioc 0 Y
left : ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ x ^ (s - 1)) (↑x : ℂ)
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) x

Tactic:
refine (?_ : ContinuousAt (fun x : ℂ => x ^ (s - 1)) _).comp continuous_ofReal.continuousAt

Premises used: Continuous.continuousAt, Complex.continuous_ofReal, ContinuousAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this :
  Eq (α := (x : ℝ) → ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) fun (x : ℝ) ↦
    s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
x : ℝ
hx : x ∈ Ioc 0 Y
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ x ^ (s - 1)) (↑x : ℂ)

Tactic:
continuousAt_cpow_const <| ofReal_mem_slitPlane.2 hx.1

Premises used: Iff.mpr, And.left, Complex.ofReal_mem_slitPlane, continuousAt_cpow_const