Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - chore(Analysis/Normed/Lp/WithLp): generalize action-related instances on WithLp #22706

Closed
wants to merge 7 commits into from
Closed

[Merged by Bors] - chore(Analysis/Normed/Lp/WithLp): generalize action-related instances on WithLp #22706

wants to merge 7 commits into from

Conversation

qawbecrdtey
Copy link
Collaborator

@qawbecrdtey qawbecrdtey commented Mar 8, 2025 •
edited by eric-wieser
Loading

This generalizes Module to weaker classes of action.

As the assumptions now vary by lemma, a variable line has been inlined into the following lemmas.

For additional benchmarking (related: #22434)

Open in Gitpod

@qawbecrdtey qawbecrdtey changed the title Initial commit - instances related to actions of WithLp. chore(Mathlib/Analysis/Normed/Lp/WithLp): Added action-related instances to WithLp Mar 8, 2025
@github-actions GitHub Actions
Copy link

github-actions bot commented Mar 8, 2025 •
edited
Loading

PR summary b1b0fa9f09

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ instDistribMulAction
+ instMulAction
+ instSMul

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).

@github-actions github-actions bot added the t-analysis Analysis (normed *, calculus) label Mar 8, 2025
@qawbecrdtey
Copy link
Collaborator Author

!bench

@qawbecrdtey qawbecrdtey requested a review from eric-wieser March 8, 2025 08:32
@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit a685563.
There were no significant changes against commit 2186c5f.

@github-actions GitHub Actions
Copy link

github-actions bot commented Mar 8, 2025

File Instructions %
build -26.847⬝10⁹ (-0.01%)
3 files, Instructions -2.0⬝10⁹
File Instructions %
Mathlib.Analysis.FunctionalSpaces.SobolevInequality -1.105⬝10⁹ (-0.89%)
Mathlib.Analysis.Calculus.FDeriv.WithLp -1.235⬝10⁹ (-6.19%)
Mathlib.Analysis.InnerProductSpace.EuclideanDist -1.303⬝10⁹ (-5.80%)
File Instructions %
Mathlib.Analysis.InnerProductSpace.PiL2 -3.929⬝10⁹ (-1.96%)
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic -5.938⬝10⁹ (-2.73%)
Mathlib.Analysis.CStarAlgebra.Matrix -7.960⬝10⁹ (-6.22%)
CI run

eric-wieser
eric-wieser reviewed Mar 8, 2025
View reviewed changes
Mathlib/Analysis/Normed/Lp/WithLp.lean Outdated
@@ -58,26 +58,35 @@ instance instNontrivial [Nontrivial V] : Nontrivial (WithLp p V) := ‹Nontrivia
instance instUnique [Unique V] : Unique (WithLp p V) := ‹Unique V›
instance instDecidableEq [DecidableEq V] : DecidableEq (WithLp p V) := ‹DecidableEq V›

variable [Semiring K] [Semiring K'] [AddCommGroup V]
instance instAddMonoid [AddMonoid V] : AddMonoid (WithLp p V) := ‹AddMonoid V›
instance instAddCommMonoid [AddCommMonoid V] : AddCommMonoid (WithLp p V) := ‹AddCommMonoid V›
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd suggest dropping these two instances from this PR, since they're not action-related. You can ungeneralize below at the same time.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggestion applied, but why? Is it because WithLp are only used along with the commutative property?

@qawbecrdtey
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 4ab1227.
There were no significant changes against commit 2186c5f.

@github-actions GitHub Actions
Copy link

github-actions bot commented Mar 8, 2025

File Instructions %
build -1.66⬝10⁹ (+0.00%)
lint +1.520⬝10⁹ (+0.01%)
CI run

@qawbecrdtey qawbecrdtey requested a review from eric-wieser March 9, 2025 06:07
@qawbecrdtey qawbecrdtey marked this pull request as ready for review March 13, 2025 15:28
@qawbecrdtey
Copy link
Collaborator Author

!bench

eric-wieser
eric-wieser reviewed Mar 13, 2025
View reviewed changes
Mathlib/Analysis/Normed/Lp/WithLp.lean Outdated
‹Module.Finite K V›

variable {K V}
variable [Module K V]
-- variable [SMul K V] [AddCommGroup V] [Semiring K] [Module K V]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If you're going to remove this line, can you also remove the one below? As written, your change puts the variables in a weird order. Usually we want the typeclasses before everything else.

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 76278bf.
There were no significant changes against commit ebb4b06.

@github-actions GitHub Actions
Copy link

File Instructions %
build -2.599⬝10⁹ (+0.00%)
lint +1.133⬝10⁹ (+0.01%)
2 files, Instructions -2.0⬝10⁹
File Instructions %
Mathlib.Analysis.CStarAlgebra.Matrix -1.11⬝10⁹ (-0.79%)
Mathlib.Analysis.Normed.Lp.WithLp -1.470⬝10⁹ (-17.43%)

CI run

@eric-wieser eric-wieser changed the title chore(Mathlib/Analysis/Normed/Lp/WithLp): Added action-related instances to WithLp chore(Analysis/Normed/Lp/WithLp): generalize action-related instances on WithLp Mar 14, 2025
eric-wieser
eric-wieser reviewed Mar 14, 2025
View reviewed changes
Mathlib/Analysis/Normed/Lp/WithLp.lean Outdated
instance instDistribMulAction [Monoid K] [AddCommGroup V] [DistribMulAction K V] :
DistribMulAction K (WithLp p V) := ‹DistribMulAction K V›
instance instModule [Semiring K] [AddCommGroup V] [Module K V] : Module K (WithLp p V) :=
‹Module K V›

/-! `WithLp p V` inherits various module-adjacent structures from `V`. -/
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this belongs up on line 60, above the instances.

eric-wieser
eric-wieser approved these changes Mar 14, 2025
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors d+

Thanks!

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Mar 14, 2025

✌️ qawbecrdtey can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@qawbecrdtey
Copy link
Collaborator Author

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Mar 14, 2025
@qawbecrdtey
chore(Analysis/Normed/Lp/WithLp): generalize action-related instances…
b6dd454 
… on `WithLp` (#22706)

This generalizes `Module` to weaker classes of action.

As the assumptions now vary by lemma, a `variable` line has been inlined into the following lemmas.



Co-authored-by: qawbecrdtey <[email protected]>
Co-authored-by: qawbecrdtey <[email protected]>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Mar 14, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(Analysis/Normed/Lp/WithLp): generalize action-related instances on WithLp [Merged by Bors] - chore(Analysis/Normed/Lp/WithLp): generalize action-related instances on WithLp Mar 14, 2025
@mathlib-bors mathlib-bors bot closed this Mar 14, 2025
@mathlib-bors mathlib-bors bot deleted the qawbecrdtey/withlp-actions branch March 14, 2025 02:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser approved these changes

Assignees
No one assigned
Labels
delegated t-analysis Analysis (normed *, calculus)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@qawbecrdtey @leanprover-bot @eric-wieser @leanprover-community-mathlib4-bot