sum_of_rdist_eq_step_condMutualInfo

lemma sum_of_rdist_eq_step_condMutualInfo {Y : Fin 4 → Ω → G}    (h_meas : ∀ i, 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;μ] := by  suffices 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) ; μ] by convert this using 2; abel  symm  have hm (f : G → G → G × G) {a b i j k l : Fin 4} :    Measurable (uncurry f ∘ ⟨Y i - Y j - (Y k - Y l), Y a - Y b⟩) := by fun_prop  have hmf : Measurable fun ω ↦ ((Y 0 - Y 1) ω, (Y 0 - Y 1) ω - (Y 0 - Y 1 - (Y 2 - Y 3)) ω) :=    hm (fun z x ↦ (x, x - z))  have hmg : Measurable fun ω ↦ ((Y 1 - Y 3) ω + (Y 0 - Y 1 - (Y 2 - Y 3)) ω, (Y 1 - Y 3) ω) :=    hm (fun z x ↦ (x + z, x))  have hmij {i j : Fin 4} : Measurable (Y i - Y j) := (h_meas _).sub (h_meas _)  have hm0123 {i j k l : Fin 4} : Measurable (Y i - Y j - (Y k - Y l)) :=    ((h_meas _).sub (h_meas _)).sub ((h_meas _).sub (h_meas _))  rw [← condMutualInfo_of_inj_map hmij hmij hm0123 (fun z x ↦ (x, x - z)),    condMutualInfo_comm hmf hmij,    ← condMutualInfo_of_inj_map hmij hmf hm0123 (fun z x ↦ (x + z, x)),    condMutualInfo_comm hmg hmf]  · congr! 3 with ω    · simp    · rw [sub_sub, add_sub_left_comm, ← sub_sub]      simp  · exact fun _ _ _ h ↦ (Prod.ext_iff.1 h).2  exact fun _ _ _ h ↦ (Prod.ext_iff.1 h).1