English
Let E be a topological vector space generated by a family p of seminorms. If q is a continuous seminorm, then there exist a finite set s of indices and a positive scalar C such that q ≤ C · s.sup p.
Русский
Пусть E — топологическое векторное пространство, генерируемое семинормами p. Если q непрерывна, то существуют конечный набор индексов s и положительная величина C такая, что q ≤ C · s.sup p.
LaTeX
$$$\\exists s: Finset ι, \\exists C: \\mathbb{R}_{>0}, q \\le C \\cdot s.sup p$$$
Lean4
/-- Let `E` be a topological vector space (over a `NontriviallyNormedField`) whose topology is
generated by some family of seminorms `p`, and let `q` be a seminorm on `E`. If `q` is continuous,
then it is uniformly controlled by *finitely many* seminorms of `p`, that is there
is some finset `s` of the index set and some `C > 0` such that `q ≤ C • s.sup p`. -/
theorem bound_of_continuous [t : TopologicalSpace E] (hp : WithSeminorms p) (q : Seminorm 𝕜 E) (hq : Continuous q) :
∃ s : Finset ι, ∃ C : ℝ≥0, C ≠ 0 ∧ q ≤ C • s.sup p := by
-- The continuity of `q` gives us a finset `s` and a real `ε > 0`
-- such that `hε : (s.sup p).ball 0 ε ⊆ q.ball 0 1`.
rcases hp.hasBasis.mem_iff.mp (ball_mem_nhds hq one_pos) with ⟨V, hV, hε⟩
rcases p.basisSets_iff.mp hV with
⟨s, ε, ε_pos, rfl⟩
-- Now forget that `E` already had a topology and view it as the (semi)normed space
-- `(E, s.sup p)`.
clear hp hq t
let _ : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
let _ : NormedSpace 𝕜 E :=
{ norm_smul_le := fun a b ↦ le_of_eq (map_smul_eq_mul (s.sup p) a b) }
-- The inclusion `hε` tells us exactly that `q` is *still* continuous for this new topology
have : Continuous q :=
Seminorm.continuous (r := 1)
(mem_of_superset (Metric.ball_mem_nhds _ ε_pos) hε)
-- Hence we can conclude by applying `bound_of_continuous_normedSpace`.
rcases bound_of_continuous_normedSpace q this with ⟨C, C_pos, hC⟩
exact
⟨s, ⟨C, C_pos.le⟩, fun H ↦ C_pos.ne.symm (congr_arg NNReal.toReal H), hC⟩
-- Note that the key ingredient for this proof is that, by scaling arguments hidden in
-- `Seminorm.continuous`, we only have to look at the `q`-ball of radius one, and the `s` we get
-- from that will automatically work for all other radii.
