Skip to content

[Merged by Bors] - feat(Decomposition/Lebesgue): SigmaFinite -> SFinite#14658

Closed
urkud wants to merge 13 commits intomasterfrom
YK-meas-sfinite
Closed

[Merged by Bors] - feat(Decomposition/Lebesgue): SigmaFinite -> SFinite#14658
urkud wants to merge 13 commits intomasterfrom
YK-meas-sfinite

Conversation

@urkud
Copy link
Copy Markdown
Member

@urkud urkud commented Jul 11, 2024 •
edited
Loading

Also generalize exists_absolutelyContinuous_isFiniteMeasure and some downstream lemmas.

Deletions:

  • MeasureTheory.Measure.restrict.instIsFiniteMeasure

Open in Gitpod

@urkud urkud added the t-measure-probability Measure theory / Probability theory label Jul 11, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 11, 2024 •
edited
Loading

PR summary 8b608b8fb7

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ HaveLebesgueDecomposition.add_left
+ HaveLebesgueDecomposition.sfinite_of_isFiniteMeasure
+ HaveLebesgueDecomposition.sum_left
+ instance (priority := 100) haveLebesgueDecomposition_of_sigmaFinite
- instance (priority := 100) haveLebesgueDecomposition_of_sigmaFinite (μ ν : Measure α)
- restrict.instIsFiniteMeasure

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>

@urkud urkud marked this pull request as ready for review July 11, 2024 19:10
@urkud urkud changed the title feat(MeasureTheory): weaken more SigmaFinite assumptions to SFinite feat(Decomposition/Lebesgue): SigmaFinite -> SFinite Jul 11, 2024
@urkud urkud added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jul 11, 2024
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jul 11, 2024
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Jul 12, 2024

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jul 12, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 12, 2024
@urkud
feat(Decomposition/Lebesgue): SigmaFinite -> SFinite (#14658)
de62025 
Also generalize `exists_absolutelyContinuous_isFiniteMeasure` and some downstream lemmas.

Deletions:
- MeasureTheory.Measure.restrict.instIsFiniteMeasure
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 12, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Decomposition/Lebesgue): SigmaFinite -> SFinite [Merged by Bors] - feat(Decomposition/Lebesgue): SigmaFinite -> SFinite Jul 12, 2024
@mathlib-bors mathlib-bors bot closed this Jul 12, 2024
@mathlib-bors mathlib-bors bot deleted the YK-meas-sfinite branch July 12, 2024 23:25
@adomani adomani mentioned this pull request Aug 1, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

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

@urkud @kim-em