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 17 research declarations. Search 10,000 more complete Mathlib declarations.
17 results
Clear filterspredictableSeqStep_apply
Plain-language statement
On the mesh cell Ioc (pred u) u containing t, the step process predictableSeqStep is constant, equal to the discrete predictable part at the cell's right endpoint u.
Source project: Brownian motion
Person-level attribution pending.
predictableSeqStep_leftContinuous
Plain-language statement
The mesh step-extension of the discrete predictable part is left-continuous in time.
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.