Second estimate

The second estimate 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$
• $I_1:=I_1[X_1+X_2:{\tilde{X}}_1+X_2|X_1+X_2+{\tilde{X}}_1+{\tilde{X}}_2]$
• $I_2:=I[X_1+X_2:X_1+{\tilde{X}}_1|X_1+X_2+{\tilde{X}}_1+{\tilde{X}}_2]$

Main results

• second_estimate : $$I_2\le 2\eta k+\frac{2\eta (2\eta k-I_1)}{1-\eta }.$$

theorem rdist_of_sums_ge' {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Module (ZMod 2) G] [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₁ 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₂) : d[X₁ + X₁' # X₂ + X₂'] ≥ d[X₁ # X₂] - p.η * (d[X₁ # X₁] + d[X₂ # X₂]) / 2

$$d[X_1+{\tilde{X}}_1;X_2+{\tilde{X}}_2]\ge k-\frac{\eta }{2}(d[X_1;X_1]+d[X_2;X_2]).$$

theorem second_estimate_aux {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Module (ZMod 2) G] [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₁ 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₂) : d[X₁ # X₁] + d[X₂ # X₂] ≤ 2 * (d[X₁ # X₂] + (2 * p.η * d[X₁ # X₂] - I[X₁ + X₂ : X₁' + X₂|X₁ + X₂ + X₁' + X₂']) / (1 - p.η))

theorem second_estimate {G : Type u_1} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Module (ZMod 2) G] [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₁ 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₂) : I[X₁ + X₂ : X₁' + X₁|X₁ + X₂ + X₁' + X₂'] ≤ 2 * p.η * d[X₁ # X₂] + 2 * p.η * (2 * p.η * d[X₁ # X₂] - I[X₁ + X₂ : X₁' + X₂|X₁ + X₂ + X₁' + X₂']) / (1 - p.η)

$$I_2\le 2\eta k+\frac{2\eta (2\eta k-I_1)}{1-\eta }.$$