Second estimate

We continue the assumptions from the preceding section. We introduce the quantity

\[ I_2 := \mathbb{I}[X_1+X_2 : X_1 + \tilde X_1 | X_1+X_2+\tilde X_1+\tilde X_2]. \]

LemmaDistance between sums #

We have

\[ d[X_1+\tilde X_1; X_2+\tilde X_2] \geq k - \frac{\eta}{2} ( d[X_1; X_1] + d[X_2;X_2] ). \]

Proof

\[ \begin{aligned} d[X_1+\tilde X_1; X_2+\tilde X_2] \geq k &- \eta(d[X^0_1;X_1] - d[X^0_1;X_1+\tilde X_1]) \\ &- \eta(d[X^0_2;X_2] - d[X^0_2;X_2+\tilde X_2]). \end{aligned} \]

Now Comparison of Ruzsa distances, I gives

\[ d[X^0_1;X_1+\tilde X_1] - d[X^0_1;X_1] \leq \tfrac{1}{2} d[X_1;X_1] \]

and

\[ d[X^0_2;X_2+\tilde X_2] - d[X^0_2;X_2] \leq \tfrac{1}{2} d[X_2;X_2], \]

and the claim follows.

Lean

Formalized as rdist_of_sums_ge'.

Sources

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

Leanrdist_of_sums_ge'

Uses 2 · Used by 1

Proof usesDistance lower bound · Comparison of Ruzsa distances, I

Used bysecond-estimate-aux

Lemmasecond-estimate-aux #

We have

\[ d[X_1;X_1] + d[X_2;X_2] \leq 2 k + \frac{2(2 \eta k - I_1)}{1-\eta}. \]

Proof

We may use Ruzsa distance in independent case to expand

\[ \begin{aligned} & d[X_1+\tilde X_1;X_2+\tilde X_2] \\ &= \mathbb{H}[X_1+\tilde X_1 + X_2 + \tilde X_2] - \tfrac{1}{2} \mathbb{H}[X_1+\tilde X_1] - \tfrac{1}{2} \mathbb{H}[X_2+\tilde X_2] \\ &= \mathbb{H}[X_1+\tilde X_1 + X_2 + \tilde X_2] - \tfrac{1}{2} \mathbb{H}[X_1] - \tfrac{1}{2} \mathbb{H}[X_2] \\ & \qquad\qquad\qquad - \tfrac{1}{2} \left( d[X_1;X_1] + d[X_2; X_2] \right), \end{aligned} \]

and hence by Entropy bound on quadruple sum

\[ d[X_1+\tilde X_1; X_2+\tilde X_2] \leq (2+\eta) k - \tfrac{1}{2} \left( d[X_1;X_1] + d[X_2;X_2] \right) - I_1. \]

Combining this bound with Distance between sums we obtain the result.

Lean

Formalized as second_estimate_aux.

Sources

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

Leansecond_estimate_aux

Uses 3 · Used by 2

Proof usesRuzsa distance in independent case · Entropy bound on quadruple sum · Distance between sums

Used bySecond estimate · Bound on distance differences

LemmaSecond estimate #

We have

\[ I_2 \leq 2 \eta k + \frac{2 \eta (2 \eta k - I_1)}{1 - \eta}. \]

Proof

We apply Specific fibring identity, but now with the choice

\[ (Y_1,Y_2,Y_3,Y_4) := (X_2, X_1, \tilde X_2, \tilde X_1). \]

Now Specific fibring identity can be rewritten as

\[ \begin{aligned} &d[X_1+\tilde X_1;X_2+\tilde X_2] + d[X_1|X_1+\tilde X_1; X_2|X_2+\tilde X_2] \\ &\quad + \mathbb{I}[X_1+X_2 : X_1 + \tilde X_1 \,|\, X_1+X_2+\tilde X_1+\tilde X_2] = 2k, \end{aligned} \]

recalling once again that \(k := d[X_1;X_2]\). From Conditional distance lower bound one has

\[ \begin{aligned} d[X_1|X_1+\tilde X_1; X_2|X_2+\tilde X_2] \geq k &- \eta (d[X^0_1;X_1] - d[X^0_1;X_1|X_1+\tilde X_1]) \\& - \eta (d[X^0_2;X_2] - d[X^0_2;X_2|X_2+\tilde X_2]) . \end{aligned} \]

while from Comparison of Ruzsa distances, I we have

\[ d[X^0_1;X_1|X_1+\tilde X_1] - d[X^0_1;X_1] \leq \tfrac{1}{2} d[X_1;X_1], \]

and

\[ d[X^0_2;X_2|X_2+\tilde X_2] - d[X^0_2;X_2] \leq \tfrac{1}{2} d[X_1;X_2]. \]

Combining all these inequalities with Distance between sums, we have

\[ \mathbb{I}[X_1+X_2 : X_1 + \tilde X_1 | X_1+X_2+\tilde X_1+\tilde X_2] \leq \eta ( d[X_1; X_1] + d[X_2; X_2] ).\qquad\text{(1)} \]

Together with Lemma second-estimate-aux, this gives the conclusion.