Cond KLDiv eq
condKLDiv_eq
Plain-language statement
If are -valued random variables, and is another random variable defined on the same sample space as , then
Source project: Polynomial Freiman-Ruzsa project
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 45 research declarations. Search 10,000 more complete Mathlib declarations.
45 results
Clear filterscondKLDiv_eq
Plain-language statement
If are -valued random variables, and is another random variable defined on the same sample space as , then
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
condMultiDist_of_cast
Plain-language statement
Conditional multidistance is unchanged when both the random variables and their conditioning variables are reindexed along an equality . As with ordinary multidistance, the value does not depend on the chosen equal presentation of the finite index type.
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
condRuzsaDistance_ge_of_min
Plain-language statement
A lower bound forced by -minimality. If minimizes the source's functional, then for measurable and conditioning variables ,
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
construct_good_prelim
Plain-language statement
A preliminary endgame bound. In the -minimizer setup, let and let measurable satisfy . Put and Then
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
dist_of_min_eq_zero'
Plain-language statement
If is a -minimizer, then .
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
dist_of_U_add_le
Plain-language statement
Let be measurable random variables in a finite abelian group with , and set . For any measurable and any , there is a measurable random variable such that
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.