English
If a holomorphic (or continuous) map f decays as |x|^{-b} at −∞ with b>0, then the same decay transfers to the restriction norm over Icc around −∞, i.e., the same big-O bound holds at −∞ for the restricted norm.
Русский
Если f распадается как |x|^{-b} при x → −∞ (b>0), то аналогично и для ограниченной нормы на Icc вокруг −∞: сохраняется та же оценка распадности.
LaTeX
$$$\\text{If } f:\\mathbb{R} \\to E \\text{ satisfies } f=O(|x|^{-b}) \\text{ at } -\\infty \\text{ with } b>0, \\text{ then } (x \\mapsto \\|f\\restriction(Icc(x+R,x+S))\\|) = O(|x|^{-b}) \\text{ at } -\\infty.$$$
Lean4
theorem isBigO_norm_Icc_restrict_atBot {f : C(ℝ, E)} {b : ℝ} (hb : 0 < b) (hf : f =O[atBot] fun x : ℝ => |x| ^ (-b))
(R S : ℝ) : (fun x : ℝ => ‖f.restrict (Icc (x + R) (x + S))‖) =O[atBot] fun x : ℝ => |x| ^ (-b) :=
by
have h1 : (f.comp (ContinuousMap.mk _ continuous_neg)) =O[atTop] fun x : ℝ => |x| ^ (-b) :=
by
convert hf.comp_tendsto tendsto_neg_atTop_atBot using 1
ext1 x; simp only [Function.comp_apply, abs_neg]
have h2 := (isBigO_norm_Icc_restrict_atTop hb h1 (-S) (-R)).comp_tendsto tendsto_neg_atBot_atTop
have : (fun x : ℝ => |x| ^ (-b)) ∘ Neg.neg = fun x : ℝ => |x| ^ (-b) := by ext1 x;
simp only [Function.comp_apply, abs_neg]
rw [this] at h2
refine (isBigO_of_le _ fun x => ?_).trans h2
rw [norm_norm, Function.comp_apply, norm_norm, ContinuousMap.norm_le _ (norm_nonneg _)]
rintro ⟨x, hx⟩
rw [ContinuousMap.restrict_apply_mk]
refine (le_of_eq ?_).trans (ContinuousMap.norm_coe_le_norm _ ⟨-x, ?_⟩)
· rw [ContinuousMap.restrict_apply_mk, ContinuousMap.comp_apply, ContinuousMap.coe_mk, ContinuousMap.coe_mk, neg_neg]
· exact ⟨by linarith [hx.2], by linarith [hx.1]⟩
