English
If a family S is VN bounded and smul by a scalar sequence tends to 0 in a suitable sense, then the scaled sequence remains in VN bounds.
Русский
Если S VN‑ограничено и умножение скалярами сходится к нулю, тогда получившиеся масштабы остаются VN‑ограниченными.
LaTeX
$$ε : ι → 𝕜, l : Filter ι, hS : IsVonNBounded 𝕜 S, hxS, hε$$
Lean4
theorem isVonNBounded_of_smul_tendsto_zero {ε : ι → 𝕜} {l : Filter ι} [l.NeBot] (hε : ∀ᶠ n in l, ε n ≠ 0) {S : Set E}
(H : ∀ x : ι → E, (∀ n, x n ∈ S) → Tendsto (ε • x) l (𝓝 0)) : IsVonNBounded 𝕜 S :=
by
rw [(nhds_basis_balanced 𝕜 E).isVonNBounded_iff]
by_contra! H'
rcases H' with ⟨V, ⟨hV, hVb⟩, hVS⟩
have : ∀ᶠ n in l, ∃ x : S, ε n • (x : E) ∉ V :=
by
filter_upwards [hε] with n hn
rw [absorbs_iff_norm] at hVS
push_neg at hVS
rcases hVS ‖(ε n)⁻¹‖ with ⟨a, haε, haS⟩
rcases Set.not_subset.mp haS with ⟨x, hxS, hx⟩
refine ⟨⟨x, hxS⟩, fun hnx => ?_⟩
rw [← Set.mem_inv_smul_set_iff₀ hn] at hnx
exact hx (hVb.smul_mono haε hnx)
rcases this.choice with ⟨x, hx⟩
refine Filter.frequently_false l (Filter.Eventually.frequently ?_)
filter_upwards [hx, (H (_ ∘ x) fun n => (x n).2).eventually (eventually_mem_set.mpr hV)] using fun n => id
