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 130 research declarations. Search 10,000 more complete Mathlib declarations.
130 results
Clear filtersProbabilityTheory.isStable_stronglyMeasurable_uncurry
Plain-language statement
The class of processes that are jointly measurable is stable.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.locally_of_ae
Plain-language statement
If the filtration satisfies the usual conditions, then a property of the paths of a process that holds almost surely holds locally.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.maximal_ineq_countable
Plain-language statement
Doob's maximal inequality for a countable index set.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.maximal_ineq_finset
Project documentation
Auxiliary lemma for maximal_ineq_countable where the index set is a Finset.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.measure_biUnion_altSet_le
Plain-language statement
The union of the alternation events over all finite subsets of a countable set of times below t has measure at most K / ((b - a) * m).
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.measure_infiniteAlt
Plain-language statement
Almost surely, there is no infinite family of alternations of X from below a to above b at times in a countable set T below t.
Source project: Brownian motion
Person-level attribution pending.