English
If a function f converges to a finite limit x along l, then f =O of the constant-1 function along l.
Русский
Если f сходится к пределу x вдоль l, то f =O(l) 1.
LaTeX
$$$ f \to x \text{ along } l \Rightarrow f =O_{𝕜;l} 1.$$$
Lean4
theorem isLittleOTVS_one [ContinuousSMul 𝕜 E] : f =o[𝕜; l] (1 : α → 𝕜) ↔ Tendsto f l (𝓝 0) :=
by
constructor
· intro hf
rw [(basis_sets _).isLittleOTVS_iff nhds_basis_ball] at hf
rw [(nhds_basis_balanced 𝕜 E).tendsto_right_iff]
rintro U ⟨hU, hUb⟩
rcases hf U hU with ⟨r, hr₀, hr⟩
lift r to ℝ≥0 using hr₀.le
norm_cast at hr₀
rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
obtain ⟨ε, hε₀, hε⟩ : ∃ ε : ℝ≥0, 0 < ε ∧ (ε * ‖c‖₊ / r : ℝ≥0∞) < 1 :=
by
apply Eventually.exists_gt
refine Continuous.tendsto' ?_ _ _ (by simp) |>.eventually_lt_const zero_lt_one
fun_prop (disch := intros;
first
| apply ENNReal.coe_ne_top
| positivity)
filter_upwards [hr ε hε₀.ne'] with x hx
refine mem_of_egauge_lt_one hUb (hx.trans_lt ?_)
calc
(ε : ℝ≥0∞) * egauge 𝕜 (ball (0 : 𝕜) r) 1 ≤ (ε * ‖c‖₊ / r : ℝ≥0∞) :=
by
rw [mul_div_assoc]
gcongr
simpa using egauge_ball_le_of_one_lt_norm (r := r) (x := (1 : 𝕜)) hc (by simp)
_ < 1 := ‹_›
· simp only [isLittleOTVS_iff]
intro hf U hU
refine ⟨ball 0 1, ball_mem_nhds _ one_pos, fun ε hε ↦ ?_⟩
rcases NormedField.exists_norm_lt 𝕜 hε.bot_lt with ⟨c, hc₀, hcε⟩
replace hc₀ : c ≠ 0 := by simpa using hc₀
filter_upwards [hf ((set_smul_mem_nhds_zero_iff hc₀).2 hU)] with a ha
calc
egauge 𝕜 U (f a) ≤ ‖c‖₊ := egauge_le_of_mem_smul ha
_ ≤ ε := (mod_cast hcε.le)
_ ≤ ε * egauge 𝕜 (ball (0 : 𝕜) 1) 1 := by
apply le_mul_of_one_le_right'
simpa using le_egauge_ball_one 𝕜 (1 : 𝕜)
