[Merged by Bors] - chore(Analysis/Convex): drop unused arguments#24392
[Merged by Bors] - chore(Analysis/Convex): drop unused arguments#24392
Conversation
PR summary e1d422bbb5Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
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 No changes to technical debt.You can run this locally as
|
YaelDillies
left a comment
YaelDillies
left a comment
There was a problem hiding this comment.
Hmm... I'm not convinced. What's your use case?
Given that the whole convexity library needs a rewrite (the current definition is mathematically incorrect over non-fields), I think that fine-tuning assumptions is currently a waste of time.
By the way, before you ask, that convexity refactor will probably happen soon because it's tangential to Toric, and in particular might help figure out how to arrange files.
|
My only argument is to reduce the number of typeclass searches. If the refactor will bring most or all of the assumptions back, I think it's OK. |
|
!bench |
|
BTW, I think that you should discuss the design choices you're making in the pending refactor on Zulip before you commit lots of time to actually doing it. |
|
Here are the benchmark results for commit e1d422b. |
2 files, Instructions -2.0⬝10⁹
|
|
Given how modest the speedup is, let's just close maybe? |
|
On the one hand, I see no downside in merging this PR. If you want to close it, then please first open a PR adding text to these TODOs explaining why they shouldn't be closed for now. |
|
Since Yury has already done the work on the files, I don't see a good reason not to merge it. |
|
🚀 Pull request has been placed on the maintainer queue by sgouezel. |
github-actions
bot
added
the
maintainer-merge
|
The good reason not to merge it is that IMO it sets a precedent for mildly disruptive low added value PRs, as we've recently seen for the last few file splits, especially since Yury is a maintainer. |
|
To me, the added value of the PR is strictly positive. Not positive enough that I would have wanted to do it myself, but since it has been done and leads to a strict improvement of the library, better merge it than not! |
|
Thanks 🎉 bors merge |
ghost
added
ready-to-merge
Also weaken typeclass assumptions here and there.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Also weaken typeclass assumptions here and there.
… 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)
5 participants
Also weaken typeclass assumptions here and there.