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,981 to 1,986 of 2,569 results.
ProbabilityTheory.measureReal_exists_abs_lt_le
Mathematical 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
Mathematical 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
Mathematical 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₂
Mathematical statement
Interpreted as functions, map₂ is just applying B pointwise.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.SimpleProcess.integral_assoc
Mathematical statement
The most general case of associativity of the elementary stochastic integral.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.stochIoc.eq_iUnion
Mathematical statement
]]σ,τ]] = ⋃ᵢ (i, i+1] × {σ ≤ i < τ} as subsets of ℕ × Ω , a purely arithmetic identity on ℕ∞, valid for any σ, τ.
Source project: Brownian motion
Person-level attribution pending.