[Merged by Bors] - chore: split `WithLp.equiv` into a new pair `WithLp.toLp`/`WithLp.ofLp` by eric-wieser · Pull Request #26459 · leanprover-community/mathlib4

eric-wieser · 2025-06-27T00:53:44Z

(WithLp.equiv p _).symm v is very inconvenient as a normal form when working with WithLp.

This introduces WithLp.toLp p v as the simp-normal spelling of this operation, and v'.ofLp as the simp-normal spelling of WithLp.equiv p _ v'. It then deprecates almost all the lemmas about WithLp.equiv, as these are no longer stated in simp-normal form.

The motivation for making toLp and ofLp as plain functions, as opposed to Equivs, is to permit them to be later adapted into a constructor and projection of a one-field structure. Almost nothing in mathlib needs them to be equivs anyway.

Zulip thread: #mathlib4 > defeq abuse in `WithLp` @ 💬

Co-authored-by: Yael Dillies yael.dillies@gmail.com
Co-authored-by: Paul Lezeau paul.lezeau@gmail.com

Alternative to #24261, which makes toLp and ofLp plain functions, and does not touch any of the existing equivs beside making them not simp-normal.

…fLp`

Co-authored-by: EtienneC30 <66847262+EtienneC30@users.noreply.github.com>

…unity/mathlib4 into with-lp-refactor

github-actions · 2025-06-27T00:54:58Z

PR summary 508c1928c2

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ EuclideanSpace.inner_toLp_toLp
+ EuclideanSpace.ofLp_single
+ EuclideanSpace.toLp_single
+ PiLp.volume_preserving_ofLp
+ PiLp.volume_preserving_toLp
+ antilipschitzWith_ofLp
+ continuous_ofLp
+ continuous_toLp
+ dist_toLp_fst
+ dist_toLp_single_same
+ dist_toLp_snd
+ edist_toLp_fst
+ edist_toLp_single_same
+ edist_toLp_snd
+ hasFDerivAt_ofLp
+ hasFDerivAt_toLp
+ hasStrictFDerivAt_ofLp
+ hasStrictFDerivAt_toLp
+ isometry_ofLp_infty
+ lipschitzWith_ofLp
+ measurable_ofLp
+ measurable_toLp
+ nndist_toLp_fst
+ nndist_toLp_single_same
+ nndist_toLp_snd
+ nnnorm_ofLp
+ nnnorm_toLp
+ nnnorm_toLp_const
+ nnnorm_toLp_const'
+ nnnorm_toLp_inl
+ nnnorm_toLp_inr
+ nnnorm_toLp_one
+ nnnorm_toLp_single
+ norm_ofLp
+ norm_ofLp_crossProduct
+ norm_toLp
+ norm_toLp_const
+ norm_toLp_const'
+ norm_toLp_equivTuple
+ norm_toLp_fst
+ norm_toLp_one
+ norm_toLp_single
+ norm_toLp_snd
+ norm_toLp_symm_crossProduct
+ ofLp
+ ofLp_add
+ ofLp_apply
+ ofLp_eq_zero
+ ofLp_fst
+ ofLp_neg
+ ofLp_smul
+ ofLp_snd
+ ofLp_sub
+ ofLp_surjective
+ ofLp_toEuclideanCLM
+ ofLp_toEuclideanLin_apply
+ ofLp_toLp
+ ofLp_zero
+ piLp_ofLp_toEuclideanLin
+ prod_antilipschitzWith_ofLp
+ prod_continuous_ofLp
+ prod_continuous_toLp
+ prod_isometry_ofLp_infty
+ prod_lipschitzWith_ofLp
+ prod_nnnorm_ofLp
+ prod_nnnorm_toLp
+ prod_norm_ofLp
+ prod_norm_toLp
+ prod_uniformContinuous_ofLp
+ prod_uniformContinuous_toLp
+ toEuclideanCLM_toLp
+ toEuclideanLin_apply_piLp_toLp
+ toEuclideanLin_toLp
+ toLp
+ toLp_add
+ toLp_eq_zero
+ toLp_fst
+ toLp_neg
+ toLp_ofLp
+ toLp_smul
+ toLp_snd
+ toLp_sub
+ toLp_surjective
+ toLp_zero
+ uniformContinuous_ofLp
+ uniformContinuous_toLp
- antilipschitzWith_equiv_aux
- aux_cobounded_eq
- aux_uniformity_eq
- lipschitzWith_equiv_aux
- prod_antilipschitzWith_equiv_aux
- prod_aux_cobounded_eq
- prod_aux_uniformity_eq
- prod_lipschitzWith_equiv_aux
-++ toLp_apply

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

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

EtienneC30

Thanks!

Mathlib/Analysis/Normed/Lp/WithLp.lean

Mathlib/Analysis/Normed/Lp/ProdLp.lean

Mathlib/Analysis/Normed/Lp/MeasurableSpace.lean

Mathlib/LinearAlgebra/Matrix/Hermitian.lean

EtienneC30 · 2025-06-28T21:52:33Z

Thanks! For me it's good to go.
maintainer merge

github-actions · 2025-06-28T21:52:45Z

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

b-mehta · 2025-06-28T21:56:22Z

Thanks!

bors merge

…p` (#26459) `(WithLp.equiv p _).symm v` is very inconvenient as a normal form when working with `WithLp`. This introduces `WithLp.toLp p v` as the simp-normal spelling of this operation, and `v'.ofLp` as the simp-normal spelling of `WithLp.equiv p _ v'`. It then deprecates almost all the lemmas about `WithLp.equiv`, as these are no longer stated in simp-normal form. The motivation for making `toLp` and `ofLp` as plain functions, as opposed to `Equiv`s, is to permit them to be later adapted into a constructor and projection of a one-field structure. Almost nothing in mathlib needs them to be equivs anyway. Zulip thread: [#mathlib4 > defeq abuse in `WithLp` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/defeq.20abuse.20in.20.60WithLp.60/near/516241777) Co-authored-by: Yael Dillies <yael.dillies@gmail.com> Co-authored-by: Paul Lezeau <paul.lezeau@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

mathlib-bors · 2025-06-28T22:43:09Z

Pull request successfully merged into master.

Build succeeded:

CI Success

This reverts commit 2da1569.

…p` (leanprover-community#26459) `(WithLp.equiv p _).symm v` is very inconvenient as a normal form when working with `WithLp`. This introduces `WithLp.toLp p v` as the simp-normal spelling of this operation, and `v'.ofLp` as the simp-normal spelling of `WithLp.equiv p _ v'`. It then deprecates almost all the lemmas about `WithLp.equiv`, as these are no longer stated in simp-normal form. The motivation for making `toLp` and `ofLp` as plain functions, as opposed to `Equiv`s, is to permit them to be later adapted into a constructor and projection of a one-field structure. Almost nothing in mathlib needs them to be equivs anyway. Zulip thread: [#mathlib4 > defeq abuse in &leanprover-community#96;WithLp&leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/defeq.20abuse.20in.20.60WithLp.60/near/516241777) Co-authored-by: Yael Dillies <yael.dillies@gmail.com> Co-authored-by: Paul Lezeau <paul.lezeau@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

YaelDillies and others added 18 commits June 7, 2025 10:18

chore: replace WithLp.equiv with a new pair WithLp.toLp/`WithLp.o…

ab1fbe1

…fLp`

deprecated aliases

b98fc55

Merge remote-tracking branch 'origin/master' into with-lp-refactor

639d4e6

Apply suggestions from code review

4c6aa61

Co-authored-by: EtienneC30 <66847262+EtienneC30@users.noreply.github.com>

fix

abaddb2

fix

a8deea3

Merge branch 'with-lp-refactor' of https://github.com/leanprover-comm…

96ee668

…unity/mathlib4 into with-lp-refactor

abbrev isnt the right lemma

6e27473

bad names

7e4b631

fix

f4948aa

replace aliases

acb95e4

fix

5449ed3

undeprecate the equiv

9b1927e

reuse the non-deprecated proofs

713e3ee

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

e9e5a7c

undeprecate the equivs

25f8a61

fix

12db0ce

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

bd23dd4

eric-wieser added 6 commits June 27, 2025 01:10

shrink diff

2159f9e

reduce diff

f6dbb6a

fix the delaborator

578e450

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

bb1c001

fix and reduce diff

fac6683

fix

d29084a

eric-wieser requested a review from YaelDillies June 27, 2025 01:37

eric-wieser added 2 commits June 27, 2025 01:43

fix

a472783

fix test

751cff8

eric-wieser added the t-analysis Analysis (normed *, calculus) label Jun 27, 2025

eric-wieser marked this pull request as ready for review June 27, 2025 12:09

eric-wieser and others added 2 commits June 28, 2025 10:48

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

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

EtienneC30 reviewed Jun 28, 2025

View reviewed changes

EtienneC30 added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 28, 2025

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

fix build

add156b

replace fst/snd with inl/inr

cf0ee60

fun_prop

f96cb70

fix docstring

9c06a13

eric-wieser added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 28, 2025

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 28, 2025

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jun 28, 2025

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jun 28, 2025

mathlib-bors bot changed the title ~~chore: split WithLp.equiv into a new pair WithLp.toLp/WithLp.ofLp~~ [Merged by Bors] - chore: split WithLp.equiv into a new pair WithLp.toLp/WithLp.ofLp Jun 28, 2025

mathlib-bors bot closed this Jun 28, 2025

mathlib-bors bot deleted the eric-wieser/with-lp-refactor branch June 28, 2025 22:43

eric-wieser added a commit that referenced this pull request Jun 28, 2025

accept all changes from #26459

2da1569

eric-wieser added a commit that referenced this pull request Jun 28, 2025

Revert "accept all changes from #26459"

7bb5303

This reverts commit 2da1569.

eric-wieser mentioned this pull request Jun 28, 2025

chore: replace WithLp.equiv with a new pair WithLp.toLp/WithLp.ofLp #24261

Closed

b-mehta mentioned this pull request Oct 20, 2025

[Merged by Bors] - chore: remove old 2024-04 deprecations #27713

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore: split `WithLp.equiv` into a new pair `WithLp.toLp`/`WithLp.ofLp`#26459

[Merged by Bors] - chore: split `WithLp.equiv` into a new pair `WithLp.toLp`/`WithLp.ofLp`#26459
eric-wieser wants to merge 33 commits intomasterfrom
eric-wieser/with-lp-refactor

eric-wieser commented Jun 27, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Jun 27, 2025 •

edited

Loading

Declarations diff

Uh oh!

EtienneC30 left a comment •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

EtienneC30 commented Jun 28, 2025

Uh oh!

github-actions bot commented Jun 28, 2025

Uh oh!

b-mehta commented Jun 28, 2025

Uh oh!

mathlib-bors bot commented Jun 28, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

eric-wieser commented Jun 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary 508c1928c2

Import changes for modified files

Declarations diff

Uh oh!

EtienneC30 left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

EtienneC30 commented Jun 28, 2025

Uh oh!

github-actions bot commented Jun 28, 2025

Uh oh!

b-mehta commented Jun 28, 2025

Uh oh!

mathlib-bors bot commented Jun 28, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

eric-wieser commented Jun 27, 2025 •

edited

Loading

github-actions bot commented Jun 27, 2025 •

edited

Loading

EtienneC30 left a comment •

edited

Loading