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 filtersMeasureTheory.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.
MeasureTheory.Submartingale.iSup_ofReal_ne_top
Plain-language statement
Alternative form of Submartingale.ae_bddAbove.
Source project: Brownian motion
Person-level attribution pending.
MeasureTheory.Submartingale.monotone_predictablePart_ae
Plain-language statement
For a submartingale indexed by a countable type, the predictable part is monotone a.e.
Source project: Brownian motion
Person-level attribution pending.