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] [MeasurableAdd₂ G] {Ω : Type u_4} [mΩ : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X₁ : Ω → G) (X₂ : Ω → G) (X₁' : Ω → G) (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 (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![X₁, X₂, X₁', X₂'] 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] [elem : ElementaryAddCommGroup G 2] [MeasurableAdd₂ 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 Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X₁ : Ω → G) (X₂ : Ω → G) (X₁' : Ω → G) (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₂) : 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] [hG : MeasurableSpace G] [MeasurableAdd₂ G] {Ω : Type u_4} [mΩ : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X₁ : Ω → G) (X₂ : Ω → G) (X₁' : Ω → G) (X₂' : Ω → G) (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[X₁ + X₂] = H[X₁' + X₂']

theorem independenceCondition1 {G : Type u_1} [AddCommGroup G] [hG : MeasurableSpace G] [MeasurableAdd₂ G] {Ω : Type u_4} [mΩ : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X₁ : Ω → G} {X₂ : Ω → G} {X₁' : Ω → G} {X₂' : Ω → G} (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') (h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![X₁, X₂, X₁', X₂'] MeasureTheory.volume) : ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => hG) ![X₁, X₂, X₁' + X₂'] MeasureTheory.volume

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

theorem independenceCondition2 {G : Type u_1} [AddCommGroup G] [hG : MeasurableSpace G] [MeasurableAdd₂ G] {Ω : Type u_4} [mΩ : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X₁ : Ω → G} {X₂ : Ω → G} {X₁' : Ω → G} {X₂' : Ω → G} (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') (h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![X₁, X₂, X₁', X₂'] MeasureTheory.volume) : ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => hG) ![X₂, X₁, X₁' + X₂'] MeasureTheory.volume

theorem independenceCondition3 {G : Type u_1} [AddCommGroup G] [hG : MeasurableSpace G] [MeasurableAdd₂ G] {Ω : Type u_4} [mΩ : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X₁ : Ω → G} {X₂ : Ω → G} {X₁' : Ω → G} {X₂' : Ω → G} (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') (h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![X₁, X₂, X₁', X₂'] MeasureTheory.volume) : ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => hG) ![X₁', X₂, X₁ + X₂'] MeasureTheory.volume

theorem independenceCondition4 {G : Type u_1} [AddCommGroup G] [hG : MeasurableSpace G] [MeasurableAdd₂ G] {Ω : Type u_4} [mΩ : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X₁ : Ω → G} {X₂ : Ω → G} {X₁' : Ω → G} {X₂' : Ω → G} (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') (h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![X₁, X₂, X₁', X₂'] MeasureTheory.volume) : ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => hG) ![X₂, X₁', X₁ + X₂'] MeasureTheory.volume

theorem independenceCondition5 {G : Type u_1} [AddCommGroup G] [hG : MeasurableSpace G] [MeasurableAdd₂ G] {Ω : Type u_4} [mΩ : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X₁ : Ω → G} {X₂ : Ω → G} {X₁' : Ω → G} {X₂' : Ω → G} (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') (h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![X₁, X₂, X₁', X₂'] MeasureTheory.volume) : ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => hG) ![X₁, X₁', X₂ + X₂'] MeasureTheory.volume

theorem independenceCondition6 {G : Type u_1} [AddCommGroup G] [hG : MeasurableSpace G] [MeasurableAdd₂ G] {Ω : Type u_4} [mΩ : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X₁ : Ω → G} {X₂ : Ω → G} {X₁' : Ω → G} {X₂' : Ω → G} (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (hX₁' : Measurable X₁') (hX₂' : Measurable X₂') (h_indep : ProbabilityTheory.iIndepFun (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![X₁, X₂, X₁', X₂'] MeasureTheory.volume) : ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => hG) ![X₂, X₂', X₁' + X₁] MeasureTheory.volume

theorem sum_dist_diff_le {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [elem : ElementaryAddCommGroup G 2] [MeasurableAdd₂ 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 Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X₁ : Ω → G) (X₂ : Ω → G) (X₁' : Ω → G) (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[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}} \big(d[X^0_i;A|S] - d[X^0_i;X_i]\big)$$ is less than or equal to $$ \leq (6 - 3\eta) k + 3(2 \eta k - I_1).$$

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

U + V + W = 0.

theorem construct_good_prelim {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [elem : ElementaryAddCommGroup G 2] [MeasurableAdd₂ 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₁ : Ω → G) (X₂ : Ω → G) (h_min : tau_minimizes p X₁ X₂) {Ω' : Type u_5} [MeasureTheory.MeasureSpace Ω'] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {T₁ : Ω' → G} {T₂ : Ω' → G} {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₁] - 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 \leq i < j \leq 3} I[T_i;T_j]$$ Then there exist random variables $T'_1, T'_2$ such that $$ d[T'_1;T'_2] + \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]) $$ is at most $$ \delta + \eta ( d[X^0_1;T_1]-d[X^0_1;X_1]) + \eta (d[X^0_2;T_2]-d[X^0_2;X_2]) $$ $$ + \tfrac12 \eta I[T_1: T_3] + \tfrac12 \eta I[T_2: T_3].$$

theorem construct_good {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [elem : ElementaryAddCommGroup G 2] [MeasurableAdd₂ 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₁ : Ω → G) (X₂ : Ω → G) (h_min : tau_minimizes p X₁ X₂) {Ω' : Type u_5} [MeasureTheory.MeasureSpace Ω'] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {T₁ : Ω' → G} {T₂ : Ω' → G} {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.η / 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 \leq i < j \leq 3} I[T_i;T_j]$$

Then there exist random variables $T'_1, T'_2$ such that

$$ d[T'_1;T'_2] + \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])$$

is at most

$$\delta + \frac{\eta}{3} \biggl( \delta + \sum_{i=1}^2 \sum_{j = 1}^3 (d[X^0_i;T_j] - d[X^0_i; X_i]) \biggr).$$

theorem construct_good' {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [elem : ElementaryAddCommGroup G 2] [MeasurableAdd₂ 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₁ : Ω → G) (X₂ : Ω → G) (h_min : tau_minimizes p X₁ X₂) {Ω' : Type u_5} [MeasureTheory.MeasureSpace Ω'] {T₁ : Ω' → G} {T₂ : Ω' → G} {T₃ : Ω' → G} (hT : T₁ + T₂ + T₃ = 0) (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃) (μ : 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 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₁ : Ω → G) (X₂ : Ω → G) {Ω' : Type u_5} [MeasureTheory.MeasureSpace Ω'] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {Y : Ω' → G} {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 ; ProbabilityTheory.cond MeasureTheory.volume (Z ⁻¹' {z})] - d[p.X₀₁ # X₁] + (d[p.X₀₂ ; MeasureTheory.volume # Y ; ProbabilityTheory.cond MeasureTheory.volume (Z ⁻¹' {z})] - d[p.X₀₂ # X₂])) x ∂MeasureTheory.Measure.map Z MeasureTheory.volume

theorem delta'_eq_integral {G : Type u_1} [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] {Ω' : Type u_5} [MeasureTheory.MeasureSpace Ω'] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {T₁ : Ω' → G} {T₂ : Ω' → G} {T₃ : Ω' → G} {R : Ω' → G} : I[T₁ : T₂|R] + I[T₂ : T₃|R] + I[T₃ : T₁|R] = ∫ (x : G), (fun (r : G) => I[T₁ : T₂ ; ProbabilityTheory.cond MeasureTheory.volume (R ⁻¹' {r})] + I[T₂ : T₃ ; ProbabilityTheory.cond MeasureTheory.volume (R ⁻¹' {r})] + I[T₃ : T₁ ; ProbabilityTheory.cond 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] [elem : ElementaryAddCommGroup G 2] [MeasurableAdd₂ 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 Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X₁ : Ω → G) (X₂ : Ω → G) (hX₁ : Measurable X₁) (hX₂ : Measurable X₂) (h_min : tau_minimizes p X₁ X₂) {Ω' : Type u_5} [MeasureTheory.MeasureSpace Ω'] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {T₁ : Ω' → G} {T₂ : Ω' → G} {T₃ : Ω' → G} (hT : T₁ + T₂ + T₃ = 0) (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃) {R : Ω' → G} (hR : Measurable R) : 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] [elem : ElementaryAddCommGroup G 2] [MeasurableAdd₂ 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 Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X₁ : Ω → G) (X₂ : Ω → G) (X₁' : Ω → G) (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η : 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.