-- 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 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
this : ∀ {j : ℝ}, b < j → j < a → IntegrableOn (fun t => t ^ (j - 1) * (|log t| * ‖f t‖)) (Ioi 0) volume
⊢ b < s.re + v

case refine_2
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
this : ∀ {j : ℝ}, b < j → j < a → IntegrableOn (fun t => t ^ (j - 1) * (|log t| * ‖f t‖)) (Ioi 0) volume
⊢ s.re + v < a

case refine_3
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
this : ∀ {j : ℝ}, b < j → j < a → IntegrableOn (fun t => t ^ (j - 1) * (|log t| * ‖f t‖)) (Ioi 0) volume
⊢ b < s.re - v

case refine_4
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
this : ∀ {j : ℝ}, b < j → j < a → IntegrableOn (fun t => t ^ (j - 1) * (|log t| * ‖f t‖)) (Ioi 0) volume
⊢ s.re - v < a

Tactic:
all_goals linarith

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_2
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
t : ℝ
⊢ ‖log t • f t‖ = |log t| * ‖f t‖

Tactic:
simp only [norm_smul, Real.norm_eq_abs]

Result:
no goals

Proof state:
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
⊢ AEStronglyMeasurable (F' s) (volume.restrict (Ioi 0))

Tactic:
apply LocallyIntegrableOn.aestronglyMeasurable

Result:
case hf
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
⊢ LocallyIntegrableOn (F' s) (Ioi 0) volume