awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.MellinTransform
Goal:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Membership.mem (γ := Set ℝ) (Ioi 0) y → ‖f y‖ ≤ d * ‖y ^ (-b)‖
refine_1 :
  AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1))
    (Measure.restrict volume (Ioo 0 ε))
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t)
    (Measure.restrict volume (Ioo 0 ε))

Tactic:
refine AEStronglyMeasurable.mul ?_ (hfc.mono_set Ioo_subset_Ioi_self)

Premises used: MeasureTheory.AEStronglyMeasurable.mono_set, Set.Ioo_subset_Ioi_self, MeasureTheory.AEStronglyMeasurable.mul
-- Module: Mathlib.Analysis.MellinTransform
Goal:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Membership.mem (γ := Set ℝ) (Ioi 0) y → ‖f y‖ ≤ d * ‖y ^ (-b)‖
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1))
    (Measure.restrict volume (Ioo 0 ε))

Tactic:
(continuousOn_of_forall_continuousAt fun t ht => ?_).aestronglyMeasurable
      measurableSet_Ioo

Premises used: continuousOn_of_forall_continuousAt, ContinuousOn.aestronglyMeasurable, measurableSet_Ioo
-- Module: Mathlib.Analysis.MellinTransform
Goal:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Membership.mem (γ := Set ℝ) (Ioi 0) y → ‖f y‖ ≤ d * ‖y ^ (-b)‖
refine_1 : ∀ (t : ℝ) (ht : t ∈ Ioo 0 ε), ContinuousAt (Y := ℝ) (fun (t : ℝ) ↦ t ^ (s - 1)) t
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1))
    (Measure.restrict volume (Ioo 0 ε))

Tactic:
refine (continuousOn_of_forall_continuousAt fun t ht => ?_).aestronglyMeasurable
      measurableSet_Ioo

Premises used: continuousOn_of_forall_continuousAt, ContinuousOn.aestronglyMeasurable, measurableSet_Ioo
-- Module: Mathlib.Analysis.MellinTransform
Goal:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Membership.mem (γ := Set ℝ) (Ioi 0) y → ‖f y‖ ≤ d * ‖y ^ (-b)‖
t : ℝ
ht : t ∈ Ioo 0 ε
⊢ ContinuousAt (Y := ℝ) (fun (t : ℝ) ↦ t ^ (s - 1)) t

Tactic:
continuousAt_rpow_const _ _ (Or.inl ht.1.ne')

Premises used: Real.continuousAt_rpow_const, LT.lt.ne', And.left, Or.inl
-- Module: Mathlib.Analysis.MellinTransform
Goal:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Membership.mem (γ := Set ℝ) (Ioi 0) y → ‖f y‖ ≤ d * ‖y ^ (-b)‖
t : ℝ
ht : t ∈ Ioo 0 ε
⊢ ContinuousAt (Y := ℝ) (fun (t : ℝ) ↦ t ^ (s - 1)) t

Tactic:
exact continuousAt_rpow_const _ _ (Or.inl ht.1.ne')

Premises used: Real.continuousAt_rpow_const, LT.lt.ne', And.left, Or.inl
-- Module: Mathlib.Analysis.MellinTransform
Goal:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Membership.mem (γ := Set ℝ) (Ioi 0) y → ‖f y‖ ≤ d * ‖y ^ (-b)‖
refine_2 :
  @HasFiniteIntegral _ ℝ _ Real.measurableSpace (fun (t : ℝ) ↦ d * t ^ (s - b - 1)) (Measure.restrict volume (Ioo 0 ε))
refine_2₁ : ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioo 0 ε), ‖a ^ (s - 1) * f a‖ ≤ d * a ^ (s - b - 1)
refine_2₂ : ℝ → ℝ
⊢ @HasFiniteIntegral _ ℝ _ Real.measurableSpace (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Measure.restrict volume (Ioo 0 ε))

Tactic:
apply HasFiniteIntegral.mono'

Premises used: MeasureTheory.HasFiniteIntegral.mono'
-- Module: Mathlib.Analysis.MellinTransform
Goal:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Membership.mem (γ := Set ℝ) (Ioi 0) y → ‖f y‖ ≤ d * ‖y ^ (-b)‖
⊢ @HasFiniteIntegral _ ℝ _ Real.measurableSpace (fun (t : ℝ) ↦ d * t ^ (s - b - 1)) (Measure.restrict volume (Ioo 0 ε))

Tactic:
(Integrable.hasFiniteIntegral ?_).const_mul _

Premises used: MeasureTheory.HasFiniteIntegral.const_mul, MeasureTheory.Integrable.hasFiniteIntegral
-- Module: Mathlib.Analysis.MellinTransform
Goal:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Membership.mem (γ := Set ℝ) (Ioi 0) y → ‖f y‖ ≤ d * ‖y ^ (-b)‖
refine_2 : @Integrable ℝ _ _ _ Real.measurableSpace (fun (t : ℝ) ↦ t ^ (s - b - 1)) (Measure.restrict volume (Ioo 0 ε))
⊢ @HasFiniteIntegral _ ℝ _ Real.measurableSpace (fun (t : ℝ) ↦ d * t ^ (s - b - 1)) (Measure.restrict volume (Ioo 0 ε))

Tactic:
refine (Integrable.hasFiniteIntegral ?_).const_mul _

Premises used: MeasureTheory.HasFiniteIntegral.const_mul, MeasureTheory.Integrable.hasFiniteIntegral
-- Module: Mathlib.Analysis.MellinTransform
Goal:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Membership.mem (γ := Set ℝ) (Ioi 0) y → ‖f y‖ ≤ d * ‖y ^ (-b)‖
refine_2 : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ (s - b - 1)) volume 0 ε
⊢ @Integrable ℝ _ _ _ Real.measurableSpace (fun (t : ℝ) ↦ t ^ (s - b - 1)) (Measure.restrict volume (Ioo 0 ε))

Tactic:
rw [← IntegrableOn, ← integrableOn_Ioc_iff_integrableOn_Ioo, ←
        intervalIntegrable_iff_integrableOn_Ioc_of_le hε.le]

Premises used: intervalIntegrable_iff_integrableOn_Ioc_of_le, MeasureTheory.IntegrableOn, LT.lt.le, integrableOn_Ioc_iff_integrableOn_Ioo
-- Module: Mathlib.Analysis.MellinTransform
Goal:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Membership.mem (γ := Set ℝ) (Ioi 0) y → ‖f y‖ ≤ d * ‖y ^ (-b)‖
linarith : s - b - 1 ≤ -1 → b - s + (s - b - 1 - -1) = 0
⊢ -1 < s - b - 1

Tactic:
linarith
-- Module: Mathlib.Analysis.MellinTransform
Goal:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Membership.mem (γ := Set ℝ) (Ioi 0) y → ‖f y‖ ≤ d * ‖y ^ (-b)‖
⊢ IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ (s - b - 1)) volume 0 ε

Tactic:
exact intervalIntegral.intervalIntegrable_rpow' (by linarith)

Premises used: intervalIntegral.intervalIntegrable_rpow'
-- Module: Mathlib.Analysis.MellinTransform
Goal:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Membership.mem (γ := Set ℝ) (Ioi 0) y → ‖f y‖ ≤ d * ‖y ^ (-b)‖
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioo 0 ε), ‖a ^ (s - 1) * f a‖ ≤ d * a ^ (s - b - 1)

Tactic:
(ae_restrict_iff' measurableSet_Ioo).mpr (Eventually.of_forall fun t ht => ?_)

Premises used: Iff.mpr, Filter.Eventually.of_forall, measurableSet_Ioo, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.Analysis.MellinTransform
Goal:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Membership.mem (γ := Set ℝ) (Ioi 0) y → ‖f y‖ ≤ d * ‖y ^ (-b)‖
refine_2 : ∀ (t : ℝ) (ht : t ∈ Ioo 0 ε), ‖t ^ (s - 1) * f t‖ ≤ d * t ^ (s - b - 1)
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioo 0 ε), ‖a ^ (s - 1) * f a‖ ≤ d * a ^ (s - b - 1)

Tactic:
refine (ae_restrict_iff' measurableSet_Ioo).mpr (Eventually.of_forall fun t ht => ?_)

Premises used: Iff.mpr, Filter.Eventually.of_forall, measurableSet_Ioo, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.Analysis.MellinTransform
Goal:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Membership.mem (γ := Set ℝ) (Ioi 0) y → ‖f y‖ ≤ d * ‖y ^ (-b)‖
t : ℝ
ht : t ∈ Ioo 0 ε
refine_2 : ‖f t‖ * ‖t ^ (s - 1)‖ ≤ d * t ^ (s - b - 1)
⊢ ‖t ^ (s - 1) * f t‖ ≤ d * t ^ (s - b - 1)

Tactic:
rw [mul_comm, norm_mul]

Premises used: norm_mul, mul_comm
-- Module: Mathlib.Analysis.MellinTransform
Goal:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Membership.mem (γ := Set ℝ) (Ioi 0) y → ‖f y‖ ≤ d * ‖y ^ (-b)‖
t : ℝ
ht : t ∈ Ioo 0 ε
refine_2 : dist t 0 < ε
refine_2₁ : ∀ (hε' : ‖f t‖ ≤ d * ‖t ^ (-b)‖), ‖f t‖ * ‖t ^ (s - 1)‖ ≤ d * t ^ (s - b - 1)
⊢ ‖f t‖ * ‖t ^ (s - 1)‖ ≤ d * t ^ (s - b - 1)

Tactic:
specialize hε' _ ht.1

Premises used: And.left
-- Module: Mathlib.Analysis.MellinTransform
Goal:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Membership.mem (γ := Set ℝ) (Ioi 0) y → ‖f y‖ ≤ d * ‖y ^ (-b)‖
t : ℝ
ht : t ∈ Ioo 0 ε
refine_2 : t < ε
⊢ dist t 0 < ε

Tactic:
rw [dist_eq_norm, sub_zero, norm_of_nonneg ht.1.le]

Premises used: dist_eq_norm, sub_zero, LT.lt.le, And.left, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.MellinTransform
Goal:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Membership.mem (γ := Set ℝ) (Ioi 0) y → ‖f y‖ ≤ d * ‖y ^ (-b)‖
t : ℝ
ht : t ∈ Ioo 0 ε
⊢ t < ε

Tactic:
ht.2

Premises used: And.right
-- Module: Mathlib.Analysis.MellinTransform
Goal:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Membership.mem (γ := Set ℝ) (Ioi 0) y → ‖f y‖ ≤ d * ‖y ^ (-b)‖
t : ℝ
ht : t ∈ Ioo 0 ε
⊢ t < ε

Tactic:
exact ht.2

Premises used: And.right
-- Module: Mathlib.Analysis.MellinTransform
Goal:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left : d > 0
ε : ℝ
hε : 0 < ε
t : ℝ
ht : t ∈ Ioo 0 ε
hε' : ‖f t‖ ≤ d * ‖t ^ (-b)‖
ha : 0 ≤ ‖t ^ (s - 1)‖
⊢ ‖f t‖ * ‖t ^ (s - 1)‖ ≤ d * ‖t ^ (-b)‖ * ‖t ^ (s - 1)‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.MellinTransform
Goal:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left : d > 0
ε : ℝ
hε : 0 < ε
t : ℝ
ht : t ∈ Ioo 0 ε
hε' : ‖f t‖ ≤ d * ‖t ^ (-b)‖
⊢ d * ‖t ^ (-b)‖ * ‖t ^ (s - 1)‖ = d * t ^ (s - b - 1)

Tactic:
?_
-- Module: Mathlib.Analysis.MellinTransform
Goal:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left : d > 0
ε : ℝ
hε : 0 < ε
t : ℝ
ht : t ∈ Ioo 0 ε
hε' : ‖f t‖ ≤ d * ‖t ^ (-b)‖
refine_2 : d * ‖t ^ (-b)‖ * ‖t ^ (s - 1)‖ = d * t ^ (s - b - 1)
⊢ ‖f t‖ * ‖t ^ (s - 1)‖ ≤ d * t ^ (s - b - 1)

Tactic:
calc _ ≤ d * ‖t ^ (-b)‖ * ‖t ^ (s - 1)‖ := by gcongr
          _ = d * t ^ (s - b - 1) := ?_

Premises used: HSub.hSub, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.MellinTransform
Goal:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left : d > 0
ε : ℝ
hε : 0 < ε
t : ℝ
ht : t ∈ Ioo 0 ε
hε' : ‖f t‖ ≤ d * ‖t ^ (-b)‖
refine_2 : d * (t ^ (-b) * t ^ (s - 1)) = d * t ^ (s - b - 1)
⊢ d * ‖t ^ (-b)‖ * ‖t ^ (s - 1)‖ = d * t ^ (s - b - 1)

Tactic:
simp_rw [norm_of_nonneg (rpow_nonneg ht.1.le _), mul_assoc]

Premises used: mul_assoc, LT.lt.le, And.left, Real.rpow_nonneg, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.MellinTransform
Goal:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left : d > 0
ε : ℝ
hε : 0 < ε
t : ℝ
ht : t ∈ Ioo 0 ε
hε' : ‖f t‖ ≤ d * ‖t ^ (-b)‖
refine_2 : d * t ^ (-b + (s - 1)) = d * t ^ (s - b - 1)
⊢ d * (t ^ (-b) * t ^ (s - 1)) = d * t ^ (s - b - 1)

Tactic:
rw [← rpow_add ht.1]

Premises used: And.left, Real.rpow_add
-- Module: Mathlib.Analysis.MellinTransform
Goal:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left : d > 0
ε : ℝ
hε : 0 < ε
t : ℝ
ht : t ∈ Ioo 0 ε
hε' : ‖f t‖ ≤ d * ‖t ^ (-b)‖
refine_2 : -b + (s - 1) = s - b - 1
⊢ d * t ^ (-b + (s - 1)) = d * t ^ (s - b - 1)

Tactic:
congr 2
-- Module: Mathlib.Analysis.MellinTransform
Goal:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
hf : IsBigO (F := ℝ) (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left : d > 0
ε : ℝ
hε : 0 < ε
t : ℝ
ht : t ∈ Ioo 0 ε
hε' : ‖f t‖ ≤ d * ‖t ^ (-b)‖
⊢ -b + (s - 1) = s - b - 1

Tactic:
abel
-- 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
obtain :
  ∀ (c1 : ℝ) (hc1 : 0 < c1)
    (hc1' : IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi c1) volume),
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi 0) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi 0) volume

Tactic:
obtain ⟨c1, hc1, hc1'⟩ := mellin_convergent_top_of_isBigO hfc.aestronglyMeasurable hf_top hs_top

Premises used: mellin_convergent_top_of_isBigO, MeasureTheory.LocallyIntegrableOn.aestronglyMeasurable
-- 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
obtain :
  ∀ (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
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi 0) volume

Tactic:
obtain ⟨c2, hc2, hc2'⟩ :=
    mellin_convergent_zero_of_isBigO hfc.aestronglyMeasurable hf_bot hs_bot

Premises used: mellin_convergent_zero_of_isBigO, MeasureTheory.LocallyIntegrableOn.aestronglyMeasurable
-- 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
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))
rw₃ rw₄ : Eq (α := Set ℝ) (Ioi 0) (Ioi 0)
⊢ Ioi 0 = Ioc 0 c2 ∪ Ioc c2 c1 ∪ Ioi c1

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]

Premises used: le_max_right, lt_min, LT.lt.le, min_le_left, min_eq_left, Set.Ioc_union_Ioi, Set.union_assoc, LE.le.trans
-- 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
⊢ 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]
-- 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
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
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi 0) volume

Tactic:
rw [this, integrableOn_union, integrableOn_union]

Premises used: MeasureTheory.integrableOn_union
-- 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
⊢ (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:
⟨⟨hc2', Iff.mp integrableOn_Icc_iff_integrableOn_Ioc ?_⟩, hc1'⟩

Premises used: And.intro, Iff.mp, integrableOn_Icc_iff_integrableOn_Ioc
-- 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
refine :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Icc c2 c1) volume
⊢ (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:
refine ⟨⟨hc2', Iff.mp integrableOn_Icc_iff_integrableOn_Ioc ?_⟩, hc1'⟩
-- 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
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Icc c2 c1) volume

Tactic:
(hfc.continuousOn_mul ?_ isOpen_Ioi.isLocallyClosed).integrableOn_compact_subset
      (fun t ht => (hc2.trans_le ht.1 : 0 < t)) isCompact_Icc

Premises used: MeasureTheory.LocallyIntegrableOn.continuousOn_mul, CompactIccSpace.isCompact_Icc, IsOpen.isLocallyClosed, isOpen_Ioi, And.left, MeasureTheory.LocallyIntegrableOn.integrableOn_compact_subset, LT.lt.trans_le
-- 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
t : ContinuousOn (Y := ℝ) (fun (t : ℝ) ↦ t ^ (s - 1)) (Ioi 0)
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Icc c2 c1) volume

Tactic:
refine
    (hfc.continuousOn_mul ?_ isOpen_Ioi.isLocallyClosed).integrableOn_compact_subset
      (fun t ht => (hc2.trans_le ht.1 : 0 < t)) isCompact_Icc

Premises used: MeasureTheory.LocallyIntegrableOn.continuousOn_mul, CompactIccSpace.isCompact_Icc, IsOpen.isLocallyClosed, isOpen_Ioi, MeasureTheory.LocallyIntegrableOn.integrableOn_compact_subset, LT.lt.trans_le