ProbabilityTheory.condMutualInfo_eq_zero

lemma condMutualInfo_eq_zero (hX : Measurable X) (hY : Measurable Y)    [IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] [FiniteRange Z] :    I[X : Y | Z ; μ] = 0 ↔ CondIndepFun X Y Z μ := by  rw [condIndepFun_iff, condMutualInfo_eq_integral_mutualInfo, integral_eq_zero_iff_of_nonneg]  · have : (fun x ↦ I[X : Y;μ[| Z ⁻¹' {x}]]) =ᵐ[μ.map Z] 0 ↔      ∀ᵐ z ∂(μ.map Z), I[X : Y ; μ[| Z ⁻¹' {z}]] = 0 := by rfl    rw [this]    apply Filter.eventually_congr    rw [ae_iff_of_countable]    intro z _hz    exact mutualInfo_eq_zero hX hY  · intro z    by_cases hz : μ (Z ⁻¹' {z}) = 0    · simp [cond_eq_zero_of_meas_eq_zero hz, mutualInfo_def]    · exact mutualInfo_nonneg hX hY _  · exact integrable_of_finiteSupport _