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.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.
ProbabilityTheory.stochIoc.eq_iUnion
Plain-language statement
]]σ,τ]] = ⋃ᵢ (i, i+1] × {σ ≤ i < τ} as subsets of ℕ × Ω , a purely arithmetic identity on ℕ∞, valid for any σ, τ.
Source project: Brownian motion
Person-level attribution pending.
ProbabilityTheory.stochIoc.exists_elementaryPredictableSet
Plain-language statement
]]σ,τ]] is an elementary predictable set for bounded stopping times on ℕ (blueprint lem:elementaryPredictableSet_stochasticInterval). With τ ≤ n, ]]σ,τ]] = ⋃_{i < n} (i, i+1] × {σ ≤ i < τ} is a finite disjoint union of predictable rectangles, which is exactly the data of an ElementaryPredictableSet.
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.