English
If f = o_{𝕜;l} g, then for every neighborhood U of 0 there exists a neighborhood V of 0 such that for all ε ≠ 0 in ENNReal, egauge 𝕜 U (f x) ≤ᶠ[l] ε · egauge 𝕜 V (g x).
Русский
Если f = o_{𝕜;l} g, то для каждой окрестности U нуля существует окрестность V нуля такая, что для всех ε ≠ 0 в ENNReal, egauge 𝕜 U (f x) ≤ᶠ[l] ε · egauge 𝕜 V (g x).
LaTeX
$$$f =o[𝕜; l] g \\Rightarrow \\forall U \\in 𝓝(0),\\ ∃ V \\in 𝓝(0),\\forall ε \\neq 0,\\ (egauge 𝕜 U (f x)) ≤^{ᶠ[l]} (ε \\cdot egauge 𝕜 V (g x)).$$$
Lean4
/-- A version of `IsLittleOTVS.exists_eventuallyLE_mul`
where `ε` is quantified over `ℝ≥0∞` instead of `ℝ≥0`. -/
theorem exists_eventuallyLE_mul_ennreal (h : f =o[𝕜; l] g) {U : Set E} (hU : U ∈ 𝓝 0) :
∃ V ∈ 𝓝 (0 : F), ∀ ε ≠ 0, (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] (fun x ↦ ε * egauge 𝕜 V (g x)) :=
by
obtain ⟨V, hV₀, hV⟩ := h.exists_eventuallyLE_mul U hU
refine ⟨V, hV₀, fun ε hε ↦ ?_⟩
cases ε with
| top => exact (hV 1 one_ne_zero).trans <| .of_forall fun _ ↦ mul_le_mul_right' le_top _
| coe ε => exact hV ε (mod_cast hε)
