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 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.Martingale.stoppedValue_min_ae_eq_condExp_of_discreteApproxSequence
Project documentation
Optional sampling theorem for general time indices (assuming existence of DiscreteApproxSequence).
Source project: Brownian motion
Person-level attribution pending.
MeasureTheory.nullMeasurable_debut
Plain-language statement
The début of an analytic set in is universally measurable: it is null-measurable for any finite measure.
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.
MeasureTheory.Submartingale.integrableOn_const_tauMesh_lt_top
Plain-language statement
The constant c is integrable on the event where τₙ(c) hits before the top element.
Source project: Brownian motion
Person-level attribution pending.