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.altSet_eq_upcrossingsBefore
Plain-language statement
altSet X F a b m is exactly the event of at least m upcrossings of [a, b] by the monotone enumeration finIdx F t of F.
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.
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.