Skip to content

[Merged by Bors] - chore: mark measure_union_ne_top and friends with finiteness#30967

Closed
grunweg wants to merge 3 commits intoleanprover-community:masterfrom
grunweg:measure-union-finite
Closed

[Merged by Bors] - chore: mark measure_union_ne_top and friends with finiteness#30967
grunweg wants to merge 3 commits intoleanprover-community:masterfrom
grunweg:measure-union-finite

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented Oct 27, 2025 •
edited
Loading

In some cases, add ≠ ∞ versions of existing < ∞ lemmas, and tag those with finiteness.
Use this to golf one proof by measurability using finiteness, which is the morally correct proof.
Motivated by #30966.

Open in Gitpod

@grunweg grunweg added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Oct 27, 2025
@github-actions github-actions bot added the t-measure-probability Measure theory / Probability theory label Oct 27, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 27, 2025 •
edited
Loading

PR summary e43769cf2a

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ measure_biUnion_ne_top
+ measure_inter_ne_top_of_left_ne_top
+ measure_inter_ne_top_of_right_ne_top

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

@ghost
Copy link
Copy Markdown

ghost commented Oct 27, 2025

!bench

@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 Oct 27, 2025
@ghost
Copy link
Copy Markdown

ghost commented Oct 27, 2025

!bench

@grunweg grunweg mentioned this pull request Oct 27, 2025
Draft
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Oct 27, 2025

Here are the benchmark results for commit c45709e.
There were no significant changes against commit 2b63991.

@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 27, 2025

File Instructions %
build +11.7⬝10⁹ (+0.00%)
lint +1.448⬝10⁹ (+0.02%)
3 files, Instructions +1.0⬝10⁹
File Instructions %
Mathlib.MeasureTheory.Measure.Real +1.388⬝10⁹ (+6.75%)
Mathlib.MeasureTheory.Measure.MeasureSpaceDef +1.228⬝10⁹ (+6.25%)
Mathlib.MeasureTheory.Measure.Typeclasses.Finite +1.184⬝10⁹ (+4.25%)
2 files, Instructions -2.0⬝10⁹
File Instructions %
Mathlib.Computability.TuringMachine -1.58⬝10⁹ (-3.13%)
Mathlib.LinearAlgebra.DirectSum.TensorProduct -1.251⬝10⁹ (-4.69%)
File Instructions %
Mathlib.MeasureTheory.Function.UnifTight -6.283⬝10⁹ (-22.21%)
CI run Lakeprof report

@grunweg grunweg force-pushed the measure-union-finite branch from c45709e to 6f8d3a1 Compare October 28, 2025 13:16
@grunweg grunweg mentioned this pull request Oct 28, 2025
Closed
1 task
@grunweg grunweg force-pushed the measure-union-finite branch from 6f8d3a1 to fccac75 Compare October 28, 2025 22:05
@ghost
Copy link
Copy Markdown

ghost commented Oct 28, 2025

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Oct 28, 2025

Here are the benchmark results for commit fccac75.
There were no significant changes against commit e43769c.

@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 28, 2025

File Instructions %
build -15.550⬝10⁹ (+0.00%)
2 files, Instructions +1.0⬝10⁹
File Instructions %
Mathlib.AlgebraicGeometry.GammaSpecAdjunction +1.361⬝10⁹ (+1.75%)
Mathlib.MeasureTheory.Measure.MeasureSpaceDef +1.32⬝10⁹ (+5.21%)
File Instructions %
Mathlib.MeasureTheory.Function.UnifTight -6.79⬝10⁹ (-21.57%)
CI run Lakeprof report

fpvandoorn
fpvandoorn reviewed Oct 29, 2025
View reviewed changes
fpvandoorn
fpvandoorn approved these changes Oct 29, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@fpvandoorn fpvandoorn left a comment

Choose a reason for hiding this comment

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

LGTM

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 29, 2025

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

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Oct 29, 2025
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Oct 29, 2025

Thanks for the quick review!
bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Oct 29, 2025
mathlib-bors bot pushed a commit that referenced this pull request Oct 29, 2025
@grunweg
chore: mark measure_union_ne_top and friends with finiteness (#30967)
15ee1d2 
In some cases, add `≠ ∞` versions of existing `< ∞` lemmas, and tag those with finiteness.
Use this to golf one proof `by measurability` using finiteness, which is the morally correct proof.
Motivated by #30966.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 29, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: mark measure_union_ne_top and friends with finiteness [Merged by Bors] - chore: mark measure_union_ne_top and friends with finiteness Oct 29, 2025
@mathlib-bors mathlib-bors bot closed this Oct 29, 2025
@grunweg grunweg deleted the measure-union-finite branch October 29, 2025 14:34
BeibeiX0 pushed a commit to BeibeiX0/mathlib4 that referenced this pull request Nov 7, 2025
@grunweg @BeibeiX0
chore: mark measure_union_ne_top and friends with finiteness (leanpro…
a5fa675 
…ver-community#30967)

In some cases, add `≠ ∞` versions of existing `< ∞` lemmas, and tag those with finiteness.
Use this to golf one proof `by measurability` using finiteness, which is the morally correct proof.
Motivated by leanprover-community#30966.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@fpvandoorn fpvandoorn fpvandoorn approved these changes

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). 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

@grunweg @leanprover-bot @fpvandoorn