English
If 𝕜' is nontrivial, vonNBoundedness is preserved under scalar restriction; otherwise, trivial case reduces to subsingleton.
Русский
Если 𝕜' не тривиально, ограниченность по фон Нейману сохраняется при ограничении скаляров; иначе существуют тривиальные случаи.
LaTeX
$$$\\text{if } 𝕜' \\text{ is nontrivial } \\operatorname{IsVonNBounded}_{\\mathbb{k}'}(s) \\Rightarrow \\operatorname{IsVonNBounded}_{\\mathbb{k}}(s)$$$
Lean4
protected theorem restrict_scalars_of_nontrivial [NormedField 𝕜] [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [Nontrivial 𝕜']
[Zero E] [TopologicalSpace E] [SMul 𝕜 E] [MulAction 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {s : Set E}
(h : IsVonNBounded 𝕜' s) : IsVonNBounded 𝕜 s := by
intro V hV
refine (h hV).restrict_scalars <| AntilipschitzWith.tendsto_cobounded (K := ‖(1 : 𝕜')‖₊⁻¹) ?_
refine AntilipschitzWith.of_le_mul_nndist fun x y ↦ ?_
rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← sub_smul, nnnorm_smul, ← div_eq_inv_mul,
mul_div_cancel_right₀ _ (nnnorm_ne_zero_iff.2 one_ne_zero)]
