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 \leq 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 (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![X₁, X₂, X₁', X₂']
MeasureTheory.volume)
(h_min : tau_minimizes p X₁ X₂)
:
$$ d[X_1+\tilde X_1; X_2+\tilde X_2] \geq 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 (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![X₁, X₂, X₁', X₂']
MeasureTheory.volume)
(h_min : tau_minimizes p X₁ X₂)
:
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 (fun (_i : Fin (Nat.succ 0).succ.succ.succ) => hG) ![X₁, X₂, X₁', X₂']
MeasureTheory.volume)
(h_min : tau_minimizes p X₁ X₂)
:
$$ I_2 \leq 2 \eta k + \frac{2 \eta (2 \eta k - I_1)}{1 - \eta}.$$