Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 70 research declarations. Search 10,000 more complete Mathlib declarations.
70 results
Clear filtersProbabilityTheory.IsBrownianReal.indep_zero
Plain-language statement
Blumenthal's zero-one law: Let 𝓕 be the canonical filtration associated to a Brownian motion. Then the σ-algebra ⨅ s > 0, 𝓕 s is trivial.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.IsLocallySquareIntegrable.isLocalSubmartingale_sq_norm
Plain-language statement
A locally square-integrable martingale has locally submartingale squared norm.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.IsLocalSubmartingale.locally_classD
Plain-language statement
A nonnegative local submartingale is locally of class D.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.isStable_classD
Plain-language statement
The Class D is stable.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.isStable_classDL
Plain-language statement
The Class DL is stable.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.isStable_hasIntegrableSup
Plain-language statement
The class of processes with integrable supremum is stable.
Source project: Brownian motion
Person-level attribution pending.