condMultiDist_eq

lemma condMultiDist_eq {m : ℕ}    {Ω : Type*} [hΩ : MeasureSpace Ω]    {S : Type*} [Fintype S] [hS : MeasurableSpace S] [MeasurableSingletonClass S]    {X : Fin m → Ω → G} (hX : ∀ i, Measurable (X i))    {Y : Fin m → Ω → S} (hY : ∀ i, Measurable (Y i))    (h_indep : iIndepFun (fun i ↦ ⟨X i, Y i⟩)) :    D[X | Y ; fun _ ↦ hΩ] =      H[fun ω ↦ ∑ i, X i ω | fun ω ↦ (fun i ↦ Y i ω)] - (∑ i, H[X i | Y i])/m := by  have : IsProbabilityMeasure (ℙ : Measure Ω) := h_indep.isProbabilityMeasure  let E := fun i (yi:S) ↦ Y i ⁻¹' {yi}  let E' := fun (y : Fin m → S) ↦ ⋂ i, E i (y i)  let f := fun (y : Fin m → S) ↦ ∏ i, Measure.real ℙ (E i (y i))  have f_eq (y : Fin m → S) : f y = (ℙ (E' y)).toReal := calc     _ = (∏ i, (ℙ (E i (y i)))).toReal := by rw [ENNReal.toReal_prod]; rfl     _ = (ℙ (⋂ i, (E i (y i)))).toReal := by      congr      exact (iIndepFun.meas_iInter h_indep fun _ ↦ mes_of_comap (.singleton _)).symm  calc    _ = ∑ y, (f y) * D[X; fun i ↦ ⟨cond ℙ (E i (y i))⟩] := by rfl    _ = ∑ y, (f y) * (H[∑ i, X i; cond ℙ (E' y)] - (∑ i, H[X i; cond ℙ (E' y)]) / m) := by      congr with y      by_cases hf : f y = 0      · simp only [hf, zero_mul]      congr 1      rw [multiDist_copy (fun i ↦ ⟨cond ℙ (E i (y i))⟩)        (fun _ ↦ ⟨cond ℙ (E' y)⟩) X X        (fun i ↦ ident_of_cond_of_indep hX hY h_indep y i (prob_nonzero_of_prod_prob_nonzero hf))]      have : IsProbabilityMeasure ℙ[|E' y] := by        apply cond_isProbabilityMeasure        rw [f_eq y, ENNReal.toReal_eq_zero_iff] at hf        simpa using hf      exact multiDist_indep _ hX <|        h_indep.cond hY (prob_nonzero_of_prod_prob_nonzero hf) fun _ ↦ .singleton _    _ = ∑ y, (f y) * H[∑ i, X i; cond ℙ (E' y)] - (∑ i, ∑ y, (f y) * H[X i; cond ℙ (E' y)])/m := by      rw [Finset.sum_comm, Finset.sum_div, ← Finset.sum_sub_distrib]      congr with y      rw [← Finset.mul_sum, mul_div_assoc, ← mul_sub]    _ = _ := by      congr      · rw [condEntropy_eq_sum_fintype]        · congr with y; congr          · calc              _ = (ℙ (⋂ i, (E i (y i)))).toReal := f_eq y              _ = _ := by                congr; ext x                simp only [Set.mem_iInter, Set.mem_preimage, Set.mem_singleton_iff, E,                  Iff.symm funext_iff]          · exact Finset.sum_fn Finset.univ fun c ↦ X c          ext x          simp only [Set.mem_iInter, Set.mem_preimage, Set.mem_singleton_iff, E']          exact Iff.symm funext_iff        exact measurable_pi_lambda (fun ω i ↦ Y i ω) hY      ext i      calc        _ = ∑ y, f y * H[X i; cond ℙ (E i (y i))] := by          congr with y          by_cases hf : f y = 0          · simp only [hf, zero_mul]          congr 1; apply IdentDistrib.entropy_congr          exact (ident_of_cond_of_indep hX hY h_indep y i            (prob_nonzero_of_prod_prob_nonzero hf)).symm        _ = ∑ y ∈ Fintype.piFinset (fun _ ↦ Finset.univ), ∏ i', (ℙ (E i' (y i'))).toReal                * (if i'=i then H[X i; cond ℙ (E i (y i'))] else 1) := by          simp only [Fintype.piFinset_univ]          congr with y; rw [Finset.prod_mul_distrib]          congr; rw [Fintype.prod_ite_eq']        _ = _ := by          convert (Finset.prod_univ_sum (fun _ ↦ Finset.univ)            (fun (i' : Fin m) (s : S) ↦ (ℙ (E i' s)).toReal *              if i' = i then H[X i ; ℙ[|E i s]] else 1)).symm          calc            _ = ∏ i', if i' = i then H[X i' | Y i'] else 1 := by              simp only [Finset.prod_ite_eq', Finset.mem_univ, ↓reduceIte]            _ = _ := by              congr with i'; by_cases h : i' = i              · simp only [h, ↓reduceIte, E]                rw [condEntropy_eq_sum_fintype _ _ _ (hY i)]                rfl              · simp only [h, ↓reduceIte, mul_one, E, ← measureReal_def]                rw [sum_measureReal_preimage_singleton]                · simp                · intro i _                  exact hY _ (measurableSet_singleton i)