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} \leq 2 η k$
ent_ofsum_le : $H [X_{1} + X_{2} + {\tilde{X}}_{1} + {\tilde{X}}_{2}] \leq \frac{1}{2} H [X_{1}] + \frac{1}{2} H [X_{2}] + (2 + η) k - I_{1} .$

theorem rdist_add_rdist_add_condMutual_eq {G : Type u_1} [addgroup : AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [MeasurableSingletonClass 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) [Module (ZMod 2) G] :

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 $2 k$ .

source

theorem rdist_of_sums_ge {G : Type u_1} [addgroup : 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} [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₂' # 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 - η (d [X_{1}^{0}; X_{1} + {\tilde{X}}_{2}] - d [X_{1}^{0}; X_{1}]) - η (d [X_{2}^{0}; X_{2} + {\tilde{X}}_{1}] - d [X_{2}^{0}; X_{2}]) .$

source

theorem condRuzsaDist_of_sums_ge {G : Type u_1} [addgroup : 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} [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₁ + 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 - η (d [X_{1}^{0}; X_{1} | X_{1} + {\tilde{X}}_{2}] - d [X_{1}^{0}; X_{1}]) - η (d [X_{2}^{0}; X_{2} | X_{2} + {\tilde{X}}_{1}] - d [X_{2}^{0}; X_{2}]) .$

source

theorem diff_rdist_le_1 {G : Type u_1} [addgroup : 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} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X₁ X₂ X₁' X₂' : Ω → G) (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) [Module (ZMod 2) G] [MeasureTheory.IsProbabilityMeasure 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.

source

theorem diff_rdist_le_2 {G : Type u_1} [addgroup : 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} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X₁ X₂ X₁' X₂' : Ω → G) (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) [Module (ZMod 2) G] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] :

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

$d [X_{2}^{0}; X_{2} + {\tilde{X}}_{1}] - d [X_{2}^{0}; X_{2}] \leq \frac{1}{2} k + \frac{1}{4} H [X_{1}] - \frac{1}{4} H [X_{2}] .$

source

theorem diff_rdist_le_3 {G : Type u_1} [addgroup : 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} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X₁ X₂ X₁' X₂' : Ω → G) (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) [Module (ZMod 2) G] [MeasureTheory.IsProbabilityMeasure 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 \frac{1}{2} k + \frac{1}{4} H [X_{1}] - \frac{1}{4} H [X_{2}] .$

source

theorem diff_rdist_le_4 {G : Type u_1} [addgroup : 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} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (X₁ X₂ X₁' X₂' : Ω → G) (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) [Module (ZMod 2) G] [MeasureTheory.IsProbabilityMeasure 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 \frac{1}{2} k + \frac{1}{4} H [X_{2}] - \frac{1}{4} H [X_{1}] .$

source

I[X₁ + X₂ : X₁' + X₂|X₁ + X₂ + X₁' + X₂'] ≤ 2 * p.η * d[X₁ # X₂]

We have $I_{1} \leq 2 η k$

source

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₂']

$H [X_{1} + X_{2} + {\tilde{X}}_{1} + {\tilde{X}}_{2}] \leq \frac{1}{2} H [X_{1}] + \frac{1}{2} H [X_{2}] + (2 + η) k - I_{1} .$

Documentation

PFR.FirstEstimate

First estimate #

Main results #