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 167 research declarations. Search 10,000 more complete Mathlib declarations.
167 results
Clear filtersProbabilityTheory.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.
ProbabilityTheory.SimpleProcess.coe_map₂
Plain-language statement
Interpreted as functions, map₂ is just applying B pointwise.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.SimpleProcess.integral_assoc
Plain-language statement
The most general case of associativity of the elementary stochastic integral.
Source project: Brownian motion
Person-level attribution pending.