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 6 research declarations. Search 10,000 more complete Mathlib declarations.
6 results
Clear filtersProbabilityTheory.countable_not_cadlagModif_ae_eq
Plain-language 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
Plain-language 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.exists_seq_gt_tendsto_of_not_countable
Plain-language 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.
ProbabilityTheory.tendsto_rightLim_comp_of_gt
Plain-language statement
Along a strictly decreasing sequence u → x from the right, the regularized values r (u k) tend to the right limit of h at x along T' ⊇ T.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.tendsto_rightLim_comp_of_lt
Plain-language statement
Along a strictly increasing sequence u → x from the left, the regularized values r (u k) tend to the left limit of h at x along T' ⊇ T.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.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.