Commit 2025-07-06 12:48 117f6405

refactor(Convex/Cone): streamline duality (#24149) Replace the three dual cones definitions we have:

Set.innerDualCone : Set H → ConvexCone ℝ H
PointedCone.dual : PointedCone ℝ H → PointedCone ℝ H
ProperCone.dual : ProperCone ℝ H → ProperCone ℝ H

by three new ones:

PointedCone.dual : Set M → PointedCone R N for a bilinear pairing p : M →ₗ[R] N →ₗ[R] R
ProperCone.dual : Set M → ProperCone R N for a continuous perfect pairing p : M →ₗ[R] N →ₗ[R] R
ProperCone.innerDual : Set H → ProperCone ℝ H for an inner product space H

Also generalise the cone hyperplane separation theorem from real inner product spaces to locally convex real vector spaces.

Motivation

The current library on cones is very centered around normed and Hilbert spaces. This is inconvenient for us in Toric where we have two spaces $M$, and $N$ that are non-canonically isomorphic to $ℝ^n$ (for the same $n$). Although we could identify $M$ and $N$ with $ℝ^n$ and get an inner product on $M = N = ℝ^n$ this way, we would lose the contravariance (resp. covariance) of $M$ (resp. $N$) in the group scheme that indexes them. We would instead like to have results that apply to perfect pairings $p : M → N → ℝ$ out of the box. Not all the theory can be generalised, of course. So, in terms of file structure, we need to draw the line somewhere. We propose to draw it at the import of NormedAddCommGroup, as this is the time where the scalars suddenly get fixed to the reals, instead of an arbitrary ordered ring. This line passes through individual files, which therefore need to be split. We operate this separation by moving the cone content that doesn't require a norm under a new folder Geometry.Convex.Cone. The content that does require it stays in Analysis.Convex.Cone. A similar operation could be performed for the rest of the Analysis.Convex, but it seems wiser to do so simultaneously with the convexity refactor.

Previous changes performed as part of the refactor

Rename the variable 𝕜 to R when it is merely a ring
Split files according to normless normful parts
Complete the existing APIs
Redefine ProperCone R M as an abbrev for ClosedSubmodule R≥0 M, similarly to how PointedCone R M is an abbrev for Submodule R≥0 M. From Toric