English
If a function f decays as |x|^{-b} along cocompact directions, then its norm after restricting to any fixed compact interval K also decays as fast as |x|^{-b}, uniformly over the cocompact direction.
Русский
Если f распадается по направлению коценом cocompact как |x|^{-b}, то нормa после ограничения на фиксированный компактный интервал сохраняет распадность как |x|^{-b}, равномерно в cocompact-направлении.
LaTeX
$$$\\forall K \\text{ compact in } \\mathbb{R},\\; \\| (f \\circ (x+\\cdot)).restrict K \\| = O_{cocompact}( |\\cdot|^{-b} ).$$$
Lean4
theorem isBigO_norm_restrict_cocompact (f : C(ℝ, E)) {b : ℝ} (hb : 0 < b)
(hf : f =O[cocompact ℝ] fun x : ℝ => |x| ^ (-b)) (K : Compacts ℝ) :
(fun x => ‖(f.comp (ContinuousMap.addRight x)).restrict K‖) =O[cocompact ℝ] (|·| ^ (-b)) :=
by
obtain ⟨r, hr⟩ := K.isCompact.isBounded.subset_closedBall 0
rw [closedBall_eq_Icc, zero_add, zero_sub] at hr
have : ∀ x : ℝ, ‖(f.comp (ContinuousMap.addRight x)).restrict K‖ ≤ ‖f.restrict (Icc (x - r) (x + r))‖ :=
by
intro x
rw [ContinuousMap.norm_le _ (norm_nonneg _)]
rintro ⟨y, hy⟩
refine (le_of_eq ?_).trans (ContinuousMap.norm_coe_le_norm _ ⟨y + x, ?_⟩)
· simp_rw [ContinuousMap.restrict_apply, ContinuousMap.comp_apply, ContinuousMap.coe_addRight]
· exact ⟨by linarith [(hr hy).1], by linarith [(hr hy).2]⟩
simp_rw [cocompact_eq_atBot_atTop, isBigO_sup] at hf ⊢
constructor
· refine (isBigO_of_le atBot ?_).trans (isBigO_norm_Icc_restrict_atBot hb hf.1 (-r) r)
simp_rw [norm_norm]; exact this
· refine (isBigO_of_le atTop ?_).trans (isBigO_norm_Icc_restrict_atTop hb hf.2 (-r) r)
simp_rw [norm_norm]; exact this
