\begin{lemma}[Alternate form of conditional multidistance]\label{cond-multidist-alt}\lean{condMultiDist_eq}\leanok
If the $(X_i,Y_i)$ are independent,
  \begin{equation}\label{multi-def-cond}
  D[ X_{[m]} | Y_{[m]}] := \bbH[\sum_{i=1}^m X_i \big| (Y_j)_{1 \leq j \leq m} ] - \frac{1}{m} \sum_{i=1}^m \bbH[ X_i | Y_i].
    \end{equation}
\end{lemma}
\begin{proof}\uses{conditional-entropy-def, multidist-def, cond-multidist-def}\leanok
  This is routine from \Cref{conditional-entropy-def} and Definitions \ref{multidist-def} and \ref{cond-multidist-def}.
\end{proof}
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, (ℙ (E i (y i))).toReal

  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))]
      exact multiDist_indep _ _ <|
        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 := Eq.symm ENNReal.toReal_prod
              _ = (ℙ (⋂ i, (E i (y i)))).toReal := by
                congr
                exact (iIndepFun.meas_iInter h_indep fun _ ↦ mes_of_comap (.singleton _)).symm
              _ = _ := 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_eq
          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]
                exact hY i
              · simp only [h, ↓reduceIte, mul_one, E]
                exact (sum_measure_preimage_singleton' _ (hY i')).symm

/-- If `(X_i, Y_i)`, `1 ≤ i ≤ m` are independent, then `D[X_[m] | Y_[m]] = ∑_{(y_i)_{1 ≤ i ≤ m}} P(Y_i=y_i ∀ i) D[(X_i | Y_i=y_i ∀ i)_{i=1}^m]`
-/