feat(ProbabilityTheory): Add Kolmogorov's inequality#36545
feat(ProbabilityTheory): Add Kolmogorov's inequality#36545yuanyi-350 wants to merge 9 commits intoleanprover-community:masterfrom
Conversation
github-actions
bot
added
the
large-import
PR summary 7d6517d1b6Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Probability.Martingale.OptionalStopping | 2422 | 2474 | +52 (+2.15%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Probability.BorelCantelli |
34 |
Mathlib.Probability.Martingale.BorelCantelli Mathlib.Probability.Martingale.OptionalStopping |
52 |
Mathlib.Probability.Martingale.Kolmogorov (new file) |
2490 |
Declarations diff
+ ae_nonneg_condVar
+ kolmogorov_ineq_martingale_sq
+ kolmogorov_ineq_wiki_version
+ kolmogorov_ineq_wiki_version_of_iIndepFun
+ square_submartingale_of_martingale
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.
You can run this locally as
./scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
github-actions
bot
added
the
t-measure-probability
mathlib-dependent-issues
bot
added
the
blocked-by-other-PR
mathlib-dependent-issues
bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
|
This is probably not the right approach. As mentioned here, Kolmogorov's inequality is both a special case of Doob's maximal inequality (and partial progress on this has already been made in https://github.com/RemyDegenne/brownian-motion) and a simple consequence of Jensen's inequality (#27953). I hope my comment does not come across as overly harsh, especially for a new contributor. If you are interested in the formalization of probability theory, you are very welcome to join Zulip—particularly the Brownian motion channel (#Brownian motion). |
4 participants
ref: https://en.wikipedia.org/wiki/Kolmogorov%27s_inequality
Mathlib/Probability/Martingale/OptionalStopping.lean#36542