-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem Gamma_integrand_deriv_integrable_B {s : ℂ} (hs : 0 < s.re) {Y : ℝ} (hY : 0 ≤ Y) :
    IntervalIntegrable (fun x : ℝ => (-x).exp * (s * x ^ (s - 1)) : ℝ → ℂ) volume 0 Y

Proof state:
case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ HasFiniteIntegral (fun a => ‖s * (↑(rexp (-a)) * ↑a ^ (s - 1))‖) (volume.restrict (Ioc 0 Y))

Tactic:
simp_rw [norm_mul]

Result:
case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ HasFiniteIntegral (fun a => ‖s‖ * (‖↑(rexp (-a))‖ * ‖↑a ^ (s - 1)‖)) (volume.restrict (Ioc 0 Y))

Proof state:
case left.hcont
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ ∀ x ∈ Ioc 0 Y, ContinuousAt (fun x => ↑x ^ (s - 1)) x

Tactic:
intro x hx

Result:
case left.hcont
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
x : ℝ
hx : x ∈ Ioc 0 Y
⊢ ContinuousAt (fun x => ↑x ^ (s - 1)) x

Proof state:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ IntegrableOn (fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))) (Ioc 0 Y) volume

Tactic:
constructor

Result:
case left
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ AEStronglyMeasurable (fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))) (volume.restrict (Ioc 0 Y))

case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ HasFiniteIntegral (fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))) (volume.restrict (Ioc 0 Y))

Proof state:
case left
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ ContinuousOn (fun x => ↑(rexp (-x)) * ↑x ^ (s - 1)) (Ioc 0 Y)

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

Result:
case left
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ ContinuousOn (fun x => ↑x ^ (s - 1)) (Ioc 0 Y)

Proof state:
case left.hcont
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
x : ℝ
hx : x ∈ Ioc 0 Y
⊢ ContinuousAt (fun x => ↑x ^ (s - 1)) x

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

Result:
case left.hcont
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
x : ℝ
hx : x ∈ Ioc 0 Y
⊢ ContinuousAt (fun x => x ^ (s - 1)) ↑x

Proof state:
case left
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ ContinuousOn (fun x => ↑x ^ (s - 1)) (Ioc 0 Y)

Tactic:
apply continuousOn_of_forall_continuousAt

Result:
case left.hcont
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ ∀ x ∈ Ioc 0 Y, ContinuousAt (fun x => ↑x ^ (s - 1)) x

Proof state:
case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ MeasurableSet (Ioc 0 Y)

Tactic:
exact measurableSet_Ioc

Result:
no goals

Proof state:
case right.h
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
x : ℝ
hx : x ∈ Ioc 0 Y
⊢ rexp (-x) * x ^ (s.re - 1) = ‖↑(rexp (-x))‖ * ‖↑x ^ (s - 1)‖

Tactic:
rw [Complex.norm_of_nonneg (exp_pos _).le, norm_cpow_eq_rpow_re_of_pos hx.1]

Result:
case right.h
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
x : ℝ
hx : x ∈ Ioc 0 Y
⊢ rexp (-x) * x ^ (s.re - 1) = rexp (-x) * x ^ (s - 1).re

Proof state:
case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ ∀ᵐ (x : ℝ), x ∈ Ioc 0 Y → rexp (-x) * x ^ (s.re - 1) = ‖↑(rexp (-x))‖ * ‖↑x ^ (s - 1)‖

Tactic:
filter_upwards with x hx

Result:
case right.h
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
x : ℝ
hx : x ∈ Ioc 0 Y
⊢ rexp (-x) * x ^ (s.re - 1) = ‖↑(rexp (-x))‖ * ‖↑x ^ (s - 1)‖

Proof state:
case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ (fun x => rexp (-x) * x ^ (s.re - 1)) =ᶠ[ae (volume.restrict (Ioc 0 Y))] fun a => ‖↑(rexp (-a))‖ * ‖↑a ^ (s - 1)‖

Tactic:
rw [EventuallyEq, ae_restrict_iff']

Result:
case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ ∀ᵐ (x : ℝ), x ∈ Ioc 0 Y → rexp (-x) * x ^ (s.re - 1) = ‖↑(rexp (-x))‖ * ‖↑x ^ (s - 1)‖

case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ MeasurableSet (Ioc 0 Y)

Proof state:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
⊢ (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))

Tactic:
ext1

Result:
case h
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
x✝ : ℝ
⊢ ↑(rexp (-x✝)) * (s * ↑x✝ ^ (s - 1)) = s * (↑(rexp (-x✝)) * ↑x✝ ^ (s - 1))

Proof state:
case right.h
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
x : ℝ
hx : x ∈ Ioc 0 Y
⊢ rexp (-x) * x ^ (s.re - 1) = rexp (-x) * x ^ (s - 1).re

Tactic:
simp

Result:
no goals

Proof state:
case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ HasFiniteIntegral (fun a => ‖s‖ * (‖↑(rexp (-a))‖ * ‖↑a ^ (s - 1)‖)) (volume.restrict (Ioc 0 Y))

Tactic:
refine (((Real.GammaIntegral_convergent hs).mono_set
  Ioc_subset_Ioi_self).hasFiniteIntegral.congr ?_).const_mul _

Result:
case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ (fun x => rexp (-x) * x ^ (s.re - 1)) =ᶠ[ae (volume.restrict (Ioc 0 Y))] fun a => ‖↑(rexp (-a))‖ * ‖↑a ^ (s - 1)‖

Proof state:
case left
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ AEStronglyMeasurable (fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))) (volume.restrict (Ioc 0 Y))

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

Result:
case left
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ ContinuousOn (fun x => ↑(rexp (-x)) * ↑x ^ (s - 1)) (Ioc 0 Y)

Proof state:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
⊢ IntervalIntegrable (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 Y

Tactic:
have : (fun x => (-x).exp * (s * x ^ (s - 1)) : ℝ → ℂ) =
    (fun x => s * ((-x).exp * x ^ (s - 1)) : ℝ → ℂ) := by ext1; ring

Result:
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ IntervalIntegrable (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 Y