English
A Schwartz map is Big-O cocompact with respect to z-powers.
Русский
Schwartz-map является Big-O относительно cocompact по z-степеням.
LaTeX
$$$ f =O[cocompact E] x \mapsto \|x\|^{k} \text{ for } k \in \mathbb{Z} $$$
Lean4
theorem isBigO_cocompact_rpow [ProperSpace E] (s : ℝ) : f =O[cocompact E] fun x => ‖x‖ ^ s :=
by
let k := ⌈-s⌉₊
have hk : -(k : ℝ) ≤ s := neg_le.mp (Nat.le_ceil (-s))
refine (isBigO_cocompact_zpow_neg_nat f k).trans ?_
suffices (fun x : ℝ => x ^ (-k : ℤ)) =O[atTop] fun x : ℝ => x ^ s from this.comp_tendsto tendsto_norm_cocompact_atTop
simp_rw [Asymptotics.IsBigO, Asymptotics.IsBigOWith]
refine ⟨1, (Filter.eventually_ge_atTop 1).mono fun x hx => ?_⟩
rw [one_mul, Real.norm_of_nonneg (Real.rpow_nonneg (zero_le_one.trans hx) _),
Real.norm_of_nonneg (zpow_nonneg (zero_le_one.trans hx) _), ← Real.rpow_intCast, Int.cast_neg, Int.cast_natCast]
exact Real.rpow_le_rpow_of_exponent_le hx hk
