Commit 2026-10-04 19:57 17e9f587

feat: properties of limitProcess (#43172) Create a new file for the definition and basic properties of MeasureTheory.Filtration.limitProcess. Proves that the limit is preserved under various continuous operations. Add a predicate HasLimitProcess which states that a stochastic process does have a limit. This is a hypothesis that often shows up. Weaken the hypotheses in memLp_limitProcess_of_eLpNorm_bdd and add an instance to make the current proof work.