Weak spaces as a class

[j-loreaux]

There is currently very little API for WeakBilin, and rather a lot of defeq abuse. Moreover, WeakDual and WeakSpace are non-abbrev type synonyms of WeakBilin, so we currently don't have a nice way to unify these theories. It gets more complicated when one wants to consider, for example, a W⋆-algebra (i.e., a C⋆-algebra which has a Banach space predual) equipped with the the weak-⋆ topology. And one can imagine yet other situations.

We propose to unify all these with a new class which states that E is equipped with the weak topology induced by a bilinear form B.

variable {𝕜 E F : Type*} [CommSemiring 𝕜] [TopologicalSpace 𝕜]
   [AddCommMonoid E] [Module 𝕜 E]
   [AddCommMonoid F] [Module 𝕜 F]
   [inst : TopologicalSpace E]

class LinearMap.IsWeak (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) where
   eq_induced := inst = .induced (B · ·) Pi.topologicalSpace

Why a class, you may ask? Indeed, we could just write this as a hypothesis: Topology.IsInducing (B · ·). However, adding a class seems to have many benefits.

1. It will help prevent defeq abuse in material involving weak topologies. Note for example, WeakBilin.eval_continuous which is not even type correct (along with many other things in that file) because it is about B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜 when it should be about B' : WeakBilin B →ₗ[𝕜] F →ₗ[𝕜] 𝕜. By providing a class, we can copy over all the theorems nicely.
2. Some theorems are naturally stated in terms of weak topologies (e.g., the bipolar theorem) relative to a bilinear form. This will allow us to have a single theorem instead of one for each different setting.
3. In a downstream project about the Mackey-Arens theorem, it became clear that the only good way to define the Mackey topology without abusing defeq was to parameterize polar topologies over this LinearMap.IsWeak class instead of using WeakBilin directly.

As a case in point, let's consider the bipolar theorem. With our class, this can be easily stated as:

/-
The **Bipolar Theorem**: The bipolar of a set `s : Set E` relative to a bilinear form
`B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜` (where `E` is equipped with the weak topology induced by `B`)
coincides with its closed absolutely convex hull.
[Conway, *A course in functional analysis*, Chapter V. 1.8][conway1990]
-/
theorem flip_polar_polar (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [hB : B.IsWeak] {s : Set E}
    (hs : s.Nonempty) :
    B.flip.polar (B.polar s) = closedAbsConvexHull 𝕜 s :=
  sorry

This will then apply simultaneously to the natural bilinear forms:

WeakBilin B →ₗ[𝕜] F →ₗ[𝕜] 𝕜
WeakDual 𝕜 E →ₗ[𝕜] E →ₗ[𝕜] 𝕜
WeakSpace 𝕜 E →ₗ[𝕜] StrongDual 𝕜 E →ₗ[𝕜] 𝕜

but also many others. I have already found this class useful for a downstream project.