English
As x approaches 0 from the right, f(x) is asymptotically ε x^{−k} g0 up to a rapidly decaying error; more precisely, f(x) − ε x^{−k} g0 = O(x^r) for every r as x → 0+.
Русский
Пусть x → 0⁺; тогда f(x) = ε x^{−k} g0 + быстро затухающее суммирование; точнее, f(x) − ε x^{−k} g0 = O(x^r) для любого r.
LaTeX
$$f(x) − (ε · x^{−k}) · g0 = O(x^r) as x → 0+$$
Lean4
/-- As `x → 0`, we have `f x = x ^ (-P.k) • constant` up to a rapidly decaying error. -/
theorem hf_zero (P : WeakFEPair E) (r : ℝ) : (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) =O[𝓝[>] 0] (· ^ r) :=
by
have := (P.hg_top (-(r + P.k))).comp_tendsto tendsto_inv_nhdsGT_zero
simp_rw [IsBigO, IsBigOWith, eventually_nhdsWithin_iff] at this ⊢
obtain ⟨C, hC⟩ := this
use ‖P.ε‖ * C
filter_upwards [hC] with x hC' (hx : 0 < x)
have h_nv2 : ↑(x ^ P.k) ≠ (0 : ℂ) := ofReal_ne_zero.mpr (rpow_pos_of_pos hx _).ne'
have h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0 := mul_ne_zero P.symm.hε h_nv2
specialize hC' hx
simp_rw [Function.comp_apply, ← one_div, P.h_feq' _ hx] at hC'
rw [← ((mul_inv_cancel₀ h_nv).symm ▸ one_smul ℂ P.g₀ :), mul_smul _ _ P.g₀, ← smul_sub, norm_smul, ←
le_div_iff₀' (lt_of_le_of_ne (norm_nonneg _) (norm_ne_zero_iff.mpr h_nv).symm)] at hC'
convert hC' using 1
· congr 3
rw [rpow_neg hx.le]
simp [field]
· simp_rw [norm_mul, norm_real, one_div, inv_rpow hx.le, rpow_neg hx.le, inv_inv, norm_inv,
norm_of_nonneg (rpow_pos_of_pos hx _).le, rpow_add hx]
field_simp
