Commit 2021-12-09 05:38 11bf7e52

feat(analysis/normed_space/weak_dual): add polar sets in preparation for Banach-Alaoglu theorem (#9836) The first of two parts to add the Banach-Alaoglu theorem about the compactness of the closed unit ball (and more generally polar sets of neighborhoods of the origin) of the dual of a normed space in the weak-star topology. This first half is about polar sets (for a set s in a normed space E, the polar s is the subset of weak_dual _ E consisting of the functionals that evaluate to something of norm at most one at all elements of s).