The 100% version of PFR

DefinitionSymmetry group#

If \(X\) is a \(G\)-valued random variable, then the symmetry group \(\mathrm{Sym}[X]\) is the set of all \(h \in G\) such that \(X +h\) has the same distribution as \(X\).

Lean

Formalized as symmGroup.

Sources
LeansymmGroup
Used by 3
Used bySymmetry group is a group · Translate is uniform on symmetry group · Zero Ruzsa distance implies large symmetry group

LemmaSymmetry group is a group#

If \(X\) is a \(G\)-valued random variable, then \(\mathrm{Sym}[X]\) is a subgroup of \(G\).

Proof

Direct verification of the group axioms.

Lean

Formalized as symmGroup.

Sources
LeansymmGroup
Uses 1 · Used by 1
Statement usesSymmetry group
Used bySymmetric 100% inverse theorem

LemmaZero Ruzsa distance implies large symmetry group#

If \(X\) is a \(G\)-valued random variable such that \(d[X ;X]=0\), and \(x,y \in G\) are such that \(P[X=x], P[X=y]>0\), then \(x-y \in \mathrm{Sym}[X]\).

Proof

Let \(X_1,X_2\) be independent copies of \(X\) (from Existence of independent copies). Let \(A\) denote the range of \(X\). From Ruzsa distance in independent case and Copy preserves Ruzsa distance we have

\[ \mathbb{H}[X_1-X_2] = \mathbb{H}[X_1]. \]

Observe from Conditional entropy and relabeling that

\[ \mathbb{H}[X_1-X_2|X_2] = \mathbb{H}[X_1|X_2] = \mathbb{H}[X_1] \]

and hence by Alternative formulae for mutual information

\[ \mathbb{I}[X_1-X_2 : X_1] = 0. \]

By Vanishing of mutual information, \(X_1-X_2\) and \(X_1\) are therefore independent, thus the law of \((X_1-X_2|X_1=x)\) does not depend on \(x \in A\). The claim follows.

Lean

Formalized as sub_mem_symmGroup.

Sources
Leansub_mem_symmGroup
Uses 7 · Used by 1
Proof usesRuzsa distance in independent case · Copy preserves Ruzsa distance · Conditional entropy and relabeling · Vanishing of mutual information · Alternative formulae for mutual information · Existence of independent copies · Symmetry group
Used byTranslate is uniform on symmetry group

LemmaTranslate is uniform on symmetry group#

If \(X\) is a \(G\)-valued random variable with \(d[X ;X]=0\), and \(x_0\) is a point with \(P[X=x_0] > 0\), then \(X-x_0\) is uniformly distributed on \(\mathrm{Sym}[X]\).

Proof

The law of \(X-x_0\) is invariant under \(\mathrm{Sym}[X]\), non-zero at the origin, and supported on \(\mathrm{Sym}[X]\), giving the claim.

Lean

Formalized as isUniform_sub_const_of_rdist_eq_zero.

Sources
LeanisUniform_sub_const_of_rdist_eq_zero
Uses 3 · Used by 2
Proof usesZero Ruzsa distance implies large symmetry group · Symmetry group · Uniform distribution
Used bypfr-rho · Symmetric 100% inverse theorem

LemmaSymmetric 100% inverse theorem#

Suppose that \(X\) is a \(G\)-valued random variable such that \(d[X ;X]=0\). Then there exists a subgroup \(H \leq G\) such that \(d[X ;U_H] = 0\).

Proof

Take \(H\) to be the symmetry group of \(X\), which is a group by Symmetry group is a group. From Translate is uniform on symmetry group, \(X-x_0\) is uniform on \(H\), and \(d[X ;X-x_0] = d[X ;X] \leq 0\), and the claim follows.

Lean

Formalized as exists_isUniform_of_rdist_self_eq_zero.

Sources
Leanexists_isUniform_of_rdist_self_eq_zero
Uses 2 · Used by 1
Proof usesSymmetry group is a group · Translate is uniform on symmetry group
Used byGeneral 100% inverse theorem

CorollaryGeneral 100% inverse theorem#

Suppose that \(X_1,X_2\) are \(G\)-valued random variables such that \(d[X_1;X_2]=0\). Then there exists a subgroup \(H \leq G\) such that \(d[X_1;U_H] = d[X_2;U_H] = 0\).

Proof

Using Ruzsa triangle inequality and Distance nonnegative we have \(d[X_1;X_1]=0\), hence by Symmetric 100% inverse theorem \(d[X_1;U_H]=0\) for some subgroup \(H\). By Ruzsa triangle inequality and Distance nonnegative again we also have \(d[X_2;U_H]\) as required.

Lean

Formalized as exists_isUniform_of_rdist_eq_zero.

Sources
Leanexists_isUniform_of_rdist_eq_zero
Uses 3 · Used by 3
Proof usesSymmetric 100% inverse theorem · Ruzsa triangle inequality · Distance nonnegative
Used byEntropy version of PFR · Improved entropy version of PFR · Vanishing

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.