ProbabilityTheory.condMutualInfo_eq_kernel_mutualInfo

lemma condMutualInfo_eq_kernel_mutualInfo    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)    (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ] [FiniteRange Z] :    I[X : Y | Z ; μ] = Ik[condDistrib (⟨X, Y⟩) Z μ, μ.map Z] := by  rcases finiteSupport_of_finiteRange (μ := μ) (X := Z) with ⟨A, hA⟩  simp_rw [condMutualInfo_def, entropy_def, Kernel.mutualInfo, Kernel.entropy,    integral_eq_setIntegral hA, setIntegral_finset _ .finset, smul_eq_mul, mul_sub,    mul_add, Finset.sum_sub_distrib, Finset.sum_add_distrib]  congr with x  · have h := condDistrib_fst_ae_eq hX hY hZ μ    rw [Filter.EventuallyEq, ae_iff_of_countable] at h    specialize h x    by_cases hx : (μ.map Z) {x} = 0    · simp [hx, Measure.real]    rw [h hx, condDistrib_apply hX hZ]    rwa [Measure.map_apply hZ (.singleton _)] at hx  · have h := condDistrib_snd_ae_eq hX hY hZ μ    rw [Filter.EventuallyEq, ae_iff_of_countable] at h    specialize h x    by_cases hx : (μ.map Z) {x} = 0    · simp [hx, Measure.real]    rw [h hx, condDistrib_apply hY hZ]    rwa [Measure.map_apply hZ (.singleton _)] at hx  · by_cases hx : (μ.map Z) {x} = 0    · simp [hx, Measure.real]    rw [condDistrib_apply (hX.prodMk hY) hZ]    rwa [Measure.map_apply hZ (.singleton _)] at hx