-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem GammaIntegral_convergent {s : ℂ} (hs : 0 < s.re) :
    IntegrableOn (fun x => (-x).exp * x ^ (s - 1) : ℝ → ℂ) (Ioi 0)

Proof state:
case right
s : ℂ
hs : 0 < s.re
⊢ HasFiniteIntegral (fun a => ‖↑(rexp (-a)) * ↑a ^ (s - 1)‖) (volume.restrict (Ioi 0))

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

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

Proof state:
case left
s : ℂ
hs : 0 < s.re
⊢ ContinuousOn (fun x => ↑x ^ (s - 1)) (Ioi 0)

Tactic:
apply continuousOn_of_forall_continuousAt

Result:
case left.hcont
s : ℂ
hs : 0 < s.re
⊢ ∀ x ∈ Ioi 0, ContinuousAt (fun x => ↑x ^ (s - 1)) x

Proof state:
case right.h
s : ℂ
hs : 0 < s.re
x : ℝ
hx : x ∈ Ioi 0
⊢ 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 _]

Result:
case right.h
s : ℂ
hs : 0 < s.re
x : ℝ
hx : x ∈ Ioi 0
⊢ rexp (-x) * x ^ (s.re - 1) = rexp (-x) * x ^ (s - 1).re

Proof state:
case right.h
s : ℂ
hs : 0 < s.re
x : ℝ
hx : x ∈ Ioi 0
⊢ rexp (-x) * x ^ (s.re - 1) = rexp (-x) * x ^ (s - 1).re

Tactic:
simp

Result:
no goals

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

Tactic:
exact ContinuousAt.comp this continuous_ofReal.continuousAt

Result:
no goals

Proof state:
case left
s : ℂ
hs : 0 < s.re
⊢ ContinuousOn (fun x => ↑(rexp (-x)) * ↑x ^ (s - 1)) (Ioi 0)

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

Result:
case left
s : ℂ
hs : 0 < s.re
⊢ ContinuousOn (fun x => ↑x ^ (s - 1)) (Ioi 0)

Proof state:
case left.hcont
s : ℂ
hs : 0 < s.re
x : ℝ
hx : x ∈ Ioi 0
⊢ ContinuousAt (fun x => ↑x ^ (s - 1)) x

Tactic:
have : ContinuousAt (fun x : ℂ => x ^ (s - 1)) ↑x :=
  continuousAt_cpow_const <| ofReal_mem_slitPlane.2 hx

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

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

Tactic:
apply (ae_restrict_iff' measurableSet_Ioi).mpr

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

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

Tactic:
refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioi

Result:
case left
s : ℂ
hs : 0 < s.re
⊢ ContinuousOn (fun x => ↑(rexp (-x)) * ↑x ^ (s - 1)) (Ioi 0)

Proof state:
case left.hcont
s : ℂ
hs : 0 < s.re
⊢ ∀ x ∈ Ioi 0, ContinuousAt (fun x => ↑x ^ (s - 1)) x

Tactic:
intro x hx

Result:
case left.hcont
s : ℂ
hs : 0 < s.re
x : ℝ
hx : x ∈ Ioi 0
⊢ ContinuousAt (fun x => ↑x ^ (s - 1)) x

Proof state:
case right
s : ℂ
hs : 0 < s.re
⊢ HasFiniteIntegral (fun x => ↑(rexp (-x)) * ↑x ^ (s - 1)) (volume.restrict (Ioi 0))

Tactic:
rw [← hasFiniteIntegral_norm_iff]

Result:
case right
s : ℂ
hs : 0 < s.re
⊢ HasFiniteIntegral (fun a => ‖↑(rexp (-a)) * ↑a ^ (s - 1)‖) (volume.restrict (Ioi 0))

Proof state:
s : ℂ
hs : 0 < s.re
⊢ IntegrableOn (fun x => ↑(rexp (-x)) * ↑x ^ (s - 1)) (Ioi 0) volume

Tactic:
constructor

Result:
case left
s : ℂ
hs : 0 < s.re
⊢ AEStronglyMeasurable (fun x => ↑(rexp (-x)) * ↑x ^ (s - 1)) (volume.restrict (Ioi 0))

case right
s : ℂ
hs : 0 < s.re
⊢ HasFiniteIntegral (fun x => ↑(rexp (-x)) * ↑x ^ (s - 1)) (volume.restrict (Ioi 0))

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

Tactic:
filter_upwards with x hx

Result:
case right.h
s : ℂ
hs : 0 < s.re
x : ℝ
hx : x ∈ Ioi 0
⊢ rexp (-x) * x ^ (s.re - 1) = ‖↑(rexp (-x)) * ↑x ^ (s - 1)‖