isBigO_norm_Icc_restrict_atTop — Mathlib

English

If a function f : C(ℝ, E) decays like |x|^{-b} at infinity with b > 0, then for any fixed numbers R, S, the function x ↦ ||f.restrict(Icc(x+R, x+S))|| has the same decay rate, i.e., is O(|x|^{-b}) as x → +∞.

Русский

Если f: ℝ → E распадается как |x|^{-b} в бесконечности (b>0), то для любых фиксированных R, S фукнция x ↦ ||f.restrict(Icc(x+R, x+S))|| имеет такой же порядок распадности: O(|x|^{-b}) при x → +∞.

LaTeX

$$$\\text{If } f : \\mathbb{R} \\to E \\text{ is } O(|x|^{-b}) \\text{ at } \\infty \\text{ with } b>0, \\text{ then } (x \\mapsto \\|f\\restriction([x+R,x+S])\\|) = O(|x|^{-b}) \\text{ at } \\infty.$$$

Lean4

/-- If `f` is `O(x ^ (-b))` at infinity, then so is the function
`fun x ↦ ‖f.restrict (Icc (x + R) (x + S))‖` for any fixed `R` and `S`. -/
theorem isBigO_norm_Icc_restrict_atTop {f : C(ℝ, E)} {b : ℝ} (hb : 0 < b) (hf : f =O[atTop] fun x : ℝ => |x| ^ (-b))
    (R S : ℝ) : (fun x : ℝ => ‖f.restrict (Icc (x + R) (x + S))‖) =O[atTop] fun x : ℝ => |x| ^ (-b) := by
  -- First establish an explicit estimate on decay of inverse powers.
    -- This is logically independent of the rest of the proof, but of no mathematical interest in
    -- itself, so it is proved in-line rather than being formulated as a separate lemma.

  have claim : ∀ x : ℝ, max 0 (-2 * R) < x → ∀ y : ℝ, x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b) :=
    fun x hx y hy ↦ by
    rw [max_lt_iff] at hx
    obtain ⟨hx1, hx2⟩ := hx
    rw [← mul_rpow] <;> try positivity
    apply rpow_le_rpow_of_nonpos <;>
      linarith
        -- Now the main proof.

  obtain ⟨c, hc, hc'⟩ := hf.exists_pos
  simp only [IsBigO, IsBigOWith, eventually_atTop] at hc' ⊢
  obtain ⟨d, hd⟩ := hc'
  refine ⟨c * (1 / 2) ^ (-b), ⟨max (1 + max 0 (-2 * R)) (d - R), fun x hx => ?_⟩⟩
  rw [ge_iff_le, max_le_iff] at hx
  have hx' : max 0 (-2 * R) < x := by linarith
  rw [max_lt_iff] at hx'
  rw [norm_norm, ContinuousMap.norm_le _ (by positivity)]
  refine fun y => (hd y.1 (by linarith [hx.1, y.2.1])).trans ?_
  have A : ∀ x : ℝ, 0 ≤ |x| ^ (-b) := fun x => by positivity
  rw [mul_assoc, mul_le_mul_iff_right₀ hc, norm_of_nonneg (A _), norm_of_nonneg (A _)]
  convert claim x (by linarith only [hx.1]) y.1 y.2.1
  · apply abs_of_nonneg; linarith [y.2.1]
  · exact abs_of_pos hx'.1

Похожие утверждения