awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
z : ℂ
hz : ‖s - z‖ < v
h : t < 1
hz' : (s - z).re ≤ v
⊢ s.re - v ≤ z.re
have hbc : ∀ (hz' : s.re - z.re ≤ v), s.re - v ≤ z.re
Tactic: rwa [sub_re, sub_le_iff_le_add, ← sub_le_iff_le_add'] at hz'
Cleared hypotheses: hz'
-- 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
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
z : ℂ
hz : ‖s - z‖ < v
h : t < 1
hz' : (s - z).re ≤ v
hbc : ∀ (hz' : s.re - z.re ≤ v), s.re - v ≤ z.re
⊢ s.re - v ≤ z.re
have hbc₁ : ∀ (hz' : s.re ≤ v + z.re), s.re - v ≤ z.re
Tactic: rwa [sub_re, sub_le_iff_le_add, ← sub_le_iff_le_add'] at hz'
Cleared hypotheses: hz'
-- 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
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
z : ℂ
hz : ‖s - z‖ < v
h : t < 1
hz' : (s - z).re ≤ v
hbc : ∀ (hz' : s.re - z.re ≤ v), s.re - v ≤ z.re
hbc₁ : ∀ (hz' : s.re ≤ v + z.re), s.re - v ≤ z.re
⊢ s.re - v ≤ z.re
have hbc₂ : ∀ (hz' : s.re - v ≤ z.re), s.re - v ≤ z.re
Tactic: rwa [sub_re, sub_le_iff_le_add, ← sub_le_iff_le_add'] at hz'
Cleared hypotheses: hz'
-- 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))
h2 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (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 h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
Tactic: have h4 : ∀ᵐ t : ℝ ∂volume.restrict (Ioi 0),
      ∀ z : ℂ, z ∈ Metric.ball s v → ‖F' z t‖ ≤ bound t := by
    refine (ae_restrict_mem measurableSet_Ioi).mono fun t ht z hz => ?_
    simp_rw [F', bound, norm_smul, norm_mul, norm_real, mul_assoc, norm_eq_abs]
    gcongr
    rw [norm_cpow_eq_rpow_re_of_pos ht]
    rcases le_or_gt 1 t with h | h
    · refine le_add_of_le_of_nonneg (rpow_le_rpow_of_exponent_le h ?_)
        (by positivity)
      rw [sub_re, one_re, sub_le_sub_iff_right]
      rw [mem_ball_iff_norm] at hz
      have hz' := (re_le_norm _).trans hz.le
      rwa [sub_re, sub_le_iff_le_add'] at hz'
    · refine
        le_add_of_nonneg_of_le (rpow_pos_of_pos ht _).le (rpow_le_rpow_of_exponent_ge ht h.le ?_)
      rw [sub_re, one_re, sub_le_iff_le_add, sub_add_cancel]
      rw [mem_ball_iff_norm'] at hz
      have hz' := (re_le_norm _).trans hz.le
      rwa [sub_re, sub_le_iff_le_add, ← sub_le_iff_le_add'] at hz'
-- 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
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) bound (Ioi 0) volume
have simp_rw : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
  (fun (t : ℝ) ↦ t ^ (s.re + v - 1) * (|log t| * ‖f t‖) + t ^ (s.re - v - 1) * (|log t| * ‖f t‖)) (Ioi 0) volume
Tactic: simp_rw [bound, add_mul, mul_assoc]
-- 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
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
this :
  ∀ {j : ℝ},
    b < j →
      j < a →
        IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (j - 1) * (|log t| * ‖f t‖))
          (Ioi 0) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ t ^ (s.re + v - 1) * (|log t| * ‖f t‖) + t ^ (s.re - v - 1) * (|log t| * ‖f t‖)) (Ioi 0) volume
have refine_1 : b < s.re + v
Tactic: refine Integrable.add (this ?_ ?_) (this ?_ ?_)
-- 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
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
this :
  ∀ {j : ℝ},
    b < j →
      j < a →
        IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (j - 1) * (|log t| * ‖f t‖))
          (Ioi 0) volume
refine_1 : b < s.re + v
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ t ^ (s.re + v - 1) * (|log t| * ‖f t‖) + t ^ (s.re - v - 1) * (|log t| * ‖f t‖)) (Ioi 0) volume
have refine_2 : s.re + v < a
Tactic: refine Integrable.add (this ?_ ?_) (this ?_ ?_)
-- 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
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
this :
  ∀ {j : ℝ},
    b < j →
      j < a →
        IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (j - 1) * (|log t| * ‖f t‖))
          (Ioi 0) volume
refine_1 : b < s.re + v
refine_2 : s.re + v < a
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ t ^ (s.re + v - 1) * (|log t| * ‖f t‖) + t ^ (s.re - v - 1) * (|log t| * ‖f t‖)) (Ioi 0) volume
have refine_3 : b < s.re - v
Tactic: refine Integrable.add (this ?_ ?_) (this ?_ ?_)
-- 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
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
this :
  ∀ {j : ℝ},
    b < j →
      j < a →
        IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (j - 1) * (|log t| * ‖f t‖))
          (Ioi 0) volume
refine_1 : b < s.re + v
refine_2 : s.re + v < a
refine_3 : b < s.re - v
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ t ^ (s.re + v - 1) * (|log t| * ‖f t‖) + t ^ (s.re - v - 1) * (|log t| * ‖f t‖)) (Ioi 0) volume
have refine_4 : s.re - v < a
Tactic: refine Integrable.add (this ?_ ?_) (this ?_ ?_)
-- 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
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
this :
  ∀ {j : ℝ},
    b < j →
      j < a →
        IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (j - 1) * (|log t| * ‖f t‖))
          (Ioi 0) volume
⊢ b < s.re + v
have linarith : s.re + v ≤ b → 2 * (0 - v) + (v - (s.re - b)) + (s.re + v - b) = 0
Tactic: linarith
-- 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
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
this :
  ∀ {j : ℝ},
    b < j →
      j < a →
        IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (j - 1) * (|log t| * ‖f t‖))
          (Ioi 0) volume
linarith : s.re + v ≤ b → 2 * (0 - v) + (v - (s.re - b)) + (s.re + v - b) = 0
⊢ b < s.re + v
have linarith₁ : s.re + v ≤ b → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
this :
  ∀ {j : ℝ},
    b < j →
      j < a →
        IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (j - 1) * (|log t| * ‖f t‖))
          (Ioi 0) volume
⊢ s.re + v < a
have linarith : a ≤ s.re + v → v - (a - s.re) + (a - (s.re + v)) = 0
Tactic: linarith
-- 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
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
this :
  ∀ {j : ℝ},
    b < j →
      j < a →
        IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (j - 1) * (|log t| * ‖f t‖))
          (Ioi 0) volume
⊢ b < s.re - v
have linarith : s.re - v ≤ b → v - (s.re - b) + (s.re - v - b) = 0
Tactic: linarith
-- 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
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
this :
  ∀ {j : ℝ},
    b < j →
      j < a →
        IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (j - 1) * (|log t| * ‖f t‖))
          (Ioi 0) volume
⊢ s.re - v < a
have linarith : a ≤ s.re - v → 2 * (0 - v) + (v - (a - s.re)) + (a - (s.re - v)) = 0
Tactic: linarith
-- 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
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
this :
  ∀ {j : ℝ},
    b < j →
      j < a →
        IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (j - 1) * (|log t| * ‖f t‖))
          (Ioi 0) volume
linarith : a ≤ s.re - v → 2 * (0 - v) + (v - (a - s.re)) + (a - (s.re - v)) = 0
⊢ s.re - v < a
have linarith₁ : a ≤ s.re - v → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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
h3 : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (F' s) (Measure.restrict volume (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ t ^ (s.re + v - 1) * (|log t| * ‖f t‖) + t ^ (s.re - v - 1) * (|log t| * ‖f t‖)) (Ioi 0) volume
have suffices : ∀ {j : ℝ},
  b < j →
    j < a →
      IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (j - 1) * (|log t| * ‖f t‖))
        (Ioi 0) volume
Tactic: suffices ∀ {j : ℝ}, b < j → j < a →
        IntegrableOn (fun t : ℝ => t ^ (j - 1) * (|log t| * ‖f t‖)) (Ioi 0) volume by
      refine Integrable.add (this ?_ ?_) (this ?_ ?_)
      all_goals linarith