English
A set S of uniform convergences is von Neumann bounded if and only if for every s ∈ 𝔖, the set { f(x) : f ∈ S, x ∈ s } is von Neumann bounded in F.
Русский
Множество S нормируемых сведений о равномерном сходстве von Neumann ограничено тогда и только тогда, когда для каждого s ∈ 𝔖 множество { f(x) : f ∈ S, x ∈ s } ограничено в F.
LaTeX
$$$$ IsVonNBounded_R(S) \iff \forall s \in \mathfrak{S},\ IsVonNBounded_R( \mathrm{Set.image2}( (f,x) \mapsto f(x) )\; S\; s ). $$$$
Lean4
/-- A set `S` of continuous linear maps with topology of uniform convergence on sets `s ∈ 𝔖`
is von Neumann bounded iff for any `s ∈ 𝔖`,
the set `{f x | (f ∈ S) (x ∈ s)}` is von Neumann bounded. -/
theorem isVonNBounded_iff {R : Type*} [NormedDivisionRing R] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module R F]
[ContinuousConstSMul R F] [SMulCommClass 𝕜₂ R F] {𝔖 : Set (Set E)} {S : Set (UniformConvergenceCLM σ F 𝔖)} :
IsVonNBounded R S ↔ ∀ s ∈ 𝔖, IsVonNBounded R (Set.image2 (fun f x ↦ f x) S s) :=
by
refine ⟨fun hS s hs ↦ isVonNBounded_image2_apply hS hs, fun h ↦ ?_⟩
simp_rw [isVonNBounded_iff_absorbing_le, nhds_zero_eq, le_iInf_iff, le_principal_iff]
intro s hs U hU
rw [Filter.mem_absorbing, Absorbs]
filter_upwards [h s hs hU, eventually_ne_cobounded 0] with c hc hc₀ f hf
rw [mem_smul_set_iff_inv_smul_mem₀ hc₀]
intro x hx
simpa only [mem_smul_set_iff_inv_smul_mem₀ hc₀] using hc (mem_image2_of_mem hf hx)
