awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
rw : Ioi 0 = Ioc 0 c2 ∪ (Ioc c2 c1 ∪ Ioi c1)
rw₁ : Ioi 0 = Ioc 0 c2 ∪ Ioi (min c2 c1)
rw₂ : Ioi 0 = Ioi (min 0 (min c2 c1))
⊢ Ioi 0 = Ioc 0 c2 ∪ Ioc c2 c1 ∪ Ioi c1
have rw₃ : Eq (α := Set ℝ) (Ioi 0) (Ioi 0)
Tactic: rw [union_assoc, Ioc_union_Ioi (le_max_right _ _),
      Ioc_union_Ioi ((min_le_left _ _).trans (le_max_right _ _)), min_eq_left (lt_min hc2 hc1).le]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (hypothesis)
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
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi 0) volume
have this : Ioi 0 = Ioc 0 c2 ∪ Ioc c2 c1 ∪ Ioi c1
Tactic: have : Ioi 0 = Ioc 0 c2 ∪ Ioc c2 c1 ∪ Ioi c1 := by
    rw [union_assoc, Ioc_union_Ioi (le_max_right _ _),
      Ioc_union_Ioi ((min_le_left _ _).trans (le_max_right _ _)), min_eq_left (lt_min hc2 hc1).le]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi 0) volume
have rw : (IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioc 0 c2) volume ∧
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioc c2 c1) volume) ∧
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi c1) volume
Tactic: rw [this, integrableOn_union, integrableOn_union]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
⊢ (IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioc 0 c2) volume ∧
      IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioc c2 c1)
        volume) ∧
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi c1) volume
have refine : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Icc c2 c1) volume
Tactic: refine ⟨⟨hc2', Iff.mp integrableOn_Icc_iff_integrableOn_Ioc ?_⟩, hc1'⟩
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Icc c2 c1) volume
have t : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ t ^ (s - 1)) (Ioi 0)
Tactic: refine
    (hfc.continuousOn_mul ?_ isOpen_Ioi.isLocallyClosed).integrableOn_compact_subset
      (fun t ht => (hc2.trans_le ht.1 : 0 < t)) isCompact_Icc
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
⊢ MellinConvergent f s
have rw : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s.re - 1) * ‖f t‖) (Ioi 0) volume
Tactic: rw [MellinConvergent,
    mellin_convergent_iff_norm Subset.rfl measurableSet_Ioi hfc.aestronglyMeasurable]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)
⊢ IsBigO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (t : ℝ) ↦ log t • f t) fun (x : ℝ) ↦ x ^ (-b)
have fun : ∀ (t : ℝ) (ht : 0 < t), Eq (α := ℝ) ((fun (x : ℝ) ↦ x ^ (a - b) • x ^ (-a)) t) ((fun (x : ℝ) ↦ x ^ (-b)) t)
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 => ?_))
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
⊢ t ^ (a - b) • t ^ (-a) = t ^ (-b)
have rw : 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]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)
⊢ t ^ (a - b) • t ^ (-a) = t ^ (-b)
have rw₁ : t ^ (a - b + -a) = t ^ (-b)
Tactic: rw [smul_eq_mul, ← rpow_add ht, ← sub_eq_add_neg, sub_eq_add_neg a, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)
⊢ t ^ (a - b) • t ^ (-a) = t ^ (-b)
have rw₂ : t ^ (a - b - a) = t ^ (-b)
Tactic: rw [smul_eq_mul, ← rpow_add ht, ← sub_eq_add_neg, sub_eq_add_neg a, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)
⊢ t ^ (a - b) • t ^ (-a) = t ^ (-b)
have rw₃ : t ^ (a + -b - a) = t ^ (-b)
Tactic: rw [smul_eq_mul, ← rpow_add ht, ← sub_eq_add_neg, sub_eq_add_neg a, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)
⊢ t ^ (a - b) • t ^ (-a) = t ^ (-b)
have rw₄ : t ^ (-b) = t ^ (-b)
Tactic: rw [smul_eq_mul, ← rpow_add ht, ← sub_eq_add_neg, sub_eq_add_neg a, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)
have refine_1 : ∀ (t : ℝ), ((fun (x : ℝ) ↦ -log x) ∘ fun (x : ℝ) ↦ x⁻¹) t = log t
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 => ?_)
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
⊢ IsLittleO (F := ℝ) (𝓝[>] 0) log fun (t : ℝ) ↦ t ^ (a - b)
have 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)
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 => ?_)
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)
⊢ Eq (α := ℝ) (((fun (x : ℝ) ↦ x ^ (b - a)) ∘ fun (x : ℝ) ↦ x⁻¹) t) ((fun (t : ℝ) ↦ t ^ (a - b)) t)
have refine_2₂ : t⁻¹ ^ (b - a) = t ^ (a - b)
Tactic: simp_rw [Function.comp_apply, inv_rpow (le_of_lt ht), ← rpow_neg (le_of_lt ht), neg_sub]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)
⊢ Eq (α := ℝ) (((fun (x : ℝ) ↦ x ^ (b - a)) ∘ fun (x : ℝ) ↦ x⁻¹) t) ((fun (t : ℝ) ↦ t ^ (a - b)) t)
have refine_2₃ : (t ^ (b - a))⁻¹ = t ^ (a - b)
Tactic: simp_rw [Function.comp_apply, inv_rpow (le_of_lt ht), ← rpow_neg (le_of_lt ht), neg_sub]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)
⊢ Eq (α := ℝ) (((fun (x : ℝ) ↦ x ^ (b - a)) ∘ fun (x : ℝ) ↦ x⁻¹) t) ((fun (t : ℝ) ↦ t ^ (a - b)) t)
have refine_2₄ : t ^ (-(b - a)) = t ^ (a - b)
Tactic: simp_rw [Function.comp_apply, inv_rpow (le_of_lt ht), ← rpow_neg (le_of_lt ht), neg_sub]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (hypothesis)
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)
⊢ IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[>] 0) (fun (t : ℝ) ↦ log t • f t) fun (x : ℝ) ↦ x ^ (-b)
have this : 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]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)
⊢ IsBigO.{0, u_1, 0} (E := E) (F := ℝ) (𝓝[>] 0) (fun (t : ℝ) ↦ log t • f t) fun (x : ℝ) ↦ x ^ (-b)
have refine : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
  Eq (α := ℝ) ((fun (x : ℝ) ↦ x ^ (a - b) • x ^ (-a)) t) ((fun (x : ℝ) ↦ x ^ (-b)) t)
Tactic: refine (this.isBigO.smul hf).congr' (Eventually.of_forall fun t => by rfl)
      (eventually_nhdsWithin_iff.mpr (Eventually.of_forall fun t ht => ?_))
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
⊢ Eq (α := ℝ) ((fun (x : ℝ) ↦ x ^ (a - b) • x ^ (-a)) t) ((fun (x : ℝ) ↦ x ^ (-b)) t)
have simp_rw : t ^ (a - b + -a) = t ^ (-b)
Tactic: simp_rw [smul_eq_mul, ← rpow_add ht]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
⊢ t ^ (a - b + -a) = t ^ (-b)
have e_a : a - b + -a = -b
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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 : ℝ), 0 < v ∧ v < s.re - b ∧ v < a - s.re
have obtain : ∀ (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_top)
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
⊢ ∃ (v : ℝ), 0 < v ∧ v < s.re - b ∧ v < a - s.re
have obtain : ∀ (w' : ℝ) (hw1' : 0 < w') (hw2' : w' < s.re - b), ∃ (v : ℝ), 0 < v ∧ v < s.re - b ∧ v < a - s.re
Tactic: obtain ⟨w', hw1', hw2'⟩ := exists_between (sub_pos.mpr hs_bot)
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ log t • f t) s ∧
    HasDerivAt (mellin f) (mellin (fun (t : ℝ) ↦ log t • f t) s) s
have 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
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⟩
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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))
have refine : ∀ (z : ℂ),
  AEStronglyMeasurable (β := ℂ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (z - 1))
    (Measure.restrict volume (Ioi 0))
Tactic: refine Eventually.of_forall fun z => AEStronglyMeasurable.smul ?_ hfc.aestronglyMeasurable
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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))
have refine : ContinuousOn (Y := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (z - 1)) (Ioi 0)
Tactic: refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioi
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)
have refine : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t), ContinuousAt (Y := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (z - 1)) t
Tactic: refine continuousOn_of_forall_continuousAt fun t ht => ?_
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (hypothesis)
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‖
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ log t • f t) s ∧
    HasDerivAt (mellin f) (mellin (fun (t : ℝ) ↦ log t • f t) s) s
have h1 : ∀ᶠ (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)
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (hypothesis)
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))
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ log t • f t) s ∧
    HasDerivAt (mellin f) (mellin (fun (t : ℝ) ↦ log t • f t) s) s
have h2 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (F s) (Ioi 0) volume
Tactic: have h2 : IntegrableOn (F s) (Ioi (0 : ℝ)) := by
    exact mellinConvergent_of_isBigO_rpow hfc hf_top hs_top hf_bot hs_bot
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
⊢ AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
have hf : LocallyIntegrableOn (F' s) (Ioi 0) volume
Tactic: apply LocallyIntegrableOn.aestronglyMeasurable