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 filtersProbabilityTheory.measure_biUnion_altSet_le
Plain-language statement
The union of the alternation events over all finite subsets of a countable set of times below t has measure at most K / ((b - a) * m).
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.measure_infiniteAlt
Plain-language statement
Almost surely, there is no infinite family of alternations of X from below a to above b at times in a countable set T below t.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.measureReal_altSet_le
Plain-language statement
Quantitative alternation bound: the probability of m alternations along any finite F ⊆ Iic t is at most K / m with K independent of F and m.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.measureReal_exists_abs_lt_le
Plain-language statement
Maximal inequality: the probability that |X| exceeds lam somewhere on a finite set F ⊆ Iic t is at most K / lam, with K independent of F.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.mul_integral_upcrossingsBefore_finIdx_le
Plain-language statement
Expectation bound on the number of upcrossings along a finite set of times F ⊆ Iic t, from the boundedness of elementary stochastic integrals at time t.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.mul_measureReal_exists_lt_le
Plain-language statement
One-sided maximal inequality along a finite skeleton for an adapted, integrable process g whose adapted {0,1}-weighted increment sums along idx have expectation at most K.
Source project: Brownian motion
Person-level attribution pending.