[Merged by Bors] - fix: cleanup measurability + prod/sum lemmas + fun_prop by fpvandoorn · Pull Request #25254 · leanprover-community/mathlib4

fpvandoorn · 2025-05-28T10:44:09Z

Add fun_prop to a few more lemmas
Rename the compositional version to something without a prime, add the compositional version for StronglyMeasurable
use the prod/fun_prod naming scheme (the compositional version is called prod_apply) for [AE][Strongly]Measurable

github-actions · 2025-05-28T10:45:27Z

PR summary 36bd1b9d93

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ Finset.aemeasurable_fun_prod
+ Finset.aemeasurable_sum'
+ Finset.measurable_fun_prod
+ Finset.measurable_prod_apply
+ Finset.measurable_sum'
+ Finset.stronglyMeasurable_prod_apply
+ List.aemeasurable_fun_prod
+ List.aemeasurable_sum'
+ List.measurable_fun_prod
+ List.measurable_sum'
+ Multiset.aemeasurable_fun_prod
+ Multiset.aemeasurable_sum'
+ Multiset.measurable_fun_prod
+ Multiset.measurable_sum'
+ _root_.Finset.aestronglyMeasurable_fun_prod
+ _root_.Finset.aestronglyMeasurable_sum'
+ _root_.Finset.stronglyMeasurable_fun_prod
+ _root_.Finset.stronglyMeasurable_sum'
+ _root_.List.aestronglyMeasurable_fun_prod
+ _root_.List.aestronglyMeasurable_sum'
+ _root_.List.stronglyMeasurable_fun_prod
+ _root_.List.stronglyMeasurable_sum'
+ _root_.Multiset.aestronglyMeasurable_fun_prod
+ _root_.Multiset.aestronglyMeasurable_sum'
+ _root_.Multiset.stronglyMeasurable_fun_prod
+ _root_.Multiset.stronglyMeasurable_sum'
+ measurable_fun_sum
+++ measurable_fun_prod
- measurable_sum
--- measurable_prod

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>

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

No changes to technical debt.

You can run this locally as

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

Mathlib/MeasureTheory/Group/Arithmetic.lean

…op, rename the compositional version

sgouezel · 2025-06-05T13:54:39Z

Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean


 @[to_additive (attr := fun_prop, measurability)]
-theorem _root_.List.aestronglyMeasurable_prod' (l : List (α → M))
+theorem _root_.List.aestronglyMeasurable_fun_prod (l : List (α → M))


I don't think that's the correct naming scheme: fun_prod should be used when there is fun somewhere, but there is no fun here. I'd call this one aestronglyMeasurable_prod, and the next one aestronglyMeasurable_fun_prod. Same thing below.

Oh, I indeed misread your previous suggestion. So the fun stands for the function-abstraction? I thought it stood for "take the product of functions" (instead of functions applied to an argument). Can you link to a Zulip discussion (or the conventions, if it's explicitly mentioned there), before I change this again?

https://leanprover-community.github.io/contribute/naming.html#unexpanded-and-expanded-forms-of-functions

I've swapped the names

RemyDegenne

@fpvandoorn it would be nice if you could find time to fix CI on this PR. It's close to being mergeable.

Mathlib/MeasureTheory/Group/Arithmetic.lean

Co-authored-by: Rémy Degenne <remydegenne@gmail.com>

sgouezel · 2025-07-15T18:15:04Z

Can you merge master? When I do lake exe cache get I don't get the full cache so maybe something went wrong (especially since it's a PR not from a fork, so less tested these days)

sgouezel

bors d+
Thanks!

Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

Mathlib/MeasureTheory/Group/Arithmetic.lean

mathlib-bors · 2025-07-15T18:17:33Z

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

grunweg · 2025-08-01T14:26:29Z

(Friendly reminder to push the button here.)

fpvandoorn · 2025-08-04T14:45:33Z

bors merge

* Add `fun_prop` to a few more lemmas * Rename the compositional version to something without a prime, add the compositional version for `StronglyMeasurable` * use the `prod/fun_prod` naming scheme (the compositional version is called `prod_apply`) for `[AE][Strongly]Measurable` Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com> Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

mathlib-bors · 2025-08-04T14:59:50Z

Build failed (retrying...):

CI Success

* Add `fun_prop` to a few more lemmas * Rename the compositional version to something without a prime, add the compositional version for `StronglyMeasurable` * use the `prod/fun_prod` naming scheme (the compositional version is called `prod_apply`) for `[AE][Strongly]Measurable` Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com> Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

mathlib-bors · 2025-08-04T15:14:47Z

Pull request successfully merged into master.

Build succeeded:

CI Success

…ommunity#25254) * Add `fun_prop` to a few more lemmas * Rename the compositional version to something without a prime, add the compositional version for `StronglyMeasurable` * use the `prod/fun_prod` naming scheme (the compositional version is called `prod_apply`) for `[AE][Strongly]Measurable` Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com> Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

fix: some fun_prop dixes

b465d4e

github-actions bot added the t-measure-probability Measure theory / Probability theory label May 28, 2025

sgouezel reviewed May 28, 2025

View reviewed changes

Mathlib/MeasureTheory/Group/Arithmetic.lean Outdated Show resolved Hide resolved

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label May 28, 2025

rename lemmas

f5c9696

fpvandoorn added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels May 30, 2025

use the prod/fun_prod naming scheme, tag some more lemmas with fun_pr…

e0fd9b7

…op, rename the compositional version

fpvandoorn changed the title ~~fix: strengthen fun_prop lemma, add two fun_props~~ fix: cleanup measurability + prod/sum lemmas + fun_prop May 30, 2025

fpvandoorn added 3 commits June 4, 2025 12:01

fix

98b07f9

one more fix

faaf0c1

Merge remote-tracking branch 'origin/master' into funpropfix

89e7d63

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 4, 2025

fpvandoorn requested a review from sgouezel June 4, 2025 23:21

sgouezel reviewed Jun 5, 2025

View reviewed changes

sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 5, 2025

fpvandoorn added 3 commits June 24, 2025 18:02

interchange names (todo: check)

99bcbe9

also translate sum

89a591d

fix

1aa02b9

fpvandoorn added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 24, 2025

RemyDegenne reviewed Jul 11, 2025

View reviewed changes

Mathlib/MeasureTheory/Group/Arithmetic.lean Outdated Show resolved Hide resolved

fpvandoorn and others added 4 commits July 14, 2025 08:25

Update Mathlib/MeasureTheory/Group/Arithmetic.lean

8330b4e

Co-authored-by: Rémy Degenne <remydegenne@gmail.com>

fix capitalization

4efe9b8

one more fix

f0ff111

fix

b8f3f07

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jul 15, 2025

fpvandoorn requested review from RemyDegenne and sgouezel July 15, 2025 16:45

sgouezel reviewed Jul 15, 2025

View reviewed changes

Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean Outdated Show resolved Hide resolved

Mathlib/MeasureTheory/Group/Arithmetic.lean Outdated Show resolved Hide resolved

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jul 15, 2025

Merge remote-tracking branch 'origin/master' into funpropfix

8db7491

grunweg mentioned this pull request Aug 1, 2025

Funpropfix mr #27806

Merged

github-actions bot added large-import Automatically added label for PRs with a significant increase in transitive imports file-removed A Lean module was (re)moved without a `deprecated_module` annotation labels Aug 1, 2025

fpvandoorn force-pushed the funpropfix branch from 6b17478 to 8db7491 Compare August 1, 2025 10:52

Merge remote-tracking branch 'origin/master' into funpropfix

7f3e7e9

github-actions bot removed large-import Automatically added label for PRs with a significant increase in transitive imports file-removed A Lean module was (re)moved without a `deprecated_module` annotation labels Aug 1, 2025

Review comments

d803039

ghost added the ready-to-merge This PR has been sent to bors. label Aug 4, 2025

mathlib-bors bot changed the title ~~fix: cleanup measurability + prod/sum lemmas + fun_prop~~ [Merged by Bors] - fix: cleanup measurability + prod/sum lemmas + fun_prop Aug 4, 2025

mathlib-bors bot closed this Aug 4, 2025

mathlib-bors bot deleted the funpropfix branch August 4, 2025 15:14

Conversation

fpvandoorn commented May 28, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented May 28, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 36bd1b9d93

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

sgouezel Jun 5, 2025

Choose a reason for hiding this comment

Uh oh!

fpvandoorn Jun 5, 2025

Choose a reason for hiding this comment

Uh oh!

sgouezel Jun 5, 2025

Choose a reason for hiding this comment

Uh oh!

fpvandoorn Jun 24, 2025

Choose a reason for hiding this comment

Uh oh!

RemyDegenne left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

sgouezel commented Jul 15, 2025

Uh oh!

sgouezel left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

mathlib-bors bot commented Jul 15, 2025

Uh oh!

grunweg commented Aug 1, 2025

Uh oh!

fpvandoorn commented Aug 4, 2025

Uh oh!

mathlib-bors bot commented Aug 4, 2025

Uh oh!

mathlib-bors bot commented Aug 4, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

fpvandoorn commented May 28, 2025 •

edited

Loading

github-actions bot commented May 28, 2025 •

edited

Loading