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 research declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,957 to 1,962 of 2,569 results.
ProbabilityTheory.ClassDL.classD
Mathematical 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
Mathematical statement
A process of class DL is locally of class D.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.countable_not_cadlagModif_ae_eq
Mathematical statement
The set of points where the cadlag modification of a real quasimartingale along a countable dense set T disagrees with X is countable.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.countable_not_rightLimWithin_ae_eq
Mathematical statement
The set of points where the right limit along a countable dense set T disagrees with X is countable.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.ElementaryPredictableSet.generateFrom_eq_predictable
Mathematical statement
The elementary predictable sets generate the predictable σ-algebra. Note that we require the time domain to have countably generated atTop so that each (t, ∞] can be written as a countable union of intervals (t, s].
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.exists_seq_gt_tendsto_of_not_countable
Mathematical statement
Any uncountable set in a separable, densely-ordered, first-countable linear order admits a strictly decreasing sequence of its elements converging to a point from the right.
Source project: Brownian motion
Person-level attribution pending.