[Merged by Bors] - feat: drop completeness assumption in the definition of `setToFun`, expand API by sgouezel · Pull Request #39615 · leanprover-community/mathlib4

sgouezel · 2026-05-20T13:20:28Z

The definition of the Bochner integral and the vector measure integral handle the non-completeness of the space in a completely parallel way. To avoid duplication and streamline proofs, we move this handling of non-completeness one step higher, to the definition of setToFun. We also expand its API -- this is cherry-picked from a work on vector measure integrals that has highlighted the need for the lemmas I am adding here.

To minimize the size of the PR, I went for minimal fixes in the files on Bochner integrals and on conditional expectations. Further cleanup will be done in subsequent PRs.

github-actions · 2026-05-20T13:21:56Z

PR summary c02c766436

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ _root_.MeasureTheory.SimpleFunc.toLp
+ enorm_setToFun_le
+ norm_setToFun_le_toReal
+ norm_toL1_eq_lintegral_enorm
+ setToFun_add_left''
+ setToFun_congr_smul_measure'
+ setToFun_of_le_map
+ setToFun_of_le_map_of_stronglyMeasurable
+ setToFun_simpleFunc
- toLp

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.

RemyDegenne

Thanks!
bors d+

RemyDegenne · 2026-05-21T08:39:31Z

 0 if the function is not integrable. -/
 def setToFun (hT : DominatedFinMeasAdditive μ T C) (f : α → E) : F :=
-  if hf : Integrable f μ then L1.setToL1 hT (hf.toL1 f) else 0
+  if _hF : CompleteSpace F then


Please update the docstring to mention that new if condition.

mathlib-bors · 2026-05-21T08:41:46Z

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

sgouezel · 2026-05-21T08:51:57Z

bors r+
Thanks for the review!

…xpand API (#39615) The definition of the Bochner integral and the vector measure integral handle the non-completeness of the space in a completely parallel way. To avoid duplication and streamline proofs, we move this handling of non-completeness one step higher, to the definition of `setToFun`. We also expand its API -- this is cherry-picked from a work on vector measure integrals that has highlighted the need for the lemmas I am adding here. To minimize the size of the PR, I went for minimal fixes in the files on Bochner integrals and on conditional expectations. Further cleanup will be done in subsequent PRs. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

mathlib-bors · 2026-05-21T09:56:17Z

Pull request successfully merged into master.

Build succeeded:

…xpand API (leanprover-community#39615) The definition of the Bochner integral and the vector measure integral handle the non-completeness of the space in a completely parallel way. To avoid duplication and streamline proofs, we move this handling of non-completeness one step higher, to the definition of `setToFun`. We also expand its API -- this is cherry-picked from a work on vector measure integrals that has highlighted the need for the lemmas I am adding here. To minimize the size of the PR, I went for minimal fixes in the files on Bochner integrals and on conditional expectations. Further cleanup will be done in subsequent PRs.

…on (#39862) This is not interesting from a mathematical point of view (in all reasonable applications, the spaces are complete), but it is a direct byproduct of the change to `setToFun` in #39615, and it means that whenever we write conditional expectations the job of Lean is easier (as it doesn't have to look for completeness) and the resulting term is simpler. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

…xpand API (leanprover-community#39615) The definition of the Bochner integral and the vector measure integral handle the non-completeness of the space in a completely parallel way. To avoid duplication and streamline proofs, we move this handling of non-completeness one step higher, to the definition of `setToFun`. We also expand its API -- this is cherry-picked from a work on vector measure integrals that has highlighted the need for the lemmas I am adding here. To minimize the size of the PR, I went for minimal fixes in the files on Bochner integrals and on conditional expectations. Further cleanup will be done in subsequent PRs. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

…on (leanprover-community#39862) This is not interesting from a mathematical point of view (in all reasonable applications, the spaces are complete), but it is a direct byproduct of the change to `setToFun` in leanprover-community#39615, and it means that whenever we write conditional expectations the job of Lean is easier (as it doesn't have to look for completeness) and the resulting term is simpler. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

…xpand API (leanprover-community#39615) The definition of the Bochner integral and the vector measure integral handle the non-completeness of the space in a completely parallel way. To avoid duplication and streamline proofs, we move this handling of non-completeness one step higher, to the definition of `setToFun`. We also expand its API -- this is cherry-picked from a work on vector measure integrals that has highlighted the need for the lemmas I am adding here. To minimize the size of the PR, I went for minimal fixes in the files on Bochner integrals and on conditional expectations. Further cleanup will be done in subsequent PRs. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

…on (leanprover-community#39862) This is not interesting from a mathematical point of view (in all reasonable applications, the spaces are complete), but it is a direct byproduct of the change to `setToFun` in leanprover-community#39615, and it means that whenever we write conditional expectations the job of Lean is easier (as it doesn't have to look for completeness) and the resulting term is simpler. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

sgouezel added 2 commits May 20, 2026 15:17

cherry pick

e0d6e97

oops

f5b02e5

github-actions Bot added the t-measure-probability Measure theory / Probability theory label May 20, 2026

sgouezel added 3 commits May 20, 2026 15:23

oops again

b0c4b52

better

071393e

fix

6e48033

sgouezel mentioned this pull request May 20, 2026

feat: integration by parts for stieltjes vector measures #39113

Draft

33 tasks

RemyDegenne approved these changes May 21, 2026

View reviewed changes

mathlib-triage Bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label May 21, 2026

sgouezel commented May 21, 2026

View reviewed changes

Comment thread Mathlib/MeasureTheory/Integral/SetToL1.lean Outdated

sgouezel added 2 commits May 21, 2026 10:46

Apply suggestion from @sgouezel

f1aef7c

file-level docstring

c02c766

mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label May 21, 2026

mathlib-bors Bot changed the title ~~feat: drop completeness assumption in the definition of setToFun, expand API~~ [Merged by Bors] - feat: drop completeness assumption in the definition of setToFun, expand API May 21, 2026

mathlib-bors Bot closed this May 21, 2026

This was referenced May 24, 2026

[Merged by Bors] - feat(MeasureTheory): the integral of a vector-valued function against a vector measure is additive #30230

Closed

[Merged by Bors] - chore: drop completeness from the definition of conditional expectation #39862

Closed

sgouezel deleted the SG_noComplete branch June 9, 2026 15:23

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

[Merged by Bors] - feat: drop completeness assumption in the definition of `setToFun`, expand API#39615

[Merged by Bors] - feat: drop completeness assumption in the definition of `setToFun`, expand API#39615
sgouezel wants to merge 7 commits into
leanprover-community:masterfrom
sgouezel:SG_noComplete

sgouezel commented May 20, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented May 20, 2026 •

edited

Loading

Declarations diff

Uh oh!

RemyDegenne left a comment

Uh oh!

RemyDegenne May 21, 2026

Uh oh!

mathlib-bors Bot commented May 21, 2026

Uh oh!

Uh oh!

sgouezel commented May 21, 2026

Uh oh!

mathlib-bors Bot commented May 21, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

sgouezel commented May 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented May 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary c02c766436

Import changes for modified files

Declarations diff

Uh oh!

RemyDegenne left a comment

Choose a reason for hiding this comment

Uh oh!

RemyDegenne May 21, 2026

Choose a reason for hiding this comment

Uh oh!

mathlib-bors Bot commented May 21, 2026

Uh oh!

Uh oh!

sgouezel commented May 21, 2026

Uh oh!

mathlib-bors Bot commented May 21, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

sgouezel commented May 20, 2026 •

edited

Loading

github-actions Bot commented May 20, 2026 •

edited

Loading