chore: replace `WithLp.equiv` with a new pair `WithLp.toLp`/`WithLp.ofLp` by Paul-Lez · Pull Request #24261 · leanprover-community/mathlib4

Paul-Lez · 2025-04-21T20:48:09Z

This PR does the following:

deprecate WithLp.equiv
Add WithLp.toLp and WithLp.ofLp (for consistency with other equivalences to type synonyms)

See Zulip discussion

github-actions · 2025-04-21T20:49:10Z

PR summary 78a26d50f7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ EuclideanSpace.measurePreserving_measurableOfLp
+ PiLp.measurePreserving_ofLp
+ coe_measurableOfLp
+ coe_measurableOfLp_symm
+ measurableOfLp
+ ofLpContinuousLinearEquiv
+ ofLpLinearEquiv
+ ofLpProdContinuousLinearEquiv
+ ofLpₗᵢ
+ prodOfLpₗᵢ
+ symm_ofLp
+ symm_toLp
- PiLp.volume_preserving_ofLp
- ofLp_surjective
- toLp_surjective

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.

Increase in tech debt: (relative, absolute) = (2.00, 0.02)

Current number	Change	Type
81	2	disabled deprecation lints

Current commit 7bb53035e4
Reference commit 78a26d50f7

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

Mathlib/Analysis/Normed/Lp/ProdLp.lean

Mathlib/Analysis/Normed/Lp/WithLp.lean

Mathlib/Analysis/Normed/Lp/ProdLp.lean

YaelDillies

Thanks!

maintainer delegate

Mathlib/Analysis/Normed/Lp/ProdLp.lean

github-actions · 2025-04-25T20:05:07Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

Mathlib/Analysis/Normed/Lp/WithLp.lean

eric-wieser

I think we should rip off the bandaid and deprecate equiv in this PR, rather than in a follow-up. Otherwise we have two spellings of everything, and reviewers have to tell contributors which one to use.

YaelDillies · 2025-04-26T21:18:18Z

Can't this be done in a second PR soon? Paul is really really focused on that refactor and definitely doesn't have 10 other things going on.

eric-wieser · 2025-04-26T21:57:08Z

I don't see any benefit in merging this PR until the other is ready to go. Mathlib shouldn't have two non-deprecated ways to spell something identical.

Paul-Lez · 2025-04-26T22:19:22Z

I can take care of this tonight!

YaelDillies · 2025-04-26T22:34:48Z

Sure, I agree. All I'm saying is that they should be in separate PR. But I am happy for both PRs to land in a short time frame.

Paul-Lez · 2025-04-26T23:52:49Z

Added the deprecations (and also removed simp tags from deprecated lemmas). Edit: there seem to be some more to do in PiLp - I'll take a look tomorrow when it's daytime:)

Along the way, I also noticed that ofLpProdContinuousLinearEquiv/prodContinuousLinearEquiv should be generalised, and added a TODO note to that effect. I think this may be better to leave to another PR since it would be natural to move it to the WithLp file, but the imports aren't quite right (and maybe we don't want to be changing those in this PR?)

Mathlib/Analysis/Normed/Lp/WithLp.lean

leanprover-community-bot-assistant · 2025-04-27T21:14:20Z

This pull request has conflicts, please merge master and resolve them.

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

…refactor

This reverts commit 2da1569.

eric-wieser · 2025-06-28T23:11:12Z

I've adjusted the diff here to show the difference with the now-merged #26459; merging this PR as is would amount to reverting that one and merging the original version of this instead. I don't think we should actually do that, but maybe there are parts of this diff we still want.

leanprover-community-bot-assistant · 2025-07-05T04:11:35Z

This pull request has conflicts, please merge master and resolve them.

…26249) Put a measurable space structure on a general `WithLp`. Define a `MeasurableEquiv` version of `WithLp.equiv`. The direction is reversed in prevision of the `WithLp` refactor in leanprover-community#24261. Define a `BorelSpace` instance.

github-actions bot added the t-analysis Analysis (normed *, calculus) label Apr 21, 2025

Paul-Lez added the WIP Work in progress label Apr 21, 2025

Paul-Lez changed the title ~~chore(Analysis/Normed/Lp/WithLp): rename WithLp.equiv, make arguments implicit and change the direction of the equivalence~~ chore(Analysis/Normed/Lp/WithLp): add WithLp.toLp Apr 22, 2025

Paul-Lez requested a review from YaelDillies April 22, 2025 23:06

YaelDillies reviewed Apr 23, 2025

View reviewed changes

Paul-Lez removed the WIP Work in progress label Apr 23, 2025

Paul-Lez requested a review from YaelDillies April 23, 2025 21:10

YaelDillies reviewed Apr 24, 2025

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 24, 2025

Paul-Lez removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 25, 2025

Paul-Lez requested a review from YaelDillies April 25, 2025 19:50

YaelDillies approved these changes Apr 25, 2025

View reviewed changes

Mathlib/Analysis/Normed/Lp/ProdLp.lean Outdated Show resolved Hide resolved

Mathlib/Analysis/Normed/Lp/ProdLp.lean Outdated Show resolved Hide resolved

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 25, 2025

b-mehta requested a review from eric-wieser April 26, 2025 09:20

eric-wieser reviewed Apr 26, 2025

View reviewed changes

Mathlib/Analysis/Normed/Lp/WithLp.lean Outdated Show resolved Hide resolved

eric-wieser added awaiting-author A reviewer has asked the author a question or requested changes. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Apr 26, 2025

eric-wieser reviewed Apr 26, 2025

View reviewed changes

eric-wieser reviewed Apr 27, 2025

View reviewed changes

Mathlib/Analysis/Normed/Lp/WithLp.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Apr 27, 2025

View reviewed changes

Mathlib/Analysis/Normed/Lp/WithLp.lean Show resolved Hide resolved

eric-wieser reviewed Apr 27, 2025

View reviewed changes

Mathlib/Analysis/Normed/Lp/WithLp.lean Outdated Show resolved Hide resolved

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 27, 2025

eric-wieser and others added 15 commits June 27, 2025 01:27

Merge branch 'with-lp-refactor' into eric-wieser/with-lp-refactor

bb1c001

fix and reduce diff

fac6683

fix

d29084a

fix

a472783

fix test

751cff8

Apply suggestions from code review

de68147

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Apply suggestions from code review

b01cbc0

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Merge branch 'master' into eric-wieser/with-lp-refactor

bb5c306

fix build

add156b

replace fst/snd with inl/inr

cf0ee60

fun_prop

f96cb70

fix docstring

9c06a13

replace fst/snd with inl/inr

5dec46c

fun_prop

0cb905c

Merge commit '508c1928c2d639ac273bb54463a9ad90df9d924f' into with-lp-…

1d0e89d

…refactor

github-actions bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 28, 2025

eric-wieser added 4 commits June 28, 2025 23:07

accept all changes from #26459

2da1569

Merge commit '9c06a13f37486ffa13042ea626a24e155f695ada' into with-lp-…

d9fe547

…refactor

Merge commit '78a26d50f75f061fd291597f9261ed07798139ba' into with-lp-…

fba5bd2

…refactor

Revert "accept all changes from #26459"

7bb5303

This reverts commit 2da1569.

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 28, 2025

eric-wieser added the WIP Work in progress label Jun 28, 2025

eric-wieser marked this pull request as draft June 28, 2025 23:10

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 5, 2025

Paul-Lez closed this Aug 4, 2025

YaelDillies deleted the with-lp-refactor branch August 4, 2025 15:11

Conversation

Paul-Lez commented Apr 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Apr 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 78a26d50f7

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented Apr 25, 2025

Uh oh!

Uh oh!

eric-wieser left a comment

Choose a reason for hiding this comment

Uh oh!

YaelDillies commented Apr 26, 2025

Uh oh!

eric-wieser commented Apr 26, 2025

Uh oh!

Paul-Lez commented Apr 26, 2025

Uh oh!

YaelDillies commented Apr 26, 2025

Uh oh!

Paul-Lez commented Apr 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

leanprover-community-bot-assistant commented Apr 27, 2025

Uh oh!

eric-wieser commented Jun 28, 2025

Uh oh!

leanprover-community-bot-assistant commented Jul 5, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Paul-Lez commented Apr 21, 2025 •

edited

Loading

github-actions bot commented Apr 21, 2025 •

edited

Loading

Paul-Lez commented Apr 26, 2025 •

edited

Loading