Skip to content

refactor(MeasureTheory): golf Mathlib/MeasureTheory/Function/AEEqOfIntegral#38350

Open
yuanyi-350 wants to merge 1 commit intoleanprover-community:masterfrom
yuanyi-350:M_1
Open

refactor(MeasureTheory): golf Mathlib/MeasureTheory/Function/AEEqOfIntegral#38350
yuanyi-350 wants to merge 1 commit intoleanprover-community:masterfrom
yuanyi-350:M_1

Conversation

@yuanyi-350
Copy link
Copy Markdown
Collaborator

  • refactors MeasureTheory/Function/AEEqOfIntegral by reusing the AEFinStronglyMeasurable zero-integral criterion for the integrable case
  • rewrites the integrable set-integral equality lemmas to delegate to the AEFinStronglyMeasurable versions instead of rebuilding the Lp and subtraction arguments inline

Extracted from #38104

Open in Gitpod

@yuanyi-350 yuanyi-350 added codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly labels Apr 22, 2026
@github-actions
Copy link
Copy Markdown

PR summary ee3a5404e5

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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 Apr 22, 2026
@yuanyi-350
Copy link
Copy Markdown
Collaborator Author

I ran a profiler comparison for the changed declarations in this PR.

Results (seconds, top-level command times):

  • MeasureTheory.Integrable.ae_eq_zero_of_forall_setIntegral_eq_zero: 0.025877 -> 0.024470 (-5.44%)
  • MeasureTheory.Integrable.ae_eq_of_forall_setIntegral_eq: 0.015411 -> 0.014461 (-6.16%)

Overall:

  • Both changed declarations are slightly faster.

@yuanyi-350
Copy link
Copy Markdown
Collaborator Author

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Apr 22, 2026

Benchmark results for 66ccf0a against ee3a540 are in. No significant results found. @yuanyi-350

  • 🟥 build//instructions: +9.1G (+0.01%)

Small changes (1🟥)

  • 🟥 build/module/Mathlib.Tactic.MinImports//instructions: +136.1M (+2.71%)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly t-measure-probability Measure theory / Probability theory

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants