Project-declaredLean 4.8.0
Chernoff estimate abs le
chernoff_estimate_abs_le
Plain-language statement
Chernoff symmetric bound for estimate
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 52 research declarations. Search 10,000 more complete Mathlib declarations.
52 results
Clear filtersView proof record
Project-declaredLean 4.8.0
Chernoff le count
chernoff_le_count
Plain-language statement
Chernoff lower bound
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Project-declaredLean 4.8.0
Cost bind
Comp.cost_bind
Plain-language statement
The cost of f >>= g is roughly f.cost + g.cost
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Project-declaredLean 4.8.0
Cost query
Comp.cost_query'
Plain-language statement
query' costs one query, plus the rest
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Project-declaredLean 4.8.0
Completeness p
completeness_p
Plain-language statement
Completeness for any valid parameters
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Project-declaredLean 4.8.0
Completeness
completeness'
Plain-language statement
Alice wins the debate with good probability
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.