English
The difference f(x) − f0 has a power-law decay at 0: specifically, f(x) − f0 = O(x^{−k}) as x → 0+.
Русский
Разность f(x) − f0 имеет степенное затухание при x → 0+: f(x) − f0 = O(x^{−k}).
LaTeX
$$f(x) − f0 = O(x^{−k}) as x → 0+$$
Lean4
/-- Power asymptotic for `f - f₀` as `x → 0`. -/
theorem hf_zero' (P : WeakFEPair E) : (fun x : ℝ ↦ P.f x - P.f₀) =O[𝓝[>] 0] (· ^ (-P.k)) :=
by
simp_rw [← fun x ↦ sub_add_sub_cancel (P.f x) ((P.ε * ↑(x ^ (-P.k))) • P.g₀) P.f₀]
refine (P.hf_zero _).add (IsBigO.sub ?_ ?_)
· rw [← isBigO_norm_norm]
simp_rw [mul_smul, norm_smul, mul_comm _ ‖P.g₀‖, ← mul_assoc, norm_real]
apply (isBigO_refl _ _).const_mul_left
· refine IsBigO.of_bound ‖P.f₀‖ (eventually_nhdsWithin_iff.mpr ?_)
filter_upwards [eventually_le_nhds zero_lt_one] with x hx' (hx : 0 < x)
apply le_mul_of_one_le_right (norm_nonneg _)
rw [norm_of_nonneg (rpow_pos_of_pos hx _).le, rpow_neg hx.le]
exact (one_le_inv₀ (rpow_pos_of_pos hx _)).2 (rpow_le_one hx.le hx' P.hk.le)
