Basic facts about minimizers

In this section we assume that \(X_1,X_2\) are \(\tau\)-minimizers. We also write \(k := d[X_1;X_2]\).

LemmaDistance lower bound#

For any \(G\)-valued random variables \(X'_1,X'_2\), one has

\[ d[X'_1;X'_2] \geq k - \eta (d[X^0_1;X'_1] - d[X^0_1;X_1] ) - \eta (d[X^0_2;X'_2] - d[X^0_2;X_2] ). \]

Proof

Immediate from \(\tau\) functional and \(\tau\) has minimum.

Lean

Formalized as distance_ge_of_min.

Sources

• Polynomial Freiman-Ruzsa blueprint: chapter/entropy_pfr.tex, line 48

Leandistance_ge_of_min

Uses 3 · Used by 6

Statement uses\(\tau\)-minimizer

Proof uses\(\tau\) functional · \(\tau\) has minimum

Used byConditional distance lower bound · Constructing good variables, I · Lower bound on distances · Distance between sums · Second estimate · Constructing good variables, I'

LemmaConditional distance lower bound#

For any \(G\)-valued random variables \(X'_1,X'_2\) and random variables \(Z,W\), one has

\[ d[X'_1|Z;X'_2|W] \geq k - \eta (d[X^0_1;X'_1|Z] - d[X^0_1;X_1] ) - \eta (d[X^0_2;X'_2|W] - d[X^0_2;X_2] ). \]

Proof

Apply Distance lower bound to conditioned random variables and then average.

Lean

Formalized as condRuzsaDistance_ge_of_min.

Sources

• Polynomial Freiman-Ruzsa blueprint: chapter/entropy_pfr.tex, line 60

LeancondRuzsaDistance_ge_of_min

Uses 3 · Used by 1

Statement uses\(\tau\)-minimizer · Conditioned Ruzsa distance

Proof usesDistance lower bound

Used byLower bound on conditional distances

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.