-- Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean
theorem hasDerivAt_GammaIntegral {s : ℂ} (hs : 0 < s.re) :
    HasDerivAt GammaIntegral (∫ t : ℝ in Ioi 0, t ^ (s - 1) * (Real.log t * Real.exp (-t))) s

Proof state:
s : ℂ
hs : 0 < s.re
⊢ HasDerivAt (mellin fun x => ↑(rexp (-x))) (∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) * (↑(Real.log t) * ↑(rexp (-t)))) s

Tactic:
convert (mellin_hasDerivAt_of_isBigO_rpow (E := ℂ) _ _ (lt_add_one _) _ hs).2

Result:
case convert_2
s : ℂ
hs : 0 < s.re
⊢ MeasureTheory.LocallyIntegrableOn (fun x => ↑(rexp (-x))) (Ioi 0) MeasureTheory.volume

case convert_3
s : ℂ
hs : 0 < s.re
⊢ (fun x => ↑(rexp (-x))) =O[atTop] fun x => x ^ (-(s.re + 1))

case convert_4
s : ℂ
hs : 0 < s.re
⊢ (fun x => ↑(rexp (-x))) =O[𝓝[>] 0] fun x => x ^ (-0)

Proof state:
case convert_2
s : ℂ
hs : 0 < s.re
⊢ Continuous fun x => ↑(rexp (-x))

Tactic:
exact continuous_ofReal.comp (Real.continuous_exp.comp continuous_neg)

Result:
no goals

Proof state:
case convert_4
s : ℂ
hs : 0 < s.re
⊢ (fun x => ↑(rexp (-x))) =O[𝓝[>] 0] fun x => x ^ (-0)

Tactic:
simp_rw [neg_zero, rpow_zero]

Result:
case convert_4
s : ℂ
hs : 0 < s.re
⊢ (fun x => ↑(rexp (-x))) =O[𝓝[>] 0] fun x => 1

Proof state:
case convert_3
s : ℂ
hs : 0 < s.re
⊢ (fun x => ‖↑(rexp (-x))‖) =O[atTop] fun x => x ^ (-(s.re + 1))

Tactic:
simp_rw [norm_real, isBigO_norm_left]

Result:
case convert_3
s : ℂ
hs : 0 < s.re
⊢ (fun x => rexp (-x)) =O[atTop] fun x => x ^ (-(s.re + 1))

Proof state:
case convert_4
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun x => ↑(rexp (-x))) (𝓝[>] 0) (𝓝 ↑(rexp (-0)))

Tactic:
exact (continuous_ofReal.comp (Real.continuous_exp.comp continuous_neg)).continuousWithinAt

Result:
no goals

Proof state:
case convert_2
s : ℂ
hs : 0 < s.re
⊢ MeasureTheory.LocallyIntegrableOn (fun x => ↑(rexp (-x))) (Ioi 0) MeasureTheory.volume

Tactic:
refine (Continuous.continuousOn ?_).locallyIntegrableOn measurableSet_Ioi

Result:
case convert_2
s : ℂ
hs : 0 < s.re
⊢ Continuous fun x => ↑(rexp (-x))

Proof state:
case convert_4
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun x => ↑(rexp (-x))) (𝓝[>] 0) (𝓝 1)

Tactic:
rw [(by simp : (1 : ℂ) = Real.exp (-0))]

Result:
case convert_4
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun x => ↑(rexp (-x))) (𝓝[>] 0) (𝓝 ↑(rexp (-0)))

Proof state:
case convert_4
s : ℂ
hs : 0 < s.re
⊢ (fun x => ↑(rexp (-x))) =O[𝓝[>] 0] fun x => 1

Tactic:
refine isBigO_const_of_tendsto (?_ : Tendsto _ _ (𝓝 (1 : ℂ))) one_ne_zero

Result:
case convert_4
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun x => ↑(rexp (-x))) (𝓝[>] 0) (𝓝 1)

Proof state:
case convert_3
s : ℂ
hs : 0 < s.re
⊢ (fun x => ↑(rexp (-x))) =O[atTop] fun x => x ^ (-(s.re + 1))

Tactic:
rw [← isBigO_norm_left]

Result:
case convert_3
s : ℂ
hs : 0 < s.re
⊢ (fun x => ‖↑(rexp (-x))‖) =O[atTop] fun x => x ^ (-(s.re + 1))

Proof state:
s : ℂ
hs : 0 < s.re
⊢ HasDerivAt GammaIntegral (∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) * (↑(Real.log t) * ↑(rexp (-t)))) s

Tactic:
rw [GammaIntegral_eq_mellin]

Result:
s : ℂ
hs : 0 < s.re
⊢ HasDerivAt (mellin fun x => ↑(rexp (-x))) (∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) * (↑(Real.log t) * ↑(rexp (-t)))) s

Proof state:
s : ℂ
hs : 0 < s.re
⊢ 1 = ↑(rexp (-0))

Tactic:
simp

Result:
no goals

Proof state:
case convert_3
s : ℂ
hs : 0 < s.re
⊢ (fun x => rexp (-x)) =O[atTop] fun x => x ^ (-(s.re + 1))

Tactic:
simpa only [neg_one_mul] using (isLittleO_exp_neg_mul_rpow_atTop zero_lt_one _).isBigO

Result:
no goals