… a single ring of scalars (#29342)

Currently the definition of Absolutely Convex in Mathlib is a little unexpected:
```
def AbsConvex (s : Set E) : Prop := Balanced 𝕜 s ∧ Convex ℝ s
```
At the time this definition was formulated, Mathlib's definition of `Convex` required the scalars to be an `OrderedSemiring` whereas the definition of `Balanced` required the scalars to be a `SeminormedRing`. Mathlib didn't  have a concept of a semi-normed ordered ring, so a set was defined as `AbsConvex` if it is balanced over a `SeminormedRing` `𝕜` and convex over `ℝ`.

Recently the requirements for the definition of `Convex` have been relaxed (#24392, #20595) so it is now possible to use a single scalar ring in common with the literature.

Previous discussion:

- #17029 (comment)
- #26345 (comment)

… a single ring of scalars (leanprover-community#29342)

Currently the definition of Absolutely Convex in Mathlib is a little unexpected:
```
def AbsConvex (s : Set E) : Prop := Balanced 𝕜 s ∧ Convex ℝ s
```
At the time this definition was formulated, Mathlib's definition of `Convex` required the scalars to be an `OrderedSemiring` whereas the definition of `Balanced` required the scalars to be a `SeminormedRing`. Mathlib didn't  have a concept of a semi-normed ordered ring, so a set was defined as `AbsConvex` if it is balanced over a `SeminormedRing` `𝕜` and convex over `ℝ`.

Recently the requirements for the definition of `Convex` have been relaxed (leanprover-community#24392, leanprover-community#20595) so it is now possible to use a single scalar ring in common with the literature.

Previous discussion:

- leanprover-community#17029 (comment)
- leanprover-community#26345 (comment)

… a single ring of scalars (leanprover-community#29342)

Currently the definition of Absolutely Convex in Mathlib is a little unexpected:
```
def AbsConvex (s : Set E) : Prop := Balanced 𝕜 s ∧ Convex ℝ s
```
At the time this definition was formulated, Mathlib's definition of `Convex` required the scalars to be an `OrderedSemiring` whereas the definition of `Balanced` required the scalars to be a `SeminormedRing`. Mathlib didn't  have a concept of a semi-normed ordered ring, so a set was defined as `AbsConvex` if it is balanced over a `SeminormedRing` `𝕜` and convex over `ℝ`.

Recently the requirements for the definition of `Convex` have been relaxed (leanprover-community#24392, leanprover-community#20595) so it is now possible to use a single scalar ring in common with the literature.

Previous discussion:

- leanprover-community#17029 (comment)
- leanprover-community#26345 (comment)

…35422)

This PR uses the material in Topology/Algebra/Module/WeakBilin.lean from the unfinished PR #26345 by @mans0954.

Given a bilinear form `B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜`, every continuous functional on `E` endowed with the `σ(E, F; B)`-topology is of the form `x ↦ B(x, y)` for some `y : F`.

The result doesn't generally seem to be named, but Narici-Beckenstein's "Topological Vector Spaces" calls it the "weak representation theorem", a term we have used for the docstring.

Co-authored-by: David Gross <[email protected]>

…eanprover-community#35422)

This PR uses the material in Topology/Algebra/Module/WeakBilin.lean from the unfinished PR leanprover-community#26345 by @mans0954.

Given a bilinear form `B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜`, every continuous functional on `E` endowed with the `σ(E, F; B)`-topology is of the form `x ↦ B(x, y)` for some `y : F`.

The result doesn't generally seem to be named, but Narici-Beckenstein's "Topological Vector Spaces" calls it the "weak representation theorem", a term we have used for the docstring.

Co-authored-by: David Gross <[email protected]>