condMultiDist_nonneg

theorem condMultiDist_nonneg [Finite 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      intros      exact ENNReal.toReal_nonneg    exact multiDist_nonneg (fun i => ⟨ℙ[|Y i ⁻¹' {y i}]⟩)      (fun i => 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 [Measure.real, hi, ENNReal.toReal_zero]