Project-declaredLean 4.8.0
Prob bind to Pmf
Prob.bind_toPmf
Plain-language statement
Prob.toPmf commutes with bind
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.8.0
Cexp eq cexp add cexp
Prob.cexp_eq_cexp_add_cexp
Plain-language statement
cexp can be decomposed as positive and negative cexps, even if there are zeros
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Project-declaredLean 4.8.0
Cexp eq cexp cexp
Prob.cexp_eq_cexp_cexp
Plain-language statement
cexp can be decomposed as a expectation over cexp's w.r.t. a function
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Project-declaredLean 4.8.0
Cond bind le first
Prob.cond_bind_le_first
Plain-language statement
Bound an enriched cond by bounding the first half if first half props relate to second half props
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Project-declaredLean 4.8.0
Cond bind le of forall le
Prob.cond_bind_le_of_forall_le
Plain-language statement
We can bound a cond bind uniformly in the first argument
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Project-declaredLean 4.8.0
Cond bind le second
Prob.cond_bind_le_second
Plain-language statement
Bound an enriched cond by bounding the second half uniformly in the first half
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.