Skip to content

[Merged by Bors] - feat(Integral.Bochner.Set): add tendsto_setIntegral_of_monotone₀#34025

Closed
lua-vr wants to merge 2 commits intoleanprover-community:masterfrom
lua-vr:tendsto_monotone_ae
Closed

[Merged by Bors] - feat(Integral.Bochner.Set): add tendsto_setIntegral_of_monotone₀#34025
lua-vr wants to merge 2 commits intoleanprover-community:masterfrom
lua-vr:tendsto_monotone_ae

Conversation

@lua-vr
Copy link
Copy Markdown
Contributor

@lua-vr lua-vr commented Jan 16, 2026

Adds the lemma tendsto_setIntegral_of_monotone₀, a version of tendsto_setIntegral_of_monotone requiring only AEMeasurableSet in the hypotheses. The previous version is redefined as a specialization.

Also renames integral_union_ae to setIntegral_union₀ for consistency with the rest of the library (it matches the existing setIntegral_union).

Open in Gitpod

Re-opened from #33206 and now taking respect for Windows users (thanks @ADedecker :).

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 16, 2026 •
edited
Loading

PR summary 721b21cf2b

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ setIntegral_diff
+ setIntegral_diff₀
+ setIntegral_union₀
+ tendsto_setIntegral_of_monotone₀

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

@github-actions github-actions bot added the t-measure-probability Measure theory / Probability theory label Jan 16, 2026
@lua-vr lua-vr mentioned this pull request Jan 16, 2026
Open
3 tasks
@lua-vr lua-vr force-pushed the tendsto_monotone_ae branch from a71da8e to a3db36c Compare January 16, 2026 03:15
ocfnash
ocfnash approved these changes Feb 17, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@ocfnash ocfnash left a comment

Choose a reason for hiding this comment

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

Thanks, including for the naming fix.

I note that many other lemmas in this file seem to be misnamed, e.g., integral_inter_add_diff₀. If you have any interest in helping us solve this in a follow-up PR this would be very welcome :-)

bors d+

Mathlib/MeasureTheory/Integral/Bochner/Set.lean Outdated
∫ x in s ∪ t, f x ∂μ = ∫ x in s, f x ∂μ + ∫ x in t, f x ∂μ := by
simp only [Measure.restrict_union₀ hst ht, integral_add_measure hfs hft]

@[deprecated (since := "2025-12-22")] alias integral_union_ae := setIntegral_union₀
Copy link
Copy Markdown
Contributor

@ocfnash ocfnash Feb 17, 2026

Choose a reason for hiding this comment

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

Let's bump this date:

Suggested change
@[deprecated (since := "2025-12-22")] alias integral_union_ae := setIntegral_union₀
@[deprecated (since := "2026-02-17")] alias integral_union_ae := setIntegral_union₀

Mathlib/MeasureTheory/Integral/Bochner/Set.lean Outdated
setIntegral_union₀ hst.aedisjoint ht.nullMeasurableSet hfs hft

theorem integral_diff (ht : MeasurableSet t) (hfs : IntegrableOn f s μ) (hts : t ⊆ s) :
theorem integral_diff₀ (ht : NullMeasurableSet t μ) (hfs : IntegrableOn f s μ) (hts : t ⊆ s) :
Copy link
Copy Markdown
Contributor

@ocfnash ocfnash Feb 17, 2026

Choose a reason for hiding this comment

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

Shouldn't this be:

Suggested change
theorem integral_diff₀ (ht : NullMeasurableSet t μ) (hfs : IntegrableOn f s μ) (hts : t ⊆ s) :
theorem setIntegral_sdiff₀ (ht : NullMeasurableSet t μ) (hfs : IntegrableOn f s μ) (hts : t ⊆ s) :

Mathlib/MeasureTheory/Integral/Bochner/Set.lean Outdated
rw [eq_sub_iff_add_eq, ← setIntegral_union₀, diff_union_of_subset hts]
exacts [disjoint_sdiff_self_left.aedisjoint, ht, hfs.mono_set diff_subset, hfs.mono_set hts]

theorem integral_diff (ht : MeasurableSet t) (hfs : IntegrableOn f s μ) (hts : t ⊆ s) :
Copy link
Copy Markdown
Contributor

@ocfnash ocfnash Feb 17, 2026

Choose a reason for hiding this comment

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

Again I think this should be:

Suggested change
theorem integral_diff (ht : MeasurableSet t) (hfs : IntegrableOn f s μ) (hts : t ⊆ s) :
theorem setIntegral_diff (ht : MeasurableSet t) (hfs : IntegrableOn f s μ) (hts : t ⊆ s) :

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 17, 2026

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

@mathlib-triage mathlib-triage bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Feb 17, 2026
@lua-vr
Copy link
Copy Markdown
Contributor Author

lua-vr commented Mar 5, 2026

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Mar 5, 2026
@lua-vr
feat(Integral.Bochner.Set): add tendsto_setIntegral_of_monotone₀ (#…
592989b 
…34025)

Adds the lemma `tendsto_setIntegral_of_monotone₀`, a version of `tendsto_setIntegral_of_monotone` requiring only `AEMeasurableSet` in the hypotheses. The previous version is redefined as a specialization.

Also renames `integral_union_ae` to `setIntegral_union₀` for consistency with the rest of the library (it matches the existing `setIntegral_union`).
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 5, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Integral.Bochner.Set): add tendsto_setIntegral_of_monotone₀ [Merged by Bors] - feat(Integral.Bochner.Set): add tendsto_setIntegral_of_monotone₀ Mar 5, 2026
@mathlib-bors mathlib-bors bot closed this Mar 5, 2026
seewoo5 pushed a commit to seewoo5/mathlib4 that referenced this pull request Mar 9, 2026
@lua-vr @seewoo5
feat(Integral.Bochner.Set): add tendsto_setIntegral_of_monotone₀ (l…
c0d9e0b 
…eanprover-community#34025)

Adds the lemma `tendsto_setIntegral_of_monotone₀`, a version of `tendsto_setIntegral_of_monotone` requiring only `AEMeasurableSet` in the hypotheses. The previous version is redefined as a specialization.

Also renames `integral_union_ae` to `setIntegral_union₀` for consistency with the rest of the library (it matches the existing `setIntegral_union`).
xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Mar 10, 2026
@lua-vr @xroblot
feat(Integral.Bochner.Set): add tendsto_setIntegral_of_monotone₀ (l…
69c9224 
…eanprover-community#34025)

Adds the lemma `tendsto_setIntegral_of_monotone₀`, a version of `tendsto_setIntegral_of_monotone` requiring only `AEMeasurableSet` in the hypotheses. The previous version is redefined as a specialization.

Also renames `integral_union_ae` to `setIntegral_union₀` for consistency with the rest of the library (it matches the existing `setIntegral_union`).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@ocfnash ocfnash ocfnash approved these changes

Assignees

@kex-y kex-y

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

@lua-vr @ocfnash @kex-y