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 research declarations. Search 10,000 more complete Mathlib declarations.
2 results
Clear filtersProbabilityTheory.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.