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 : Ω → H} {Z_2 : Ω → H} (h : ProbabilityTheory.IndepFun Z_1 Z_2 μ) (h1 : Measurable Z_1) (h2 : Measurable Z_2) [FiniteRange Z_1] [FiniteRange Z_2] : d[Z_1 ; μ # Z_2 ; μ] = d[⇑π ∘ Z_1 ; μ # ⇑π ∘ Z_2 ; μ] + d[Z_1 | ⇑π ∘ Z_1 ; μ # Z_2 | ⇑π ∘ Z_2 ; μ] + I[Z_1 - Z_2 : ⟨⇑π ∘ Z_1, ⇑π ∘ Z_2⟩|⇑π ∘ (Z_1 - 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] : d[⇑π ∘ Z_1 ; μ # ⇑π ∘ Z_2 ; μ'] + d[Z_1 | ⇑π ∘ Z_1 ; μ # Z_2 | ⇑π ∘ Z_2 ; μ'] ≤ d[Z_1 ; μ # 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[⇑π ∘ Z_1 ; μ # ⇑π ∘ Z_2 ; μ'] ≤ d[Z_1 ; μ # 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)) : d[⟨Y 0, Y 2⟩ | Y 0 - Y 2 ; μ # ⟨Y 1, Y 3⟩ | Y 1 - Y 3 ; μ] = d[Y 0 | Y 0 - Y 2 ; μ # Y 1 | Y 1 - Y 3 ; μ]

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)) : I[⟨Y 0 - Y 1, Y 2 - Y 3⟩ : ⟨Y 0 - Y 2, Y 1 - Y 3⟩|Y 0 - Y 1 - (Y 2 - Y 3);μ] = I[Y 0 - Y 1 : Y 1 - Y 3|Y 0 - Y 1 - Y 2 + Y 3;μ]

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)) : d[Y 0 ; μ # Y 1 ; μ] + d[Y 2 ; μ # Y 3 ; μ] = d[Y 0 - Y 2 ; μ # Y 1 - Y 3 ; μ] + d[Y 0 | Y 0 - Y 2 ; μ # Y 1 | Y 1 - Y 3 ; μ] + I[Y 0 - Y 1 : Y 1 - Y 3|Y 0 - Y 1 - Y 2 + Y 3;μ]

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 μ] [ElementaryAddCommGroup G 2] (Y : Fin 4 → Ω → G) (h_indep : ProbabilityTheory.iIndepFun (fun (x : Fin 4) => hG) Y μ) (h_meas : ∀ (i : Fin 4), Measurable (Y i)) : d[Y 0 ; μ # Y 1 ; μ] + d[Y 2 ; μ # Y 3 ; μ] = d[Y 0 + Y 2 ; μ # Y 1 + Y 3 ; μ] + d[Y 0 | Y 0 + Y 2 ; μ # Y 1 | Y 1 + Y 3 ; μ] + I[Y 0 + Y 1 : Y 1 + Y 3|Y 0 + Y 1 + Y 2 + Y 3;μ]

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].$$