Skip to content

[Merged by Bors] - feat: the identity function is a.e.-strongly measurable w.r.t. the map by an a.e.-strongly measurable function#39644

Closed
EtienneC30 wants to merge 3 commits into
leanprover-community:masterfrom
EtienneC30:asm_id
Closed

[Merged by Bors] - feat: the identity function is a.e.-strongly measurable w.r.t. the map by an a.e.-strongly measurable function#39644
EtienneC30 wants to merge 3 commits into
leanprover-community:masterfrom
EtienneC30:asm_id

Conversation

@EtienneC30

@EtienneC30 EtienneC30 commented May 21, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

If AEStronglyMeasurable f µ then AEStronglyMeasurable id (µ.map f). Contrary to aestronglyMeasurable_id this does not require the identity to be defined over a second-countable space as f has a.e.-separable range.

Open in Gitpod

@EtienneC30 EtienneC30 added the t-measure-probability Measure theory / Probability theory label May 21, 2026
@EtienneC30 EtienneC30 mentioned this pull request May 21, 2026
Closed
1 task
@github-actions

github-actions Bot commented May 21, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary 605d3215ac

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ aestronglyMeasurable_id_map
+ aestronglyMeasurable_id_of_isSeparable

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.
No changes to weak technical debt.

sgouezel
sgouezel reviewed May 21, 2026
View reviewed changes
Comment thread Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean Outdated
@sgouezel sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes. label May 21, 2026
@EtienneC30 EtienneC30 removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 21, 2026
@sgouezel

sgouezel commented May 21, 2026

Copy link
Copy Markdown
Contributor

bors r+
Thanks!

mathlib-bors Bot pushed a commit that referenced this pull request May 21, 2026
@EtienneC30
feat: the identity function is a.e.-strongly measurable w.r.t. the ma…
c642998 
…p by an a.e.-strongly measurable function (#39644)

If `AEStronglyMeasurable f µ` then `AEStronglyMeasurable id (µ.map f)`. Contrary to [aestronglyMeasurable_id](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.html#aestronglyMeasurable_id) this does not require the identity to be defined over a second-countable space as `f` has a.e.-separable range.
@mathlib-triage mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label May 21, 2026
@mathlib-bors

mathlib-bors Bot commented May 21, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title feat: the identity function is a.e.-strongly measurable w.r.t. the map by an a.e.-strongly measurable function [Merged by Bors] - feat: the identity function is a.e.-strongly measurable w.r.t. the map by an a.e.-strongly measurable function May 21, 2026
@mathlib-bors mathlib-bors Bot closed this May 21, 2026
RaggedR pushed a commit to RaggedR/mathlib4 that referenced this pull request May 22, 2026
@EtienneC30
feat: the identity function is a.e.-strongly measurable w.r.t. the ma…
0e99751 
…p by an a.e.-strongly measurable function (leanprover-community#39644)

If `AEStronglyMeasurable f µ` then `AEStronglyMeasurable id (µ.map f)`. Contrary to [aestronglyMeasurable_id](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.html#aestronglyMeasurable_id) this does not require the identity to be defined over a second-countable space as `f` has a.e.-separable range.
b-mehta pushed a commit to b-mehta/mathlib4 that referenced this pull request Jun 2, 2026
@EtienneC30 @b-mehta
feat: the identity function is a.e.-strongly measurable w.r.t. the ma…
527a6bb 
…p by an a.e.-strongly measurable function (leanprover-community#39644)

If `AEStronglyMeasurable f µ` then `AEStronglyMeasurable id (µ.map f)`. Contrary to [aestronglyMeasurable_id](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.html#aestronglyMeasurable_id) this does not require the identity to be defined over a second-countable space as `f` has a.e.-separable range.
Bergschaf pushed a commit to Bergschaf/mathlib4 that referenced this pull request Jun 3, 2026
@EtienneC30 @Bergschaf
feat: the identity function is a.e.-strongly measurable w.r.t. the ma…
6a9ea57 
…p by an a.e.-strongly measurable function (leanprover-community#39644)

If `AEStronglyMeasurable f µ` then `AEStronglyMeasurable id (µ.map f)`. Contrary to [aestronglyMeasurable_id](https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.html#aestronglyMeasurable_id) this does not require the identity to be defined over a second-countable space as `f` has a.e.-separable range.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sgouezel sgouezel sgouezel left review comments

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-measure-probability Measure theory / Probability theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@EtienneC30 @sgouezel