multiDist_chainRule

lemma multiDist_chainRule {G H : Type*} [hG : MeasurableSpace G] [MeasurableSingletonClass G]    [AddCommGroup G] [Finite G] [hH : MeasurableSpace H]    [MeasurableSingletonClass H] [AddCommGroup H]    [Fintype H] (π : G →+ H) {m : ℕ} {Ω : Type*} (hΩ : MeasureSpace Ω)    {X : Fin m → Ω → G} (hmes : ∀ i, Measurable (X i))    (h_indep : iIndepFun X) :    D[X; fun _ ↦ hΩ] = D[X | fun i ↦ π ∘ X i; fun _ ↦ hΩ]      + D[fun i ↦ π ∘ X i; fun _ ↦ hΩ]      + I[∑ i, X i : fun ω ↦ (fun i ↦ π (X i ω)) | π ∘ (∑ i, X i)] := by  have : IsProbabilityMeasure (ℙ : Measure Ω) := h_indep.isProbabilityMeasure  set S := ∑ i, X i  set piX := fun ω ↦ (fun i ↦ π (X i ω))  set avg_HX := (∑ i, H[X i]) / m  set avg_HpiX := (∑ i, H[π ∘ X i])/m  set avg_HXpiX := (∑ i, H[X i | π ∘ X i])/m  have hSmes : Measurable S := by fun_prop  have hpiXmes : Measurable piX := by    rw [measurable_pi_iff]    intro i    exact Measurable.comp .of_discrete (hmes i)  have eq1 : I[S : piX | π ∘ S] = H[S | π ∘ S] + H[piX | π ∘ S] - H[⟨S, piX⟩ | π ∘ S] := by    rw [condMutualInfo_eq hSmes hpiXmes (Measurable.comp .of_discrete hSmes)]  have eq1a : H[S | π ∘ S] = H[S] - H[π ∘ S] :=    condEntropy_comp_self hSmes .of_discrete  have eq1b : H[piX | π ∘ S] = H[piX] - H[π ∘ S] := by    set g := fun (y : Fin m → H) ↦ ∑ i, y i    have : π ∘ S = g ∘ piX := by      ext x      simp only [comp_apply, Finset.sum_apply, _root_.map_sum, S, g, piX]    rw [this]    exact condEntropy_comp_self hpiXmes .of_discrete  have eq1c : H[⟨S, piX⟩ | π ∘ S] = H[⟨S, piX⟩] - H[π ∘ S] := by    set g := fun (x : G × (Fin m → H)) ↦ π x.1    have : π ∘ S = g ∘ ⟨S, piX⟩ := by      ext x      simp only [comp_apply, Finset.sum_apply, _root_.map_sum, S, g, piX]    rw [this]    apply condEntropy_comp_self (Measurable.prodMk hSmes hpiXmes) .of_discrete  have eq2 : H[⟨S, piX⟩] = H[piX] + H[S | piX] := chain_rule _ hSmes hpiXmes  have eq3 : D[X; fun _ ↦ hΩ] = H[S] - avg_HX := multiDist_indep _ hmes h_indep  have eq4 : D[X | fun i ↦ π ∘ X i; fun _ ↦ hΩ] = H[S | piX] - avg_HXpiX := by    dsimp [S, piX]    convert! condMultiDist_eq (S := H) hmes _ _    · exact Fintype.sum_apply _ _    · intro i      exact Measurable.comp .of_discrete (hmes i)    set g : G → G × H := fun x ↦ ⟨x, π x⟩    change iIndepFun (fun i ↦ g ∘ X i) ℙ    exact h_indep.comp _ fun _ ↦ .of_discrete  have eq5 : D[fun i ↦ π ∘ X i; fun _ ↦ hΩ] = H[π ∘ S] - avg_HpiX := by    convert multiDist_indep _ (X := fun i ↦ π ∘ X i) (by fun_prop) _    · ext _      simp only [comp_apply, Finset.sum_apply, _root_.map_sum, S]    apply iIndepFun.comp h_indep    exact fun _ ↦ .of_discrete  have eq6 : avg_HX = avg_HpiX + avg_HXpiX := by    dsimp [avg_HX, avg_HpiX, avg_HXpiX]    rw [← add_div, ← Finset.sum_add_distrib]    congr with i    rw [condEntropy_comp_self (hmes i) .of_discrete]    abel  linarith only [eq1, eq1a, eq1b, eq1c, eq2, eq3, eq4, eq5, eq6]