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 70 research declarations. Search 10,000 more complete Mathlib declarations.
70 results
Clear filtersProbabilityTheory.tendsto_rightLim_nhdsLT
Plain-language statement
The right-limit regularization inherits left limits of h along T.
Source project: Brownian motion
Person-level attribution pending.
stoppedValue_predictablePart_tauMesh_le
Plain-language statement
The stopped valued of the predictable part with respect to τₙ(c) is less than or equal to c.
Source project: Brownian motion
Person-level attribution pending.
stronglyAdapted_predictableSeqStep
Plain-language statement
The mesh step-extension of the discrete predictable part is strongly adapted.
Source project: Brownian motion
Person-level attribution pending.
tendsto_of_eventually_monotone_of_tendsto_on_dense
Plain-language statement
We combine limsup_le_of_eventually_monotone_of_tendsto_on_dense and le_liminf_of_eventually_monotone_of_tendsto_on_dense to prove that F · a converges to f a if f is continuous at a.
Source project: Brownian motion
Person-level attribution pending.