The fibring identity #
The proof of the fibring identity, which is a key component of the proof of PFR.
Main statement #
sum_of_rdist_eq: If $Y_1,Y_2,Y_3,Y_4$ are independent, then $d[Y_1; Y_2] + d[Y_3; Y_4]$ is equal to the sum of $$d[Y_1+Y_3; Y_2+Y_4] + d[Y_1|Y_1+Y_3; Y_2|Y_2+Y_4] $$ and $$ I[Y_1+Y_2 : Y_2 + Y_4 | Y_1+Y_2+Y_3+Y_4].$$
theorem
rdist_of_indep_eq_sum_fibre
{H : Type u_1}
[AddCommGroup H]
[Countable H]
[hH : MeasurableSpace H]
[MeasurableSingletonClass H]
{H' : Type u_2}
[AddCommGroup H']
[Countable H']
[hH' : MeasurableSpace H']
[MeasurableSingletonClass H']
(π : H →+ H')
{Ω : Type u_3}
[mΩ : MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{Z_1 Z_2 : Ω → H}
(h : ProbabilityTheory.IndepFun Z_1 Z_2 μ)
(h1 : Measurable Z_1)
(h2 : Measurable Z_2)
[FiniteRange Z_1]
[FiniteRange Z_2]
:
If $Z_1, Z_2$ are independent, then $d[Z_1; Z_2]$ is equal to $$ d[\pi(Z_1);\pi(Z_2)] + d[Z_1|\pi(Z_1); Z_2 |\pi(Z_2)]$$ plus $$I( Z_1 - Z_2 : (\pi(Z_1), \pi(Z_2)) | \pi(Z_1 - Z_2) ).$$
theorem
rdist_le_sum_fibre
{H : Type u_1}
[AddCommGroup H]
[Countable H]
[hH : MeasurableSpace H]
[MeasurableSingletonClass H]
{H' : Type u_2}
[AddCommGroup H']
[Countable H']
[hH' : MeasurableSpace H']
[MeasurableSingletonClass H']
(π : H →+ H')
{Ω : Type u_3}
{Ω' : Type u_4}
[mΩ : MeasurableSpace Ω]
[mΩ' : MeasurableSpace Ω']
{μ : MeasureTheory.Measure Ω}
{μ' : MeasureTheory.Measure Ω'}
[MeasureTheory.IsProbabilityMeasure μ]
[MeasureTheory.IsProbabilityMeasure μ']
{Z_1 : Ω → H}
{Z_2 : Ω' → H}
(h1 : Measurable Z_1)
(h2 : Measurable Z_2)
[FiniteRange Z_1]
[FiniteRange Z_2]
:
theorem
rdist_of_hom_le
{H : Type u_1}
[AddCommGroup H]
[Countable H]
[hH : MeasurableSpace H]
[MeasurableSingletonClass H]
{H' : Type u_2}
[AddCommGroup H']
[Countable H']
[hH' : MeasurableSpace H']
[MeasurableSingletonClass H']
(π : H →+ H')
{Ω : Type u_3}
{Ω' : Type u_4}
[mΩ : MeasurableSpace Ω]
[mΩ' : MeasurableSpace Ω']
{μ : MeasureTheory.Measure Ω}
{μ' : MeasureTheory.Measure Ω'}
[MeasureTheory.IsProbabilityMeasure μ]
[MeasureTheory.IsProbabilityMeasure μ']
{Z_1 : Ω → H}
{Z_2 : Ω' → H}
(h1 : Measurable Z_1)
(h2 : Measurable Z_2)
[FiniteRange Z_1]
[FiniteRange Z_2]
:
[d[X;Y]\geq d[\pi(X);\pi(Y)].]
theorem
sum_of_rdist_eq_step_condRuzsaDist
{G : Type u_1}
[AddCommGroup G]
[Fintype G]
[hG : MeasurableSpace G]
[MeasurableSingletonClass G]
{Ω : Type u_2}
[mΩ : MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{Y : Fin 4 → Ω → G}
(h_indep : ProbabilityTheory.iIndepFun (fun (x : Fin 4) => hG) Y μ)
(h_meas : ∀ (i : Fin 4), Measurable (Y i))
:
The conditional Ruzsa Distance step of sum_of_rdist_eq
theorem
sum_of_rdist_eq_step_condMutualInfo
{G : Type u_1}
[AddCommGroup G]
[Fintype G]
[hG : MeasurableSpace G]
[MeasurableSingletonClass G]
{Ω : Type u_2}
[mΩ : MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{Y : Fin 4 → Ω → G}
(h_meas : ∀ (i : Fin 4), Measurable (Y i))
:
The conditional mutual information step of sum_of_rdist_eq
theorem
sum_of_rdist_eq
{G : Type u_1}
[AddCommGroup G]
[Fintype G]
[hG : MeasurableSpace G]
[MeasurableSingletonClass G]
{Ω : Type u_2}
[mΩ : MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
(Y : Fin 4 → Ω → G)
(h_indep : ProbabilityTheory.iIndepFun (fun (x : Fin 4) => hG) Y μ)
(h_meas : ∀ (i : Fin 4), Measurable (Y i))
:
Let $Y_1,Y_2,Y_3$ and $Y_4$ be independent $G$-valued random variables. Then $$d[Y_1-Y_3; Y_2-Y_4] + d[Y_1|Y_1-Y_3; Y_2|Y_2-Y_4] $$ $$ + I[Y_1-Y_2 : Y_2 - Y_4 | Y_1-Y_2-Y_3+Y_4] = d[Y_1; Y_2] + d[Y_3; Y_4].$$
theorem
sum_of_rdist_eq_char_2
{G : Type u_1}
[AddCommGroup G]
[Fintype G]
[hG : MeasurableSpace G]
[MeasurableSingletonClass G]
{Ω : Type u_2}
[mΩ : MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
[Module (ZMod 2) G]
(Y : Fin 4 → Ω → G)
(h_indep : ProbabilityTheory.iIndepFun (fun (x : Fin 4) => hG) Y μ)
(h_meas : ∀ (i : Fin 4), Measurable (Y i))
:
Let $Y_1,Y_2,Y_3$ and $Y_4$ be independent $G$-valued random variables. Then $$d[Y_1+Y_3; Y_2+Y_4] + d[Y_1|Y_1+Y_3; Y_2|Y_2+Y_4] $$ $$ + I[Y_1+Y_2 : Y_2 + Y_4 | Y_1+Y_2+Y_3+Y_4] = d[Y_1; Y_2] + d[Y_3; Y_4].$$
theorem
sum_of_rdist_eq_char_2'
{G : Type u_1}
[AddCommGroup G]
[Fintype G]
[hG : MeasurableSpace G]
[MeasurableSingletonClass G]
{Ω : Type u_2}
[mΩ : MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
[Module (ZMod 2) G]
(X Y X' Y' : Ω → G)
(h_indep : ProbabilityTheory.iIndepFun (fun (x : Fin 4) => hG) ![X, Y, X', Y'] μ)
(hX : Measurable X)
(hY : Measurable Y)
(hX' : Measurable X')
(hY' : Measurable Y')
: