[Merged by Bors] - doc(overview): some additions to the Analysis section

docs/overview.yaml

@@ -225,7 +225,6 @@ Topology:
     completion of a topological ring: 'uniform_space.completion.ring'
     topological module: 'has_continuous_smul'
     continuous linear map: 'continuous_linear_map'
-    weak-* topology: 'weak_dual.topological_space'
     Haar measure on a locally compact Hausdorff group: 'measure_theory.measure.haar_measure'
   Metric spaces:
     metric space: 'metric_space'
@@ -241,13 +240,19 @@ Topology:
     Gromov-Hausdorff space: 'Gromov_Hausdorff.GH_space'
 
 Analysis:
+  Topological vector spaces:
+    local convexity: 'locally_convex_space'
+    Bornology: 'bornology'
+    weak-* topology for dualities: 'weak_bilin.topological_space'
+
   Normed vector spaces/Banach spaces:
     normed vector space over a normed field: 'normed_space'
     topology on a normed vector space: 'normed_space.has_bounded_smul'
     equivalence of norms in finite dimension: 'linear_equiv.to_continuous_linear_equiv'
     finite dimensional normed spaces over complete normed fields are complete: 'submodule.complete_of_finite_dimensional'
     Heine-Borel theorem (finite dimensional normed spaces are proper): 'finite_dimensional.proper'
     norm of a continuous linear map: 'linear_map.mk_continuous'
+    Banach-Steinhaus theorem: 'banach_steinhaus'
     Banach open mapping theorem: 'continuous_linear_map.is_open_map'
     absolutely convergent series in Banach spaces: 'summable_of_summable_norm'
     Hahn-Banach theorem: 'exists_extension_norm_eq'
@@ -265,6 +270,7 @@ Analysis:
     existence of Hilbert basis: 'exists_hilbert_basis'
     eigenvalues from Rayleigh quotient: 'inner_product_space.is_self_adjoint.has_eigenvector_of_is_local_extr_on'
     Fréchet-Riesz representation of the dual of a Hilbert space: 'inner_product_space.to_dual'
+    Lax-Milgram theorem: 'is_coercive.continuous_linear_equiv_of_bilin'
 
   Differentiability:
     differentiable function between normed vector spaces: 'has_fderiv_at'