The rho functional

Definition of the rho functional and basic facts

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

The set of possible values 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$. We also require an absolute continuity condition so that the KL divergence makes sense in ℝ.

To avoid universe issues, we express this using measures on G, but the equivalence with the above point of view follows from rhoMinus_le below.

Equations

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

theorem map_prod_uniformOn_ne_zero {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {A : Finset G} {y : G} (hA : A.Nonempty) {μ : MeasureTheory.Measure G} [MeasureTheory.IsProbabilityMeasure μ] (hμ : ∀ (x : G), μ {x} ≠ 0) : (MeasureTheory.Measure.map (Prod.fst + Prod.snd) (μ.prod (ProbabilityTheory.uniformOn ↑A))) {y} ≠ 0

theorem nonempty_rhoMinusSet {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → G} {A : Finset G} [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hA : A.Nonempty) : (rhoMinusSet X A μ).Nonempty

theorem nonneg_of_mem_rhoMinusSet {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → G} {A : Finset G} [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : Measurable X) {x : ℝ} (hx : x ∈ rhoMinusSet X A μ) : 0 ≤ x

theorem bddBelow_rhoMinusSet {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → G} {A : Finset G} [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : Measurable X) : BddBelow (rhoMinusSet X A μ)

theorem rhoMinusSet_eq_of_identDistrib {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → G} {A : Finset G} {Ω' : Type u_2} [MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} {X' : Ω' → G} (h : ProbabilityTheory.IdentDistrib X X' μ μ') : rhoMinusSet X A μ = rhoMinusSet X' A μ'

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

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

• ρ⁻[X; μ # A] = sInf (rhoMinusSet X A μ)

def «termρ⁻[_;_#_]» : Lean.ParserDescr

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.

def «termρ⁻[_#_]» : Lean.ParserDescr

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.

theorem rhoMinus_eq_of_identDistrib {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → G} {A : Finset G} {Ω' : Type u_2} [MeasurableSpace Ω'] {X' : Ω' → G} {μ' : MeasureTheory.Measure Ω'} (h : ProbabilityTheory.IdentDistrib X X' μ μ') : ρ⁻[X; μ # A] = ρ⁻[X'; μ' # A]

theorem rhoMinus_le_def {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → G} {A : Finset G} [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : Measurable X) {μ' : MeasureTheory.Measure G} [MeasureTheory.IsProbabilityMeasure μ'] (habs : ∀ (y : G), (MeasureTheory.Measure.map (Prod.fst + Prod.snd) (μ'.prod (ProbabilityTheory.uniformOn ↑A))) {y} = 0 → (MeasureTheory.Measure.map X μ) {y} = 0) : ρ⁻[X; μ # A] ≤ KL[X; μ # Prod.fst + Prod.snd; μ'.prod (ProbabilityTheory.uniformOn ↑A)]

theorem rhoMinus_le {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → G} {A : Finset G} [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : Measurable X) (hA : A.Nonempty) {Ω' : Type u_2} [MeasurableSpace Ω'] {T U : Ω' → G} {μ' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure μ'] (hunif : ProbabilityTheory.IsUniform (↑A) U μ') (hT : Measurable T) (hU : Measurable U) (h_indep : ProbabilityTheory.IndepFun T U μ') (habs : ∀ (y : G), (MeasureTheory.Measure.map (T + U) μ') {y} = 0 → (MeasureTheory.Measure.map X μ) {y} = 0) : ρ⁻[X; μ # A] ≤ KL[X; μ # T + U; μ']

theorem rhoMinus_nonneg {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsZeroOrProbabilityMeasure μ] {X : Ω → G} {A : Finset G} (hX : Measurable X) : 0 ≤ ρ⁻[X; μ # A]

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

theorem rhoMinus_zero_measure {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (hP : μ = 0) {X : Ω → G} {A : Finset G} : ρ⁻[X; μ # A] = 0

theorem rhoMinus_continuous {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {A : Finset G} [TopologicalSpace G] [DiscreteTopology G] (hA : A.Nonempty) : Continuous fun (μ : MeasureTheory.ProbabilityMeasure G) => ρ⁻[id; ↑μ # A]

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

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

Equations

• ρ⁺[X; μ # A] = ρ⁻[X; μ # A] + H[X; μ] - Real.log ↑(Nat.card ↥A)

def «termρ⁺[_;_#_]» : Lean.ParserDescr

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

Equations

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

def «termρ⁺[_#_]» : Lean.ParserDescr

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

Equations

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

theorem rhoPlus_continuous {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {A : Finset G} [TopologicalSpace G] [DiscreteTopology G] (hA : A.Nonempty) : Continuous fun (μ : MeasureTheory.ProbabilityMeasure G) => ρ⁺[id; ↑μ # A]

theorem rhoPlus_eq_of_identDistrib {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → G} {A : Finset G} {Ω' : Type u_2} [MeasurableSpace Ω'] {X' : Ω' → G} {μ' : MeasureTheory.Measure Ω'} (h : ProbabilityTheory.IdentDistrib X X' μ μ') : ρ⁺[X; μ # A] = ρ⁺[X'; μ' # A]

theorem bddAbove_card_inter_add {G : Type uG} [AddCommGroup G] [Finite G] {A H : Set G} : BddAbove {x : ℕ | ∃ (t : G), Nat.card ↑(A ∩ (t +ᵥ H)) = x}

theorem exists_mem_card_inter_add {G : Type uG} [AddCommGroup G] [Finite G] (H : AddSubgroup G) {A : Set G} (hA : A.Nonempty) : ∃ k > 0, k ∈ {x : ℕ | ∃ (t : G), Nat.card ↑(A ∩ (t +ᵥ ↑H)) = x}

theorem exists_card_inter_add_eq_sSup {G : Type uG} [AddCommGroup G] [Finite G] (H : AddSubgroup G) {A : Set G} (hA : A.Nonempty) : ∃ (t : G), Nat.card ↑(A ∩ (t +ᵥ ↑H)) = sSup {x : ℕ | ∃ (t : G), Nat.card ↑(A ∩ (t +ᵥ ↑H)) = x} ∧ 0 < Nat.card ↑(A ∩ (t +ᵥ ↑H))

theorem rhoMinus_of_subgroup {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {H : AddSubgroup G} {U : Ω → G} (hunif : ProbabilityTheory.IsUniform (↑H) U μ) {A : Finset G} (hA : A.Nonempty) (hU : Measurable U) : ρ⁻[U; μ # A] = Real.log ↑(Nat.card ↥A) - Real.log ↑(sSup {x : ℕ | ∃ (t : G), Nat.card ↑(↑A ∩ (t +ᵥ ↑H)) = x})

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

theorem rhoPlus_of_subgroup {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {H : AddSubgroup G} {U : Ω → G} (hunif : ProbabilityTheory.IsUniform (↑H) U μ) {A : Finset G} (hA : A.Nonempty) (hU : Measurable U) : ρ⁺[U; μ # A] = Real.log ↑(↑H).ncard - Real.log ↑(sSup {x : ℕ | ∃ (t : G), Nat.card ↑(↑A ∩ (t +ᵥ ↑H)) = x})

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} [MeasurableSpace Ω] (X : Ω → G) (A : Finset G) (μ : MeasureTheory.Measure Ω) : ℝ

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

Equations

• ρ[X; μ # A] = (ρ⁻[X; μ # A] + ρ⁺[X; μ # A]) / 2

def «termρ[_;_#_]» : Lean.ParserDescr

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

Equations

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

def «termρ[_#_]» : Lean.ParserDescr

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

Equations

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

theorem rho_eq_of_identDistrib {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → G} {A : Finset G} {Ω' : Type u_2} [MeasurableSpace Ω'] {X' : Ω' → G} {μ' : MeasureTheory.Measure Ω'} (h : ProbabilityTheory.IdentDistrib X X' μ μ') : ρ[X; μ # A] = ρ[X'; μ' # A]

theorem rho_of_uniform {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {U : Ω → G} {A : Finset G} (hunif : ProbabilityTheory.IsUniform (↑A) U μ) (hU : Measurable U) (hA : A.Nonempty) : ρ[U; μ # A] = 0

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

theorem rho_of_subgroup {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {H : AddSubgroup G} {U : Ω → G} (hunif : ProbabilityTheory.IsUniform (↑H) U μ) {A : Finset G} (hA : A.Nonempty) (hU : Measurable U) (r : ℝ) (hr : ρ[U; μ # A] ≤ r) : ∃ (t : G), Real.exp (-r) * ↑(Nat.card ↥A) ^ (1 / 2) * ↑(↑H).ncard ^ (1 / 2) ≤ ↑(Nat.card ↑(↑A ∩ (t +ᵥ ↑H))) ∧ ↑(Nat.card ↥A) ≤ Real.exp (2 * r) * ↑(↑H).ncard ∧ ↑(↑H).ncard ≤ Real.exp (2 * r) * ↑(Nat.card ↥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 e^{-r} \sqrt{|A||H|}$, and $|H|/|A| \in [e^{-2r}, e^{2r}]$.

theorem rho_of_submodule {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [Module (ZMod 2) G] {H : Submodule (ZMod 2) G} {U : Ω → G} (hunif : ProbabilityTheory.IsUniform (↑H) U μ) {A : Finset G} (hA : A.Nonempty) (hU : Measurable U) (r : ℝ) (hr : ρ[U; μ # A] ≤ r) : ∃ (t : G), Real.exp (-r) * ↑(Nat.card ↥A) ^ (1 / 2) * ↑(↑H).ncard ^ (1 / 2) ≤ ↑(Nat.card ↑(↑A ∩ (t +ᵥ ↑H))) ∧ ↑(Nat.card ↥A) ≤ Real.exp (2 * r) * ↑(↑H).ncard ∧ ↑(↑H).ncard ≤ Real.exp (2 * r) * ↑(Nat.card ↥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 e^{-r} \sqrt{|A||H|}$, and $|H|/|A| \in [e^{-2r}, e^{2r}]$.

theorem rho_continuous {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] [TopologicalSpace G] [DiscreteTopology G] [BorelSpace G] {A : Finset G} (hA : A.Nonempty) : Continuous fun (μ : MeasureTheory.ProbabilityMeasure G) => ρ[id; ↑μ # A]

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

theorem tendsto_rho_probabilityMeasure {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {A : Finset G} {α : Type u_2} {l : Filter α} [TopologicalSpace Ω] [BorelSpace Ω] [TopologicalSpace G] [BorelSpace G] [DiscreteTopology G] {X : Ω → G} (hX : Continuous X) (hA : A.Nonempty) {μ : α → MeasureTheory.ProbabilityMeasure Ω} {ν : MeasureTheory.ProbabilityMeasure Ω} (hμ : Filter.Tendsto μ l (nhds ν)) : Filter.Tendsto (fun (n : α) => ρ[X; ↑(μ n) # A]) l (nhds ρ[X; ↑ν # A])

theorem rhoMinus_of_sum {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X Y : Ω → G} {A : Finset G} [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (hA : A.Nonempty) (h_indep : ProbabilityTheory.IndepFun X Y μ) : ρ⁻[X + Y; μ # A] ≤ ρ⁻[X; μ # A]

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

theorem rho_of_sum {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X Y : Ω → G} {A : Finset G} [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (hA : A.Nonempty) (h_indep : ProbabilityTheory.IndepFun X Y μ) : ρ[X + Y; μ # A] ≤ ρ[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]).$$

theorem rho_of_translate {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → G} {A : Finset G} [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : Measurable X) (hA : A.Nonempty) (s : G) : ρ[fun (ω : Ω) => X ω + s; μ # A] = ρ[X; μ # A]

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

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

Equations

• ρ[X | Y; μ # A] = ∑' (s : S), μ.real (Y ⁻¹' {s}) * ρ[X; μ[|Y ⁻¹' {s}] # A]

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

Average of rhoMinus along the fibers.

Equations

• ρ⁻[X | Y; μ # A] = ∑' (s : S), μ.real (Y ⁻¹' {s}) * ρ⁻[X; μ[|Y ⁻¹' {s}] # A]

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

Average of rhoPlus along the fibers.

Equations

• ρ⁺[X | Y; μ # A] = ∑' (s : S), μ.real (Y ⁻¹' {s}) * ρ⁺[X; μ[|Y ⁻¹' {s}] # A]

def «termρ[_|_;_#_]» : Lean.ParserDescr

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

Equations

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

def «termρ[_|_#_]» : Lean.ParserDescr

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

Equations

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

def «termρ⁻[_|_;_#_]» : Lean.ParserDescr

Average of rhoMinus along the fibers.

Equations

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

def «termρ⁺[_|_;_#_]» : Lean.ParserDescr

Average of rhoPlus along the fibers.

Equations

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

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

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

theorem condRho_eq_of_identDistrib {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {A : Finset G} {S : Type u_2} [MeasurableSpace S] [MeasurableSingletonClass S] {Y : Ω → G} {W : Ω → S} {Ω' : Type u_3} [MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} {Y' : Ω' → G} {W' : Ω' → S} (hY : Measurable Y) (hW : Measurable W) (hY' : Measurable Y') (hW' : Measurable W') (h : ProbabilityTheory.IdentDistrib (prod Y W) (prod Y' W') μ μ') : ρ[Y | W; μ # A] = ρ[Y' | W'; μ' # A]

theorem condRhoMinus_le {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → G} {A : Finset G} [MeasureTheory.IsZeroOrProbabilityMeasure μ] {S : Type u_2} [MeasurableSpace S] [Finite S] [MeasurableSingletonClass S] {Z : Ω → S} (hX : Measurable X) (hZ : Measurable Z) (hA : A.Nonempty) : ρ⁻[X | Z; μ # A] ≤ ρ⁻[X; μ # A] + H[X; μ] - H[X | Z; μ]

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

theorem condRhoPlus_le {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → G} {A : Finset G} [MeasureTheory.IsProbabilityMeasure μ] {S : Type u_2} [MeasurableSpace S] [Finite S] [MeasurableSingletonClass S] {Z : Ω → S} (hX : Measurable X) (hZ : Measurable Z) (hA : A.Nonempty) : ρ⁺[X | Z; μ # A] ≤ ρ⁺[X; μ # A]

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

theorem condRho_eq {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → G} {A : Finset G} {S : Type u_2} [Finite S] {Z : Ω → S} : ρ[X | Z; μ # A] = (ρ⁻[X | Z; μ # A] + ρ⁺[X | Z; μ # A]) / 2

theorem condRho_le {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → G} {A : Finset G} [MeasureTheory.IsProbabilityMeasure μ] {S : Type u_2} [MeasurableSpace S] [Finite S] [MeasurableSingletonClass S] {Z : Ω → S} (hX : Measurable X) (hZ : Measurable Z) (hA : A.Nonempty) : ρ[X | Z; μ # A] ≤ ρ[X; μ # A] + (H[X; μ] - H[X | Z; μ]) / 2

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

theorem condRho_prod_eq_sum {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → G} {A : Finset G} [MeasureTheory.IsProbabilityMeasure μ] {S : Type u_2} [MeasurableSpace S] [Fintype S] [MeasurableSingletonClass S] {Z T : Ω → S} (hZ : Measurable Z) (hT : Measurable T) : ρ[X | prod Z T; μ # A] = ∑ g : S, μ.real (T ⁻¹' {g}) * ρ[X | Z; μ[|T ⁻¹' {g}] # A]

theorem condRho_prod_le {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → G} {A : Finset G} [MeasureTheory.IsProbabilityMeasure μ] {S : Type u_2} [MeasurableSpace S] [Finite S] [MeasurableSingletonClass S] {Z T : Ω → S} (hX : Measurable X) (hZ : Measurable Z) (hT : Measurable T) (hA : A.Nonempty) : ρ[X | prod Z T; μ # A] ≤ ρ[X | T; μ # A] + (H[X | T; μ] - H[X | prod Z T; μ]) / 2

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

theorem condRho_prod_eq_of_indepFun {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {A : Finset G} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → G} {S : Type u_2} [Finite S] [MeasurableSpace S] [MeasurableSingletonClass S] {W W' : Ω → S} (hX : Measurable X) (hW : Measurable W) (hW' : Measurable W') (h : ProbabilityTheory.IndepFun (prod X W) W' μ) : ρ[X | prod W W'; μ # A] = ρ[X | W; μ # A]

theorem rho_of_sum_le {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X Y : Ω → G} {A : Finset G} [Module (ZMod 2) G] [MeasureTheory.IsZeroOrProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (hA : A.Nonempty) (h_indep : ProbabilityTheory.IndepFun X Y μ) : ρ[X + Y; μ # A] ≤ (ρ[X; μ # A] + ρ[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] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X Y : Ω → G} {A : Finset G} [Module (ZMod 2) G] [MeasureTheory.IsProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (hA : A.Nonempty) (h_indep : ProbabilityTheory.IndepFun X Y μ) : ρ[X | X + Y; μ # A] ≤ (ρ[X; μ # A] + ρ[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 pfrPhi {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type u_2} [MeasurableSpace Ω] (X Y : Ω → G) (η : ℝ) (A : Finset G) (μ : MeasureTheory.Measure Ω) : ℝ

Given $G$-valued random variables $X,Y$, define $$ \phi[X;Y] := d[X;Y] + \eta(\rho(X) + \rho(Y))$$.

Equations

• pfrPhi X Y η A μ = d[X; μ # Y; μ] + η * (ρ[X; μ # A] + ρ[Y; μ # A])

def phiMinimizes {G : Type uG} [AddCommGroup G] [hGm : MeasurableSpace G] {Ω : Type u_2} [MeasurableSpace Ω] (X Y : Ω → G) (η : ℝ) (A : Finset G) (μ : MeasureTheory.Measure Ω) : 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

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

theorem phiMinimizes_of_identDistrib {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {Ω' : Type u_2} [MeasureTheory.MeasureSpace Ω'] {X Y : Ω → G} {X' Y' : Ω' → G} {η : ℝ} {A : Finset G} (h_min : phiMinimizes X Y η A MeasureTheory.volume) (h₁ : ProbabilityTheory.IdentDistrib X X' MeasureTheory.volume MeasureTheory.volume) (h₂ : ProbabilityTheory.IdentDistrib Y Y' MeasureTheory.volume MeasureTheory.volume) : phiMinimizes X' Y' η A MeasureTheory.volume

theorem phiMinimizes_comm {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X Y : Ω → G} {η : ℝ} {A : Finset G} (h_min : phiMinimizes X Y η A MeasureTheory.volume) : phiMinimizes Y X η A MeasureTheory.volume

theorem phi_min_exists {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {A : Finset G} {η : ℝ} (hA : A.Nonempty) : ∃ (μ : MeasureTheory.Measure (G × G)), MeasureTheory.IsProbabilityMeasure μ ∧ phiMinimizes Prod.fst Prod.snd η A μ

There exists a $\phi$-minimizer.

theorem le_rdist_of_phiMinimizes {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {A : Finset G} {η : ℝ} {X₁ X₂ : Ω → G} (h_min : phiMinimizes X₁ X₂ η A MeasureTheory.volume) {Ω₁ : Type u_2} {Ω₂ : Type u_3} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] {X₁' : Ω₁ → G} {X₂' : Ω₂ → G} (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') : d[X₁ # X₂] - η * (ρ[X₁'; μ₁ # A] - ρ[X₁ # A]) - η * (ρ[X₂'; μ₂ # A] - ρ[X₂ # A]) ≤ d[X₁'; μ₁ # X₂'; μ₂]

theorem le_rdist_of_phiMinimizes' {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {A : Finset G} {η : ℝ} {X₁ X₂ : Ω → G} (h_min : phiMinimizes X₁ X₂ η A MeasureTheory.volume) {Ω₁ : Type u_2} {Ω₂ : Type u_3} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] {X₁' : Ω₁ → G} {X₂' : Ω₂ → G} (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') : d[X₁ # X₂] ≤ d[X₁'; μ₁ # X₂'; μ₂] + η * (ρ[X₁'; μ₁ # A] - ρ[X₁ # A]) + η * (ρ[X₂'; μ₂ # A] - ρ[X₂ # A])

theorem condRho_le_condRuzsaDist_of_phiMinimizes {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {A : Finset G} {η : ℝ} {X₁ X₂ X₁' X₂' : Ω → G} [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {S : Type u_2} {T : Type u_3} [Finite S] [MeasurableSpace S] [MeasurableSingletonClass S] [Finite T] [MeasurableSpace T] [MeasurableSingletonClass T] (h : phiMinimizes X₁ X₂ η A MeasureTheory.volume) (h1 : Measurable X₁') (h2 : Measurable X₂') {Z : Ω → S} {W : Ω → T} (hZ : Measurable Z) (hW : Measurable W) : d[X₁ # X₂] - η * (ρ[X₁' | Z # A] - ρ[X₁ # A]) - η * (ρ[X₂' | W # A] - ρ[X₂ # A]) ≤ d[X₁' | Z # X₂' | W]

theorem I_one_le {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {A : Finset G} {η : ℝ} (hη : 0 < η) {X₁ X₂ X₁' X₂' : Ω → G} (h_min : phiMinimizes X₁ X₂ η A MeasureTheory.volume) (h₁ : ProbabilityTheory.IdentDistrib X₁ X₁' MeasureTheory.volume MeasureTheory.volume) (h₂ : ProbabilityTheory.IdentDistrib X₂ X₂' MeasureTheory.volume MeasureTheory.volume) (h_indep : ProbabilityTheory.iIndepFun ![X₁, X₂, X₁', X₂'] MeasureTheory.volume) (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [Module (ZMod 2) G] (hA : A.Nonempty) : I[X₁ + X₂ : X₁' + X₂|X₁ + X₂ + X₁' + X₂'] ≤ 2 * η * d[X₁ # X₂]

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

theorem I_two_aux {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {X₁ X₂ X₁' X₂' : Ω → G} (h₁ : ProbabilityTheory.IdentDistrib X₁ X₁' MeasureTheory.volume MeasureTheory.volume) (h₂ : ProbabilityTheory.IdentDistrib X₂ X₂' MeasureTheory.volume MeasureTheory.volume) (h_indep : ProbabilityTheory.iIndepFun ![X₁, X₂, X₁', X₂'] MeasureTheory.volume) (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [Module (ZMod 2) G] : d[X₁ # X₁] + d[X₂ # X₂] = d[X₁ + X₂' # X₂ + X₁'] + d[X₁ | X₁ + X₂' # X₂ | X₂ + X₁'] + I[X₁ + X₂ : X₁ + X₁'|X₁ + X₂ + X₁' + X₂']

theorem rdist_add_rdist_eq {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {X₁ X₂ X₁' X₂' : Ω → G} (h₁ : ProbabilityTheory.IdentDistrib X₁ X₁' MeasureTheory.volume MeasureTheory.volume) (h₂ : ProbabilityTheory.IdentDistrib X₂ X₂' MeasureTheory.volume MeasureTheory.volume) (h_indep : ProbabilityTheory.iIndepFun ![X₁, X₂, X₁', X₂'] MeasureTheory.volume) (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [Module (ZMod 2) 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_aux' {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {X₁ X₂ X₁' X₂' : Ω → G} (h₁ : ProbabilityTheory.IdentDistrib X₁ X₁' MeasureTheory.volume MeasureTheory.volume) (h₂ : ProbabilityTheory.IdentDistrib X₂ X₂' MeasureTheory.volume MeasureTheory.volume) (h_indep : ProbabilityTheory.iIndepFun ![X₁, X₂, X₁', X₂'] MeasureTheory.volume) (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [Module (ZMod 2) G] : 2 * d[X₁ # X₂] = d[X₁ + X₁' # X₂ + X₂'] + d[X₁ | X₁ + X₁' # X₂ | X₂ + X₂'] + I[X₁ + X₂ : X₁ + X₁'|X₁ + X₂ + X₁' + X₂']

theorem I_two_le {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {A : Finset G} {η : ℝ} (hη : 0 < η) {X₁ X₂ X₁' X₂' : Ω → G} (h_min : phiMinimizes X₁ X₂ η A MeasureTheory.volume) (h₁ : ProbabilityTheory.IdentDistrib X₁ X₁' MeasureTheory.volume MeasureTheory.volume) (h₂ : ProbabilityTheory.IdentDistrib X₂ X₂' MeasureTheory.volume MeasureTheory.volume) (h_indep : ProbabilityTheory.iIndepFun ![X₁, X₂, X₁', X₂'] MeasureTheory.volume) (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [Module (ZMod 2) G] (hA : A.Nonempty) (h'η : η < 1) : 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] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {A : Finset G} {η : ℝ} {X₁ X₂ : Ω → G} (h_min : phiMinimizes X₁ X₂ η A MeasureTheory.volume) [Module (ZMod 2) G] {Ω' : Type u_2} [MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure μ] {T₁ T₂ T₃ : Ω' → G} (hsum : T₁ + T₂ + T₃ = 0) (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃) : d[X₁ # X₂] ≤ 3 * I[T₁ : T₂; μ] + (2 * H[T₃; μ] - H[T₁; μ] - H[T₂; μ]) + η * (ρ[T₁ | T₃; μ # A] + ρ[T₂ | T₃; μ # A] - ρ[X₁ # A] - ρ[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_cond {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {A : Finset G} {η : ℝ} {X₁ X₂ : Ω → G} (h_min : phiMinimizes X₁ X₂ η A MeasureTheory.volume) [Module (ZMod 2) G] {Ω' : Type u_2} [MeasureTheory.MeasureSpace Ω'] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {T₁ T₂ T₃ S : Ω' → G} (hsum : T₁ + T₂ + T₃ = 0) (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃) (hS : Measurable S) : d[X₁ # X₂] ≤ 3 * I[T₁ : T₂|S] + (2 * H[T₃ | S] - H[T₁ | S] - H[T₂ | S]) + η * (ρ[T₁ | prod T₃ S # A] + ρ[T₂ | prod T₃ S # A] - ρ[X₁ # A] - ρ[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_cond' {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {A : Finset G} {η : ℝ} {X₁ X₂ : Ω → G} (h_min : phiMinimizes X₁ X₂ η A MeasureTheory.volume) [Module (ZMod 2) G] {Ω' : Type u_2} [MeasureTheory.MeasureSpace Ω'] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {T₁ T₂ T₃ : Ω' → G} (S : Ω' → G) (hsum : T₁ + T₂ + T₃ = 0) (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃) (hS : Measurable S) : d[X₁ # X₂] ≤ I[T₁ : T₂|S] + I[T₁ : T₃|S] + I[T₂ : T₃|S] + η / 3 * (ρ[T₁ | prod T₂ S # A] + ρ[T₂ | prod T₁ S # A] - ρ[X₁ # A] - ρ[X₂ # A] + (ρ[T₁ | prod T₃ S # A] + ρ[T₃ | prod T₁ S # A] - ρ[X₁ # A] - ρ[X₂ # A]) + (ρ[T₂ | prod T₃ S # A] + ρ[T₃ | prod T₂ S # A] - ρ[X₁ # A] - ρ[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 new_gen_ineq_aux1 {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {A : Finset G} [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [Module (ZMod 2) G] {Y₁ Y₂ Y₃ Y₄ : Ω → G} (hY₁ : Measurable Y₁) (hY₂ : Measurable Y₂) (hY₃ : Measurable Y₃) (hY₄ : Measurable Y₄) (h_indep : ProbabilityTheory.iIndepFun ![Y₁, Y₂, Y₃, Y₄] MeasureTheory.volume) (hA : A.Nonempty) : ρ[Y₁ + Y₂ | prod (Y₁ + Y₃) (Y₁ + Y₂ + Y₃ + Y₄) # A] ≤ (ρ[Y₁ # A] + ρ[Y₂ # A] + ρ[Y₃ # A] + ρ[Y₄ # A]) / 4 + (d[Y₁ # Y₂] + d[Y₃ # Y₄]) / 4 + (d[Y₁ + Y₂ # Y₃ + Y₄] + I[Y₁ + Y₂ : Y₁ + Y₃|Y₁ + Y₂ + Y₃ + Y₄]) / 2

theorem new_gen_ineq_aux2 {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {A : Finset G} [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [Module (ZMod 2) G] {Y₁ Y₂ Y₃ Y₄ : Ω → G} (hY₁ : Measurable Y₁) (hY₂ : Measurable Y₂) (hY₃ : Measurable Y₃) (hY₄ : Measurable Y₄) (h_indep : ProbabilityTheory.iIndepFun ![Y₁, Y₂, Y₃, Y₄] MeasureTheory.volume) (hA : A.Nonempty) : ρ[Y₁ + Y₂ | prod (Y₁ + Y₃) (Y₁ + Y₂ + Y₃ + Y₄) # A] ≤ (ρ[Y₁ # A] + ρ[Y₂ # A] + ρ[Y₃ # A] + ρ[Y₄ # A]) / 4 + (d[Y₁ # Y₃] + d[Y₂ # Y₄]) / 4 + d[Y₁ | Y₁ + Y₃ # Y₂ | Y₂ + Y₄] / 2

theorem new_gen_ineq {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {A : Finset G} [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [Module (ZMod 2) G] {Y₁ Y₂ Y₃ Y₄ : Ω → G} (hY₁ : Measurable Y₁) (hY₂ : Measurable Y₂) (hY₃ : Measurable Y₃) (hY₄ : Measurable Y₄) (h_indep : ProbabilityTheory.iIndepFun ![Y₁, Y₂, Y₃, Y₄] MeasureTheory.volume) (hA : A.Nonempty) : ρ[Y₁ + Y₂ | prod (Y₁ + Y₃) (Y₁ + Y₂ + Y₃ + Y₄) # A] ≤ (ρ[Y₁ # A] + ρ[Y₂ # A] + ρ[Y₃ # A] + ρ[Y₄ # A]) / 4 + (d[Y₁ # Y₂] + d[Y₃ # Y₄] + d[Y₁ # Y₃] + d[Y₂ # Y₄]) / 8 + (d[Y₁ + Y₂ # Y₃ + Y₄] + I[Y₁ + Y₂ : Y₁ + Y₃|Y₁ + Y₂ + Y₃ + Y₄] + d[Y₁ | Y₁ + Y₃ # Y₂ | Y₂ + Y₄]) / 4

theorem condRho_sum_le {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {A : Finset G} [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [Module (ZMod 2) G] {Y₁ Y₂ Y₃ Y₄ : Ω → G} (hY₁ : Measurable Y₁) (hY₂ : Measurable Y₂) (hY₃ : Measurable Y₃) (hY₄ : Measurable Y₄) (h_indep : ProbabilityTheory.iIndepFun ![Y₁, Y₂, Y₃, Y₄] MeasureTheory.volume) (hA : A.Nonempty) : ρ[Y₁ + Y₂ | prod (Y₁ + Y₃) (Y₁ + Y₂ + Y₃ + Y₄) # A] + ρ[Y₁ + Y₃ | prod (Y₁ + Y₂) (Y₁ + Y₂ + Y₃ + Y₄) # A] - (ρ[Y₁ # A] + ρ[Y₂ # A] + ρ[Y₃ # A] + ρ[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] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {A : Finset G} [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [Module (ZMod 2) G] {Y₁ Y₂ Y₃ Y₄ : Ω → G} (hY₁ : Measurable Y₁) (hY₂ : Measurable Y₂) (hY₃ : Measurable Y₃) (hY₄ : Measurable Y₄) (h_indep : ProbabilityTheory.iIndepFun ![Y₁, Y₂, Y₃, Y₄] MeasureTheory.volume) (hA : A.Nonempty) : have S := Y₁ + Y₂ + Y₃ + Y₄; have T₁ := Y₁ + Y₂; have T₂ := Y₁ + Y₃; have T₃ := Y₂ + Y₃; ρ[T₁ | prod T₂ S # A] + ρ[T₂ | prod T₁ S # A] + ρ[T₁ | prod T₃ S # A] + ρ[T₃ | prod T₁ S # A] + ρ[T₂ | prod T₃ S # A] + ρ[T₃ | prod T₂ S # A] - 3 * (ρ[Y₁ # A] + ρ[Y₂ # A] + ρ[Y₃ # A] + ρ[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] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {A : Finset G} {η : ℝ} (hη : 0 < η) {X₁ X₂ X₁' X₂' : Ω → G} (h_min : phiMinimizes X₁ X₂ η A MeasureTheory.volume) (h₁ : ProbabilityTheory.IdentDistrib X₁ X₁' MeasureTheory.volume MeasureTheory.volume) (h₂ : ProbabilityTheory.IdentDistrib X₂ X₂' MeasureTheory.volume MeasureTheory.volume) (h_indep : ProbabilityTheory.iIndepFun ![X₁, X₂, X₁', X₂'] MeasureTheory.volume) (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [Module (ZMod 2) G] (hA : A.Nonempty) (hη' : η < 1 / 8) : d[X₁ # X₂] = 0

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

theorem dist_of_min_eq_zero {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {A : Finset G} {η : ℝ} (hη : 0 < η) {X₁ X₂ : Ω → G} (h_min : phiMinimizes X₁ X₂ η A MeasureTheory.volume) (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [Module (ZMod 2) G] (hA : A.Nonempty) (hη' : η < 1 / 8) : d[X₁ # X₂] = 0

theorem phiMinimizer_exists_rdist_eq_zero {G : Type uG} [AddCommGroup G] [Finite G] [hGm : MeasurableSpace G] [DiscreteMeasurableSpace G] {A : Finset G} [Module (ZMod 2) G] (hA : A.Nonempty) : ∃ (Ω : Type uG) (x : MeasureTheory.MeasureSpace Ω) (X₁ : Ω → G) (X₂ : Ω → G), Measurable X₁ ∧ Measurable X₂ ∧ MeasureTheory.IsProbabilityMeasure MeasureTheory.volume ∧ phiMinimizes X₁ X₂ (1 / 8) A MeasureTheory.volume ∧ d[X₁ # X₂] = 0

For η ≤ 1/8, there exist phi-minimizers X₁, X₂ at zero Rusza distance. For η < 1/8, all minimizers are fine, by dist_of_min_eq_zero. For η = 1/8, we use a limit of minimizers for η < 1/8, which exists by compactness.

theorem rho_PFR_conjecture {G : Type uG} [AddCommGroup G] [Finite G] [Module (ZMod 2) G] {Ω : Type uG} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasurableSpace G] [DiscreteMeasurableSpace G] (Y₁ Y₂ : Ω → G) (hY₁ : Measurable Y₁) (hY₂ : Measurable Y₂) (A : Finset G) (hA : A.Nonempty) : ∃ (H : Submodule (ZMod 2) G) (Ω' : Type uG) (mΩ' : MeasureTheory.MeasureSpace Ω') (U : Ω' → G), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume ∧ Measurable U ∧ ProbabilityTheory.IsUniform (↑H) U MeasureTheory.volume ∧ 2 * ρ[U # A] ≤ ρ[Y₁ # A] + ρ[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_aux0 {G : Type uG} [AddCommGroup G] [Finite G] [Module (ZMod 2) G] {A : Set G} (h₀A : A.Nonempty) {K : ℝ} (hA : ↑(Nat.card ↑(A + A)) ≤ K * ↑(Nat.card ↑A)) : ∃ (H : Submodule (ZMod 2) G) (t : G), K ^ (-4) * ↑(Nat.card ↑A) ^ (1 / 2) * ↑(↑H).ncard ^ (1 / 2) ≤ ↑(Nat.card ↑(A ∩ (↑H + {t}))) ∧ ↑(Nat.card ↑A) ≤ K ^ 8 * ↑(↑H).ncard ∧ ↑(↑H).ncard ≤ K ^ 8 * ↑(Nat.card ↑A)

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]$.

theorem better_PFR_conjecture_aux {G : Type uG} [AddCommGroup G] [Finite G] [Module (ZMod 2) G] {A : Set G} (h₀A : A.Nonempty) {K : ℝ} (hA : ↑(Nat.card ↑(A + A)) ≤ K * ↑(Nat.card ↑A)) : ∃ (H : Submodule (ZMod 2) G) (c : Set G), ↑(Nat.card ↑c) ≤ K ^ 5 * ↑(Nat.card ↑A) ^ (1 / 2) * ↑(↑H).ncard ^ (-1 / 2) ∧ ↑(↑H).ncard ≤ K ^ 8 * ↑(Nat.card ↑A) ∧ ↑(Nat.card ↑A) ≤ K ^ 8 * ↑(↑H).ncard ∧ A ⊆ c + ↑H

Auxiliary statement towards the polynomial Freiman-Ruzsa (PFR) conjecture: if $A$ is a subset of an elementary abelian 2-group of doubling constant at most $K$, then there exists a subgroup $H$ such that $A$ can be covered by at most $K^5 |A|^{1/2} / |H|^{1/2}$ cosets of $H$, and $H$ has the same cardinality as $A$ up to a multiplicative factor $K^8$.

theorem better_PFR_conjecture {G : Type uG} [AddCommGroup G] [Finite G] [Module (ZMod 2) G] {A : Set G} (h₀A : A.Nonempty) {K : ℝ} (hA : ↑(Nat.card ↑(A + A)) ≤ K * ↑(Nat.card ↑A)) : ∃ (H : Submodule (ZMod 2) G) (c : Set G), ↑(Nat.card ↑c) < 2 * K ^ 9 ∧ (↑H).ncard ≤ 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$.

theorem better_PFR_conjecture' {G : Type u_1} [AddCommGroup G] [Module (ZMod 2) G] {A : Set G} {K : ℝ} (h₀A : A.Nonempty) (Afin : A.Finite) (hA : ↑(Nat.card ↑(A + A)) ≤ K * ↑(Nat.card ↑A)) : ∃ (H : Submodule (ZMod 2) G) (c : Set G), c.Finite ∧ (↑H).Finite ∧ ↑(Nat.card ↑c) < 2 * K ^ 9 ∧ (↑H).ncard ≤ Nat.card ↑A ∧ A ⊆ c + ↑H

Corollary of better_PFR_conjecture in which the ambient group is not required to be finite (but) then $H$ and $c$ are finite.