-- Mathlib/Analysis/MellinTransform.lean
theorem mellin_convergent_top_of_isBigO {f : ℝ → ℝ}
    (hfc : AEStronglyMeasurable f <| volume.restrict (Ioi 0)) {a s : ℝ}
    (hf : f =O[atTop] (· ^ (-a))) (hs : s < a) :
    ∃ c : ℝ, 0 < c ∧ IntegrableOn (fun t : ℝ => t ^ (s - 1) * f t) (Ioi c)

Proof state:
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < e ⊔ 1
⊢ ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi (e ⊔ 1)), ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d

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

Result:
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < e ⊔ 1
t : ℝ
ht : t ∈ Ioi (e ⊔ 1)
⊢ ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d

Proof state:
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
⊢ ∃ c, 0 < c ∧ IntegrableOn (fun t => t ^ (s - 1) * f t) (Ioi c) volume

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

Result:
case intro
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d : ℝ
hd' : IsBigOWith d atTop f fun x => x ^ (-a)
⊢ ∃ c, 0 < c ∧ IntegrableOn (fun t => t ^ (s - 1) * f t) (Ioi c) volume

Proof state:
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < e ⊔ 1
this : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi (e ⊔ 1)), ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d
⊢ s - 1 + -a < -1

Tactic:
linarith

Result:
no goals

Proof state:
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < e ⊔ 1
t : ℝ
ht : t ∈ Ioi (e ⊔ 1)
ht' : 0 < t
⊢ t ^ (s - 1) * ‖f t‖ ≤ t ^ (s - 1) * (d * ‖t ^ (-a)‖)

Tactic:
gcongr

Result:
case h
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < e ⊔ 1
t : ℝ
ht : t ∈ Ioi (e ⊔ 1)
ht' : 0 < t
⊢ ‖f t‖ ≤ d * ‖t ^ (-a)‖

Proof state:
case intro
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d : ℝ
hd' : IsBigOWith d atTop f fun x => x ^ (-a)
⊢ ∃ c, 0 < c ∧ IntegrableOn (fun t => t ^ (s - 1) * f t) (Ioi c) volume

Tactic:
simp_rw [IsBigOWith, eventually_atTop] at hd'

Result:
case intro
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d : ℝ
hd' : ∃ a_1, ∀ b ≥ a_1, ‖f b‖ ≤ d * ‖b ^ (-a)‖
⊢ ∃ c, 0 < c ∧ IntegrableOn (fun t => t ^ (s - 1) * f t) (Ioi c) volume

Proof state:
case intro.intro.refine_1
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < e ⊔ 1
t : ℝ
ht : t ∈ Ioi (e ⊔ 1)
⊢ ContinuousAt (fun t => t ^ (s - 1)) t

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

Result:
no goals

Proof state:
case intro.intro
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < e ⊔ 1
⊢ ∃ c, 0 < c ∧ IntegrableOn (fun t => t ^ (s - 1) * f t) (Ioi c) volume

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

Result:
case intro.intro.refine_1
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < e ⊔ 1
⊢ AEStronglyMeasurable (fun t => t ^ (s - 1) * f t) (volume.restrict (Ioi (e ⊔ 1)))

case intro.intro.refine_2
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < e ⊔ 1
⊢ HasFiniteIntegral (fun t => t ^ (s - 1) * f t) (volume.restrict (Ioi (e ⊔ 1)))

Proof state:
case intro.intro.refine_2
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < e ⊔ 1
⊢ HasFiniteIntegral (fun t => t ^ (s - 1) * f t) (volume.restrict (Ioi (e ⊔ 1)))

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

Result:
case intro.intro.refine_2
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < e ⊔ 1
this : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi (e ⊔ 1)), ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d
⊢ HasFiniteIntegral (fun t => t ^ (s - 1) * f t) (volume.restrict (Ioi (e ⊔ 1)))

Proof state:
case intro.intro.refine_2
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < e ⊔ 1
this : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi (e ⊔ 1)), ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d
⊢ HasFiniteIntegral (fun a_1 => a_1 ^ (s - 1 + -a)) (volume.restrict (Ioi (e ⊔ 1)))

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

Result:
no goals

Proof state:
case intro.intro
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
⊢ ∃ c, 0 < c ∧ IntegrableOn (fun t => t ^ (s - 1) * f t) (Ioi c) volume

Tactic:
have he' : 0 < max e 1 := zero_lt_one.trans_le (le_max_right _ _)

Result:
case intro.intro
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < e ⊔ 1
⊢ ∃ c, 0 < c ∧ IntegrableOn (fun t => t ^ (s - 1) * f t) (Ioi c) volume

Proof state:
case intro
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d : ℝ
hd' : ∃ a_1, ∀ b ≥ a_1, ‖f b‖ ≤ d * ‖b ^ (-a)‖
⊢ ∃ c, 0 < c ∧ IntegrableOn (fun t => t ^ (s - 1) * f t) (Ioi c) volume

Tactic:
obtain ⟨e, he⟩ := hd'

Result:
case intro.intro
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
⊢ ∃ c, 0 < c ∧ IntegrableOn (fun t => t ^ (s - 1) * f t) (Ioi c) volume

Proof state:
case intro.intro.refine_1
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < e ⊔ 1
⊢ AEStronglyMeasurable (fun t => t ^ (s - 1)) (volume.restrict (Ioi (e ⊔ 1)))

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

Result:
case intro.intro.refine_1
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < e ⊔ 1
t : ℝ
ht : t ∈ Ioi (e ⊔ 1)
⊢ ContinuousAt (fun t => t ^ (s - 1)) t