English
A Schwartz map is Big-O at infinity with respect to cocompact filter of any real power.
Русский
Schwartz-отображение является Big-O в бесконечности относительно фильтра cocompact по любой вещественной степени.
LaTeX
$$$ f =O[cocompact E] x \mapsto \|x\|^{s} \quad\text{for any } s \in \mathbb{R}$$$
Lean4
/-- Auxiliary lemma, used in proving the more general result `isBigO_cocompact_rpow`. -/
theorem isBigO_cocompact_zpow_neg_nat (k : ℕ) : f =O[cocompact E] fun x => ‖x‖ ^ (-k : ℤ) :=
by
obtain ⟨d, _, hd'⟩ := f.decay k 0
simp only [norm_iteratedFDeriv_zero] at hd'
simp_rw [Asymptotics.IsBigO, Asymptotics.IsBigOWith]
refine ⟨d, Filter.Eventually.filter_mono Filter.cocompact_le_cofinite ?_⟩
refine (Filter.eventually_cofinite_ne 0).mono fun x hx => ?_
rw [Real.norm_of_nonneg (zpow_nonneg (norm_nonneg _) _), zpow_neg, ← div_eq_mul_inv, le_div_iff₀']
exacts [hd' x, zpow_pos (norm_pos_iff.mpr hx) _]
