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.isStable_left_limit
Plain-language statement
The processes with left limits are a stable class.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.isStable_rightContinuous
Plain-language statement
The processes with right-continuous paths are a stable class.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.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.