Sum dist diff le
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.
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 filterssum_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.
tau_min_exists_measure
Plain-language statement
A pair of measures minimizing exists.
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
tau_minimizer_exists_rdist_eq_zero
Plain-language statement
For p.η ≤ 1/8, there exist τ-minimizers X₁, X₂ at zero Rusza distance. For p.η < 1/8, all minimizers are fine, by tau_strictly_decreases'. For p.η = 1/8, we use a limit of minimizers for η < 1/8, which exists by compactness.
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.
tau_strictly_decreases
Plain-language statement
If then there are -valued random variables such that . Phrased in the contrapositive form for convenience of proof.
Source project: Polynomial Freiman-Ruzsa project
Person-level attribution pending.