First estimate

We continue the assumptions from the preceding section.

Let \(X_1, X_2, \tilde X_1, \tilde X_2\) be independent random variables, with \(X_1,\tilde X_1\) copies of \(X_1\) and \(X_2,\tilde X_2\) copies of \(X_2\). (This is possible thanks to Existence of independent copies.)

We also define the quantity

\[ I_1 := I [X_1+X_2 : \tilde X_1 + X_2 | X_1+X_2+\tilde X_1+\tilde X_2]. \]

LemmaFibring identity for first estimate#

We have

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

Immediate from Specific fibring identity.

Lean

Formalized as rdist_add_rdist_add_condMutual_eq.

Sources
Leanrdist_add_rdist_add_condMutual_eq
Uses 1 · Used by 4
Proof usesSpecific fibring identity
Used byFirst estimate · Entropy bound on quadruple sum · I1-I2-diff · phi-first-estimate

LemmaLower bound on distances#

We have

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

Immediate from Distance lower bound.

Lean

Formalized as rdist_of_sums_ge.

Sources
Leanrdist_of_sums_ge
Uses 1 · Used by 1
Proof usesDistance lower bound
Used byFirst estimate

LemmaLower bound on conditional distances#

We have

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

Immediate from Conditional distance lower bound.

Lean

Formalized as condRuzsaDist_of_sums_ge.

Sources
LeancondRuzsaDist_of_sums_ge
Uses 1 · Used by 2
Proof usesConditional distance lower bound
Used byFirst estimate · Entropy bound on quadruple sum

LemmaUpper bound on distance differences#

We have

\[ \begin{aligned} d[X^0_1; X_1+\tilde X_2] - d[X^0_1; X_1] &\leq \tfrac{1}{2} k + \tfrac{1}{4} \mathbb{H}[X_2] - \tfrac{1}{4} \mathbb{H}[X_1]\\ d[X^0_2;X_2+\tilde X_1] - d[X^0_2; X_2] &\leq \tfrac{1}{2} k + \tfrac{1}{4} \mathbb{H}[X_1] - \tfrac{1}{4} \mathbb{H}[X_2], \\ d[X_1^0;X_1|X_1+\tilde X_2] - d[X_1^0;X_1] &\leq \tfrac{1}{2} k + \tfrac{1}{4} \mathbb{H}[X_1] - \tfrac{1}{4} \mathbb{H}[X_2] \\ d[X_2^0; X_2|X_2+\tilde X_1] - d[X_2^0; X_2] &\leq \tfrac{1}{2}k + \tfrac{1}{4} \mathbb{H}[X_2] - \tfrac{1}{4} \mathbb{H}[X_1]. \end{aligned} \]
Proof

Immediate from Comparison of Ruzsa distances, I (and recalling that \(k\) is defined to be \(d[X_1;X_2]\)).

Lean

Formalized as diff_rdist_le_1, diff_rdist_le_2, diff_rdist_le_3, diff_rdist_le_4.

Sources
Leandiff_rdist_le_1 · diff_rdist_le_2 · diff_rdist_le_3 · diff_rdist_le_4
Uses 1 · Used by 2
Proof usesComparison of Ruzsa distances, I
Used byFirst estimate · Entropy bound on quadruple sum

LemmaFirst estimate#

We have \(I_1 \leq 2 \eta k\).

Proof

Take a suitable linear combination of Fibring identity for first estimate, Lower bound on distances, Lower bound on conditional distances, and Upper bound on distance differences.

Lean

Formalized as first_estimate.

Sources
Leanfirst_estimate
Uses 4 · Used by 1
Proof usesFibring identity for first estimate · Lower bound on distances · Lower bound on conditional distances · Upper bound on distance differences
Used by\(\tau\)-decrement

One can also extract the following useful inequality from the proof of the above lemma.

LemmaEntropy bound on quadruple sum#

With the same notation, we have

\[ \mathbb{H}[X_1+X_2+\tilde X_1+\tilde X_2] \le \tfrac{1}{2} \mathbb{H}[X_1]+\tfrac{1}{2} \mathbb{H}[X_2] + (2 + \eta) k - I_1.\qquad\text{(1)} \]
Proof

Subtracting Lower bound on conditional distances from Fibring identity for first estimate, and combining the resulting inequality with Upper bound on distance differences gives the bound

\[ d[X_1+\tilde X_2;X_2+\tilde X_1] \le (1 + \eta) k - I_1, \]

and the claim follows from Ruzsa distance in independent case and the definition of \(k\).

Lean

Formalized as ent_ofsum_le.

Sources
Leanent_ofsum_le
Uses 4 · Used by 2
Proof usesLower bound on conditional distances · Fibring identity for first estimate · Upper bound on distance differences · Ruzsa distance in independent case
Used byBound on distance increments · second-estimate-aux

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.