Polar set #
In this file we define the polar set. There are different notions of the polar, we will define the
absolute polar. The advantage over the real polar is that we can define the absolute polar for
any bilinear form
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜, where
𝕜 is a normed commutative ring and
F are modules over
Main definitions #
LinearMap.polar: The polar of a bilinear form
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜.
Main statements #
LinearMap.polar_eq_iInter: The polar as an intersection.
LinearMap.subset_bipolar: The polar is a subset of the bipolar.
LinearMap.polar_weak_closed: The polar is closed in the weak topology induced by
- [H. H. Schaefer, Topological Vector Spaces][schaefer1966]
The (absolute) polar of
s : Set E is given by the set of all
y : F such that
‖B x y‖ ≤ 1
x ∈ s.