7.3 The pointwise dual and compact polar balls
The dual \(\mathrm{SchDual}\) is the space of continuous linear functionals \(\mathcal{S}(\mathbb {R},\mathbb {R}) \to \mathbb {R}\) carrying Mathlib’s topology of pointwise (weak-\(*\)) convergence (PointwiseConvergenceCLM). For a seminorm \(q\) on \(\mathcal{S}(\mathbb {R},\mathbb {R})\), the polar ball is \(\mathrm{polarBall}(q) = \{ F \in \mathrm{SchDual} \mid \forall \varphi ,\ |F\varphi | \le q(\varphi )\} \); it contains \(0\) and is monotone in \(q\).
For a continuous seminorm \(q\), the polar ball \(\mathrm{polarBall}(q)\) is compact in the pointwise topology. The proof pushes through the embedding of \(\mathrm{SchDual}\) into the product space \(\mathcal{S}(\mathbb {R},\mathbb {R}) \to \mathbb {R}\): the image is the intersection of the closed coordinatewise linearity conditions with the pointwise bound, inside the Tychonoff-compact box \(\prod _\varphi [-q(\varphi ), q(\varphi )]\), and a pointwise limit obeying the bound is automatically continuous because it is dominated by the continuous seminorm \(q\). No Ascoli-type argument is needed.
The special seminorms \(\mathrm{ratSeminorm}(c, s) = c \cdot \sup _{(k,n) \in s} p_{k,n}\), indexed by \(c \in \mathbb {R}_{\ge 0}\) and finite sets \(s \subseteq \mathbb {N} \times \mathbb {N}\), are continuous, and their polar balls form a cofinal family: every pointwise-bounded family \((\mathcal{F}_i)\) in the dual is contained in a single compact polar ball \(\mathrm{polarBall}(\mathrm{ratSeminorm}(c,s))\). This combines the Banach–Steinhaus dominating-seminorm corollary with the characterization of continuous seminorms on a space with seminorms.
For a continuous seminorm \(q\) and a dense set \(D\), membership \(F \in \mathrm{polarBall}(q)\) is equivalent to the bound \(|F\varphi | \le q(\varphi )\) holding for \(\varphi \in D\) only. Specialized to the named countable dense set \(\mathcal{D}\), the confinement event becomes a countable intersection of evaluation events, which is the measurability input for the probabilistic core.