Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: 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
⊢ IntegrableOn (fun t ↦ t ^ (j - 1) * (|log t| * ‖f t‖)) (Ioi 0) volume

Tactic:
refine mellin_convergent_of_isBigO_scalar ?_ ?_ hw1' ?_ hw2

Goal state after:
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
j : ℝ
hj : b < j
hj' : j < a
w : ℝ
hw1 : b < w
hw2 : w < j
w' : ℝ
hw1' : j < w'
hw2' : w' < a
⊢ LocallyIntegrableOn (fun t ↦ |log t| * ‖f t‖) (Ioi 0) volume

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
j : ℝ
hj : b < j
hj' : j < a
w : ℝ
hw1 : b < w
hw2 : w < j
w' : ℝ
hw1' : j < w'
hw2' : w' < a
⊢ (fun t ↦ |log t| * ‖f t‖) =O[atTop] fun x ↦ x ^ (-w')

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
j : ℝ
hj : b < j
hj' : j < a
w : ℝ
hw1 : b < w
hw2 : w < j
w' : ℝ
hw1' : j < w'
hw2' : w' < a
⊢ (fun t ↦ |log t| * ‖f t‖) =O[𝓝[>] 0] fun x ↦ x ^ (-w)