Project-declaredLean 4.8.0
Post steps V
post_stepsV
Plain-language statement
Relate stepsV and steps
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Source-pinned research
Research proof index
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 filtersView proof record
Project-declaredLean 4.33.0-rc1
Predictable Convex Step left Continuous
predictableConvexStep_leftContinuous
Plain-language statement
predictableConvexStep is left-continuous in time.
probabilitystochastic processesmeasure theory
Source project: Brownian motion
Person-level attribution pending.
Project-declaredLean 4.33.0-rc1
Predictable Part add
predictablePart_add
Plain-language statement
The predictable part is additive for integrable processes.
probabilitystochastic processesmeasure theory
Source project: Brownian motion
Person-level attribution pending.
Project-declaredLean 4.33.0-rc1
Predictable Seq Step apply
predictableSeqStep_apply
Plain-language statement
On the mesh cell Ioc (pred u) u containing t, the step process predictableSeqStep is constant, equal to the discrete predictable part at the cell's right endpoint u.
probabilitystochastic processesmeasure theory
Source project: Brownian motion
Person-level attribution pending.
Project-declaredLean 4.33.0-rc1
Predictable Seq Step left Continuous
predictableSeqStep_leftContinuous
Plain-language statement
The mesh step-extension of the discrete predictable part is left-continuous in time.
probabilitystochastic processesmeasure theory
Source project: Brownian motion
Person-level attribution pending.
Project-declaredLean 4.8.0
Bayes
Prob.bayes'
Project documentation
The no-ratio version of Bayes' theorem holds unconditionally
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.