awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)))
have refine_1 : AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1))
  (Measure.restrict volume (Ioi (max e 1)))
Tactic: refine AEStronglyMeasurable.mul ?_ (hfc.mono_set (Ioi_subset_Ioi he'.le))
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)))
have refine_1 : ∀ (t : ℝ) (ht : t ∈ Ioi (max e 1)), ContinuousAt (Y := ℝ) (fun (t : ℝ) ↦ t ^ (s - 1)) t
Tactic: refine (continuousOn_of_forall_continuousAt fun t ht => ?_).aestronglyMeasurable
      measurableSet_Ioi
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
have refine : ∀ (t : ℝ) (ht : t ∈ 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 => ?_
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (hypothesis)
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)
⊢ ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d
have ht' : 0 < t
Tactic: have ht' : 0 < t := he'.trans ht
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
⊢ ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d
have rw : t ^ (s - 1) * ‖f t‖ ≤ t ^ (s - 1) * (d * ‖t ^ (-a)‖)
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 _)]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
⊢ t ^ (s - 1) * ‖f t‖ ≤ t ^ (s - 1) * (d * ‖t ^ (-a)‖)
have hbc : ‖f t‖ ≤ d * ‖t ^ (-a)‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (hypothesis)
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
⊢ @HasFiniteIntegral _ ℝ _ Real.measurableSpace (fun (t : ℝ) ↦ t ^ (s - 1) * f t)
    (Measure.restrict volume (Ioi (max e 1)))
have this : ∀ᵐ (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
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)))
have refine_2 : @HasFiniteIntegral _ ℝ _ Real.measurableSpace (fun (a_1 : ℝ) ↦ a_1 ^ (s - 1 + -a))
  (Measure.restrict volume (Ioi (max e 1)))
Tactic: refine (HasFiniteIntegral.mul_const ?_ _).mono' this
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
⊢ s - 1 + -a < -1
have linarith : -1 ≤ s - 1 + -a → s - a + (-1 - (s - 1 + -a)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
⊢ ∃ (c : ℝ),
    0 < c ∧ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioc 0 c) volume
have 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
Tactic: obtain ⟨d, _, hd'⟩ := hf.exists_pos
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (hypothesis)
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)
⊢ ∃ (c : ℝ),
    0 < c ∧ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioc 0 c) volume
have hd'₁ : ∃ (ε : ℝ), 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'
Cleared hypotheses: hd'
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)‖
⊢ ∃ (c : ℝ),
    0 < c ∧ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioc 0 c) volume
have 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
Tactic: obtain ⟨ε, hε, hε'⟩ := hd'
Cleared hypotheses: hd'
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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
have refine_1 : AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t)
  (Measure.restrict volume (Ioo 0 ε))
Tactic: refine ⟨ε, hε, Iff.mpr integrableOn_Ioc_iff_integrableOn_Ioo ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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 ε))
⊢ ∃ (c : ℝ),
    0 < c ∧ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioc 0 c) volume
have refine_2 : @HasFiniteIntegral _ ℝ _ Real.measurableSpace (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Measure.restrict volume (Ioo 0 ε))
Tactic: refine ⟨ε, hε, Iff.mpr integrableOn_Ioc_iff_integrableOn_Ioo ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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 ε))
have refine_1 : AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1))
  (Measure.restrict volume (Ioo 0 ε))
Tactic: refine AEStronglyMeasurable.mul ?_ (hfc.mono_set Ioo_subset_Ioi_self)
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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 ε))
have refine_1 : ∀ (t : ℝ) (ht : t ∈ Ioo 0 ε), ContinuousAt (Y := ℝ) (fun (t : ℝ) ↦ t ^ (s - 1)) t
Tactic: refine (continuousOn_of_forall_continuousAt fun t ht => ?_).aestronglyMeasurable
      measurableSet_Ioo
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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 : ℝ) ↦ t ^ (s - 1) * f t) (Measure.restrict volume (Ioo 0 ε))
have refine_2 : @HasFiniteIntegral _ ℝ _ Real.measurableSpace (fun (t : ℝ) ↦ d * t ^ (s - b - 1)) (Measure.restrict volume (Ioo 0 ε))
Tactic: apply HasFiniteIntegral.mono'
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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 ε))
⊢ @HasFiniteIntegral _ ℝ _ Real.measurableSpace (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Measure.restrict volume (Ioo 0 ε))
have refine_2₁ : ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioo 0 ε), ‖a ^ (s - 1) * f a‖ ≤ d * a ^ (s - b - 1)
Tactic: apply HasFiniteIntegral.mono'
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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 ε))
have refine_2 : @Integrable ℝ _ _ _ Real.measurableSpace (fun (t : ℝ) ↦ t ^ (s - b - 1)) (Measure.restrict volume (Ioo 0 ε))
Tactic: refine (Integrable.hasFiniteIntegral ?_).const_mul _
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)‖
⊢ @Integrable ℝ _ _ _ Real.measurableSpace (fun (t : ℝ) ↦ t ^ (s - b - 1)) (Measure.restrict volume (Ioo 0 ε))
have refine_2 : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ t ^ (s - b - 1)) volume 0 ε
Tactic: rw [← IntegrableOn, ← integrableOn_Ioc_iff_integrableOn_Ioo, ←
        intervalIntegrable_iff_integrableOn_Ioc_of_le hε.le]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)‖
⊢ -1 < s - b - 1
have linarith : s - b - 1 ≤ -1 → b - s + (s - b - 1 - -1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)
have refine_2 : ∀ (t : ℝ) (ht : t ∈ Ioo 0 ε), ‖t ^ (s - 1) * f t‖ ≤ d * t ^ (s - b - 1)
Tactic: refine (ae_restrict_iff' measurableSet_Ioo).mpr (Eventually.of_forall fun t ht => ?_)
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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 ^ (s - 1) * f t‖ ≤ d * t ^ (s - b - 1)
have refine_2 : ‖f t‖ * ‖t ^ (s - 1)‖ ≤ d * t ^ (s - b - 1)
Tactic: rw [mul_comm, norm_mul]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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 ε
⊢ ‖f t‖ * ‖t ^ (s - 1)‖ ≤ d * t ^ (s - b - 1)
have refine_2 : dist t 0 < ε
Tactic: specialize hε' _ ht.1
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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 < ε
⊢ ‖f t‖ * ‖t ^ (s - 1)‖ ≤ d * t ^ (s - b - 1)
have refine_2₁ : ∀ (hε' : ‖f t‖ ≤ d * ‖t ^ (-b)‖), ‖f t‖ * ‖t ^ (s - 1)‖ ≤ d * t ^ (s - b - 1)
Tactic: specialize hε' _ ht.1
Cleared hypotheses: hε'
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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 ε
⊢ dist t 0 < ε
have refine_2 : t < ε
Tactic: rw [dist_eq_norm, sub_zero, norm_of_nonneg ht.1.le]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)‖
⊢ ‖f t‖ * ‖t ^ (s - 1)‖ ≤ d * ‖t ^ (-b)‖ * ‖t ^ (s - 1)‖
have ha : 0 ≤ ‖t ^ (s - 1)‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)‖
⊢ ‖f t‖ * ‖t ^ (s - 1)‖ ≤ d * t ^ (s - b - 1)
have refine_2 : d * ‖t ^ (-b)‖ * ‖t ^ (s - 1)‖ = d * t ^ (s - b - 1)
Tactic: calc _ ≤ d * ‖t ^ (-b)‖ * ‖t ^ (s - 1)‖ := by gcongr
          _ = d * t ^ (s - b - 1) := ?_
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)
have refine_2 : d * (t ^ (-b) * t ^ (s - 1)) = d * t ^ (s - b - 1)
Tactic: simp_rw [norm_of_nonneg (rpow_nonneg ht.1.le _), mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)
have refine_2 : d * t ^ (-b + (s - 1)) = d * t ^ (s - b - 1)
Tactic: rw [← rpow_add ht.1]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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 + (s - 1)) = d * t ^ (s - b - 1)
have refine_2 : -b + (s - 1) = s - b - 1
Tactic: congr 2
-- 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
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi 0) volume
have 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
Tactic: obtain ⟨c1, hc1, hc1'⟩ := mellin_convergent_top_of_isBigO hfc.aestronglyMeasurable hf_top hs_top
-- 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
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi 0) volume
have 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
Tactic: obtain ⟨c2, hc2, hc2'⟩ :=
    mellin_convergent_zero_of_isBigO hfc.aestronglyMeasurable hf_bot hs_bot
-- 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
⊢ Ioi 0 = Ioc 0 c2 ∪ Ioc c2 c1 ∪ Ioi c1
have rw : 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]
-- 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)
⊢ Ioi 0 = Ioc 0 c2 ∪ Ioc c2 c1 ∪ Ioi c1
have rw₁ : Ioi 0 = Ioc 0 c2 ∪ Ioi (min c2 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]
-- 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)
⊢ Ioi 0 = Ioc 0 c2 ∪ Ioc c2 c1 ∪ Ioi c1
have rw₂ : Ioi 0 = Ioi (min 0 (min c2 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]