isLittleOTVS_iff_tendsto_inv_smul

English

Simp lemmas equate Big-O on a pi-type with coordinatewise Big-O statements and provide symmetry.

Русский

Lemmas simp устанавливают равенство Big-O на pi-типе через координаты и симметрию.

LaTeX

$$$\text{IsBigOTVS pi simp: } (f =O_{𝕜;l} g) \iff (\forall i, f_i =O_{𝕜;l} g). $$$

Lean4

theorem isLittleOTVS_iff_tendsto_inv_smul [ContinuousSMul 𝕜 E] {f : α → 𝕜} {g : α → E} {l : Filter α}
    (h₀ : ∀ᶠ x in l, f x = 0 → g x = 0) : g =o[𝕜; l] f ↔ Tendsto (fun x ↦ (f x)⁻¹ • g x) l (𝓝 0) :=
  by
  refine ⟨IsLittleOTVS.tendsto_inv_smul, fun h ↦ ?_⟩
  refine (((isLittleOTVS_one (𝕜 := 𝕜)).mpr h).smul_left f).congr' (h₀.mono fun x hx ↦ ?_) (by simp)
  by_cases h : f x = 0 <;> simp [h, hx]

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