\begin{lemma}[Conditional multidistance nonnegative]\label{cond-multidist-nonneg}\uses{cond-multidist-def}\lean{condMultiDist_nonneg}\leanok If $X_{[m]} = (X_i)_{1 \leq i \leq m}$ and $Y_{[m]} = (Y_i)_{1 \leq i \leq m}$ are tuples of random variables, then $D[ X_{[m]} | Y_{[m]} ] \geq 0$.
\end{lemma}
\begin{proof}\uses{multidist-nonneg}\leanok Clear from \Cref{multidist-nonneg} and \Cref{cond-multidist-def}, except that some care may need to be taken to deal with the $y_i$ where $p_{Y_i}$ vanish.
\end{proof}
/--Conditional multidistance is nonnegative. -/
theorem condMultiDist_nonneg [Fintype G] {m : ℕ} {Ω : Fin m → Type*} (hΩ : ∀ i, MeasureSpace (Ω i)) (hprob : ∀ i, IsProbabilityMeasure (ℙ : Measure (Ω i))) {S : Type*} [Fintype S] (X : ∀ i, (Ω i) → G) (Y : ∀ i, (Ω i) → S) (hX : ∀ i, Measurable (X i)) : 0 ≤ D[X | Y; hΩ] := by
  dsimp [condMultiDist]
  apply Finset.sum_nonneg
  intro y _
  by_cases h: ∀ i : Fin m, ℙ (Y i ⁻¹' {y i}) ≠ 0
  . apply mul_nonneg
    . apply Finset.prod_nonneg
      intro i _
      exact ENNReal.toReal_nonneg
    exact multiDist_nonneg (fun i => ⟨ℙ[|Y i ⁻¹' {y i}]⟩)
      (fun i => ProbabilityTheory.cond_isProbabilityMeasure (h i)) X hX
  simp only [ne_eq, not_forall, Decidable.not_not] at h
  obtain ⟨i, hi⟩ := h
  apply le_of_eq
  symm
  convert zero_mul ?_
  apply Finset.prod_eq_zero (Finset.mem_univ i)
  simp only [hi, ENNReal.zero_toReal]

/-- A technical lemma: can push a constant into a product at a specific term -/
private lemma Finset.prod_mul {α β:Type*} [Fintype α] [DecidableEq α] [CommMonoid β] (f:α → β) (c: β) (i₀:α) : (∏ i, f i) * c = ∏ i, (if i=i₀ then f i * c else f i) := calc
  _ = (∏ i, f i) * (∏ i, if i = i₀ then c else 1) := by
    congr
    simp only [prod_ite_eq', mem_univ, ↓reduceIte]
  _ = _ := by
    rw [← Finset.prod_mul_distrib]
    apply Finset.prod_congr rfl
    intro i _
    by_cases h : i = i₀
    . simp [h]
    simp [h]

/-- A technical lemma: a preimage of a singleton of Y i is measurable with respect to the comap of <X i, Y i> -/
private lemma mes_of_comap {Ω S G : Type*} [hG : MeasurableSpace G] [hS : MeasurableSpace S]
    {X : Ω → G} {Y : Ω → S} {s : Set S} (hs : MeasurableSet s) :
    MeasurableSet[(hG.prod hS).comap fun ω ↦ (X ω, Y ω)] (Y ⁻¹' s) :=
  ⟨.univ ×ˢ s, MeasurableSet.univ.prod hs, by ext; simp [eq_comm]⟩

/-- A technical lemma: two different ways of conditioning independent variables gives identical distributions -/
private lemma ident_of_cond_of_indep
    {G : Type*} [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Countable G]
    {m : ℕ} {Ω : Type*} [hΩ : MeasureSpace Ω]
    {S : Type*} [Fintype S] [hS : MeasurableSpace S] [MeasurableSingletonClass S]
    {X : Fin m → Ω → G} (hX : (i:Fin m) → Measurable (X i))
    {Y : Fin m → Ω → S} (hY : (i:Fin m) → Measurable (Y i))
    (h_indep : ProbabilityTheory.iIndepFun (fun i ↦ ⟨X i, Y i⟩))
    (y : Fin m → S) (i : Fin m) (hy: ∀ i, ℙ (Y i ⁻¹' {y i}) ≠ 0) :
    IdentDistrib (X i) (X i) (cond ℙ (Y i ⁻¹' {y i})) (cond ℙ (⋂ i, Y i ⁻¹' {y i})) where
  aemeasurable_fst := Measurable.aemeasurable (hX i)
  aemeasurable_snd := Measurable.aemeasurable (hX i)
  map_eq := by
    ext s hs
    rw [Measure.map_apply (hX i) hs, Measure.map_apply (hX i) hs]
    let s' : Finset (Fin m) := {i}
    let f' := fun _ : Fin m ↦ X i ⁻¹' s
    have hf' : ∀ i' ∈ s', MeasurableSet[hG.comap (X i')] (f' i') := by
      intro i' hi'
      simp only [Finset.mem_singleton.mp hi']
      exact MeasurableSet.preimage hs (comap_measurable (X i))
    have h := cond_iInter hY h_indep hf' (fun _ _ ↦ hy _) fun _ ↦ .singleton _
    simp only [Finset.mem_singleton, Set.iInter_iInter_eq_left, Finset.prod_singleton,
      s'] at h
    exact h.symm

/-- A technical lemma: if a product of probabilities is nonzero, then each probability is
individually non-zero -/
private lemma prob_nonzero_of_prod_prob_nonzero {m : ℕ}
    {Ω : Type*} [hΩ : MeasureSpace Ω]
    {S : Type*} [Fintype S] [MeasurableSpace S] [MeasurableSingletonClass S]
    {Y : Fin m → Ω → S} {y : Fin m → S} (hf : ∏ i, (ℙ (Y i ⁻¹' {y i})).toReal ≠ 0) :
    ∀ i, ℙ (Y i ⁻¹' {y i}) ≠ 0 := by
  simp [Finset.prod_ne_zero_iff, ENNReal.toReal_eq_zero_iff, forall_and] at hf
  exact hf.1

/-- If `(X_i, Y_i)`, `1 ≤ i ≤ m` are independent, then
`D[X_[m] | Y_[m]] = H[∑ i, X_i | (Y_1, ..., Y_m)] - 1/m * ∑ i, H[X_i | Y_i]`
-/