congr_of_eventuallyEq — Mathlib

English

Given f ≡ g at infinity and both grow polynomially, f and g have the same polynomial-growth class: congr_of_eventuallyEq.

Русский

Если две функции совпадают на бесконечности и обе растут полиномиально, то они принадлежат к одному классу полиномиального роста.

LaTeX

$$f =ᶠ[atTop] g ∧ GrowsPolynomially g ⇒ GrowsPolynomially f$$

Lean4

theorem congr_of_eventuallyEq {f g : ℝ → ℝ} (hfg : f =ᶠ[atTop] g) (hg : GrowsPolynomially g) : GrowsPolynomially f :=
  by
  intro b hb
  have hg' := hg b hb
  obtain ⟨c₁, hc₁_mem, c₂, hc₂_mem, hg'⟩ := hg'
  refine ⟨c₁, hc₁_mem, c₂, hc₂_mem, ?_⟩
  filter_upwards [hg', (tendsto_id.const_mul_atTop hb.1).eventually_forall_ge_atTop hfg, hfg] with x hx₁ hx₂ hx₃
  intro u hu
  rw [hx₂ u hu.1, hx₃]
  exact hx₁ u hu

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