PFR

Let $G, G'$ be finite abelian $2$-groups. Let $f : G \to G'$ be a function, and suppose that there is a proportion of at least $K^{-1}$ pairs $(x,y) \in G^2$ such that $f(x+y) = f(x) + f(y).$ Then there exists a homomorphism $\phi : G \to G'$ and a constant $c \in G'$ such that $f(x) = \phi(x)+c$ for at least $|G| / (2 ^ {144} * K ^ {122})$ values of $x \in G$.

For Mathlib?

The quantity I_3 = I[V:W|S] is equal to I_2.

I[U : V | S] + I[V : W | S] + I[W : U | S] is less than or equal to 6 * η * k - (1 - 5 * η) / (1 - η) * (2 * η * k - I₁).

$\sum_{i=1}^2 \sum_{A\in\{U,V,W\}} \big(d[X^0_i;A|S] - d[X^0_i;X_i]\big)$ is less than or equal to $\leq (6 - 3\eta) k + 3(2 \eta k - I_1).$

If $T_1, T_2, T_3$ are $G$-valued random variables with $T_1+T_2+T_3=0$ holds identically and $\delta := \sum_{1 \leq i < j \leq 3} I[T_i;T_j]$ Then there exist random variables $T'_1, T'_2$ such that $d[T'_1;T'_2] + \eta (d[X_1^0;T'_1] - d[X_1^0;X_1]) + \eta(d[X_2^0;T'_2] - d[X_2^0;X_2])$ is at most $\delta + \eta ( d[X^0_1;T_1]-d[X^0_1;X_1]) + \eta (d[X^0_2;T_2]-d[X^0_2;X_2])$ $+ \tfrac12 \eta I[T_1: T_3] + \tfrac12 \eta I[T_2: T_3].$

If $T_1, T_2, T_3$ are $G$-valued random variables with $T_1+T_2+T_3=0$ holds identically and

$\delta := \sum_{1 \leq i < j \leq 3} I[T_i;T_j]$

Then there exist random variables $T'_1, T'_2$ such that

$d[T'_1;T'_2] + \eta (d[X_1^0;T'_1] - d[X_1^0;X _1]) + \eta(d[X_2^0;T'_2] - d[X_2^0;X_2])$

is at most

If $d[X_1;X_2] > 0$ then there are $G$-valued random variables $X'_1, X'_2$ such that $\tau[X'_1;X'_2] < \tau[X_1;X_2]$. Phrased in the contrapositive form for convenience of proof.

entropic_PFR_conjecture: For two $G$-valued random variables $X^0_1, X^0_2$, 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]$.

If $Z_1, Z_2$ are independent, then $d[Z_1; Z_2]$ is equal to $d[\pi(Z_1);\pi(Z_2)] + d[Z_1|\pi(Z_1); Z_2 |\pi(Z_2)]$ plus $I( Z_1 - Z_2 : (\pi(Z_1), \pi(Z_2)) | \pi(Z_1 - Z_2) ).$

The conditional Ruzsa Distance step of sum_of_rdist_eq