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 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.
ProbabilityTheory.altSet_eq_upcrossingsBefore
Plain-language statement
altSet X F a b m is exactly the event of at least m upcrossings of [a, b] by the monotone enumeration finIdx F t of F.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.classD_of_uniformIntegrable_bounded_stoppingTime
Plain-language statement
If {stoppedValue X T : T is a bounded stopping time} is uniformly integrable, then X is of class D.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.ClassDL.classD
Plain-language statement
If the index type has a top element, then class DL implies class D.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.ClassDL.locally_classD
Plain-language statement
A process of class DL is locally of class D.
Source project: Brownian motion
Person-level attribution pending.