Improved PFR

An improvement to PFR that lowers the exponent from 12 to 11.

theorem gen_ineq_aux1 {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Module (ZMod 2) G] [MeasurableAdd₂ G] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {Ω₀ : Type u_3} [MeasureTheory.MeasureSpace Ω₀] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (Y : Ω₀ → G) (hY : Measurable Y) (Z₁ Z₂ Z₃ Z₄ : Ω → G) (hZ₁ : Measurable Z₁) (hZ₂ : Measurable Z₂) (hZ₃ : Measurable Z₃) (hZ₄ : Measurable Z₄) (h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume) : d[Y # Z₁ + Z₂ | ⟨Z₁ + Z₃, Z₁ + Z₂ + Z₃ + Z₄⟩] ≤ d[Y # Z₁] + (d[Z₁ # Z₂] + d[Z₁ # Z₃] + d[Z₂ # Z₄] - d[Z₁ | Z₁ + Z₂ # Z₃ | Z₃ + Z₄]) / 2 + (H[Z₁ + Z₂] - H[Z₃ + Z₄] + H[Z₂] - H[Z₁]) / 4

theorem gen_ineq_aux2 {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Module (ZMod 2) G] [MeasurableAdd₂ G] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {Ω₀ : Type u_3} [MeasureTheory.MeasureSpace Ω₀] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (Y : Ω₀ → G) (hY : Measurable Y) (Z₁ Z₂ Z₃ Z₄ : Ω → G) (hZ₁ : Measurable Z₁) (hZ₂ : Measurable Z₂) (hZ₃ : Measurable Z₃) (hZ₄ : Measurable Z₄) (h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume) : d[Y # Z₁ + Z₂ | ⟨Z₁ + Z₃, Z₁ + Z₂ + Z₃ + Z₄⟩] ≤ d[Y # Z₁] + (d[Z₁ # Z₃] + d[Z₁ | Z₁ + Z₃ # Z₂ | Z₂ + Z₄]) / 2 + (H[Z₂ | Z₂ + Z₄] - H[Z₁ | Z₁ + Z₃] + H[Z₁] - H[Z₃]) / 4

theorem gen_ineq_00 {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Module (ZMod 2) G] [MeasurableAdd₂ G] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {Ω₀ : Type u_3} [MeasureTheory.MeasureSpace Ω₀] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (Y : Ω₀ → G) (hY : Measurable Y) (Z₁ Z₂ Z₃ Z₄ : Ω → G) (hZ₁ : Measurable Z₁) (hZ₂ : Measurable Z₂) (hZ₃ : Measurable Z₃) (hZ₄ : Measurable Z₄) (h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume) : d[Y # Z₁ + Z₂ | ⟨Z₁ + Z₃, Z₁ + Z₂ + Z₃ + Z₄⟩] - d[Y # Z₁] ≤ (d[Z₁ # Z₂] + 2 * d[Z₁ # Z₃] + d[Z₂ # Z₄]) / 4 + (d[Z₁ | Z₁ + Z₃ # Z₂ | Z₂ + Z₄] - d[Z₁ | Z₁ + Z₂ # Z₃ | Z₃ + Z₄]) / 4 + (H[Z₁ + Z₂] - H[Z₃ + Z₄] + H[Z₂] - H[Z₃] + H[Z₂ | Z₂ + Z₄] - H[Z₁ | Z₁ + Z₃]) / 8

Let Z₁, Z₂, Z₃, Z₄ be independent G-valued random variables, and let Y be another G-valued random variable. Set S := Z₁ + Z₂ + Z₃ + Z₄. Then d[Y # Z₁ + Z₂ | ⟨Z₁ + Z₃, Sum⟩] - d[Y # Z₁] ≤ (d[Z₁ # Z₂] + 2 * d[Z₁ # Z₃] + d[Z₂ # Z₄]) / 4 + (d[Z₁ | Z₁ + Z₃ # Z₂ | Z₂ + Z₄] - d[Z₁ | Z₁ + Z₂ # Z₃ | Z₃ + Z₄]) / 4 + (H[Z₁ + Z₂] - H[Z₃ + Z₄] + H[Z₂] - H[Z₃] + H[Z₂ | Z₂ + Z₄] - H[Z₁ | Z₁ + Z₃]) / 8.

theorem gen_ineq_01 {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Module (ZMod 2) G] [MeasurableAdd₂ G] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {Ω₀ : Type u_3} [MeasureTheory.MeasureSpace Ω₀] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (Y : Ω₀ → G) (hY : Measurable Y) (Z₁ Z₂ Z₃ Z₄ : Ω → G) (hZ₁ : Measurable Z₁) (hZ₂ : Measurable Z₂) (hZ₃ : Measurable Z₃) (hZ₄ : Measurable Z₄) (h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume) : d[Y # Z₁ + Z₂ | ⟨Z₂ + Z₄, Z₁ + Z₂ + Z₃ + Z₄⟩] - d[Y # Z₁] ≤ (d[Z₁ # Z₂] + 2 * d[Z₁ # Z₃] + d[Z₂ # Z₄]) / 4 + (d[Z₁ | Z₁ + Z₃ # Z₂ | Z₂ + Z₄] - d[Z₁ | Z₁ + Z₂ # Z₃ | Z₃ + Z₄]) / 4 + (H[Z₁ + Z₂] - H[Z₃ + Z₄] + H[Z₂] - H[Z₃] + H[Z₂ | Z₂ + Z₄] - H[Z₁ | Z₁ + Z₃]) / 8

Other version of gen_ineq_00, in which we switch to the complement in the second term.

theorem gen_ineq_10 {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Module (ZMod 2) G] [MeasurableAdd₂ G] {Ω : Type u_2} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {Ω₀ : Type u_3} [MeasureTheory.MeasureSpace Ω₀] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (Y : Ω₀ → G) (hY : Measurable Y) (Z₁ Z₂ Z₃ Z₄ : Ω → G) (hZ₁ : Measurable Z₁) (hZ₂ : Measurable Z₂) (hZ₃ : Measurable Z₃) (hZ₄ : Measurable Z₄) (h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![Z₁, Z₂, Z₃, Z₄] MeasureTheory.volume) : d[Y # Z₃ + Z₄ | ⟨Z₁ + Z₃, Z₁ + Z₂ + Z₃ + Z₄⟩] - d[Y # Z₁] ≤ (d[Z₁ # Z₂] + 2 * d[Z₁ # Z₃] + d[Z₂ # Z₄]) / 4 + (d[Z₁ | Z₁ + Z₃ # Z₂ | Z₂ + Z₄] - d[Z₁ | Z₁ + Z₂ # Z₃ | Z₃ + Z₄]) / 4 + (H[Z₁ + Z₂] - H[Z₃ + Z₄] + H[Z₂] - H[Z₃] + H[Z₂ | Z₂ + Z₄] - H[Z₁ | Z₁ + Z₃]) / 8

Other version of gen_ineq_00, in which we switch to the complement in the first term.

theorem construct_good_prelim' {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Module (ZMod 2) G] {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] {p : refPackage Ω₀₁ Ω₀₂ G} {Ω : Type u_4} [MeasureTheory.MeasureSpace Ω] {X₁ X₂ : Ω → G} (h_min : tau_minimizes p X₁ X₂) {Ω' : Type u_5} [MeasureTheory.MeasureSpace Ω'] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {T₁ T₂ T₃ : Ω' → G} (hT : T₁ + T₂ + T₃ = 0) (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃) : d[X₁ # X₂] ≤ I[T₁ : T₂] + I[T₂ : T₃] + I[T₃ : T₁] + p.η * (d[p.X₀₁ # T₁ | T₃] - d[p.X₀₁ # X₁] + (d[p.X₀₂ # T₂ | T₃] - d[p.X₀₂ # X₂]))

For any $T_1, T_2, T_3$ adding up to $0$, then $k$ is at most $$ \delta + \eta (d[X^0_1;T_1|T_3]-d[X^0_1;X_1]) + \eta (d[X^0_2;T_2|T_3]-d[X^0_2;X_2])$$ where $\delta = I[T₁ : T₂ ; μ] + I[T₂ : T₃ ; μ] + I[T₃ : T₁ ; μ]$.

theorem construct_good_improved' {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Module (ZMod 2) G] {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] {p : refPackage Ω₀₁ Ω₀₂ G} {Ω : Type u_4} [MeasureTheory.MeasureSpace Ω] {X₁ X₂ : Ω → G} (h_min : tau_minimizes p X₁ X₂) {Ω' : Type u_5} [MeasureTheory.MeasureSpace Ω'] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {T₁ T₂ T₃ : Ω' → G} (hT : T₁ + T₂ + T₃ = 0) (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃) : d[X₁ # X₂] ≤ I[T₁ : T₂] + I[T₂ : T₃] + I[T₃ : T₁] + p.η / 6 * (d[p.X₀₁ # T₁ | T₂] - d[p.X₀₁ # X₁] + (d[p.X₀₁ # T₁ | T₃] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # T₂ | T₁] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # T₂ | T₃] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # T₃ | T₁] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # T₃ | T₂] - d[p.X₀₁ # X₁]) + (d[p.X₀₂ # T₁ | T₂] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # T₁ | T₃] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # T₂ | T₁] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # T₂ | T₃] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # T₃ | T₁] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # T₃ | T₂] - d[p.X₀₂ # X₂]))

In fact $k$ is at most $$ \delta + \frac{\eta}{6} \sum_{i=1}^2 \sum_{1 \leq j,l \leq 3; j \neq l} (d[X^0_i;T_j|T_l] - d[X^0_i; X_i]).$$

theorem construct_good_improved'' {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Module (ZMod 2) G] {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] {p : refPackage Ω₀₁ Ω₀₂ G} {Ω : Type u_4} [MeasureTheory.MeasureSpace Ω] {X₁ X₂ : Ω → G} (h_min : tau_minimizes p X₁ X₂) {Ω' : Type u_6} [MeasurableSpace Ω'] (μ : MeasureTheory.Measure Ω') [MeasureTheory.IsProbabilityMeasure μ] {T₁ T₂ T₃ : Ω' → G} (hT : T₁ + T₂ + T₃ = 0) (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃) : d[X₁ # X₂] ≤ I[T₁ : T₂ ; μ] + I[T₂ : T₃ ; μ] + I[T₃ : T₁ ; μ] + p.η / 6 * (d[p.X₀₁ ; MeasureTheory.volume # T₁ | T₂ ; μ] - d[p.X₀₁ # X₁] + (d[p.X₀₁ ; MeasureTheory.volume # T₁ | T₃ ; μ] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ ; MeasureTheory.volume # T₂ | T₁ ; μ] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ ; MeasureTheory.volume # T₂ | T₃ ; μ] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ ; MeasureTheory.volume # T₃ | T₁ ; μ] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ ; MeasureTheory.volume # T₃ | T₂ ; μ] - d[p.X₀₁ # X₁]) + (d[p.X₀₂ ; MeasureTheory.volume # T₁ | T₂ ; μ] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ ; MeasureTheory.volume # T₁ | T₃ ; μ] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ ; MeasureTheory.volume # T₂ | T₁ ; μ] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ ; MeasureTheory.volume # T₂ | T₃ ; μ] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ ; MeasureTheory.volume # T₃ | T₁ ; μ] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ ; MeasureTheory.volume # T₃ | T₂ ; μ] - d[p.X₀₂ # X₂]))

Rephrase construct_good_improved' with an explicit probability measure, as we will apply it to (varying) conditional measures.

theorem averaged_construct_good {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Module (ZMod 2) G] {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] {p : refPackage Ω₀₁ Ω₀₂ G} {Ω : Type u_4} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X₁ X₂ X₁' X₂' : Ω → G} (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') (h_min : tau_minimizes p X₁ X₂) : d[X₁ # X₂] ≤ I[X₁ + X₂ : X₁' + X₂|X₁ + X₂ + X₁' + X₂'] + I[X₁' + X₂ : X₁' + X₁|X₁ + X₂ + X₁' + X₂'] + I[X₁' + X₁ : X₁ + X₂|X₁ + X₂ + X₁' + X₂'] + p.η / 6 * (d[p.X₀₁ # X₁ + X₂ | ⟨X₁' + X₂, X₁ + X₂ + X₁' + X₂'⟩] - d[p.X₀₁ # X₁] + (d[p.X₀₁ # X₁ + X₂ | ⟨X₁' + X₁, X₁ + X₂ + X₁' + X₂'⟩] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # X₁' + X₂ | ⟨X₁ + X₂, X₁ + X₂ + X₁' + X₂'⟩] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # X₁' + X₂ | ⟨X₁' + X₁, X₁ + X₂ + X₁' + X₂'⟩] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # X₁' + X₁ | ⟨X₁ + X₂, X₁ + X₂ + X₁' + X₂'⟩] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # X₁' + X₁ | ⟨X₁' + X₂, X₁ + X₂ + X₁' + X₂'⟩] - d[p.X₀₁ # X₁]) + (d[p.X₀₂ # X₁ + X₂ | ⟨X₁' + X₂, X₁ + X₂ + X₁' + X₂'⟩] - d[p.X₀₂ # X₂] + (d[p.X₀₂ # X₁ + X₂ | ⟨X₁' + X₁, X₁ + X₂ + X₁' + X₂'⟩] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # X₁' + X₂ | ⟨X₁ + X₂, X₁ + X₂ + X₁' + X₂'⟩] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # X₁' + X₂ | ⟨X₁' + X₁, X₁ + X₂ + X₁' + X₂'⟩] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # X₁' + X₁ | ⟨X₁ + X₂, X₁ + X₂ + X₁' + X₂'⟩] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # X₁' + X₁ | ⟨X₁' + X₂, X₁ + X₂ + X₁' + X₂'⟩] - d[p.X₀₂ # X₂])))

$k$ is at most $$ \leq I(U : V \, | \, S) + I(V : W \, | \,S) + I(W : U \, | \, S) + \frac{\eta}{6} \sum_{i=1}^2 \sum_{A,B \in \{U,V,W\}: A \neq B} (d[X^0_i;A|B,S] - d[X^0_i; X_i]).$$

theorem dist_diff_bound_1 {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Module (ZMod 2) G] {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (p : refPackage Ω₀₁ Ω₀₂ G) {Ω : Type u_4} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X₁ X₂ X₁' X₂' : Ω → G} (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') (h₁ : ProbabilityTheory.IdentDistrib X₁ X₁' MeasureTheory.volume MeasureTheory.volume) (h₂ : ProbabilityTheory.IdentDistrib X₂ X₂' MeasureTheory.volume MeasureTheory.volume) (h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![X₁, X₂, X₂', X₁'] MeasureTheory.volume) : d[p.X₀₁ # X₁ + X₂ | ⟨X₁' + X₂, X₁ + X₂ + X₁' + X₂'⟩] - d[p.X₀₁ # X₁] + (d[p.X₀₁ # X₁ + X₂ | ⟨X₁' + X₁, X₁ + X₂ + X₁' + X₂'⟩] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # X₁' + X₂ | ⟨X₁ + X₂, X₁ + X₂ + X₁' + X₂'⟩] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # X₁' + X₂ | ⟨X₁' + X₁, X₁ + X₂ + X₁' + X₂'⟩] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # X₁' + X₁ | ⟨X₁ + X₂, X₁ + X₂ + X₁' + X₂'⟩] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # X₁' + X₁ | ⟨X₁' + X₂, X₁ + X₂ + X₁' + X₂'⟩] - d[p.X₀₁ # X₁]) ≤ (16 * d[X₁ # X₂] + 6 * d[X₁ # X₁] + 2 * d[X₂ # X₂]) / 4 + (H[X₁ + X₁'] - H[X₂ + X₂']) / 4 + (H[X₂ | X₂ + X₂'] - H[X₁ | X₁ + X₁']) / 4

theorem dist_diff_bound_2 {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Module (ZMod 2) G] {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (p : refPackage Ω₀₁ Ω₀₂ G) {Ω : Type u_4} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X₁ X₂ X₁' X₂' : Ω → G} (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') (h₁ : ProbabilityTheory.IdentDistrib X₁ X₁' MeasureTheory.volume MeasureTheory.volume) (h₂ : ProbabilityTheory.IdentDistrib X₂ X₂' MeasureTheory.volume MeasureTheory.volume) (h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![X₁, X₂, X₂', X₁'] MeasureTheory.volume) : d[p.X₀₂ # X₁ + X₂ | ⟨X₁' + X₂, X₁ + X₂ + X₁' + X₂'⟩] - d[p.X₀₂ # X₂] + (d[p.X₀₂ # X₁ + X₂ | ⟨X₁' + X₁, X₁ + X₂ + X₁' + X₂'⟩] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # X₁' + X₂ | ⟨X₁ + X₂, X₁ + X₂ + X₁' + X₂'⟩] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # X₁' + X₂ | ⟨X₁' + X₁, X₁ + X₂ + X₁' + X₂'⟩] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # X₁' + X₁ | ⟨X₁ + X₂, X₁ + X₂ + X₁' + X₂'⟩] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # X₁' + X₁ | ⟨X₁' + X₂, X₁ + X₂ + X₁' + X₂'⟩] - d[p.X₀₂ # X₂]) ≤ (16 * d[X₁ # X₂] + 6 * d[X₂ # X₂] + 2 * d[X₁ # X₁]) / 4 + (H[X₂ + X₂'] - H[X₁ + X₁']) / 4 + (H[X₁ | X₁ + X₁'] - H[X₂ | X₂ + X₂']) / 4

theorem averaged_final {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Module (ZMod 2) G] {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (p : refPackage Ω₀₁ Ω₀₂ G) {Ω : Type u_4} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X₁ X₂ X₁' X₂' : Ω → G} (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') (h₁ : ProbabilityTheory.IdentDistrib X₁ X₁' MeasureTheory.volume MeasureTheory.volume) (h₂ : ProbabilityTheory.IdentDistrib X₂ X₂' MeasureTheory.volume MeasureTheory.volume) (h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![X₁, X₂, X₂', X₁'] MeasureTheory.volume) (h_min : tau_minimizes p X₁ X₂) : d[X₁ # X₂] ≤ 6 * p.η * d[X₁ # X₂] - (1 - 5 * p.η) / (1 - p.η) * (2 * p.η * d[X₁ # X₂] - I[X₁ + X₂ : X₁' + X₂|X₁ + X₂ + X₁' + X₂']) + p.η / 6 * (8 * d[X₁ # X₂] + 2 * (d[X₁ # X₁] + d[X₂ # X₂]))

theorem tau_strictly_decreases_aux' {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Module (ZMod 2) G] {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (p : refPackage Ω₀₁ Ω₀₂ G) {Ω : Type u_4} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X₁ X₂ X₁' X₂' : Ω → G} (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') (h₁ : ProbabilityTheory.IdentDistrib X₁ X₁' MeasureTheory.volume MeasureTheory.volume) (h₂ : ProbabilityTheory.IdentDistrib X₂ X₂' MeasureTheory.volume MeasureTheory.volume) (h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![X₁, X₂, X₂', X₁'] MeasureTheory.volume) (h_min : tau_minimizes p X₁ X₂) (hp : 8 * p.η < 1) : d[X₁ # X₂] = 0

Suppose $0 < \eta < 1/8$. Let $X_1, X_2$ be tau-minimizers. Then $d[X_1;X_2] = 0$. The proof of this lemma uses copies X₁', X₂' already in the context. For a version that does not assume these are given and constructs them instead, use tau_strictly_decreases'.

theorem tau_strictly_decreases' {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Module (ZMod 2) G] {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (p : refPackage Ω₀₁ Ω₀₂ G) {Ω : Type u_4} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X₁ X₂ : Ω → G} (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (h_min : tau_minimizes p X₁ X₂) (hp : 8 * p.η < 1) : d[X₁ # X₂] = 0

theorem tau_minimizer_exists_rdist_eq_zero {Ω₀₁ : Type u_1} {Ω₀₂ : Type u_2} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {G : Type uG} [AddCommGroup G] [Module (ZMod 2) G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] (p : refPackage Ω₀₁ Ω₀₂ G) : ∃ (Ω : Type uG) (x : MeasureTheory.MeasureSpace Ω) (X₁ : Ω → G) (X₂ : Ω → G), Measurable X₁ ∧ Measurable X₂ ∧ MeasureTheory.IsProbabilityMeasure MeasureTheory.volume ∧ tau_minimizes p X₁ X₂ ∧ d[X₁ # X₂] = 0

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

theorem entropic_PFR_conjecture_improv {Ω₀₁ : Type u_1} {Ω₀₂ : Type u_2} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {G : Type uG} [AddCommGroup G] [Module (ZMod 2) G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] (p : refPackage Ω₀₁ Ω₀₂ G) (hpη : p.η = 1 / 8) : ∃ (H : Submodule (ZMod 2) G) (Ω : Type uG) (mΩ : MeasureTheory.MeasureSpace Ω) (U : Ω → G), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume ∧ Measurable U ∧ ProbabilityTheory.IsUniform (↑H) U MeasureTheory.volume ∧ d[p.X₀₁ # U] + d[p.X₀₂ # U] ≤ 10 * d[p.X₀₁ # p.X₀₂]

entropic_PFR_conjecture_improv: 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 10 d[X^0_1;X^0_2]$.

theorem entropic_PFR_conjecture_improv' {Ω₀₁ : Type u_1} {Ω₀₂ : Type u_2} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {G : Type uG} [AddCommGroup G] [Module (ZMod 2) G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] (p : refPackage Ω₀₁ Ω₀₂ G) (hpη : p.η = 1 / 8) : ∃ (H : AddSubgroup G) (Ω : Type uG) (mΩ : MeasureTheory.MeasureSpace Ω) (U : Ω → G), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume ∧ Measurable U ∧ ProbabilityTheory.IsUniform (↑H) U MeasureTheory.volume ∧ d[p.X₀₁ # U] + d[p.X₀₂ # U] ≤ 10 * d[p.X₀₁ # p.X₀₂] ∧ d[p.X₀₁ # U] ≤ 11 / 2 * d[p.X₀₁ # p.X₀₂] ∧ d[p.X₀₂ # U] ≤ 11 / 2 * d[p.X₀₁ # p.X₀₂]

entropic_PFR_conjecture_improv': 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 10 d[X^0_1;X^0_2]$., and d[X^0_1; U_H] and d[X^0_2; U_H] are at most 5/2 * d[X^0_1;X^0_2]

theorem PFR_conjecture_improv_aux {G : Type u_1} [AddCommGroup G] [Module (ZMod 2) G] [Fintype G] {A : Set G} {K : ℝ} (h₀A : A.Nonempty) (hA : ↑(Nat.card ↑(A + A)) ≤ K * ↑(Nat.card ↑A)) : ∃ (H : Submodule (ZMod 2) G) (c : Set G), ↑(Nat.card ↑c) ≤ K ^ 6 * ↑(Nat.card ↑A) ^ (1 / 2) * ↑(Nat.card ↥H) ^ (-1 / 2) ∧ ↑(Nat.card ↥H) ≤ K ^ 10 * ↑(Nat.card ↑A) ∧ ↑(Nat.card ↑A) ≤ K ^ 10 * ↑(Nat.card ↥H) ∧ 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^6 |A|^{1/2} / |H|^{1/2}$ cosets of $H$, and $H$ has the same cardinality as $A$ up to a multiplicative factor $K^10$.

theorem PFR_conjecture_improv {G : Type u_1} [AddCommGroup G] [Module (ZMod 2) G] [Fintype G] {A : Set G} {K : ℝ} (h₀A : A.Nonempty) (hA : ↑(Nat.card ↑(A + A)) ≤ K * ↑(Nat.card ↑A)) : ∃ (H : Submodule (ZMod 2) G) (c : Set G), ↑(Nat.card ↑c) < 2 * K ^ 11 ∧ Nat.card ↥H ≤ Nat.card ↑A ∧ A ⊆ c + ↑H

The polynomial Freiman-Ruzsa (PFR) conjecture: if $A$ is a subset of an elementary abelian 2-group of doubling constant at most $K$, then $A$ can be covered by at most $2K^{11$} cosets of a subgroup of cardinality at most $|A|$.

theorem PFR_conjecture_improv' {G : Type u_3} [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 ^ 11 ∧ Nat.card ↥H ≤ Nat.card ↑A ∧ A ⊆ c + ↑H

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