isLittleO_iff_exists_eq_mul — Mathlib

English

Another formulation: u = o[l] v iff there exists φ with Tendsto φ to 0 and u = φ v almost everywhere.

Русский

Еще одно формулирование: u = o[l] v эквивалентно существованию φ с Tendsto φ→0 и u = φ v почти всюду.

LaTeX

$$$ u =o[l] v \\iff \\exists \\phi : α \\to 𝕜, Tendsto \\phi l (\\mathcal{N} 0) ∧ u =ᶠ[l] \\phi \\cdot v $$$

Lean4

theorem isLittleO_iff_exists_eq_mul : u =o[l] v ↔ ∃ φ : α → 𝕜, Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v :=
  by
  constructor
  · exact fun h => ⟨fun x => u x / v x, h.tendsto_div_nhds_zero, h.eventually_mul_div_cancel.symm⟩
  · simp only [IsLittleO_def]
    rintro ⟨φ, hφ, huvφ⟩ c hpos
    rw [NormedAddCommGroup.tendsto_nhds_zero] at hφ
    exact isBigOWith_of_eq_mul _ ((hφ c hpos).mono fun x => le_of_lt) huvφ

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