awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : IsBigO (F := ℝ) (𝓝[>] 0) f 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 (m₀ := MeasureSpace.toMeasurableSpace) (F z) (Measure.restrict volume (Ioi 0))
h2 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (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
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝[>] 0) (fun (t : ℝ) ↦ |log t| * ‖f t‖) fun (x : ℝ) ↦ x ^ (-w)

Tactic:
(isBigO_rpow_zero_log_smul hw1 hf_bot).norm_left.congr_left fun t ↦ ?_

Premises used: Asymptotics.IsBigO.norm_left, Asymptotics.IsBigO.congr_left, isBigO_rpow_zero_log_smul
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : IsBigO (F := ℝ) (𝓝[>] 0) f 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 (m₀ := MeasureSpace.toMeasurableSpace) (F z) (Measure.restrict volume (Ioi 0))
h2 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (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
refine_3 : ∀ (t : ℝ), ‖log t • f t‖ = |log t| * ‖f t‖
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝[>] 0) (fun (t : ℝ) ↦ |log t| * ‖f t‖) fun (x : ℝ) ↦ x ^ (-w)

Tactic:
refine (isBigO_rpow_zero_log_smul hw1 hf_bot).norm_left.congr_left fun t ↦ ?_

Premises used: Asymptotics.IsBigO.norm_left, Asymptotics.IsBigO.congr_left, isBigO_rpow_zero_log_smul
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : IsBigO (F := ℝ) (𝓝[>] 0) f 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 (m₀ := MeasureSpace.toMeasurableSpace) (F z) (Measure.restrict volume (Ioi 0))
h2 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) bound (Ioi 0) volume

Tactic:
have h5 : IntegrableOn bound (Ioi 0) := by
    simp_rw [bound, add_mul, mul_assoc]
    suffices ∀ {j : ℝ}, b < j → j < a →
        IntegrableOn (fun t : ℝ => t ^ (j - 1) * (|log t| * ‖f t‖)) (Ioi 0) volume by
      refine Integrable.add (this ?_ ?_) (this ?_ ?_)
      all_goals linarith
    · intro j hj hj'
      obtain ⟨w, hw1, hw2⟩ := exists_between hj
      obtain ⟨w', hw1', hw2'⟩ := exists_between hj'
      refine mellin_convergent_of_isBigO_scalar ?_ ?_ hw1' ?_ hw2
      · simp_rw [mul_comm]
        refine hfc.norm.mul_continuousOn ?_ isOpen_Ioi.isLocallyClosed
        refine Continuous.comp_continuousOn _root_.continuous_abs (continuousOn_log.mono ?_)
        exact subset_compl_singleton_iff.mpr self_notMem_Ioi
      · refine (isBigO_rpow_top_log_smul hw2' hf_top).norm_left.congr_left fun t ↦ ?_
        simp only [norm_smul, Real.norm_eq_abs]
      · refine (isBigO_rpow_zero_log_smul hw1 hf_bot).norm_left.congr_left fun t ↦ ?_
        simp only [norm_smul, Real.norm_eq_abs]
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : IsBigO (F := ℝ) (𝓝[>] 0) f 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 (m₀ := MeasureSpace.toMeasurableSpace) (F z) (Measure.restrict volume (Ioi 0))
h2 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
h5 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) bound (Ioi 0) volume
⊢ ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ y ∈ Metric.ball s v, HasDerivAt (fun (z : ℂ) ↦ F z t) (F' y t) y

Tactic:
(ae_restrict_mem measurableSet_Ioi).mono fun t ht y _ => ?_

Premises used: MeasureTheory.ae_restrict_mem, measurableSet_Ioi, Filter.Eventually.mono
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : IsBigO (F := ℝ) (𝓝[>] 0) f 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 (m₀ := MeasureSpace.toMeasurableSpace) (F z) (Measure.restrict volume (Ioi 0))
h2 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
h5 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) bound (Ioi 0) volume
refine :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
    ∀ y ∈ Metric.ball s v, HasDerivAt (fun (z : ℂ) ↦ F z t) (F' y t) y
⊢ ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ y ∈ Metric.ball s v, HasDerivAt (fun (z : ℂ) ↦ F z t) (F' y t) y

Tactic:
refine (ae_restrict_mem measurableSet_Ioi).mono fun t ht y _ => ?_

Premises used: MeasureTheory.ae_restrict_mem, measurableSet_Ioi, Filter.Eventually.mono
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : IsBigO (F := ℝ) (𝓝[>] 0) f 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 (m₀ := MeasureSpace.toMeasurableSpace) (F z) (Measure.restrict volume (Ioi 0))
h2 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
h5 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) bound (Ioi 0) volume
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
y : ℂ
h : y ∈ Metric.ball s v
⊢ (↑t : ℂ) ≠ 0

Tactic:
have ht' : (t : ℂ) ≠ 0 := ofReal_ne_zero.mpr (ne_of_gt ht)
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : IsBigO (F := ℝ) (𝓝[>] 0) f 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 (m₀ := MeasureSpace.toMeasurableSpace) (F z) (Measure.restrict volume (Ioi 0))
h2 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
h5 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) bound (Ioi 0) volume
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
y : ℂ
h : y ∈ Metric.ball s v
ht' : (↑t : ℂ) ≠ 0
⊢ HasDerivAt (fun (x : ℂ) ↦ (↑t : ℂ) ^ (x - 1)) ((↑t : ℂ) ^ (y - 1) * Complex.log (↑t : ℂ) * 1) y

Tactic:
((hasDerivAt_id' y).sub_const 1).const_cpow (Or.inl ht')

Premises used: hasDerivAt_id', HasDerivAt.sub_const, Or.inl, OfNat.ofNat, HasDerivAt.const_cpow
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : IsBigO (F := ℝ) (𝓝[>] 0) f 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 (m₀ := MeasureSpace.toMeasurableSpace) (F z) (Measure.restrict volume (Ioi 0))
h2 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
h5 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) bound (Ioi 0) volume
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
y : ℂ
h_1 : y ∈ Metric.ball s v
ht' : (↑t : ℂ) ≠ 0
h : (↑t : ℂ) ^ (y - 1) * (↑(log t) : ℂ) = (↑t : ℂ) ^ (y - 1) * Complex.log (↑t : ℂ) * 1
⊢ HasDerivAt (fun (z : ℂ) ↦ (↑t : ℂ) ^ (z - 1)) ((↑t : ℂ) ^ (y - 1) * (↑(log t) : ℂ)) y

Tactic:
convert! ((hasDerivAt_id' y).sub_const 1).const_cpow (Or.inl ht') using 1

Premises used: hasDerivAt_id', HasDerivAt.sub_const, Or.inl, OfNat.ofNat, HasDerivAt.const_cpow
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : IsBigO (F := ℝ) (𝓝[>] 0) f 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 (m₀ := MeasureSpace.toMeasurableSpace) (F z) (Measure.restrict volume (Ioi 0))
h2 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
h5 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) bound (Ioi 0) volume
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
y : ℂ
h_1 : y ∈ Metric.ball s v
ht' : (↑t : ℂ) ≠ 0
h : (↑t : ℂ) ^ (y - 1) * Complex.log (↑t : ℂ) = (↑t : ℂ) ^ (y - 1) * Complex.log (↑t : ℂ) * 1
⊢ (↑t : ℂ) ^ (y - 1) * (↑(log t) : ℂ) = (↑t : ℂ) ^ (y - 1) * Complex.log (↑t : ℂ) * 1

Tactic:
rw [ofReal_log (le_of_lt ht)]

Premises used: Complex.ofReal_log, le_of_lt
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : IsBigO (F := ℝ) (𝓝[>] 0) f 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 (m₀ := MeasureSpace.toMeasurableSpace) (F z) (Measure.restrict volume (Ioi 0))
h2 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
h5 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) bound (Ioi 0) volume
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
y : ℂ
h : y ∈ Metric.ball s v
ht' : (↑t : ℂ) ≠ 0
⊢ (↑t : ℂ) ^ (y - 1) * Complex.log (↑t : ℂ) = (↑t : ℂ) ^ (y - 1) * Complex.log (↑t : ℂ) * 1

Tactic:
ring
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : IsBigO (F := ℝ) (𝓝[>] 0) f 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 (m₀ := MeasureSpace.toMeasurableSpace) (F z) (Measure.restrict volume (Ioi 0))
h2 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
h5 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) bound (Ioi 0) volume
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
y : ℂ
h : y ∈ Metric.ball s v
ht' : (↑t : ℂ) ≠ 0
⊢ HasDerivAt (fun (z : ℂ) ↦ (↑t : ℂ) ^ (z - 1)) ((↑t : ℂ) ^ (y - 1) * (↑(log t) : ℂ)) y

Tactic:
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
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : IsBigO (F := ℝ) (𝓝[>] 0) f 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 (m₀ := MeasureSpace.toMeasurableSpace) (F z) (Measure.restrict volume (Ioi 0))
h2 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
h5 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) bound (Ioi 0) volume
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
y : ℂ
h : y ∈ Metric.ball s v
ht' : (↑t : ℂ) ≠ 0
u1 : HasDerivAt (fun (z : ℂ) ↦ (↑t : ℂ) ^ (z - 1)) ((↑t : ℂ) ^ (y - 1) * (↑(log t) : ℂ)) y
⊢ HasDerivAt (fun (z : ℂ) ↦ F z t) (F' y t) y

Tactic:
u1.smul_const (f t)

Premises used: HasDerivAt.smul_const
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : IsBigO (F := ℝ) (𝓝[>] 0) f 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 (m₀ := MeasureSpace.toMeasurableSpace) (F z) (Measure.restrict volume (Ioi 0))
h2 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
h5 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) bound (Ioi 0) volume
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
y : ℂ
h : y ∈ Metric.ball s v
ht' : (↑t : ℂ) ≠ 0
u1 : HasDerivAt (fun (z : ℂ) ↦ (↑t : ℂ) ^ (z - 1)) ((↑t : ℂ) ^ (y - 1) * (↑(log t) : ℂ)) y
⊢ HasDerivAt (fun (z : ℂ) ↦ F z t) (F' y t) y

Tactic:
exact u1.smul_const (f t)

Premises used: HasDerivAt.smul_const
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : IsBigO (F := ℝ) (𝓝[>] 0) f 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 (m₀ := MeasureSpace.toMeasurableSpace) (F z) (Measure.restrict volume (Ioi 0))
h2 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
h5 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) bound (Ioi 0) volume
⊢ ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ y ∈ Metric.ball s v, HasDerivAt (fun (z : ℂ) ↦ F z t) (F' y t) y

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)
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : IsBigO (F := ℝ) (𝓝[>] 0) f 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 (m₀ := MeasureSpace.toMeasurableSpace) (F z) (Measure.restrict volume (Ioi 0))
h2 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
h5 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) bound (Ioi 0) volume
h6 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ y ∈ Metric.ball s v, HasDerivAt (fun (z : ℂ) ↦ F z t) (F' y t) y
⊢ @Integrable _ _ _ _ Real.measurableSpace (F' s) (Measure.restrict volume (Ioi 0)) ∧
    HasDerivAt.{0, u_1} (F := E)
      (fun (n : ℂ) ↦ @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦ F n a)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦ F' s a) s

Tactic:
have main :=
    hasDerivAt_integral_of_dominated_loc_of_deriv_le (Metric.ball_mem_nhds _ hv0) h1 h2 h3 h4 h5 h6