Skip to content

[Merged by Bors] - feat: a measurable space structure on WithLp#26249

Closed
EtienneC30 wants to merge 18 commits intoleanprover-community:masterfrom
EtienneC30:measurableSpace_WithLp
Closed

[Merged by Bors] - feat: a measurable space structure on WithLp#26249
EtienneC30 wants to merge 18 commits intoleanprover-community:masterfrom
EtienneC30:measurableSpace_WithLp

Conversation

@EtienneC30
Copy link
Copy Markdown
Member

@EtienneC30 EtienneC30 commented Jun 21, 2025 •
edited
Loading

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 #24261. Define a BorelSpace instance.

Open in Gitpod

@EtienneC30 EtienneC30 added the t-measure-probability Measure theory / Probability theory label Jun 21, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 21, 2025 •
edited
Loading

PR summary ddf91f1569

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Analysis.Normed.Lp.MeasurableSpace (new file) 1838

Declarations diff

+ coe_toLp
+ coe_toLp_symm
+ measurableSpace
+ measurable_equiv
+ measurable_equiv_symm
+ toLp
+ toLp_apply
+ toLp_symm_apply
++ borelSpace

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

@EtienneC30 EtienneC30 marked this pull request as draft June 21, 2025 11:36
@EtienneC30 EtienneC30 marked this pull request as ready for review June 21, 2025 11:39
@EtienneC30 EtienneC30 marked this pull request as draft June 21, 2025 11:48
@EtienneC30 EtienneC30 marked this pull request as ready for review June 21, 2025 20:41
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 21, 2025
@EtienneC30 EtienneC30 force-pushed the measurableSpace_WithLp branch from a7387b2 to b79f4d2 Compare June 22, 2025 11:37
@EtienneC30 EtienneC30 mentioned this pull request Jun 22, 2025
Closed
2 tasks
RemyDegenne
RemyDegenne approved these changes Jun 23, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@RemyDegenne RemyDegenne left a comment

Choose a reason for hiding this comment

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

Looks good!
bors d+
(please wait for the PR this depends on to go through bors).

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 23, 2025

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

@RemyDegenne RemyDegenne added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jun 23, 2025
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 23, 2025
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Jun 23, 2025

This PR/issue depends on:

@EtienneC30
Copy link
Copy Markdown
Member Author

EtienneC30 commented Jun 23, 2025

Thanks!
bors merge

mathlib-bors bot pushed a commit that referenced this pull request Jun 23, 2025
@EtienneC30
feat: a measurable space structure on WithLp (#26249)
8b584e5 
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 #24261. Define a `BorelSpace` instance.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 23, 2025

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Jun 23, 2025
@EtienneC30
feat: a measurable space structure on WithLp (#26249)
f355283 
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 #24261. Define a `BorelSpace` instance.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 23, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: a measurable space structure on WithLp [Merged by Bors] - feat: a measurable space structure on WithLp Jun 23, 2025
@mathlib-bors mathlib-bors bot closed this Jun 23, 2025
Rida-Hamadani pushed a commit to Rida-Hamadani/mathlib4 that referenced this pull request Jun 24, 2025
@EtienneC30 @Rida-Hamadani
feat: a measurable space structure on WithLp (leanprover-community#…
4d5250d 
…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.
joelriou pushed a commit to joelriou/mathlib4 that referenced this pull request Jul 7, 2025
@EtienneC30 @joelriou
feat: a measurable space structure on WithLp (leanprover-community#…
653bf62 
…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.
callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025
@EtienneC30 @callesonne
feat: a measurable space structure on WithLp (leanprover-community#…
88cae1f 
…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.
@EtienneC30 EtienneC30 mentioned this pull request Aug 26, 2025
Closed
3 tasks
@EtienneC30 EtienneC30 mentioned this pull request Nov 2, 2025
Closed
mathlib-bors bot pushed a commit that referenced this pull request Nov 4, 2025
@EtienneC30
chore: remove redundant measurable space structure on WithLp (#31190)
d4c295d 
The `MeasurableSpace` structure over `WithLp` was introduced globally in [#26249](#26249), so the particular instances that were introduced for [NumberField.mixedEmbedding.euclidean.mixedSpace](https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.html#NumberField.mixedEmbedding.euclidean.mixedSpace) and `EuclideanSpace` are no longer needed.

The measurable space structure on `WithLp` is not imported in the file where [EuclideanSpace.measurableEquiv](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Measure/Haar/OfBasis.html#EuclideanSpace.measurableEquiv) is defined, so if I want to deprecate `EuclideanSpace.measurableEquiv` I either have to add a useless import, or deprecate the instances in the file instead of removing them. Thus I did not deprecate it and just removed it.
@EtienneC30 EtienneC30 deleted the measurableSpace_WithLp branch March 30, 2026 13:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@RemyDegenne RemyDegenne RemyDegenne approved these changes

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-measure-probability Measure theory / Probability theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@EtienneC30 @mathlib4-dependent-issues-bot @RemyDegenne