Conclusion

TheoremEntropy version of PFR#

Let \(G = \mathbb{F}_2^n\), and suppose that \(X^0_1, X^0_2\) are \(G\)-valued random variables. Then there is some subgroup \(H \leq G\) such that

\[ d[X^0_1;U_H] + d[X^0_2;U_H] \le 11 d[X^0_1;X^0_2], \]

where \(U_H\) is uniformly distributed on \(H\). Furthermore, both \(d[X^0_1;U_H]\) and \(d[X^0_2;U_H]\) are at most \(6 d[X^0_1;X^0_2]\).

Proof

Let \(X_1, X_2\) be the \(\tau\)-minimizer from \(\tau\) has minimum. From \(\tau\)-decrement, \(d[X_1;X_2]=0\). From General 100% inverse theorem, \(d[X_1;U_H] = d[X_2; U_H] = 0\). Also from \(\tau\)-minimization we have \(\tau[X_1;X_2] \leq \tau[X^0_2;X^0_1]\). Using this and the Ruzsa triangle inequality we can conclude.

Lean

Formalized as entropic_PFR_conjecture.

Sources
Leanentropic_PFR_conjecture
Uses 4 · Used by 1
Proof uses\(\tau\)-decrement · \(\tau\) has minimum · General 100% inverse theorem · Ruzsa triangle inequality
Used bypfr_aux

Note: a “stretch goal” for this project would be to obtain a ‘decidable‘ analogue of this result (see the remark at the end of Section 2 for some related discussion).

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.