Hoeffdings lemma
hoeffdings_lemma
Project documentation
The Beroulli case of Hoeffding's lemma
Source project: debate
Person-level attribution pending.
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,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,345 to 1,350 of 2,569 results.
hoeffdings_lemma
Project documentation
The Beroulli case of Hoeffding's lemma
Source project: debate
Person-level attribution pending.
holder_van_der_corput
Mathematical statement
If is supported in the ball , then the oscillatory integral with phase difference satisfies
Source project: Carleson formalization
Person-level attribution pending.
HolderOnWith.of_iHolENorm_ne_top
Mathematical statement
If the project’s inhomogeneous -Hölder norm of on the ball is finite and , then is -Hölder on that ball. A valid Hölder constant is the finite normalized norm divided by .
Source project: Carleson formalization
Person-level attribution pending.
homomorphism_pfr
Project documentation
Let be a function, and let denote the set Then there exists a homomorphism such that
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
HPMap.funext_pos_trace
Mathematical statement
Two maps are equal if they agree on all positive inputs with trace one
Source project: quantumInfo
Person-level attribution pending.
Hₛ_le_log_d
Mathematical statement
Shannon entropy of a distribution is at most ln d.
Source project: quantumInfo
Person-level attribution pending.