First estimate

The first estimate on tau-minimizers.

Assumptions:

• $X_1, X_2$ are tau-minimizers
• $X_1, X_2, \tilde X_1, \tilde X_2$ are independent random variables, with $X_1,\tilde X_1$ copies of $X_1$ and $X_2,\tilde X_2$ copies of $X_2$.
• $k := d[X_1;X_2]$
• $I_1 := I [X_1+X_2 : \tilde X_1 + X_2 | X_1+X_2+\tilde X_1+\tilde X_2]$

Main results

• first_estimate : $I_1 ≤ 2 η k$
• ent_ofsum_le : $H[X_1+X_2+\tilde X_1+\tilde X_2] \le \tfrac{1}{2} H[X_1]+\tfrac{1}{2} H[X_2] + (2 + \eta) k - I_1.$

theorem rdist_add_rdist_add_condMutual_eq {G : Type u_1} [addgroup : AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [elem : ElementaryAddCommGroup G 2] {Ω : Type u_4} [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) : d[X₁ + X₂' # X₂ + X₁'] + d[X₁ | X₁ + X₂' # X₂ | X₂ + X₁'] + I[X₁ + X₂ : X₁' + X₂|X₁ + X₂ + X₁' + X₂'] = 2 * d[X₁ # X₂]

The sum of $$ d[X_1+\tilde X_2;X_2+\tilde X_1] + d[X_1|X_1+\tilde X_2; X_2|X_2+\tilde X_1] $$ and $$ I[X_1+ X_2 : \tilde X_1 + X_2 ,|, X_1 + X_2 + \tilde X_1 + \tilde X_2] $$ is equal to $2k$.

theorem rdist_of_sums_ge {G : Type u_1} [addgroup : AddCommGroup G] [hG : MeasurableSpace G] [MeasurableAdd₂ G] {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] (p : refPackage Ω₀₁ Ω₀₂ G) {Ω : Type u_4} [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_min : tau_minimizes p X₁ X₂) : d[X₁ + X₂' # X₂ + X₁'] ≥ d[X₁ # X₂] - p.η * (d[p.X₀₁ # X₁ + X₂'] - d[p.X₀₁ # X₁]) - p.η * (d[p.X₀₂ # X₂ + X₁'] - d[p.X₀₂ # X₂])

The distance $d[X_1+\tilde X_2; X_2+\tilde X_1]$ is at least $$ k - \eta (d[X^0_1; X_1+\tilde X_2] - d[X^0_1; X_1]) - \eta (d[X^0_2; X_2+\tilde X_1] - d[X^0_2; X_2]).$$

theorem condRuzsaDist_of_sums_ge {G : Type u_1} [addgroup : AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [MeasurableAdd₂ G] {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [MeasureTheory.MeasureSpace Ω₀₁] [MeasureTheory.MeasureSpace Ω₀₂] (p : refPackage Ω₀₁ Ω₀₂ G) {Ω : Type u_4} [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_min : tau_minimizes p X₁ X₂) : d[X₁ | X₁ + X₂' # X₂ | X₂ + X₁'] ≥ d[X₁ # X₂] - p.η * (d[p.X₀₁ # X₁ | X₁ + X₂'] - d[p.X₀₁ # X₁]) - p.η * (d[p.X₀₂ # X₂ | X₂ + X₁'] - d[p.X₀₂ # X₂])

The distance $d[X_1|X_1+\tilde X_2; X_2|X_2+\tilde X_1]$ is at least $$ k - \eta (d[X^0_1; X_1 | X_1 + \tilde X_2] - d[X^0_1; X_1]) - \eta(d[X^0_2; X_2 | X_2 + \tilde X_1] - d[X^0_2; X_2]).$$

theorem diff_rdist_le_1 {G : Type u_1} [addgroup : 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] (p : refPackage Ω₀₁ Ω₀₂ G) {Ω : Type u_4} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X₁ : Ω → G) (X₂ : Ω → G) (X₁' : Ω → G) (X₂' : Ω → G) (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) : d[p.X₀₁ # X₁ + X₂'] - d[p.X₀₁ # X₁] ≤ d[X₁ # X₂] / 2 + H[X₂] / 4 - H[X₁] / 4

d[X₀₁ # X₁ + X₂'] - d[X₀₁ # X₁] ≤ k/2 + H[X₂]/4 - H[X₁]/4.

theorem diff_rdist_le_2 {G : Type u_1} [addgroup : 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] (p : refPackage Ω₀₁ Ω₀₂ G) {Ω : Type u_4} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X₁ : Ω → G) (X₂ : Ω → G) (X₁' : Ω → G) (X₂' : Ω → G) (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) : d[p.X₀₂ # X₂ + X₁'] - d[p.X₀₂ # X₂] ≤ d[X₁ # X₂] / 2 + H[X₁] / 4 - H[X₂] / 4

$$ d[X^0_2;X_2+\tilde X_1] - d[X^0_2; X_2] \leq \tfrac{1}{2} k + \tfrac{1}{4} \mathbb{H}[X_1] - \tfrac{1}{4} \mathbb{H}[X_2].$$

theorem diff_rdist_le_3 {G : Type u_1} [addgroup : 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] (p : refPackage Ω₀₁ Ω₀₂ G) {Ω : Type u_4} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X₁ : Ω → G) (X₂ : Ω → G) (X₁' : Ω → G) (X₂' : Ω → G) (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) : d[p.X₀₁ # X₁ | X₁ + X₂'] - d[p.X₀₁ # X₁] ≤ d[X₁ # X₂] / 2 + H[X₁] / 4 - H[X₂] / 4

$$ d[X_1^0;X_1|X_1+\tilde X_2] - d[X_1^0;X_1] \leq \tfrac{1}{2} k + \tfrac{1}{4} \mathbb{H}[X_1] - \tfrac{1}{4} \mathbb{H}[X_2].$$

theorem diff_rdist_le_4 {G : Type u_1} [addgroup : 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] (p : refPackage Ω₀₁ Ω₀₂ G) {Ω : Type u_4} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X₁ : Ω → G) (X₂ : Ω → G) (X₁' : Ω → G) (X₂' : Ω → G) (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) : d[p.X₀₂ # X₂ | X₂ + X₁'] - d[p.X₀₂ # X₂] ≤ d[X₁ # X₂] / 2 + H[X₂] / 4 - H[X₁] / 4

$$ d[X_2^0; X_2|X_2+\tilde X_1] - d[X_2^0; X_2] \leq \tfrac{1}{2}k + \tfrac{1}{4} \mathbb{H}[X_2] - \tfrac{1}{4} \mathbb{H}[X_1].$$

theorem first_estimate {G : Type u_1} [addgroup : 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} [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₂'] ≤ 2 * p.η * d[X₁ # X₂]

We have $I_1 \leq 2 \eta k$

theorem ent_ofsum_le {G : Type u_1} [addgroup : 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} [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₂) : H[X₁ + X₂ + X₁' + X₂'] ≤ H[X₁] / 2 + H[X₂] / 2 + (2 + p.η) * d[X₁ # X₂] - I[X₁ + X₂ : X₁' + X₂|X₁ + X₂ + X₁' + X₂']

$$\mathbb{H}[X_1+X_2+\tilde X_1+\tilde X_2] \le \tfrac{1}{2} \mathbb{H}[X_1]+\tfrac{1}{2} \mathbb{H}[X_2] + (2 + \eta) k - I_1.$$