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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,717 to 1,722 of 2,569 results.
MeasureTheory.IsStronglyProgressive.hasStronglyMeasurableSupProcess
Mathematical 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
Mathematical 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.Matrix.TransvectionStruct.measurePreserving
Mathematical statement
A transvection preserves addHaar on ι → F.
Source project: Fermat's Last Theorem
Person-level attribution pending.
MeasureTheory.nullMeasurable_debut
Mathematical 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.ringHaarChar_complex
Mathematical statement
The distributive Haar character of the action of ℂˣ on ℂ is the usual norm squared. This means that volume (z • s) = ‖z‖ ^ 2 * volume s for all z : ℂ and s : Set ℂ. See Complex.volume_complex_smul.
Source project: Fermat's Last Theorem
Person-level attribution pending.