English
Let R be a normed commutative ring and M an R-module with a topology. For any subset s of M, the polar polarR(s) consists of those functionals in the strong dual that send every element z ∈ s to an element whose norm is at most 1.
Русский
Пусть R — нормированное коммутативное кольцо и M — пространство над R с топологией. Для подмножества s ⊆ M поляр polarR(s) состоит из тех функционалов в сильном двойственном пространстве, которые отправляют каждый элемент z ∈ s в элемент с нормой, не превышающей 1.
LaTeX
$$$\operatorname{polar}_R(s) = \{ \varphi \in \mathrm{StrongDual}(R,M) \mid \forall z \in s, \|\varphi(z)\| \le 1 \}$$$
Lean4
/-- Given a subset `s` in a monoid `M` (over a commutative ring `R`), the polar `polar R s` is the
subset of `StrongDual R M` consisting of those functionals which evaluate to something of norm at
most one at all points `z ∈ s`. -/
def polar (R : Type*) [NormedCommRing R] {M : Type*} [AddCommMonoid M] [TopologicalSpace M] [Module R M] :
Set M → Set (StrongDual R M) :=
(topDualPairing R M).flip.polar
