[Merged by Bors] - feat: define IsKolmogorovProcess

[RemyDegenne]

A stochastic process X : T → Ω → E on an index space T and a measurable space Ω with measure P is said to satisfy the Kolmogorov condition with exponents p, q and constant M if for all s, t : T, the pair (X s, X t) is measurable for the Borel sigma-algebra on E × E and the following condition holds:
∫⁻ ω, edist (X s ω) (X t ω) ^ p ∂P ≤ M * edist s t ^ q.

This is the main assumption of the Kolmogorov-Chentsov theorem, which gives the existence of a continuous modification of the process.

From the Brownian motion project.

---

[github-actions]

PR summary 83404a604c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Probability.Process.Kolmogorov (new file)	1793

---

Declarations diff

+ IsAEKolmogorovProcess
+ IsAEKolmogorovProcess.aemeasurable
+ IsAEKolmogorovProcess.aemeasurable_edist
+ IsAEKolmogorovProcess.aestronglyMeasurable_edist
+ IsAEKolmogorovProcess.edist_eq_zero
+ IsAEKolmogorovProcess.edist_eq_zero_of_const_eq_zero
+ IsKolmogorovProcess
+ IsKolmogorovProcess.IsAEKolmogorovProcess
+ IsKolmogorovProcess.edist_eq_zero
+ IsKolmogorovProcess.edist_eq_zero_of_const_eq_zero
+ IsKolmogorovProcess.measurable
+ IsKolmogorovProcess.measurable_edist
+ IsKolmogorovProcess.mk_of_secondCountableTopology
+ IsKolmogorovProcess.stronglyMeasurable_edist
+ IsKolmogorovProcess_mk
+ ae_eq_mk
+ congr
+ kolmogorovCondition
+ mk
+ p_pos
+ q_pos

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

[EtienneC30]

Thanks!

[EtienneC30]

Thanks!
maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by EtienneC30.

[sgouezel]

Looks great, thanks!
bors d+

[mathlib-bors]

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

[RemyDegenne]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• CI Success