\begin{lemma}[Nonnegativity]\label{multidist-nonneg}\lean{multiDist_nonneg}\uses{multidist-def}\leanok  For any such tuple, we have $D[X_{[m]}] \geq 0$.
\end{lemma}
\begin{proof}\uses{sumset-lower}  From \Cref{sumset-lower} one has
$$ \bbH[\sum_{i =1}^m \tilde X_i] \geq \bbH[\tilde X_i]$$
for each $1 \leq i \leq m$.  Averaging over $i$, we obtain the claim.
\end{proof}
/-- We have `D[X_[m]] ≥ 0`. -/
lemma multiDist_nonneg [Fintype G] {m : ℕ} {Ω : Fin m → Type*} (hΩ : ∀ i, MeasureSpace (Ω i))
    (hprob : ∀ i, IsProbabilityMeasure (ℙ : Measure (Ω i))) (X : ∀ i, (Ω i) → G)
    (hX : ∀ i, Measurable (X i)) :
    0 ≤ D[X ; hΩ] := by
  obtain ⟨A, mA, μA, Y, isProb, h_indep, hY⟩ :=
    ProbabilityTheory.independent_copies' X hX (fun i => ℙ)
  convert multiDist_nonneg_of_indep ⟨μA⟩ Y (fun i => (hY i).1) h_indep using 1
  apply multiDist_copy
  exact fun i => (hY i).2.symm