-- Mathlib/Analysis/MellinTransform.lean
theorem mellin_hasDerivAt_of_isBigO_rpow [NormedSpace ℂ E] {a b : ℝ}
    {f : ℝ → E} {s : ℂ} (hfc : LocallyIntegrableOn f (Ioi 0)) (hf_top : f =O[atTop] (· ^ (-a)))
    (hs_top : s.re < a) (hf_bot : f =O[𝓝[>] 0] (· ^ (-b))) (hs_bot : b < s.re) :
    MellinConvergent (fun t => log t • f t) s ∧
      HasDerivAt (mellin f) (mellin (fun t => log t • f t) s) s

Proof state:
case intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x => x ^ (-a)
hs_top : s.re < a
hf_bot : f =O[𝓝[>] 0] fun x => x ^ (-b)
hs_bot : b < s.re
F : ℂ → ℝ → E := fun z t => ↑t ^ (z - 1) • f t
F' : ℂ → ℝ → E := fun z t => (↑t ^ (z - 1) * ↑(log t)) • f t
v : ℝ
hv0 : 0 < v
hv1 : v < s.re - b
hv2 : v < a - s.re
bound : ℝ → ℝ := fun t => (t ^ (s.re + v - 1) + t ^ (s.re - v - 1)) * |log t| * ‖f t‖
h1 : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) (volume.restrict (Ioi 0))
h2 : IntegrableOn (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (F' s) (volume.restrict (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
h5 : IntegrableOn bound (Ioi 0) volume
⊢ MellinConvergent (fun t => log t • f t) s ∧ HasDerivAt (mellin f) (mellin (fun t => log t • f t) s) s

Tactic:
have h6 : ∀ᵐ t : ℝ ∂volume.restrict (Ioi 0),
    ∀ y : ℂ, y ∈ Metric.ball s v → HasDerivAt (fun z : ℂ => F z t) (F' y t) y := by
  refine (ae_restrict_mem measurableSet_Ioi).mono fun t ht y _ => ?_
  have ht' : (t : ℂ) ≠ 0 := ofReal_ne_zero.mpr (ne_of_gt ht)
  have u1 : HasDerivAt (fun z : ℂ => (t : ℂ) ^ (z - 1)) (t ^ (y - 1) * log t) y := by
    convert ((hasDerivAt_id' y).sub_const 1).const_cpow (Or.inl ht') using 1
    rw [ofReal_log (le_of_lt ht)]
    ring
  exact u1.smul_const (f t)

Result:
case intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x => x ^ (-a)
hs_top : s.re < a
hf_bot : f =O[𝓝[>] 0] fun x => x ^ (-b)
hs_bot : b < s.re
F : ℂ → ℝ → E := fun z t => ↑t ^ (z - 1) • f t
F' : ℂ → ℝ → E := fun z t => (↑t ^ (z - 1) * ↑(log t)) • f t
v : ℝ
hv0 : 0 < v
hv1 : v < s.re - b
hv2 : v < a - s.re
bound : ℝ → ℝ := fun t => (t ^ (s.re + v - 1) + t ^ (s.re - v - 1)) * |log t| * ‖f t‖
h1 : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) (volume.restrict (Ioi 0))
h2 : IntegrableOn (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (F' s) (volume.restrict (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
h5 : IntegrableOn bound (Ioi 0) volume
h6 : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), ∀ y ∈ Metric.ball s v, HasDerivAt (fun z => F z t) (F' y t) y
⊢ MellinConvergent (fun t => log t • f t) s ∧ HasDerivAt (mellin f) (mellin (fun t => log t • f t) s) s

Proof state:
case intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x => x ^ (-a)
hs_top : s.re < a
hf_bot : f =O[𝓝[>] 0] fun x => x ^ (-b)
hs_bot : b < s.re
F : ℂ → ℝ → E := fun z t => ↑t ^ (z - 1) • f t
F' : ℂ → ℝ → E := fun z t => (↑t ^ (z - 1) * ↑(log t)) • f t
w : ℝ
hw1 : 0 < w
hw2 : w < a - s.re
⊢ ∃ v, 0 < v ∧ v < s.re - b ∧ v < a - s.re

Tactic:
obtain ⟨w', hw1', hw2'⟩ := exists_between (sub_pos.mpr hs_bot)

Result:
case intro.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x => x ^ (-a)
hs_top : s.re < a
hf_bot : f =O[𝓝[>] 0] fun x => x ^ (-b)
hs_bot : b < s.re
F : ℂ → ℝ → E := fun z t => ↑t ^ (z - 1) • f t
F' : ℂ → ℝ → E := fun z t => (↑t ^ (z - 1) * ↑(log t)) • f t
w : ℝ
hw1 : 0 < w
hw2 : w < a - s.re
w' : ℝ
hw1' : 0 < w'
hw2' : w' < s.re - b
⊢ ∃ v, 0 < v ∧ v < s.re - b ∧ v < a - s.re

Proof state:
case hf.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x => x ^ (-a)
hs_top : s.re < a
hf_bot : f =O[𝓝[>] 0] fun x => x ^ (-b)
hs_bot : b < s.re
F : ℂ → ℝ → E := fun z t => ↑t ^ (z - 1) • f t
F' : ℂ → ℝ → E := fun z t => (↑t ^ (z - 1) * ↑(log t)) • f t
v : ℝ
hv0 : 0 < v
hv1 : v < s.re - b
hv2 : v < a - s.re
bound : ℝ → ℝ := fun t => (t ^ (s.re + v - 1) + t ^ (s.re - v - 1)) * |log t| * ‖f t‖
h1 : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) (volume.restrict (Ioi 0))
h2 : IntegrableOn (F s) (Ioi 0) volume
t : ℝ
ht : t ∈ Ioi 0
⊢ ContinuousAt (fun t => ↑t ^ (s - 1)) t

Tactic:
exact continuousAt_ofReal_cpow_const _ _ (Or.inr <| ne_of_gt ht)

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x => x ^ (-a)
hs_top : s.re < a
hf_bot : f =O[𝓝[>] 0] fun x => x ^ (-b)
hs_bot : b < s.re
F : ℂ → ℝ → E := fun z t => ↑t ^ (z - 1) • f t
F' : ℂ → ℝ → E := fun z t => (↑t ^ (z - 1) * ↑(log t)) • f t
v : ℝ
hv0 : 0 < v
hv1 : v < s.re - b
hv2 : v < a - s.re
bound : ℝ → ℝ := fun t => (t ^ (s.re + v - 1) + t ^ (s.re - v - 1)) * |log t| * ‖f t‖
h1 : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) (volume.restrict (Ioi 0))
h2 : IntegrableOn (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (F' s) (volume.restrict (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
j : ℝ
hj : b < j
hj' : j < a
w : ℝ
hw1 : b < w
hw2 : w < j
w' : ℝ
hw1' : j < w'
hw2' : w' < a
⊢ LocallyIntegrableOn (fun t => ‖f t‖ * |log t|) (Ioi 0) volume

Tactic:
refine hfc.norm.mul_continuousOn ?_ isOpen_Ioi.isLocallyClosed

Result:
case intro.intro.intro.intro.refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x => x ^ (-a)
hs_top : s.re < a
hf_bot : f =O[𝓝[>] 0] fun x => x ^ (-b)
hs_bot : b < s.re
F : ℂ → ℝ → E := fun z t => ↑t ^ (z - 1) • f t
F' : ℂ → ℝ → E := fun z t => (↑t ^ (z - 1) * ↑(log t)) • f t
v : ℝ
hv0 : 0 < v
hv1 : v < s.re - b
hv2 : v < a - s.re
bound : ℝ → ℝ := fun t => (t ^ (s.re + v - 1) + t ^ (s.re - v - 1)) * |log t| * ‖f t‖
h1 : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) (volume.restrict (Ioi 0))
h2 : IntegrableOn (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (F' s) (volume.restrict (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
j : ℝ
hj : b < j
hj' : j < a
w : ℝ
hw1 : b < w
hw2 : w < j
w' : ℝ
hw1' : j < w'
hw2' : w' < a
⊢ ContinuousOn (fun t => |log t|) (Ioi 0)