isEquivalent_iff_exists_eq_mul — Mathlib

English

If u ~_l v, then there exists φ with φ → 1 along l such that u = φ v eventually.

Русский

Если u ~_l v, то существует φ с φ → 1 по l, такое что u = φ v почти наверняка по l.

LaTeX

$$$ (u \\sim_{l} v) \\Rightarrow \\exists \\phi: \\alpha \\to \\beta,\\ (Tendsto\\ \\phi\\ l\\ (\\mathcal{N} 1)) \\land u =_l^{\\text{ev}} (\\phi \\cdot v) $$$

Lean4

theorem isEquivalent_iff_exists_eq_mul : u ~[l] v ↔ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v :=
  by
  rw [IsEquivalent, isLittleO_iff_exists_eq_mul]
  constructor <;> rintro ⟨φ, hφ, h⟩ <;> [refine ⟨φ + 1, ?_, ?_⟩; refine ⟨φ - 1, ?_, ?_⟩]
  · conv in 𝓝 _ => rw [← zero_add (1 : β)]
    exact hφ.add tendsto_const_nhds
  · convert h.fun_add (EventuallyEq.refl l v) <;> simp [add_mul]
  · conv in 𝓝 _ => rw [← sub_self (1 : β)]
    exact hφ.sub tendsto_const_nhds
  · convert h.fun_sub (EventuallyEq.refl l v); simp [sub_mul]

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