The rho functional

Definition of the rho functional and basic facts

Main definitions:

Main results

noncomputable def rho_minus {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (X : Ω → G) (A : Finset G) : ℝ

For any $G$-valued random variable $X$, we define $\rho^-(X)$ to be the infimum of $D_{KL}(X \Vert U_A + T)$, where $U_A$ is uniform on $A$ and $T$ ranges over $G$-valued random variables independent of $U_A$.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def rho_plus {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (X : Ω → G) (A : Finset G) : ℝ

For any $G$-valued random variable $X$, we define $\rho^+(X) := \rho^-(X) + \bbH(X) - \bbH(U_A)$.

Equations

• rho_plus X A = rho_minus X A + H[X] - (↑(Nat.card { x : G // x ∈ A })).log

theorem rho_minus_nonneg {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (X : Ω → G) (A : Finset G) : rho_minus X A ≥ 0

We have $\rho^-(X) \geq 0$.

theorem rho_minus_of_subgroup {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] (H : AddSubgroup G) {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (U : Ω → G) (hunif : ProbabilityTheory.IsUniform (↑H) U MeasureTheory.volume) (A : Finset G) : rho_minus U A = (↑(Nat.card { x : G // x ∈ A })).log - (sSup (Set.range fun (t : G) => ↑(Nat.card ↑(↑A ∩ (t +ᵥ H.carrier))))).log

If $H$ is a finite subgroup of $G$, then $\rho^-(U_H) = \log |A| - \log \max_t |A \cap (H+t)|$.

theorem rho_plus_of_subgroup {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] (H : AddSubgroup G) {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (U : Ω → G) (hunif : ProbabilityTheory.IsUniform (↑H) U MeasureTheory.volume) (A : Finset G) : rho_plus U A = (↑(Nat.card ↥H)).log - (sSup (Set.range fun (t : G) => ↑(Nat.card ↑(↑A ∩ (t +ᵥ H.carrier))))).log

If $H$ is a finite subgroup of $G$, then $\rho^+(U_H) = \log |H| - \log \max_t |A \cap (H+t)|$.

noncomputable def rho {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (X : Ω → G) (A : Finset G) : ℝ

We define $\rho(X) := (\rho^+(X) + \rho^-(X))/2$.

Equations

• rho X A = (rho_minus X A + rho_plus X A) / 2

theorem rho_of_uniform {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (U : Ω → G) (A : Finset G) (hunif : ProbabilityTheory.IsUniform (↑A) U MeasureTheory.volume) : rho U A = 0

We have $\rho(U_A) = 0$.

theorem rho_of_subgroup {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] (H : AddSubgroup G) {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (U : Ω → G) (hunif : ProbabilityTheory.IsUniform (↑H) U MeasureTheory.volume) (A : Finset G) (r : ℝ) (hr : rho U A ≤ r) : ∃ (t : G), ↑(Nat.card ↑(↑A ∩ (t +ᵥ H.carrier))) ≤ 2 ^ (-r) * (↑(Nat.card { x : G // x ∈ A }) * ↑(Nat.card ↥H)) ^ (1 / 2) ∧ ↑(Nat.card { x : G // x ∈ A }) ≤ 2 ^ (2 * r) * ↑(Nat.card ↥H) ∧ ↑(Nat.card ↥H) ≤ 2 ^ (2 * r) * ↑(Nat.card { x : G // x ∈ A })

If $H$ is a finite subgroup of $G$, and $\rho(U_H) \leq r$, then there exists $t$ such that $|A \cap (H+t)| \geq 2^{-r} \sqrt{|A||H|}$, and $|H|/|A|\in[2^{-2r},2^{2r}]$.

theorem rho_of_translate {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (X : Ω → G) (A : Finset G) (s : G) : rho (fun (ω : Ω) => X ω + s) A = rho X A

For any $s \in G$, $\rho(X+s) = \rho(X)$.

theorem rho_continuous {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {A : Finset G} [TopologicalSpace G] [DiscreteTopology G] [BorelSpace G] : Continuous fun (μ : MeasureTheory.ProbabilityMeasure G) => rho id A

\rho(X)$ depends continuously on the distribution of $X$.

theorem rho_minus_of_sum {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (X : Ω → G) (Y : Ω → G) (A : Finset G) (hindep : ProbabilityTheory.IndepFun X Y MeasureTheory.volume) : rho_minus (X + Y) A ≤ rho_minus X A

If $X,Y$ are independent, one has $$ \rho^-(X+Y) \leq \rho^-(X)$$

theorem rho_plus_of_sum {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (X : Ω → G) (Y : Ω → G) (A : Finset G) (hindep : ProbabilityTheory.IndepFun X Y MeasureTheory.volume) : rho_plus (X + Y) A ≤ rho_plus X A + H[X + Y] - H[X]

If $X,Y$ are independent, one has $$ \rho^+(X+Y) \leq \rho^+(X) + \bbH[X+Y] - \bbH[X]$$

theorem rho_of_sum {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (X : Ω → G) (Y : Ω → G) (A : Finset G) (hindep : ProbabilityTheory.IndepFun X Y MeasureTheory.volume) : rho (X + Y) A ≤ rho X A + (H[X + Y] - H[X]) / 2

If $X,Y$ are independent, one has $$ \rho(X+Y) \leq \rho(X) + \frac{1}{2}( \bbH[X+Y] - \bbH[X] ).$$

noncomputable def condRho {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type u_1} {S : Type u_2} [MeasureTheory.MeasureSpace Ω] (X : Ω → G) (Y : Ω → S) (A : Finset G) : ℝ

We define $\rho(X|Y) := \sum_y {\bf P}(Y=y) \rho(X|Y=y)$.

Equations

• condRho X Y A = ∑' (s : S), (MeasureTheory.volume (Y ⁻¹' {s})).toReal * rho X A

noncomputable def condRho_minus {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type u_1} {S : Type u_2} [MeasureTheory.MeasureSpace Ω] (X : Ω → G) (Y : Ω → S) (A : Finset G) : ℝ

Equations

• condRho_minus X Y A = ∑' (s : S), (MeasureTheory.volume (Y ⁻¹' {s})).toReal * rho_minus X A

noncomputable def condRho_plus {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type u_1} {S : Type u_2} [MeasureTheory.MeasureSpace Ω] (X : Ω → G) (Y : Ω → S) (A : Finset G) : ℝ

Equations

• condRho_plus X Y A = ∑' (s : S), (MeasureTheory.volume (Y ⁻¹' {s})).toReal * rho_plus X A

theorem condRho_of_translate {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type u_1} {S : Type u_2} [MeasureTheory.MeasureSpace Ω] (X : Ω → G) (Y : Ω → S) (A : Finset G) (s : G) : condRho (fun (ω : Ω) => X ω + s) Y A = condRho X Y A

For any $s\in G$, $\rho(X+s|Y)=\rho(X|Y)$.

theorem condRho_of_injective {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type u_1} {S : Type u_2} {T : Type u_3} [MeasureTheory.MeasureSpace Ω] (X : Ω → G) (Y : Ω → S) (A : Finset G) (f : S → T) (hf : Function.Injective f) : condRho X (f ∘ Y) A = condRho X Y A

If $f$ is injective, then $\rho(X|f(Y))=\rho(X|Y)$.

theorem condRho_minus_le {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type u_1} {S : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasurableSpace S] (X : Ω → G) (Z : Ω → S) (A : Finset G) : condRho_minus X Z A ≤ rho_minus X A + H[X] - H[X | Z]

$$ \rho^-(X|Z) \leq \rho^-(X) + \bbH[X] - \bbH[X|Z]$$

theorem condRho_plus_le {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type u_1} {S : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasurableSpace S] (X : Ω → G) (Z : Ω → S) (A : Finset G) : condRho_plus X Z A ≤ rho_plus X A

$$ \rho^+(X|Z) \leq \rho^+(X)$$

theorem condRho_le {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type u_1} {S : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasurableSpace S] (X : Ω → G) (Z : Ω → S) (A : Finset G) : condRho X Z A ≤ rho X A + (H[X] - H[X | Z]) / 2

$$ \rho(X|Z) \leq \rho(X) + \frac{1}{2}( \bbH[X] - \bbH[X|Z] )$$

theorem rho_of_sum_le {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (X : Ω → G) (Y : Ω → G) (A : Finset G) (hindep : ProbabilityTheory.IndepFun X Y MeasureTheory.volume) : rho (X + Y) A ≤ (rho X A + rho Y A + d[X # Y]) / 2

If $X,Y$ are independent, then $$ \rho(X+Y) \leq \frac{1}{2}(\rho(X)+\rho(Y) + d[X;Y]).$$

theorem condRho_of_sum_le {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (X : Ω → G) (Y : Ω → G) (A : Finset G) (hindep : ProbabilityTheory.IndepFun X Y MeasureTheory.volume) : condRho X (X + Y) A ≤ (rho X A + rho Y A + d[X # Y]) / 2

If $X,Y$ are independent, then $$ \rho(X | X+Y) \leq \frac{1}{2}(\rho(X)+\rho(Y) + d[X;Y]).$$

noncomputable def phi {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (X : Ω → G) (Y : Ω → G) (η : ℝ) (A : Finset G) : ℝ

Equations

• phi X Y η A = d[X # Y] + η * (rho X A + rho Y A)

def phiMinimizes {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type uG} [MeasureTheory.MeasureSpace Ω] (X : Ω → G) (Y : Ω → G) (η : ℝ) (A : Finset G) : Prop

Given $G$-valued random variables $X,Y$, define $$ \phi[X;Y] := d[X;Y] + \eta(\rho(X) + \rho(Y))$$ and define a \emph{$\phi$-minimizer} to be a pair of random variables $X,Y$ which minimizes $\phi[X;Y]$.

Equations

• phiMinimizes X Y η A = ∀ (Ω' : Type uG) (x : MeasureTheory.MeasureSpace Ω') (X' Y' : Ω' → G), phi X Y η A ≤ phi X' Y' η A

theorem phi_min_exists {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] (η : ℝ) (A : Finset G) : ∃ (Ω : Type uG) (x : MeasureTheory.MeasureSpace Ω) (X : Ω → G) (Y : Ω → G), phiMinimizes X Y η A

There exists a $\phi$-minimizer.

theorem I_one_le {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] (η : ℝ) {Ω : Type uG} [MeasureTheory.MeasureSpace Ω] (X₁ : Ω → G) (X₂ : Ω → G) (X'₁ : Ω → G) (X'₂ : Ω → G) : I[X₁ + X₂ : X'₁ + X₂|X₁ + X₂ + X'₁ + X'₂] ≤ 2 * η * d[X₁ # X₂]

$I_1\le 2\eta d[X_1;X_2]$

theorem dist_add_dist_eq {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type uG} [MeasureTheory.MeasureSpace Ω] (X₁ : Ω → G) (X₂ : Ω → G) (X'₁ : Ω → G) (X'₂ : Ω → G) : d[X₁ # X₁] + d[X₂ # X₂] = 2 * d[X₁ # X₂] + (I[X₁ + X₂ : X₁ + X'₁|X₁ + X₂ + X'₁ + X'₂] - I[X₁ + X₂ : X'₁ + X₂|X₁ + X₂ + X'₁ + X'₂])

$d[X_1;X_1]+d[X_2;X_2]= 2d[X_1;X_2]+(I_2-I_1)$.

theorem I_two_le {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] (η : ℝ) {Ω : Type uG} [MeasureTheory.MeasureSpace Ω] (X₁ : Ω → G) (X₂ : Ω → G) (X'₁ : Ω → G) (X'₂ : Ω → G) : I[X₁ + X₂ : X₁ + X'₁|X₁ + X₂ + X'₁ + X'₂] ≤ 2 * η * d[X₁ # X₂] + η / (1 - η) * (2 * η * d[X₁ # X₂] - I[X₁ + X₂ : X'₁ + X₂|X₁ + X₂ + X'₁ + X'₂])

$I_2\le 2\eta d[X_1;X_2] + \frac{\eta}{1-\eta}(2\eta d[X_1;X_2]-I_1)$.

theorem dist_le_of_sum_zero {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] (η : ℝ) (A : Finset G) {Ω : Type uG} [MeasureTheory.MeasureSpace Ω] (X₁ : Ω → G) (X₂ : Ω → G) {Ω' : Type uG} [MeasureTheory.MeasureSpace Ω'] (T₁ : Ω' → G) (T₂ : Ω' → G) (T₃ : Ω' → G) (hsum : T₁ + T₂ + T₃ = 0) : d[X₁ # X₂] ≤ 3 * I[T₁ : T₂|T₃] + (2 * H[T₃] - H[T₁] - H[T₂]) + η * (condRho T₁ T₃ A + condRho T₂ T₃ A - rho X₁ A - rho X₂ A)

If $G$-valued random variables $T_1,T_2,T_3$ satisfy $T_1+T_2+T_3=0$, then $$d[X_1;X_2]\le 3\bbI[T_1:T_2\mid T_3] + (2\bbH[T_3]-\bbH[T_1]-\bbH[T_2])+ \eta(\rho(T_1|T_3)+\rho(T_2|T_3)-\rho(X_1)-\rho(X_2)).$$

theorem dist_le_of_sum_zero' {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] (η : ℝ) (A : Finset G) {Ω : Type uG} [MeasureTheory.MeasureSpace Ω] (X₁ : Ω → G) (X₂ : Ω → G) {Ω' : Type uG} [MeasureTheory.MeasureSpace Ω'] (T₁ : Ω' → G) (T₂ : Ω' → G) (T₃ : Ω' → G) (hsum : T₁ + T₂ + T₃ = 0) : d[X₁ # X₂] ≤ I[T₁ : T₂] + I[T₁ : T₃] + I[T₂ : T₃] + η / 3 * (condRho T₁ T₂ A + condRho T₂ T₁ A - rho X₁ A - rho X₂ A + (condRho T₁ T₃ A + condRho T₃ T₁ A - rho X₁ A - rho X₂ A) + (condRho T₂ T₃ A + condRho T₃ T₂ A - rho X₁ A - rho X₂ A))

If $G$-valued random variables $T_1,T_2,T_3$ satisfy $T_1+T_2+T_3=0$, then $$d[X_1;X_2] \leq \sum_{1 \leq i < j \leq 3} \bbI[T_i:T_j] + \frac{\eta}{3} \sum_{1 \leq i < j \leq 3} (\rho(T_i|T_j) + \rho(T_j|T_i) -\rho(X_1)-\rho(X_2))$$

theorem condRho_sum_le {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] (A : Finset G) {Ω' : Type uG} [MeasureTheory.MeasureSpace Ω'] (Y₁ : Ω' → G) (Y₂ : Ω' → G) (Y₃ : Ω' → G) (Y₄ : Ω' → G) (hindep : ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hGm) ![Y₁, Y₂, Y₃, Y₄] MeasureTheory.volume) : let S := Y₁ + Y₂ + Y₃ + Y₄; let T₁ := Y₁ + Y₂; let T₂ := Y₁ + Y₃; condRho T₁ T₂ A + condRho T₂ T₁ A - (rho Y₁ A + rho Y₂ A + rho Y₃ A + rho Y₄ A) / 2 ≤ (d[Y₁ # Y₂] + d[Y₃ # Y₄] + d[Y₁ # Y₃] + d[Y₂ # Y₄]) / 2

For independent random variables $Y_1,Y_2,Y_3,Y_4$ over $G$, define $S:=Y_1+Y_2+Y_3+Y_4$, $T_1:=Y_1+Y_2$, $T_2:=Y_1+Y_3$. Then $$\rho(T_1|T_2,S)+\rho(T_2|T_1,S) - \frac{1}{2}\sum_{i} \rho(Y_i)\le \frac{1}{2}(d[Y_1;Y_2]+d[Y_3;Y_4]+d[Y_1;Y_3]+d[Y_2;Y_4]).$$

theorem condRho_sum_le' {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] (A : Finset G) {Ω' : Type uG} [MeasureTheory.MeasureSpace Ω'] (Y₁ : Ω' → G) (Y₂ : Ω' → G) (Y₃ : Ω' → G) (Y₄ : Ω' → G) (hindep : ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ.succ) => hGm) ![Y₁, Y₂, Y₃, Y₄] MeasureTheory.volume) : let S := Y₁ + Y₂ + Y₃ + Y₄; let T₁ := Y₁ + Y₂; let T₂ := Y₁ + Y₃; let T₃ := Y₂ + Y₃; condRho T₁ T₂ A + condRho T₂ T₁ A + condRho T₁ T₃ A + condRho T₃ T₁ A + condRho T₂ T₃ A + condRho T₃ T₂ A - 3 * (rho Y₁ A + rho Y₂ A + rho Y₃ A + rho Y₄ A) / 2 ≤ d[Y₁ # Y₂] + d[Y₁ # Y₃] + d[Y₁ # Y₄] + d[Y₂ # Y₃] + d[Y₂ # Y₄] + d[Y₃ # Y₄]

For independent random variables $Y_1,Y_2,Y_3,Y_4$ over $G$, define $T_1:=Y_1+Y_2,T_2:=Y_1+Y_3,T_3:=Y_2+Y_3$ and $S:=Y_1+Y_2+Y_3+Y_4$. Then $$\sum_{1 \leq i < j \leq 3} (\rho(T_i|T_j,S) + \rho(T_j|T_i,S) - \frac{1}{2}\sum_{i} \rho(Y_i))\le \sum_{1\leq i < j \leq 4}d[Y_i;Y_j]$$

theorem dist_of_min_eq_zero {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] (η : ℝ) {Ω : Type uG} [MeasureTheory.MeasureSpace Ω] (X₁ : Ω → G) (X₂ : Ω → G) (hη' : η < 1 / 8) : d[X₁ # X₂] = 0

If $X_1,X_2$ is a $\phi$-minimizer, then $d[X_1;X_2] = 0$.

theorem rho_PFR_conjecture {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] (η : ℝ) (hη : η > 0) (hη' : η < 1 / 8) {Ω : Type uG} [MeasureTheory.MeasureSpace Ω] (Y₁ : Ω → G) (Y₂ : Ω → G) (A : Finset G) : ∃ (H : AddSubgroup G) (Ω' : Type uG) (mΩ' : MeasureTheory.MeasureSpace Ω) (U : Ω → G), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume ∧ Measurable U ∧ ProbabilityTheory.IsUniform (↑H) U MeasureTheory.volume ∧ 2 * rho U A ≤ rho Y₁ A + rho Y₂ A + 8 * d[Y₁ # Y₂]

For any random variables $Y_1,Y_2$, there exist a subgroup $H$ such that $$ 2\rho(U_H) \leq \rho(Y_1) + \rho(Y_2) + 8 d[Y_1;Y_2].$$

theorem better_PFR_conjecture_aux {G : Type uG} [AddCommGroup G] {K : ℕ} {A : Set G} (h₀A : A.Nonempty) (hA : Nat.card ↑(A + A) ≤ K * Nat.card ↑A) : ∃ (H : AddSubgroup G) (c : Set G), ↑(Nat.card ↑c) ≤ ↑K ^ 4 * ↑(Nat.card ↑A) ^ (1 / 2) * ↑(Nat.card ↑↑H) ^ (-1 / 2) ∧ ↑(Nat.card ↥H) ≤ ↑K ^ 8 * ↑(Nat.card ↑A) ∧ ↑(Nat.card ↑A) ≤ ↑K ^ 8 * ↑(Nat.card ↥H) ∧ A ⊆ c + ↑H

If $|A+A| \leq K|A|$, then there exists a subgroup $H$ and $t\in G$ such that $|A \cap (H+t)| \geq K^{-4} \sqrt{|A||V|}$, and $|H|/|A|\in[K^{-8},K^8]$. \end{corollary}

theorem better_PFR_conjecture {G : Type uG} [AddCommGroup G] {K : ℕ} {A : Set G} (h₀A : A.Nonempty) (hA : Nat.card ↑(A + A) ≤ K * Nat.card ↑A) : ∃ (H : AddSubgroup G) (c : Set G), ↑(Nat.card ↑c) < 2 * ↑K ^ 9 ∧ Nat.card ↥H ≤ Nat.card ↑A ∧ A ⊆ c + ↑H

If $A \subset {\bf F}_2^n$ is finite non-empty with $|A+A| \leq K|A|$, then there exists a subgroup $H$ of ${\bf F}_2^n$ with $|H| \leq |A|$ such that $A$ can be covered by at most $2K^9$ translates of $H$.