awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
T : Set ℝ
hT : T ⊆ Ioi 0
hT' : MeasurableSet T
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
s : ℂ
⊢ ∀ x ∈ T, ContinuousAt (Y := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1)) x

Tactic:
exact fun t ht => continuousAt_ofReal_cpow_const _ _ (Or.inr <| ne_of_gt (hT 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
f : ℝ → E
T : Set ℝ
hT : T ⊆ Ioi 0
hT' : MeasurableSet T
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
s : ℂ
⊢ AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t)
    (Measure.restrict volume T)

Tactic:
have : AEStronglyMeasurable (fun t : ℝ => (t : ℂ) ^ (s - 1) • f t) (volume.restrict T) := by
    refine ((continuousOn_of_forall_continuousAt ?_).aestronglyMeasurable hT').smul
      (hfc.mono_set hT)
    exact fun t ht => continuousAt_ofReal_cpow_const _ _ (Or.inr <| ne_of_gt (hT ht))
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
T : Set ℝ
hT : T ⊆ Ioi 0
hT' : MeasurableSet T
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
s : ℂ
this :
  AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t)
    (Measure.restrict volume T)
rw :
  IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (a : ℝ) ↦ ‖(↑a : ℂ) ^ (s - 1) • f a‖) T volume ↔
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s.re - 1) * ‖f t‖) T volume
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t) T
      volume ↔
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s.re - 1) * ‖f t‖) T volume

Tactic:
rw [IntegrableOn, ← integrable_norm_iff this, ← IntegrableOn]

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.integrable_norm_iff
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
T : Set ℝ
hT : T ⊆ Ioi 0
hT' : MeasurableSet T
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
s : ℂ
this :
  AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t)
    (Measure.restrict volume T)
⊢ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (a : ℝ) ↦ ‖(↑a : ℂ) ^ (s - 1) • f a‖) T volume ↔
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s.re - 1) * ‖f t‖) T volume

Tactic:
integrableOn_congr_fun (fun t ht => ?_) hT'

Premises used: MeasureTheory.integrableOn_congr_fun
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
T : Set ℝ
hT : T ⊆ Ioi 0
hT' : MeasurableSet T
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
s : ℂ
this :
  AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t)
    (Measure.restrict volume T)
refine : ∀ (t : ℝ) (ht : t ∈ T), ‖(↑t : ℂ) ^ (s - 1) • f t‖ = t ^ (s.re - 1) * ‖f t‖
⊢ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (a : ℝ) ↦ ‖(↑a : ℂ) ^ (s - 1) • f a‖) T volume ↔
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s.re - 1) * ‖f t‖) T volume

Tactic:
refine integrableOn_congr_fun (fun t ht => ?_) hT'

Premises used: MeasureTheory.integrableOn_congr_fun
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
T : Set ℝ
hT : T ⊆ Ioi 0
hT' : MeasurableSet T
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
s : ℂ
this :
  AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t)
    (Measure.restrict volume T)
t : ℝ
ht : t ∈ T
simp_rw : ‖(↑t : ℂ) ^ (s - 1)‖ * ‖f t‖ = t ^ (s.re - 1) * ‖f t‖
simp_rw₁ : t ^ (s - 1).re * ‖f t‖ = t ^ (s.re - 1) * ‖f t‖
simp_rw₂ : t ^ (s.re - re 1) * ‖f t‖ = t ^ (s.re - 1) * ‖f t‖
⊢ ‖(↑t : ℂ) ^ (s - 1) • f t‖ = t ^ (s.re - 1) * ‖f t‖

Tactic:
simp_rw [norm_smul, norm_cpow_eq_rpow_re_of_pos (hT ht), sub_re, one_re]

Premises used: norm_smul, Complex.sub_re, Complex.one_re, Complex.norm_cpow_eq_rpow_re_of_pos
-- Module: Mathlib.Analysis.MellinTransform
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
obtain :
  ∀ (d : ℝ) (hd' : IsBigOWith (F := ℝ) d atTop f fun (x : ℝ) ↦ x ^ (-a)),
    ∃ (c : ℝ),
      0 < c ∧ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi c) volume
⊢ ∃ (c : ℝ), 0 < c ∧ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi c) volume

Tactic:
obtain ⟨d, hd'⟩ := hf.isBigOWith

Premises used: Asymptotics.IsBigO.isBigOWith
-- Module: Mathlib.Analysis.MellinTransform
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d : ℝ
hd' : IsBigOWith (F := ℝ) d atTop f fun (x : ℝ) ↦ x ^ (-a)
⊢ ∃ (a_1 : ℝ), ∀ b ≥ a_1, ‖f b‖ ≤ d * ‖b ^ (-a)‖

Tactic:
simp_rw [IsBigOWith, eventually_atTop] at hd'

Premises used: Asymptotics.IsBigOWith, Filter.eventually_atTop
-- Module: Mathlib.Analysis.MellinTransform
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d : ℝ
hd' : ∃ (a_1 : ℝ), ∀ b ≥ a_1, ‖f b‖ ≤ d * ‖b ^ (-a)‖
obtain :
  ∀ (e : ℝ) (he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖),
    ∃ (c : ℝ),
      0 < c ∧ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi c) volume
⊢ ∃ (c : ℝ), 0 < c ∧ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi c) volume

Tactic:
obtain ⟨e, he⟩ := hd'
-- Module: Mathlib.Analysis.MellinTransform
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
⊢ 0 < max e 1

Tactic:
have he' : 0 < max e 1 := zero_lt_one.trans_le (le_max_right _ _)
-- Module: Mathlib.Analysis.MellinTransform
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
⊢ ∃ (c : ℝ), 0 < c ∧ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi c) volume

Tactic:
⟨max e 1, he', ?_, ?_⟩

Premises used: Max.max, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.MellinTransform
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
refine_1 :
  AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t)
    (Measure.restrict volume (Ioi (max e 1)))
refine_2 :
  @HasFiniteIntegral _ ℝ _ Real.measurableSpace (fun (t : ℝ) ↦ t ^ (s - 1) * f t)
    (Measure.restrict volume (Ioi (max e 1)))
⊢ ∃ (c : ℝ), 0 < c ∧ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi c) volume

Tactic:
refine ⟨max e 1, he', ?_, ?_⟩
-- Module: Mathlib.Analysis.MellinTransform
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t)
    (Measure.restrict volume (Ioi (max e 1)))

Tactic:
AEStronglyMeasurable.mul ?_ (hfc.mono_set (Ioi_subset_Ioi he'.le))

Premises used: LT.lt.le, MeasureTheory.AEStronglyMeasurable.mono_set, Set.Ioi_subset_Ioi, MeasureTheory.AEStronglyMeasurable.mul
-- Module: Mathlib.Analysis.MellinTransform
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
refine_1 :
  AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1))
    (Measure.restrict volume (Ioi (max e 1)))
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t)
    (Measure.restrict volume (Ioi (max e 1)))

Tactic:
refine AEStronglyMeasurable.mul ?_ (hfc.mono_set (Ioi_subset_Ioi he'.le))

Premises used: LT.lt.le, MeasureTheory.AEStronglyMeasurable.mono_set, Set.Ioi_subset_Ioi, MeasureTheory.AEStronglyMeasurable.mul
-- Module: Mathlib.Analysis.MellinTransform
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1))
    (Measure.restrict volume (Ioi (max e 1)))

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

Premises used: continuousOn_of_forall_continuousAt, ContinuousOn.aestronglyMeasurable, measurableSet_Ioi
-- Module: Mathlib.Analysis.MellinTransform
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
refine_1 : ∀ (t : ℝ) (ht : t ∈ Ioi (max e 1)), ContinuousAt (Y := ℝ) (fun (t : ℝ) ↦ t ^ (s - 1)) t
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1))
    (Measure.restrict volume (Ioi (max e 1)))

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

Premises used: continuousOn_of_forall_continuousAt, ContinuousOn.aestronglyMeasurable, measurableSet_Ioi
-- Module: Mathlib.Analysis.MellinTransform
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
t : ℝ
ht : t ∈ Ioi (max e 1)
⊢ ContinuousAt (Y := ℝ) (fun (t : ℝ) ↦ t ^ (s - 1)) t

Tactic:
continuousAt_rpow_const _ _ (Or.inl <| (he'.trans ht).ne')

Premises used: Real.continuousAt_rpow_const, LT.lt.ne', LT.lt.trans, Or.inl
-- Module: Mathlib.Analysis.MellinTransform
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
t : ℝ
ht : t ∈ Ioi (max e 1)
⊢ ContinuousAt (Y := ℝ) (fun (t : ℝ) ↦ t ^ (s - 1)) t

Tactic:
exact continuousAt_rpow_const _ _ (Or.inl <| (he'.trans ht).ne')

Premises used: Real.continuousAt_rpow_const, LT.lt.ne', LT.lt.trans, Or.inl
-- Module: Mathlib.Analysis.MellinTransform
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
⊢ ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi (max e 1)), ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d

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

Premises used: MeasureTheory.ae_restrict_mem, measurableSet_Ioi, Filter.Eventually.mono
-- Module: Mathlib.Analysis.MellinTransform
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
refine : ∀ (t : ℝ) (ht : t ∈ Ioi (max e 1)), ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d
⊢ ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi (max e 1)), ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d

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

Premises used: MeasureTheory.ae_restrict_mem, measurableSet_Ioi, Filter.Eventually.mono
-- Module: Mathlib.Analysis.MellinTransform
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
t : ℝ
ht : t ∈ Ioi (max e 1)
⊢ 0 < t

Tactic:
have ht' : 0 < t := he'.trans ht
-- Module: Mathlib.Analysis.MellinTransform
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
t : ℝ
ht : t ∈ Ioi (max e 1)
ht' : 0 < t
rw : t ^ (s - 1) * ‖f t‖ ≤ t ^ (s - 1) * (d * ‖t ^ (-a)‖)
⊢ ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d

Tactic:
rw [norm_mul, rpow_add ht', ← norm_of_nonneg (rpow_nonneg ht'.le (-a)), mul_assoc,
        mul_comm _ d, norm_of_nonneg (rpow_nonneg ht'.le _)]

Premises used: mul_assoc, LT.lt.le, norm_mul, mul_comm, Real.rpow_add, Real.rpow_nonneg, Neg.neg, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.MellinTransform
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
t : ℝ
ht : t ∈ Ioi (max e 1)
ht' : 0 < t
hbc : ‖f t‖ ≤ d * ‖t ^ (-a)‖
⊢ t ^ (s - 1) * ‖f t‖ ≤ t ^ (s - 1) * (d * ‖t ^ (-a)‖)

Tactic:
gcongr
-- Module: Mathlib.Analysis.MellinTransform
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
t : ℝ
ht : t ∈ Ioi (max e 1)
ht' : 0 < t
⊢ ‖f t‖ ≤ d * ‖t ^ (-a)‖

Tactic:
he t ((le_max_left e 1).trans_lt ht).le

Premises used: LT.lt.le, OfNat.ofNat, le_max_left, LE.le.trans_lt
-- Module: Mathlib.Analysis.MellinTransform
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
t : ℝ
ht : t ∈ Ioi (max e 1)
ht' : 0 < t
⊢ ‖f t‖ ≤ d * ‖t ^ (-a)‖

Tactic:
exact he t ((le_max_left e 1).trans_lt ht).le

Premises used: LT.lt.le, OfNat.ofNat, le_max_left, LE.le.trans_lt
-- Module: Mathlib.Analysis.MellinTransform
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
⊢ ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi (max e 1)), ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d

Tactic:
have : ∀ᵐ t : ℝ ∂volume.restrict (Ioi <| max e 1),
        ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d := by
      refine (ae_restrict_mem measurableSet_Ioi).mono fun t ht => ?_
      have ht' : 0 < t := he'.trans ht
      rw [norm_mul, rpow_add ht', ← norm_of_nonneg (rpow_nonneg ht'.le (-a)), mul_assoc,
        mul_comm _ d, norm_of_nonneg (rpow_nonneg ht'.le _)]
      gcongr
      exact he t ((le_max_left e 1).trans_lt ht).le
-- Module: Mathlib.Analysis.MellinTransform
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
this : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi (max e 1)), ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d
⊢ @HasFiniteIntegral _ ℝ _ Real.measurableSpace (fun (t : ℝ) ↦ t ^ (s - 1) * f t)
    (Measure.restrict volume (Ioi (max e 1)))

Tactic:
(HasFiniteIntegral.mul_const ?_ _).mono' this

Premises used: MeasureTheory.HasFiniteIntegral.mul_const, MeasureTheory.HasFiniteIntegral.mono'
-- Module: Mathlib.Analysis.MellinTransform
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
this : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi (max e 1)), ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d
refine_2 :
  @HasFiniteIntegral _ ℝ _ Real.measurableSpace (fun (a_1 : ℝ) ↦ a_1 ^ (s - 1 + -a))
    (Measure.restrict volume (Ioi (max e 1)))
⊢ @HasFiniteIntegral _ ℝ _ Real.measurableSpace (fun (t : ℝ) ↦ t ^ (s - 1) * f t)
    (Measure.restrict volume (Ioi (max e 1)))

Tactic:
refine (HasFiniteIntegral.mul_const ?_ _).mono' this

Premises used: MeasureTheory.HasFiniteIntegral.mul_const, MeasureTheory.HasFiniteIntegral.mono'
-- Module: Mathlib.Analysis.MellinTransform
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
this : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi (max e 1)), ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d
linarith : -1 ≤ s - 1 + -a → s - a + (-1 - (s - 1 + -a)) = 0
⊢ s - 1 + -a < -1

Tactic:
linarith
-- Module: Mathlib.Analysis.MellinTransform
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
this : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi (max e 1)), ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d
⊢ @HasFiniteIntegral _ ℝ _ Real.measurableSpace (fun (a_1 : ℝ) ↦ a_1 ^ (s - 1 + -a))
    (Measure.restrict volume (Ioi (max e 1)))

Tactic:
exact (integrableOn_Ioi_rpow_of_lt (by linarith) he').hasFiniteIntegral

Premises used: integrableOn_Ioi_rpow_of_lt, 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
obtain :
  ∀ d > 0,
    ∀ (hd' : IsBigOWith (F := ℝ) d (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)),
      ∃ (c : ℝ),
        0 < c ∧ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioc 0 c) volume
⊢ ∃ (c : ℝ),
    0 < c ∧ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioc 0 c) volume

Tactic:
obtain ⟨d, _, hd'⟩ := hf.exists_pos

Premises used: Asymptotics.IsBigO.exists_pos
-- 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
hd' : IsBigOWith (F := ℝ) d (𝓝[>] 0) f fun (x : ℝ) ↦ x ^ (-b)
⊢ ∃ (ε : ℝ), 0 < ε ∧ ∀ ⦃y : ℝ⦄, dist y 0 < ε → Membership.mem (γ := Set ℝ) (Ioi 0) y → ‖f y‖ ≤ d * ‖y ^ (-b)‖

Tactic:
simp_rw [IsBigOWith, eventually_nhdsWithin_iff, Metric.eventually_nhds_iff, gt_iff_lt] at hd'

Premises used: Asymptotics.IsBigOWith, Metric.eventually_nhds_iff, eventually_nhdsWithin_iff, gt_iff_lt
-- 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
hd' : ∃ (ε : ℝ), 0 < ε ∧ ∀ ⦃y : ℝ⦄, dist y 0 < ε → Membership.mem (γ := Set ℝ) (Ioi 0) y → ‖f y‖ ≤ d * ‖y ^ (-b)‖
obtain :
  ∀ (ε : ℝ) (hε : 0 < ε)
    (hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Membership.mem (γ := Set ℝ) (Ioi 0) y → ‖f y‖ ≤ d * ‖y ^ (-b)‖),
    ∃ (c : ℝ),
      0 < c ∧ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioc 0 c) volume
⊢ ∃ (c : ℝ),
    0 < c ∧ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioc 0 c) volume

Tactic:
obtain ⟨ε, hε, hε'⟩ := hd'
-- 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)‖
⊢ ∃ (c : ℝ),
    0 < c ∧ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioc 0 c) volume

Tactic:
⟨ε, hε, Iff.mpr integrableOn_Ioc_iff_integrableOn_Ioo ⟨?_, ?_⟩⟩

Premises used: Iff.mpr, And.intro, Exists.intro, 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)‖
refine_1 :
  AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t)
    (Measure.restrict volume (Ioo 0 ε))
refine_2 :
  @HasFiniteIntegral _ ℝ _ Real.measurableSpace (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Measure.restrict volume (Ioo 0 ε))
⊢ ∃ (c : ℝ),
    0 < c ∧ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioc 0 c) volume

Tactic:
refine ⟨ε, hε, Iff.mpr 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)‖
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t)
    (Measure.restrict volume (Ioo 0 ε))

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

Premises used: MeasureTheory.AEStronglyMeasurable.mono_set, Set.Ioo_subset_Ioi_self, MeasureTheory.AEStronglyMeasurable.mul