English
The Theta relation is symmetric: f =Θ[l] g iff g =Θ[l] f.
Русский
Отношение θета симметрично: f =Θ[l] g эквивалентно g =Θ[l] f.
LaTeX
$$$ f =Θ[l] g \iff g =Θ[l] f. $$$
Lean4
/-- If `f` converges along `l` to a finite limit `x`, then `f =O[𝕜, l] 1`. -/
theorem isBigOTVS_one [ContinuousAdd E] [ContinuousSMul 𝕜 E] {x : E} (h : Tendsto f l (𝓝 x)) :
f =O[𝕜; l] (fun _ ↦ 1 : α → 𝕜) :=
by
replace h : Tendsto (f · - x) l (𝓝 0) := by simpa [sub_eq_add_neg] using h.add (tendsto_const_nhds (x := -x))
rw [(nhds_basis_balanced 𝕜 E).add_self.isBigOTVS_iff nhds_basis_ball]
rintro U ⟨hU₀, hUb⟩
obtain ⟨r, hr₀, hr₁, hr⟩ : ∃ r : ℝ≥0, 0 < r ∧ r ≤ 1 ∧ (r : ℝ≥0∞) ≤ (egauge 𝕜 U x)⁻¹ :=
by
apply Eventually.exists_gt
refine .and (eventually_le_nhds one_pos) ?_
refine (ENNReal.tendsto_coe.mpr tendsto_id).eventually_le_const ?_
suffices ∃ c : 𝕜, x ∈ c • U by simpa [egauge_eq_top]
simpa using (absorbent_nhds_zero (𝕜 := 𝕜) hU₀ x).exists
use r, by positivity
filter_upwards [h.eventually_mem hU₀] with a ha
calc
egauge 𝕜 (U + U) (f a) ≤ max (egauge 𝕜 U (f a - x)) (egauge 𝕜 U x) := by
simpa using egauge_add_add_le hUb hUb (f a - x) x
_ ≤ (r : ℝ≥0∞)⁻¹ := by
apply max_le
· refine (egauge_le_one _ ha).trans ?_
simp [hr₁]
· rwa [ENNReal.le_inv_iff_le_inv]
_ ≤ egauge 𝕜 (ball (0 : 𝕜) _) 1 := by simpa using div_le_egauge_ball 𝕜 r (1 : 𝕜)
