trans_tendsto_norm_atTop — Mathlib

English

The map x ↦ floor x (cast to the same type) is equivalent to the identity on large x with respect to atTop; i.e., ⌊x⌋₊ is asymptotically equivalent to x.

Русский

Отображение x ↦ floor x (приведённое к тем же числам) асимптотически эквивалентно тождественному отображению на бесконечности.

LaTeX

$$$\text{isEquivalent}(\, \operatorname{Nat.floor}\, )$$$

Lean4

theorem trans_tendsto_norm_atTop {α : Type*} {u v : α → 𝕜} {l : Filter α} (huv : u =O[l] v)
    (hu : Tendsto (fun x => ‖u x‖) l atTop) : Tendsto (fun x => ‖v x‖) l atTop :=
  by
  rcases huv.exists_pos with ⟨c, hc, hcuv⟩
  rw [IsBigOWith] at hcuv
  convert Tendsto.atTop_div_const hc (tendsto_atTop_mono' l hcuv hu)
  rw [mul_div_cancel_left₀ _ hc.ne.symm]

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