Project-declaredLean 4.8.0
Hoeffdings lemma
hoeffdings_lemma
Project documentation
The Beroulli case of Hoeffding's lemma
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
Iterated Deriv Within eq iterated Deriv
iteratedDerivWithin_eq_iteratedDeriv
Plain-language statement
Get rid of Within from iteratedDeriv for smooth functions
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Project-declaredLean 4.8.0
Oracle fold succ prob
Oracle.fold_succ_prob
Plain-language statement
(o.fold (n+1)).prob y decomposes as a product
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
Project-declaredLean 4.8.0
PMF integrable of support finite
PMF.integrable_of_support_finite
Plain-language statement
Everything is integrable over PMFs with finite support
probabilitycomplexity theoryinteractive protocols
Source project: debate
Person-level attribution pending.
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.
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.