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 167 research declarations. Search 10,000 more complete Mathlib declarations.
167 results
Clear filtersProbabilityTheory.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.
ProbabilityTheory.countable_not_cadlagModif_ae_eq
Plain-language statement
The set of points where the cadlag modification of a real quasimartingale along a countable dense set T disagrees with X is countable.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.countable_not_rightLimWithin_ae_eq
Plain-language statement
The set of points where the right limit along a countable dense set T disagrees with X is countable.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.ElementaryPredictableSet.generateFrom_eq_predictable
Plain-language statement
The elementary predictable sets generate the predictable σ-algebra. Note that we require the time domain to have countably generated atTop so that each (t, ∞] can be written as a countable union of intervals (t, s].
Source project: Brownian motion
Person-level attribution pending.