awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.MellinTransform
Goal:
a b : ℝ
f : ℝ → ℝ
s : ℝ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs_top : s < a
hf_bot : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
hs_bot : b < s
c1 : ℝ
hc1 : 0 < c1
hc1' : IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi c1) volume
c2 : ℝ
hc2 : 0 < c2
hc2' : IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioc 0 c2) volume
this : Ioi 0 = Ioc 0 c2 ∪ Ioc c2 c1 ∪ Ioi c1
⊢ ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ t ^ (s - 1)) (Ioi 0)

Tactic:
continuousOn_of_forall_continuousAt
    fun t ht ↦ continuousAt_rpow_const _ _ <| Or.inl <| ne_of_gt ht

Premises used: continuousOn_of_forall_continuousAt, Real.continuousAt_rpow_const, HSub.hSub, ne_of_gt, Or.inl, OfNat.ofNat
-- Module: Mathlib.Analysis.MellinTransform
Goal:
a b : ℝ
f : ℝ → ℝ
s : ℝ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs_top : s < a
hf_bot : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
hs_bot : b < s
c1 : ℝ
hc1 : 0 < c1
hc1' : IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi c1) volume
c2 : ℝ
hc2 : 0 < c2
hc2' : IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioc 0 c2) volume
this : Ioi 0 = Ioc 0 c2 ∪ Ioc c2 c1 ∪ Ioi c1
⊢ ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ t ^ (s - 1)) (Ioi 0)

Tactic:
exact continuousOn_of_forall_continuousAt
    fun t ht ↦ continuousAt_rpow_const _ _ <| Or.inl <| ne_of_gt ht

Premises used: continuousOn_of_forall_continuousAt, Real.continuousAt_rpow_const, ne_of_gt, Or.inl
-- 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
rw : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s.re - 1) * ‖f t‖) (Ioi 0) volume
⊢ MellinConvergent f s

Tactic:
rw [MellinConvergent,
    mellin_convergent_iff_norm Subset.rfl measurableSet_Ioi hfc.aestronglyMeasurable]

Premises used: measurableSet_Ioi, Set.Subset.rfl, MellinConvergent, mellin_convergent_iff_norm, MeasureTheory.LocallyIntegrableOn.aestronglyMeasurable
-- 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
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s.re - 1) * ‖f t‖) (Ioi 0) volume

Tactic:
mellin_convergent_of_isBigO_scalar hfc.norm hf_top.norm_left hs_top hf_bot.norm_left hs_bot

Premises used: Asymptotics.IsBigO.norm_left, mellin_convergent_of_isBigO_scalar, MeasureTheory.LocallyIntegrableOn.norm
-- 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
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s.re - 1) * ‖f t‖) (Ioi 0) volume

Tactic:
exact mellin_convergent_of_isBigO_scalar hfc.norm hf_top.norm_left hs_top hf_bot.norm_left hs_bot

Premises used: Asymptotics.IsBigO.norm_left, mellin_convergent_of_isBigO_scalar, MeasureTheory.LocallyIntegrableOn.norm
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : b < a
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
t : ℝ
⊢ Eq.{u_1 + 1} (α := E) ((fun (x : ℝ) ↦ log x • f x) t) ((fun (t : ℝ) ↦ log t • f t) t)

Tactic:
rfl
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : b < a
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
fun : ∀ (t : ℝ) (ht : 0 < t), Eq (α := ℝ) ((fun (x : ℝ) ↦ x ^ (a - b) • x ^ (-a)) t) ((fun (x : ℝ) ↦ x ^ (-b)) t)
⊢ IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (t : ℝ) ↦ log t • f t) fun (x : ℝ) ↦ x ^ (-b)

Tactic:
refine
    ((isLittleO_log_rpow_atTop (sub_pos.mpr hab)).isBigO.smul hf).congr'
      (Eventually.of_forall fun t => by rfl)
      ((eventually_gt_atTop 0).mp (Eventually.of_forall fun t ht => ?_))

Premises used: Iff.mpr, sub_pos, Asymptotics.IsBigO.smul, Filter.Eventually.of_forall, isLittleO_log_rpow_atTop, Asymptotics.IsBigO.congr', Asymptotics.IsLittleO.isBigO, Filter.Eventually.mp, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : b < a
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
t : ℝ
ht : 0 < t
rw : t ^ (a - b) * t ^ (-a) = t ^ (-b)
rw₁ : t ^ (a - b + -a) = t ^ (-b)
rw₂ : t ^ (a - b - a) = t ^ (-b)
rw₃ : t ^ (a + -b - a) = t ^ (-b)
rw₄ rw₅ : t ^ (-b) = t ^ (-b)
⊢ t ^ (a - b) • t ^ (-a) = t ^ (-b)

Tactic:
rw [smul_eq_mul, ← rpow_add ht, ← sub_eq_add_neg, sub_eq_add_neg a, add_sub_cancel_left]

Premises used: add_sub_cancel_left, sub_eq_add_neg, Real.rpow_add, smul_eq_mul
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-a)
⊢ IsLittleO (F := ℝ) (𝓝[>] 0) log fun (t : ℝ) ↦ t ^ (a - b)

Tactic:
((isLittleO_log_rpow_atTop (sub_pos.mpr hab)).neg_left.comp_tendsto
          tendsto_inv_nhdsGT_zero).congr'
      (.of_forall fun t => ?_)
      (eventually_mem_nhdsWithin.mono fun t ht => ?_)

Premises used: Iff.mpr, sub_pos, eventually_mem_nhdsWithin, tendsto_inv_nhdsGT_zero, Filter.Eventually.of_forall, isLittleO_log_rpow_atTop, Asymptotics.IsLittleO.neg_left, Filter.Eventually.mono, Asymptotics.IsLittleO.congr', Asymptotics.IsLittleO.comp_tendsto
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-a)
refine_1 : ∀ (t : ℝ), ((fun (x : ℝ) ↦ -log x) ∘ fun (x : ℝ) ↦ x⁻¹) t = log t
refine_2 :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
    Eq (α := ℝ) (((fun (x : ℝ) ↦ x ^ (b - a)) ∘ fun (x : ℝ) ↦ x⁻¹) t) ((fun (t : ℝ) ↦ t ^ (a - b)) t)
⊢ IsLittleO (F := ℝ) (𝓝[>] 0) log fun (t : ℝ) ↦ t ^ (a - b)

Tactic:
refine ((isLittleO_log_rpow_atTop (sub_pos.mpr hab)).neg_left.comp_tendsto
          tendsto_inv_nhdsGT_zero).congr'
      (.of_forall fun t => ?_)
      (eventually_mem_nhdsWithin.mono fun t ht => ?_)

Premises used: Iff.mpr, sub_pos, eventually_mem_nhdsWithin, tendsto_inv_nhdsGT_zero, Filter.Eventually.of_forall, isLittleO_log_rpow_atTop, Asymptotics.IsLittleO.neg_left, Filter.Eventually.mono, Asymptotics.IsLittleO.congr', Asymptotics.IsLittleO.comp_tendsto
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-a)
t : ℝ
⊢ ((fun (x : ℝ) ↦ -log x) ∘ fun (x : ℝ) ↦ x⁻¹) t = log t

Tactic:
simp
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-a)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
refine_2 refine_2₁ : ((fun (x : ℝ) ↦ x ^ (b - a)) ∘ fun (x : ℝ) ↦ x⁻¹) t = t ^ (a - b)
refine_2₂ : t⁻¹ ^ (b - a) = t ^ (a - b)
refine_2₃ : (t ^ (b - a))⁻¹ = t ^ (a - b)
refine_2₄ : t ^ (-(b - a)) = t ^ (a - b)
⊢ Eq (α := ℝ) (((fun (x : ℝ) ↦ x ^ (b - a)) ∘ fun (x : ℝ) ↦ x⁻¹) t) ((fun (t : ℝ) ↦ t ^ (a - b)) t)

Tactic:
simp_rw [Function.comp_apply, inv_rpow (le_of_lt ht), ← rpow_neg (le_of_lt ht), neg_sub]

Premises used: Real.inv_rpow, neg_sub, le_of_lt, Function.comp_apply, Real.rpow_neg
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-a)
⊢ IsLittleO (F := ℝ) (𝓝[>] 0) log fun (t : ℝ) ↦ t ^ (a - b)

Tactic:
have : log =o[𝓝[>] 0] fun t : ℝ => t ^ (a - b) := by
    refine ((isLittleO_log_rpow_atTop (sub_pos.mpr hab)).neg_left.comp_tendsto
          tendsto_inv_nhdsGT_zero).congr'
      (.of_forall fun t => ?_)
      (eventually_mem_nhdsWithin.mono fun t ht => ?_)
    · simp
    · simp_rw [Function.comp_apply, inv_rpow (le_of_lt ht), ← rpow_neg (le_of_lt ht), neg_sub]
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-a)
this : IsLittleO (F := ℝ) (𝓝[>] 0) log fun (t : ℝ) ↦ t ^ (a - b)
t : ℝ
⊢ Eq.{u_1 + 1} (α := E) ((fun (x : ℝ) ↦ log x • f x) t) ((fun (t : ℝ) ↦ log t • f t) t)

Tactic:
rfl
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-a)
this : IsLittleO (F := ℝ) (𝓝[>] 0) log fun (t : ℝ) ↦ t ^ (a - b)
refine :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
    Eq (α := ℝ) ((fun (x : ℝ) ↦ x ^ (a - b) • x ^ (-a)) t) ((fun (x : ℝ) ↦ x ^ (-b)) t)
⊢ IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[>] 0) (fun (t : ℝ) ↦ log t • f t) fun (x : ℝ) ↦ x ^ (-b)

Tactic:
refine (this.isBigO.smul hf).congr' (Eventually.of_forall fun t => by rfl)
      (eventually_nhdsWithin_iff.mpr (Eventually.of_forall fun t ht => ?_))

Premises used: Iff.mpr, Asymptotics.IsBigO.smul, Filter.Eventually.of_forall, Asymptotics.IsBigO.congr', Asymptotics.IsLittleO.isBigO, eventually_nhdsWithin_iff
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-a)
this : IsLittleO (F := ℝ) (𝓝[>] 0) log fun (t : ℝ) ↦ t ^ (a - b)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
simp_rw : t ^ (a - b + -a) = t ^ (-b)
⊢ Eq (α := ℝ) ((fun (x : ℝ) ↦ x ^ (a - b) • x ^ (-a)) t) ((fun (x : ℝ) ↦ x ^ (-b)) t)

Tactic:
simp_rw [smul_eq_mul, ← rpow_add ht]

Premises used: Real.rpow_add, smul_eq_mul
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-a)
this : IsLittleO (F := ℝ) (𝓝[>] 0) log fun (t : ℝ) ↦ t ^ (a - b)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
e_a : a - b + -a = -b
⊢ t ^ (a - b + -a) = t ^ (-b)

Tactic:
congr 1
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : a < b
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-a)
this : IsLittleO (F := ℝ) (𝓝[>] 0) log fun (t : ℝ) ↦ t ^ (a - b)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ a - b + -a = -b

Tactic:
abel
-- 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
obtain : ∀ (w : ℝ) (hw1 : 0 < w) (hw2 : w < a - s.re), ∃ (v : ℝ), 0 < v ∧ v < s.re - b ∧ v < 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_top)

Premises used: Iff.mpr, sub_pos, exists_between
-- 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
w : ℝ
hw1 : 0 < w
hw2 : w < a - s.re
obtain : ∀ (w' : ℝ) (hw1' : 0 < w') (hw2' : w' < s.re - b), ∃ (v : ℝ), 0 < v ∧ v < s.re - b ∧ v < 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)

Premises used: Iff.mpr, sub_pos, exists_between
-- 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
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

Tactic:
⟨min w w', lt_min hw1 hw1', (min_le_right _ _).trans_lt hw2', (min_le_left _ _).trans_lt hw2⟩

Premises used: lt_min, min_le_left, And.intro, min_le_right, Exists.intro, LE.le.trans_lt, Min.min
-- 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
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

Tactic:
exact
      ⟨min w w', lt_min hw1 hw1', (min_le_right _ _).trans_lt hw2', (min_le_left _ _).trans_lt hw2⟩
-- 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
obtain :
  ∀ (v : ℝ) (hv0 : 0 < v) (hv1 : v < s.re - b) (hv2 : v < a - s.re),
    MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ log t • f t) s ∧
      HasDerivAt (mellin f) (mellin (fun (t : ℝ) ↦ log t • f t) s) s
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ log t • f t) s ∧
    HasDerivAt (mellin f) (mellin (fun (t : ℝ) ↦ log t • f t) s) s

Tactic:
obtain ⟨v, hv0, hv1, hv2⟩ : ∃ v : ℝ, 0 < v ∧ v < s.re - b ∧ v < a - s.re := by
    obtain ⟨w, hw1, hw2⟩ := exists_between (sub_pos.mpr hs_top)
    obtain ⟨w', hw1', hw2'⟩ := exists_between (sub_pos.mpr hs_bot)
    exact
      ⟨min w w', lt_min hw1 hw1', (min_le_right _ _).trans_lt hw2', (min_le_left _ _).trans_lt hw2⟩

Premises used: Complex.re
-- 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‖
⊢ ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F z) (Measure.restrict volume (Ioi 0))

Tactic:
Eventually.of_forall fun z => AEStronglyMeasurable.smul ?_ hfc.aestronglyMeasurable

Premises used: Filter.Eventually.of_forall, MeasureTheory.AEStronglyMeasurable.smul, MeasureTheory.LocallyIntegrableOn.aestronglyMeasurable
-- 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‖
refine :
  ∀ (z : ℂ),
    AEStronglyMeasurable (β := ℂ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (z - 1))
      (Measure.restrict volume (Ioi 0))
⊢ ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F z) (Measure.restrict volume (Ioi 0))

Tactic:
refine Eventually.of_forall fun z => AEStronglyMeasurable.smul ?_ hfc.aestronglyMeasurable

Premises used: Filter.Eventually.of_forall, MeasureTheory.AEStronglyMeasurable.smul, MeasureTheory.LocallyIntegrableOn.aestronglyMeasurable
-- 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‖
z : ℂ
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (z - 1))
    (Measure.restrict volume (Ioi 0))

Tactic:
ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioi

Premises used: ContinuousOn.aestronglyMeasurable, measurableSet_Ioi
-- 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‖
z : ℂ
refine : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (z - 1)) (Ioi 0)
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (z - 1))
    (Measure.restrict volume (Ioi 0))

Tactic:
refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioi

Premises used: ContinuousOn.aestronglyMeasurable, measurableSet_Ioi
-- 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‖
z : ℂ
⊢ ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (z - 1)) (Ioi 0)

Tactic:
continuousOn_of_forall_continuousAt fun t ht => ?_

Premises used: continuousOn_of_forall_continuousAt
-- 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‖
z : ℂ
refine :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t), ContinuousAt (Y := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (z - 1)) t
⊢ ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (z - 1)) (Ioi 0)

Tactic:
refine continuousOn_of_forall_continuousAt fun t ht => ?_

Premises used: continuousOn_of_forall_continuousAt
-- 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‖
z : ℂ
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ ContinuousAt (Y := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (z - 1)) t

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

Premises used: ne_of_gt, Or.inr, Complex.continuousAt_ofReal_cpow_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‖
z : ℂ
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ ContinuousAt (Y := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (z - 1)) t

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

Premises used: ne_of_gt, Or.inr, Complex.continuousAt_ofReal_cpow_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‖
⊢ ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F z) (Measure.restrict volume (Ioi 0))

Tactic:
have h1 : ∀ᶠ z : ℂ in 𝓝 s, AEStronglyMeasurable (F z) (volume.restrict <| Ioi 0) := by
    refine Eventually.of_forall fun z => AEStronglyMeasurable.smul ?_ hfc.aestronglyMeasurable
    refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioi
    refine continuousOn_of_forall_continuousAt fun t ht => ?_
    exact continuousAt_ofReal_cpow_const _ _ (Or.inr <| ne_of_gt ht)