mathlib3

11bf7e52 - feat(analysis/normed_space/weak_dual): add polar sets in preparation for Banach-Alaoglu theorem (#9836)

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`). Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>