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 11 research declarations. Search 10,000 more complete Mathlib declarations.
11 results
Clear filtersMeasureTheory.IsStronglyProgressive.hasStronglyMeasurableSupProcess
Plain-language statement
If the filtration satisfies the usual conditions, every progressively measurable process has a strongly measurable sup process.
Source project: Brownian motion
Person-level attribution pending.
MeasureTheory.Martingale.classDL
Plain-language statement
A martingale with right-continuous paths is of class DL.
Source project: Brownian motion
Person-level attribution pending.
MeasureTheory.Submartingale.classDL
Plain-language statement
A nonnegative right-continuous submartingale is of class DL.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.classD_of_uniformIntegrable_bounded_stoppingTime
Plain-language statement
If {stoppedValue X T : T is a bounded stopping time} is uniformly integrable, then X is of class D.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.ClassDL.classD
Plain-language statement
If the index type has a top element, then class DL implies class D.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.ClassDL.locally_classD
Plain-language statement
A process of class DL is locally of class D.
Source project: Brownian motion
Person-level attribution pending.