Second estimate
second_estimate
Plain-language statement
The second information estimate for -minimizers. Let be independent copies of , set , , and . 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 83 research declarations. Search 10,000 more complete Mathlib declarations.
83 results
Clear filterssecond_estimate
Plain-language statement
The second information estimate for -minimizers. Let be independent copies of , set , , and . Then .
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
sifting_cor
Plain-language statement
A dependent-random-choice corollary. Let be nonempty, let and , and let be a nonzero even integer satisfying . Then there are sets such that the normalized difference distribution assigns mass at least to the source's sifted set . Both sets retain explicit density: for .
Source project: Arithmetic Progressions Almost Periodicity
Person-level attribution pending.
sub_condMultiDistance_le
Project documentation
If is a -minimizer, and , then for any other tuples and with the G$-valued, one has
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
sum_dist_diff_le
Plain-language statement
In the -minimizer endgame, let be independent copies of , set , , , , , and . If , then .
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
sum_of_rdist_eq
Plain-language statement
Let and be independent -valued random variables. Then
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
sum_of_rdist_eq_step_condMutualInfo
Plain-language statement
For four measurable random variables in a finite abelian group, the conditional mutual-information term used in the fibring identity can be reduced to
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.