Skip to content

[Merged by Bors] - feat: if a sigma-algebra is independent from itself then all sets in it have measure 0 or 1#39750

Closed
mathlib-splicebot[bot] wants to merge 3 commits into
masterfrom
splice-bot/pr-37259-Mathlib-Probability-Independence-ZeroOne.lean-1106d86409-k7j2uz0
Closed

[Merged by Bors] - feat: if a sigma-algebra is independent from itself then all sets in it have measure 0 or 1#39750
mathlib-splicebot[bot] wants to merge 3 commits into
masterfrom
splice-bot/pr-37259-Mathlib-Probability-Independence-ZeroOne.lean-1106d86409-k7j2uz0

Conversation

@mathlib-splicebot

@mathlib-splicebot mathlib-splicebot Bot commented May 23, 2026 •
edited by EtienneC30
Loading

Copy link
Copy Markdown
Contributor

@EtienneC30 EtienneC30 changed the title chore(Mathlib/Probability/Independence/ZeroOne.lean): automated extraction feat: if a sigma-algebra is independent from itself then all sets in it have measure 0 or 1 May 23, 2026
@EtienneC30 EtienneC30 added t-measure-probability Measure theory / Probability theory brownian Part of the ongoing formalization of the Brownian motion and stochastic integrals labels May 23, 2026
@github-actions

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

Copy link
Copy Markdown

PR summary c0a4362b73

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Kernel.measure_eq_zero_or_one_of_indep_self
+ measure_eq_zero_or_one_of_indep_self

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.

@EtienneC30 EtienneC30 mentioned this pull request May 23, 2026
Draft
6 tasks
vihdzp
vihdzp reviewed May 23, 2026
View reviewed changes
Comment thread Mathlib/Probability/Independence/ZeroOne.lean

lemma measure_eq_zero_or_one_of_indep_self [IsFiniteMeasure μ] (hm : Indep m m μ)
{t : Set Ω} (ht : MeasurableSet[m] t) :
μ t = 0 ∨ μ t = 1 := by

@vihdzp vihdzp May 23, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

Can we use MeasureTheory.IsZeroOneMeasure to state this?

@EtienneC30 EtienneC30 May 23, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

I don't think so, the statement might be IsZeroOneMeasure (µ.trim m _) but this would require m to be smaller than the ambient sigma-algebra, which is not needed here.

@mathlib-dependent-issues mathlib-dependent-issues Bot added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels May 23, 2026
@mathlib-dependent-issues

mathlib-dependent-issues Bot commented May 26, 2026

Copy link
Copy Markdown

This PR/issue depends on:

RemyDegenne
RemyDegenne approved these changes May 27, 2026
View reviewed changes

@RemyDegenne RemyDegenne left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Thanks!
bors r+

@mathlib-triage mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label May 27, 2026
mathlib-bors Bot pushed a commit that referenced this pull request May 27, 2026
@mathlib-splicebot @EtienneC30
feat: if a sigma-algebra is independent from itself then all sets in …
3b514fe 
…it have measure `0` or `1` (#39750)

This PR was automatically created from PR #37259 by @EtienneC30 via a [review comment](#37259 (comment)) by @EtienneC30.

- [x] depends on: #39748

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

mathlib-bors Bot commented May 27, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title feat: if a sigma-algebra is independent from itself then all sets in it have measure 0 or 1 [Merged by Bors] - feat: if a sigma-algebra is independent from itself then all sets in it have measure 0 or 1 May 27, 2026
@mathlib-bors mathlib-bors Bot closed this May 27, 2026
grunweg pushed a commit to grunweg/mathlib4 that referenced this pull request May 30, 2026
@mathlib-splicebot @EtienneC30 @grunweg
feat: if a sigma-algebra is independent from itself then all sets in …
1e84224 
…it have measure `0` or `1` (leanprover-community#39750)

This PR was automatically created from PR leanprover-community#37259 by @EtienneC30 via a [review comment](leanprover-community#37259 (comment)) by @EtienneC30.

- [x] depends on: leanprover-community#39748

Co-authored-by: EtienneC30 <66847262+EtienneC30@users.noreply.github.com>
Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>
b-mehta pushed a commit to b-mehta/mathlib4 that referenced this pull request Jun 2, 2026
@mathlib-splicebot @EtienneC30 @b-mehta
feat: if a sigma-algebra is independent from itself then all sets in …
b910a04 
…it have measure `0` or `1` (leanprover-community#39750)

This PR was automatically created from PR leanprover-community#37259 by @EtienneC30 via a [review comment](leanprover-community#37259 (comment)) by @EtienneC30.

- [x] depends on: leanprover-community#39748

Co-authored-by: EtienneC30 <66847262+EtienneC30@users.noreply.github.com>
Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>
Bergschaf pushed a commit to Bergschaf/mathlib4 that referenced this pull request Jun 3, 2026
@mathlib-splicebot @EtienneC30 @Bergschaf
feat: if a sigma-algebra is independent from itself then all sets in …
e593011 
…it have measure `0` or `1` (leanprover-community#39750)

This PR was automatically created from PR leanprover-community#37259 by @EtienneC30 via a [review comment](leanprover-community#37259 (comment)) by @EtienneC30.

- [x] depends on: leanprover-community#39748

Co-authored-by: EtienneC30 <66847262+EtienneC30@users.noreply.github.com>
Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@EtienneC30 EtienneC30 EtienneC30 left review comments
@RemyDegenne RemyDegenne RemyDegenne approved these changes
+1 more reviewer
@vihdzp vihdzp vihdzp left review comments
Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

brownian Part of the ongoing formalization of the Brownian motion and stochastic integrals 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.

3 participants

@RemyDegenne @vihdzp @EtienneC30