Skip to content

refactor(Probability/Process): rework predictable and progressive processes#38254

Open
jvanwinden wants to merge 18 commits intoleanprover-community:masterfrom
jvanwinden:strongly_progressive_predictable
Open

refactor(Probability/Process): rework predictable and progressive processes#38254
jvanwinden wants to merge 18 commits intoleanprover-community:masterfrom
jvanwinden:strongly_progressive_predictable

Conversation

@jvanwinden
Copy link
Copy Markdown
Contributor

@jvanwinden jvanwinden commented Apr 19, 2026

The purpose of this PR is to rework IsProgressive and ProgMeasurable to have a weak (i.e., Measurable) and strong (i.e., StronglyMeasurable) variant, so that they are more in line with Adapted/StronglyAdapted.

As a side effect, some lemmas can have certain typeclasses removed (which were previously needed to go back and forth between Measurable and StronglyMeasurable).

Zulip discussion at #Brownian motion > Adapted Filtrations for Markov Chains and Markov Processes

Open in Gitpod

@jvanwinden jvanwinden marked this pull request as draft April 19, 2026 14:55
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors Bot commented Apr 19, 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.

@github-actions
Copy link
Copy Markdown

github-actions Bot commented Apr 19, 2026 •
edited
Loading

PR summary 3853566136

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ IsPredictable.adapted
+ IsPredictable.iff_measurable_add_one
+ IsPredictable.measurable_add_one
+ IsPredictable.of_measurable_add_one
+ IsPredictable.progMeasurable
+ IsStronglyPredictable
+ IsStronglyProgressive
+ IsStronglyProgressive.stoppedProcess
+ IsStronglyProgressive.stronglyAdapted_stoppedProcess
+ IsStronglyProgressive.stronglyMeasurable_stoppedProcess
+ ProgMeasurable.add
+ ProgMeasurable.comp
+ ProgMeasurable.div'
+ ProgMeasurable.finset_prod
+ ProgMeasurable.finset_prod'
+ ProgMeasurable.finset_sum
+ ProgMeasurable.finset_sum'
+ ProgMeasurable.inv
+ ProgMeasurable.mul
+ ProgMeasurable.neg
+ ProgMeasurable.norm
+ ProgMeasurable.stronglyAdapted
+ ProgMeasurable.sub
+ StronglyAdapted.isStronglyProgressive_of_continuous
+ StronglyAdapted.isStronglyProgressive_of_discrete
+ iff_measurable_add_one
+ isStronglyProgressive
+ isStronglyProgressive_const
+ isStronglyProgressive_min_stopping_time
+ isStronglyProgressive_of_tendsto
+ isStronglyProgressive_of_tendsto'
+ measurable_inclusion_predictable
+ of_measurable_add_one
++- stronglyAdapted
- ProgMeasurable.stronglyMeasurable_stoppedProcess
- adapted
- isPredictable_iff_measurable_add_one
- isPredictable_of_measurable_add_one
- progMeasurable

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 19, 2026
@jvanwinden
Copy link
Copy Markdown
Contributor Author

jvanwinden commented Apr 19, 2026

WIP

@github-actions github-actions Bot added the WIP Work in progress label Apr 19, 2026
@RemyDegenne RemyDegenne added the brownian Part of the ongoing formalization of the Brownian motion and stochastic integrals label Apr 19, 2026
@jvanwinden jvanwinden marked this pull request as ready for review April 20, 2026 18:51
@jvanwinden
Copy link
Copy Markdown
Contributor Author

jvanwinden commented Apr 20, 2026

-WIP

@github-actions github-actions Bot removed the WIP Work in progress label Apr 20, 2026
@jvanwinden
Copy link
Copy Markdown
Contributor Author

jvanwinden commented Apr 20, 2026 •
edited
Loading

This PR is now ready for review. It includes the following changes:

  • Rename ProgMeasurable to IsStronglyProgressive.
  • Rename IsPredictable to IsStronglyPredictable.
  • Generalize various proofs relating to predictability and progressive measurability to get rid of [SecondCountableTopology] and other unneeded typeclasses.
  • Deprecate Predictable.stronglyAdapted (which does not make use of IsStronglyPredictable)

The intent is to introduce Measurable variants of IsStronglyProgressive and IsPredictable and duplicate the surrounding API in future PRs.

@RemyDegenne
Copy link
Copy Markdown
Contributor

RemyDegenne commented Apr 24, 2026

Looks good, thanks!
bors r+

@mathlib-triage mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label Apr 24, 2026
@RemyDegenne
Copy link
Copy Markdown
Contributor

RemyDegenne commented Apr 24, 2026

bors r-

Sorry, but we also need deprecations for all the lemmas that changed names.

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors Bot commented Apr 24, 2026

Canceled.

Address comments or fix if necessary, and then someone with permission can run bors r+.

@RemyDegenne RemyDegenne added awaiting-author A reviewer has asked the author a question or requested changes. and removed ready-to-merge This PR has been sent to bors. labels Apr 24, 2026
@jvanwinden
Copy link
Copy Markdown
Contributor Author

jvanwinden commented Apr 24, 2026

bors r-

Sorry, but we also need deprecations for all the lemmas that changed names.

Do you mean I should add @[deprecated (since := ...)] alias ... := ... above the relevant lemmas? Should I do the same for the definitions which changed name?

@RemyDegenne
Copy link
Copy Markdown
Contributor

RemyDegenne commented Apr 24, 2026

Yes, below each lemma and definition for which the name changed, you can type "deprecate" in your editor, choose deprecate alias in the autocompletion menu, and it will create a line @[deprecated (since := "2026-04-24")] alias := . You should complete it to be @[deprecated (since := "2026-04-24")] alias old_name := new_name.

@jvanwinden
Copy link
Copy Markdown
Contributor Author

jvanwinden commented Apr 24, 2026

I added the notices and aliases. However, I am not 100% sure if I handled the @[to_additive] aliases correctly, so perhaps you could briefly look at those @RemyDegenne.

@jvanwinden
Copy link
Copy Markdown
Contributor Author

jvanwinden commented Apr 24, 2026

-awaiting-author

@github-actions github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 24, 2026
EtienneC30
EtienneC30 reviewed Apr 24, 2026
View reviewed changes
Comment thread Mathlib/Probability/Process/Adapted.lean Outdated
EtienneC30
EtienneC30 reviewed Apr 24, 2026
View reviewed changes
Comment thread Mathlib/Probability/Process/Adapted.lean
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@EtienneC30 EtienneC30 EtienneC30 left review comments

Assignees

@kex-y kex-y

Labels

brownian Part of the ongoing formalization of the Brownian motion and stochastic integrals t-measure-probability Measure theory / Probability theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@jvanwinden @RemyDegenne @EtienneC30 @kex-y