English
Definition HasMellin(f,s,m) encodes that MellinConvergent f s holds and the Mellin transform at s equals m.
Русский
Определение HasMellin(f,s,m) кодирует, что выполняется MellinConvergent f s и значение преобразования Меллина в s равно m.
LaTeX
$$$\text{HasMellin}(f,s,m) \iff \text{MellinConvergent}(f,s) \land \operatorname{mellin}(f)(s)=m.$$$
Lean4
/-- If `f` is `O(x ^ (-a))` as `x → 0`, then `log • f` is `O(x ^ (-b))` for every `a < b`. -/
theorem isBigO_rpow_zero_log_smul [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} (hab : a < b) (hf : f =O[𝓝[>] 0] (· ^ (-a))) :
(fun t : ℝ => log t • f t) =O[𝓝[>] 0] (· ^ (-b)) :=
by
have : log =o[𝓝[>] 0] fun t : ℝ => t ^ (a - b) :=
by
refine
((isLittleO_log_rpow_atTop (sub_pos.mpr hab)).neg_left.comp_tendsto tendsto_inv_nhdsGT_zero).congr'
(.of_forall fun t => ?_) (eventually_mem_nhdsWithin.mono fun t ht => ?_)
· simp
· simp_rw [Function.comp_apply, inv_rpow (le_of_lt ht), ← rpow_neg (le_of_lt ht), neg_sub]
refine
(this.isBigO.smul hf).congr' (Eventually.of_forall fun t => by rfl)
(eventually_nhdsWithin_iff.mpr (Eventually.of_forall fun t ht => ?_))
simp_rw [smul_eq_mul, ← rpow_add ht]
congr 1
abel
