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 filtersIsCadlag.not_accPt_largeLeftJumpSet
Plain-language statement
The set of large left jump times has no accumulation points. TODO: maybe to_dual can be extended to simplify this proof as the proof of the second part is very similar to the first part.
Source project: Brownian motion
Person-level attribution pending.
IsCompactSystem.equiv
Plain-language statement
Transport a compact system along an equivalence of types.
Source project: Brownian motion
Person-level attribution pending.
IsCompactSystem.finsetCoe
Plain-language statement
The set of Finset coercions forms a compact system.
Source project: Brownian motion
Person-level attribution pending.
isLocallyBounded_of_isCadlag
Plain-language statement
A càdlàg function is locally bounded.
Source project: Brownian motion
Person-level attribution pending.
le_liminf_of_eventually_monotone_of_tendsto_on_dense
Plain-language statement
This is the dual of limsup_le_of_eventually_monotone_of_tendsto_on_dense.
Source project: Brownian motion
Person-level attribution pending.
limsup_le_of_eventually_monotone_of_tendsto_on_dense
Plain-language statement
Convergence on a dense set of a collection of monotone function controls the limsup at a point if f is right continuous at a. We prove this under the assumption that α has both a bottom element and a top element. The bottom element is needed because otherwise limsup evaluated at the bottome element may give a junk value to break the inequality.
Source project: Brownian motion
Person-level attribution pending.