English
A function is little-OTVS iff it is Little-O with respect to the same comparison.
Русский
Функция равна малой-OTVS тогда и только тогда, когда она равна little-O по той же связи.
LaTeX
$$$ f =o_{𝕜;l} g \iff f =o_{l} g. $$$
Lean4
theorem isLittleOTVS_iff_isLittleO {f : α → E} {g : α → F} {l : Filter α} : f =o[𝕜; l] g ↔ f =o[l] g :=
by
rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc : 1 < ‖c‖₊⟩
have hc₀ : 0 < ‖c‖₊ := one_pos.trans hc
simp only [isLittleO_iff, nhds_basis_ball.isLittleOTVS_iff nhds_basis_ball]
refine ⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ⟨1, one_pos, fun δ hδ ↦ ?_⟩⟩
· rcases h ε hε with ⟨δ, hδ₀, hδ⟩
lift ε to ℝ≥0 using hε.le; lift δ to ℝ≥0 using hδ₀.le; norm_cast at hε hδ₀
filter_upwards [hδ (δ / ‖c‖₊) (div_pos hδ₀ hc₀).ne'] with x hx
suffices (‖f x‖₊ / ε : ℝ≥0∞) ≤ ‖g x‖₊ by
rw [← ENNReal.coe_div hε.ne'] at this
rw [← div_le_iff₀' (NNReal.coe_pos.2 hε)]
exact_mod_cast this
calc
(‖f x‖₊ / ε : ℝ≥0∞) ≤ egauge 𝕜 (ball 0 ε) (f x) := div_le_egauge_ball 𝕜 _ _
_ ≤ ↑(δ / ‖c‖₊) * egauge 𝕜 (ball 0 ↑δ) (g x) := hx
_ ≤ (δ / ‖c‖₊) * (‖c‖₊ * ‖g x‖₊ / δ) := by
gcongr
exacts [ENNReal.coe_div_le, egauge_ball_le_of_one_lt_norm hc (.inl <| ne_of_gt hδ₀)]
_ = (δ / δ) * (‖c‖₊ / ‖c‖₊) * ‖g x‖₊ := by simp only [div_eq_mul_inv]; ring
_ ≤ 1 * 1 * ‖g x‖₊ := by gcongr <;> exact ENNReal.div_self_le_one
_ = ‖g x‖₊ := by simp
· filter_upwards [@h ↑(ε * δ / ‖c‖₊) (by positivity)] with x (hx : ‖f x‖₊ ≤ ε * δ / ‖c‖₊ * ‖g x‖₊)
lift ε to ℝ≥0 using hε.le
calc
egauge 𝕜 (ball 0 ε) (f x) ≤ ‖c‖₊ * ‖f x‖₊ / ε := egauge_ball_le_of_one_lt_norm hc (.inl <| ne_of_gt hε)
_ ≤ ‖c‖₊ * (↑(ε * δ / ‖c‖₊) * ‖g x‖₊) / ε := by gcongr; exact_mod_cast hx
_ = (‖c‖₊ / ‖c‖₊) * (ε / ε) * δ * ‖g x‖₊ := by
simp only [div_eq_mul_inv, ENNReal.coe_inv hc₀.ne', ENNReal.coe_mul]; ring
_ ≤ 1 * 1 * δ * ‖g x‖₊ := by gcongr <;> exact ENNReal.div_self_le_one
_ = δ * ‖g x‖₊ := by simp
_ ≤ δ * egauge 𝕜 (ball 0 1) (g x) := by gcongr; apply le_egauge_ball_one
