[Merged by Bors] - refactor(Analysis/LocallyConvex/AbsConvex): Redefine AbsConvex to use a single ring of scalars

[mans0954]

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:

• [Merged by Bors] - feat(Analysis/LocallyConvex/AbsConvex): Define the Absolutely Convex Hull #17029 (comment)
• feat(Analysis/LocallyConvex/Polar): Bipolar theorem #26345 (comment)

---

• depends on: [Merged by Bors] - feature(Analysis/Convex/Basic): Convexity and the algebra map #29248

[github-actions]

PR summary 724a6cb9d7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feature(Analysis/Convex/Basic): Convexity and the algebra map #29248
  By Dependent Issues (🤖). Happy coding!

[j-loreaux]

I'd venture that this is the most controversial part of this PR. I think this PR is a good change, but in the past many people have been resistant to letting ℂ (and hence also RCLike 𝕜) have a PartialOrder instance.

Suggested change

	open ComplexOrder
	open scoped ComplexOrder

I think this PR likely warrants a Zulip discussion.

[mans0954]

Zulip discussion

[j-loreaux]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build
• Post-Build Step