Endgame

The endgame on tau-minimizers.

Assumptions:

• $X_1,X_2$ are tau-minimizers
• $X_1,X_2,{\tilde{X}}_1,{\tilde{X}}_2$ be independent random variables, with $X_1,{\tilde{X}}_1$ copies of $X_1$ and $X_2,{\tilde{X}}_2$ copies of $X_2$.
• $d[X_1;X_2]=k$
• $U:=X_1+X_2$
• $V:={\tilde{X}}_1+X_2$
• $W:=X_1+{\tilde{X}}_1$
• $S:=X_1+X_2+{\tilde{X}}_1+{\tilde{X}}_2$.
• $I_1:=I[U:V|S]$
• $I_2:=I[U:W|S]$
• $I_3:=I[V:W|S]$ (not explicitly defined in Lean)

Main results:

• sum_condMutual_le : An upper bound on the total conditional mutual information $I_1+I_2+I_3$.
• sum_dist_diff_le: A sum of the "costs" of $U$, $V$, $W$.
• construct_good: A construction of two random variables with small Ruzsa distance between them given some random variables with control on total cost, as well as total mutual information.

theorem I₃_eq {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] {Ω : Type u_4} [mΩ : MeasureTheory.MeasureSpace Ω] (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_indep : ProbabilityTheory.iIndepFun ![X₁, X₂, X₁', X₂'] MeasureTheory.volume) [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] : I[X₁' + X₂ : X₁' + X₁|X₁ + X₂ + X₁' + X₂'] = I[X₁ + X₂ : X₁' + X₁|X₁ + X₂ + X₁' + X₂']

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

theorem sum_condMutual_le {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass 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} [mΩ : MeasureTheory.MeasureSpace Ω] (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 ![X₁, X₂, X₁', X₂'] MeasureTheory.volume) (h_min : tau_minimizes p X₁ X₂) [Module (ZMod 2) G] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] : 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₂'] ≤ 6 * p.η * d[X₁ # X₂] - (1 - 5 * p.η) / (1 - p.η) * (2 * p.η * d[X₁ # X₂] - I[X₁ + X₂ : X₁' + X₂|X₁ + X₂ + X₁' + X₂'])

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₁).

theorem hU {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] {Ω : Type u_4} [mΩ : 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) [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] : H[X₁ + X₂] = H[X₁' + X₂']

theorem independenceCondition1 {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] {Ω : Type u_4} [mΩ : MeasureTheory.MeasureSpace Ω] {X₁ X₂ X₁' X₂' : Ω → G} (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') (h_indep : ProbabilityTheory.iIndepFun ![X₁, X₂, X₁', X₂'] MeasureTheory.volume) : ProbabilityTheory.iIndepFun ![X₁, X₂, X₁' + X₂'] MeasureTheory.volume

theorem hV {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] {Ω : Type u_4} [mΩ : 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) [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] : H[X₁' + X₂] = H[X₁ + X₂']

theorem independenceCondition2 {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] {Ω : Type u_4} [mΩ : MeasureTheory.MeasureSpace Ω] {X₁ X₂ X₁' X₂' : Ω → G} (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') (h_indep : ProbabilityTheory.iIndepFun ![X₁, X₂, X₁', X₂'] MeasureTheory.volume) : ProbabilityTheory.iIndepFun ![X₂, X₁, X₁' + X₂'] MeasureTheory.volume

theorem independenceCondition3 {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] {Ω : Type u_4} [mΩ : MeasureTheory.MeasureSpace Ω] {X₁ X₂ X₁' X₂' : Ω → G} (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') (h_indep : ProbabilityTheory.iIndepFun ![X₁, X₂, X₁', X₂'] MeasureTheory.volume) : ProbabilityTheory.iIndepFun ![X₁', X₂, X₁ + X₂'] MeasureTheory.volume

theorem independenceCondition4 {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] {Ω : Type u_4} [mΩ : MeasureTheory.MeasureSpace Ω] {X₁ X₂ X₁' X₂' : Ω → G} (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') (h_indep : ProbabilityTheory.iIndepFun ![X₁, X₂, X₁', X₂'] MeasureTheory.volume) : ProbabilityTheory.iIndepFun ![X₂, X₁', X₁ + X₂'] MeasureTheory.volume

theorem independenceCondition5 {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] {Ω : Type u_4} [mΩ : MeasureTheory.MeasureSpace Ω] {X₁ X₂ X₁' X₂' : Ω → G} (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') (h_indep : ProbabilityTheory.iIndepFun ![X₁, X₂, X₁', X₂'] MeasureTheory.volume) : ProbabilityTheory.iIndepFun ![X₁, X₁', X₂ + X₂'] MeasureTheory.volume

theorem independenceCondition6 {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] {Ω : Type u_4} [mΩ : MeasureTheory.MeasureSpace Ω] {X₁ X₂ X₁' X₂' : Ω → G} (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') (h_indep : ProbabilityTheory.iIndepFun ![X₁, X₂, X₁', X₂'] MeasureTheory.volume) : ProbabilityTheory.iIndepFun ![X₂, X₂', X₁' + X₁] MeasureTheory.volume

theorem sum_dist_diff_le {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass 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} [mΩ : MeasureTheory.MeasureSpace Ω] (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 ![X₁, X₂, X₁', X₂'] MeasureTheory.volume) (h_min : tau_minimizes p X₁ X₂) [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [Module (ZMod 2) G] : d[p.X₀₁ # X₁ + X₂ | X₁ + X₂ + X₁' + X₂'] - d[p.X₀₁ # X₁] + (d[p.X₀₂ # X₁ + X₂ | X₁ + X₂ + X₁' + X₂'] - d[p.X₀₂ # X₂]) + (d[p.X₀₁ # X₁' + X₂ | X₁ + X₂ + X₁' + X₂'] - d[p.X₀₁ # X₁] + (d[p.X₀₂ # X₁' + X₂ | X₁ + X₂ + X₁' + X₂'] - d[p.X₀₂ # X₂])) + (d[p.X₀₁ # X₁' + X₁ | X₁ + X₂ + X₁' + X₂'] - d[p.X₀₁ # X₁] + (d[p.X₀₂ # X₁' + X₁ | X₁ + X₂ + X₁' + X₂'] - d[p.X₀₂ # X₂])) ≤ (6 - 3 * p.η) * d[X₁ # X₂] + 3 * (2 * p.η * d[X₁ # X₂] - I[X₁ + X₂ : X₁' + X₂|X₁ + X₂ + X₁' + X₂'])

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

theorem sum_uvw_eq_zero {G : Type u_1} [AddCommGroup G] {Ω : Type u_4} (X₁ X₂ X₁' : Ω → G) [Module (ZMod 2) G] : X₁ + X₂ + (X₁' + X₂) + (X₁' + X₁) = 0

U + V + W = 0.

theorem cond_c_eq_integral {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] (p : refPackage Ω₀₁ Ω₀₂ G) {Ω : Type u_4} [mΩ : MeasureTheory.MeasureSpace Ω] (X₁ X₂ : Ω → G) {Ω' : Type u_5} [MeasureTheory.MeasureSpace Ω'] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {Y Z : Ω' → G} (hY : Measurable Y) (hZ : Measurable Z) : d[p.X₀₁ # Y | Z] - d[p.X₀₁ # X₁] + (d[p.X₀₂ # Y | Z] - d[p.X₀₂ # X₂]) = ∫ (x : G), (fun (z : G) => d[p.X₀₁ ; MeasureTheory.volume # Y ; MeasureTheory.volume[|Z ⁻¹' {z}]] - d[p.X₀₁ # X₁] + (d[p.X₀₂ ; MeasureTheory.volume # Y ; MeasureTheory.volume[|Z ⁻¹' {z}]] - d[p.X₀₂ # X₂])) x ∂MeasureTheory.Measure.map Z MeasureTheory.volume

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

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\le i<j\le 3}I[T_i;T_j]$$ Then there exist random variables $T_1^{\prime },T_2^{\prime }$ such that $$d[T_1^{\prime };T_2^{\prime }]+\eta (d[X_1^0;T_1^{\prime }]-d[X_1^0;X_1])+\eta (d[X_2^0;T_2^{\prime }]-d[X_2^0;X_2])$$ is at most $$\delta +\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])$$ $$+\frac{1}{2}\eta I[T_1:T_3]+\frac{1}{2}\eta I[T_2:T_3].$$

theorem construct_good {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass 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} [mΩ : MeasureTheory.MeasureSpace Ω] (X₁ X₂ : Ω → G) (h_min : tau_minimizes p X₁ X₂) {Ω' : Type u_5} [MeasureTheory.MeasureSpace Ω'] {T₁ T₂ T₃ : Ω' → G} (hT : T₁ + T₂ + T₃ = 0) (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃) [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [Module (ZMod 2) G] : d[X₁ # X₂] ≤ I[T₁ : T₂] + I[T₂ : T₃] + I[T₃ : T₁] + p.η / 3 * (I[T₁ : T₂] + I[T₂ : T₃] + I[T₃ : T₁] + (d[p.X₀₁ # T₁] - d[p.X₀₁ # X₁] + (d[p.X₀₂ # T₁] - d[p.X₀₂ # X₂])) + (d[p.X₀₁ # T₂] - d[p.X₀₁ # X₁] + (d[p.X₀₂ # T₂] - d[p.X₀₂ # X₂])) + (d[p.X₀₁ # T₃] - d[p.X₀₁ # X₁] + (d[p.X₀₂ # T₃] - d[p.X₀₂ # X₂])))

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\le i<j\le 3}I[T_i;T_j]$$

Then there exist random variables $T_1^{\prime },T_2^{\prime }$ such that

$$d[T_1^{\prime };T_2^{\prime }]+\eta (d[X_1^0;T_1^{\prime }]-d[X_1^0;X_1])+\eta (d[X_2^0;T_2^{\prime }]-d[X_2^0;X_2])$$

is at most

$$\delta +\frac{\eta }{3}(\delta +\sum _{i=1}^2\sum _{j=1}^3(d[X_i^0;T_j]-d[X_i^0;X_i])).$$

theorem construct_good' {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass 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} [mΩ : MeasureTheory.MeasureSpace Ω] (X₁ X₂ : Ω → G) (h_min : tau_minimizes p X₁ X₂) {Ω' : Type u_5} [MeasureTheory.MeasureSpace Ω'] {T₁ T₂ T₃ : Ω' → G} (hT : T₁ + T₂ + T₃ = 0) (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃) [Module (ZMod 2) G] (μ : MeasureTheory.Measure Ω') [MeasureTheory.IsProbabilityMeasure μ] : d[X₁ # X₂] ≤ I[T₁ : T₂ ; μ] + I[T₂ : T₃ ; μ] + I[T₃ : T₁ ; μ] + p.η / 3 * (I[T₁ : T₂ ; μ] + I[T₂ : T₃ ; μ] + I[T₃ : T₁ ; μ] + (d[p.X₀₁ ; MeasureTheory.volume # T₁ ; μ] - d[p.X₀₁ # X₁] + (d[p.X₀₂ ; MeasureTheory.volume # T₁ ; μ] - d[p.X₀₂ # X₂])) + (d[p.X₀₁ ; MeasureTheory.volume # T₂ ; μ] - d[p.X₀₁ # X₁] + (d[p.X₀₂ ; MeasureTheory.volume # T₂ ; μ] - d[p.X₀₂ # X₂])) + (d[p.X₀₁ ; MeasureTheory.volume # T₃ ; μ] - d[p.X₀₁ # X₁] + (d[p.X₀₂ ; MeasureTheory.volume # T₃ ; μ] - d[p.X₀₂ # X₂])))

theorem delta'_eq_integral {G : Type u_1} [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] {Ω' : Type u_5} [MeasureTheory.MeasureSpace Ω'] {T₁ T₂ T₃ : Ω' → G} [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {R : Ω' → G} : I[T₁ : T₂|R] + I[T₂ : T₃|R] + I[T₃ : T₁|R] = ∫ (x : G), (fun (r : G) => I[T₁ : T₂ ; MeasureTheory.volume[|R ⁻¹' {r}]] + I[T₂ : T₃ ; MeasureTheory.volume[|R ⁻¹' {r}]] + I[T₃ : T₁ ; MeasureTheory.volume[|R ⁻¹' {r}]]) x ∂MeasureTheory.Measure.map R MeasureTheory.volume

theorem cond_construct_good {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass 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} [mΩ : MeasureTheory.MeasureSpace Ω] (X₁ X₂ : Ω → G) (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (h_min : tau_minimizes p X₁ X₂) {Ω' : Type u_5} [MeasureTheory.MeasureSpace Ω'] {T₁ T₂ T₃ : Ω' → G} (hT : T₁ + T₂ + T₃ = 0) (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃) [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [Module (ZMod 2) G] {R : Ω' → G} (hR : Measurable R) [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] : d[X₁ # X₂] ≤ I[T₁ : T₂|R] + I[T₂ : T₃|R] + I[T₃ : T₁|R] + p.η / 3 * (I[T₁ : T₂|R] + I[T₂ : T₃|R] + I[T₃ : T₁|R] + (d[p.X₀₁ # T₁ | R] - d[p.X₀₁ # X₁] + (d[p.X₀₂ # T₁ | R] - d[p.X₀₂ # X₂])) + (d[p.X₀₁ # T₂ | R] - d[p.X₀₁ # X₁] + (d[p.X₀₂ # T₂ | R] - d[p.X₀₂ # X₂])) + (d[p.X₀₁ # T₃ | R] - d[p.X₀₁ # X₁] + (d[p.X₀₂ # T₃ | R] - d[p.X₀₂ # X₂])))

theorem tau_strictly_decreases_aux {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass 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} [mΩ : MeasureTheory.MeasureSpace Ω] (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 ![X₁, X₂, X₁', X₂'] MeasureTheory.volume) (h_min : tau_minimizes p X₁ X₂) [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [Module (ZMod 2) G] (hpη : p.η = 1 / 9) : d[X₁ # X₂] = 0

If d[X₁ ; X₂] > 0 then there are G-valued random variables X₁', X₂' such that Phrased in the contrapositive form for convenience of proof.