Skip to content

feat: fun_prop for integrability#39323

Draft
lecopivo wants to merge 20 commits into
masterfrom
lecopivo/integrability
Draft

feat: fun_prop for integrability#39323
lecopivo wants to merge 20 commits into
masterfrom
lecopivo/integrability

Conversation

@lecopivo
Copy link
Copy Markdown
Collaborator

@lecopivo lecopivo commented May 13, 2026

setting up fun_prop with integrability

-->

Open in Gitpod

lecopivo and others added 18 commits May 12, 2026 21:51
@lecopivo
tactic that execute autoParam tactic tac on the goal autoParam P tac
b9945a2
@mcdoll
initial commit
eea91cb
@lecopivo
add more integrability tests
cc3804e
@lecopivo
Merge remote-tracking branch 'origin/mcdoll/integrable_funprop' into …
67dd15f 
…lecopivo/integrability_tests
@lecopivo
update integrability tests
3949fa2
@lecopivo
Integrable predicate does not have meaningful composition theorem the…
e257ac9 
…refore we want to run transition theorems even on function that can be non-trivially decomposed into two functions.

Therefore we add an additional check that if the number of composition theorems is zero we allow
application of transition theorems
@mcdoll
initial commit
0dc157a
@lecopivo
Merge branch 'lecopivo/integrability_tests' into lecopivo/integrability
dcda579
@lecopivo
properly run transition theorems if there are no composition theorems
db150de
@lecopivo
update integrability tests
d26a1ce
@lecopivo
Merge remote-tracking branch 'origin/mcdoll/integrableOn_funprop' int…
1a3fcd3 
…o lecopivo/integrability
@lecopivo
one test works now
6e53503
@lecopivo
correctly apply transition theorem when there is not composition theorem
7521c17
@lecopivo
fix test
6b73ebb
@lecopivo
update tests
53a53c4
@lecopivo
add option to mark fun_prop declaration with eager_transition for f…
2cff205 
…unction properties that do no have strong composition theorem and it will eagerly apply transition theorems
@lecopivo
Merge branch 'lecopivo/fun_prop_eager_transition' into lecopivo/integ…
a3c3212 
…rability
@lecopivo
mark integrability with eager_transition
2fbbc56
@github-actions
Copy link
Copy Markdown

github-actions Bot commented May 13, 2026 •
edited
Loading

PR summary af807749bc

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Tactic.RunAutoParam (new file) 1
Mathlib.MeasureTheory.Integral.test_funprop (new file) 2611

Declarations diff

+ IntegrableOn.const_smul
+ IntegrableOn.indicator₀
+ IntegrableOn.left_inter
+ IntegrableOn.right_inter
+ IntegrableOn.smul
+ IntegrableOn.univ
+ cancel_self_div
+ continuous_complex_ofReal
+ eager_triv
+ integrableOn_complex_ofReal
+ noneager_triv
+ runAutoParam
+ tacticToDischarge'
+ triv

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.

⚠️ Scripts folder reminder

This PR adds files under scripts/.
Please consider whether each added script belongs in this repository or in leanprover-community/mathlib-ci.

A script belongs in mathlib-ci if it is a CI automation script that interacts with GitHub (e.g. managing labels, posting comments, triggering bots), runs from a trusted external checkout in CI, or requires access to secrets.

A script belongs in this repository (scripts/) if it is a developer or maintainer tool to be run locally, a code maintenance or analysis utility, a style linting tool, or a data file used by the library's own linters.

See the mathlib-ci README for more details.

Added scripts files:

  • scripts/update-integrability-tactic-counts.sh

@github-actions
Copy link
Copy Markdown

github-actions Bot commented May 13, 2026 •
edited
Loading

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

@lecopivo lecopivo added the WIP Work in progress label May 13, 2026
@lecopivo lecopivo changed the title fun_prop for integrability feat: fun_prop for integrability May 13, 2026
@lecopivo lecopivo marked this pull request as draft May 13, 2026 20:42
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors Bot commented May 13, 2026

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

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

Reviewers

No reviews

Assignees

No one assigned

Labels

WIP Work in progress

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@lecopivo @mcdoll