"entropy_density b M \<nu> = log b \<circ> real \<circ> RN_deriv M \<nu>"

   "entropy_density b M N = log b \<circ> real \<circ> RN_deriv M N"

   "KL_divergence b M \<nu> = integral\<^isup>L (M\<lparr>measure := \<nu>\<rparr>) (entropy_density b M \<nu>)"

   "KL_divergence b M N = integral\<^isup>L N (entropy_density b M N)"

   assumes ps: "prob_space (M\<lparr>measure := \<nu>\<rparr>)"

   assumes ac: "absolutely_continuous M N" "sets N = events"

   assumes ac: "absolutely_continuous \<nu>"

   shows "entropy_density b M N \<in> borel_measurable M"

   shows "entropy_density b M \<nu> \<in> borel_measurable M"

 proof -

 proof -

   from borel_measurable_RN_deriv[OF ac] b_gt_1 show ?thesis

   interpret \<nu>: prob_space "M\<lparr>measure := \<nu>\<rparr>" by fact

   have "measure_space (M\<lparr>measure := \<nu>\<rparr>)" by fact

   from RN_deriv[OF this ac] b_gt_1 show ?thesis

   assumes ps: "prob_space (M\<lparr>measure := \<nu>\<rparr>)"

   fixes D :: "'a \<Rightarrow> real"

   assumes ac: "absolutely_continuous \<nu>"

   assumes "prob_space (density M D)"

   assumes int: "integrable (M\<lparr> measure := \<nu> \<rparr>) (entropy_density b M \<nu>)"

   assumes D: "D \<in> borel_measurable M" "AE x in M. 0 \<le> D x"

   assumes A: "A \<in> sets M" "\<nu> A \<noteq> \<mu> A"

   assumes int: "integrable M (\<lambda>x. D x * log b (D x))"

   shows "0 < KL_divergence b M \<nu>"

   assumes A: "density M D \<noteq> M"

 proof -

   shows "0 < KL_divergence b M (density M D)"

   interpret \<nu>: prob_space "M\<lparr>measure := \<nu>\<rparr>" by fact

 proof -

   have ms: "measure_space (M\<lparr>measure := \<nu>\<rparr>)" by default

   interpret N: prob_space "density M D" by fact

   have fms: "finite_measure (M\<lparr>measure := \<nu>\<rparr>)" by unfold_locales

   note RN = RN_deriv[OF ms ac]

   obtain A where "A \<in> sets M" "emeasure (density M D) A \<noteq> emeasure M A"

     using measure_eqI[of "density M D" M] `density M D \<noteq> M` by auto

   from real_RN_deriv[OF fms ac] guess D . note D = this

   with absolutely_continuous_AE[OF ms] ac

   let ?D_set = "{x\<in>space M. D x \<noteq> 0}"

   have D\<nu>: "AE x in M\<lparr>measure := \<nu>\<rparr>. RN_deriv M \<nu> x = ereal (D x)"

   have [simp, intro]: "?D_set \<in> sets M"

     by auto

     using D by auto

   def f \<equiv> "\<lambda>x. if D x = 0 then 1 else 1 / D x"

   with D have f_borel: "f \<in> borel_measurable M"

     by (auto intro!: measurable_If)

   have "KL_divergence b M \<nu> = 1 / ln b * (\<integral> x. ln b * entropy_density b M \<nu> x \<partial>M\<lparr>measure := \<nu>\<rparr>)"

     unfolding KL_divergence_def using int b_gt_1

     by (simp add: integral_cmult)

   { fix A assume "A \<in> sets M"

     with RN D have "\<nu>.\<mu> A = (\<integral>\<^isup>+ x. ereal (D x) * indicator A x \<partial>M)"

       by (auto intro!: positive_integral_cong_AE) }

   note D_density = this

   have ln_entropy: "(\<lambda>x. ln b * entropy_density b M \<nu> x) \<in> borel_measurable M"

     using measurable_entropy_density[OF ps ac] by auto

   have "integrable (M\<lparr>measure := \<nu>\<rparr>) (\<lambda>x. ln b * entropy_density b M \<nu> x)"

     using int by auto

   moreover have "integrable (M\<lparr>measure := \<nu>\<rparr>) (\<lambda>x. ln b * entropy_density b M \<nu> x) \<longleftrightarrow>

       integrable M (\<lambda>x. D x * (ln b * entropy_density b M \<nu> x))"

     using D D_density ln_entropy

     by (intro integral_translated_density) auto

   ultimately have M_int: "integrable M (\<lambda>x. D x * (ln b * entropy_density b M \<nu> x))"

     by simp

   have "(\<integral>\<^isup>+ x. ereal (D x) \<partial>M) = \<nu> (space M)"

   have "(\<integral>\<^isup>+ x. ereal (D x) \<partial>M) = emeasure (density M D) (space M)"

     using RN D by (auto intro!: positive_integral_cong_AE)

     using D by (simp add: emeasure_density cong: positive_integral_cong)

     using \<nu>.measure_space_1 by simp

     using N.emeasure_space_1 by simp

   have "integrable M D"

   have "integrable M D" "integral\<^isup>L M D = 1"

     using D_pos D_neg D by (auto simp: integrable_def)

     using D D_pos D_neg unfolding integrable_def lebesgue_integral_def by simp_all

   have "integral\<^isup>L M D = 1"

   have "0 \<le> 1 - measure M ?D_set"

     using D_pos D_neg by (auto simp: lebesgue_integral_def)

   let ?D_set = "{x\<in>space M. D x \<noteq> 0}"

   have [simp, intro]: "?D_set \<in> sets M"

     using D by (auto intro: sets_Collect)

   have "0 \<le> 1 - \<mu>' ?D_set"

     by (simp add: \<mu>'_def)

     by (simp add: emeasure_eq_measure)

   also have "\<dots> < (\<integral> x. D x * (ln b * entropy_density b M \<nu> x) \<partial>M)"

   also have "\<dots> < (\<integral> x. D x * (ln b * log b (D x)) \<partial>M)"

     show "integrable M (\<lambda>x. D x * (ln b * entropy_density b M \<nu> x))"

     from integral_cmult(1)[OF int, of "ln b"]

       by fact

     show "integrable M (\<lambda>x. D x * (ln b * log b (D x)))" 

       by (simp add: ac_simps)

     show "\<mu> {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<noteq> 0"

     show "emeasure M {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<noteq> 0"

       assume eq_0: "\<mu> {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} = 0"

       assume eq_0: "emeasure M {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} = 0"

       then have disj: "AE x. D x = 1 \<or> D x = 0"

       then have disj: "AE x in M. D x = 1 \<or> D x = 0"

       have "\<mu> {x\<in>space M. D x = 1} = (\<integral>\<^isup>+ x. indicator {x\<in>space M. D x = 1} x \<partial>M)"

       have "emeasure M {x\<in>space M. D x = 1} = (\<integral>\<^isup>+ x. indicator {x\<in>space M. D x = 1} x \<partial>M)"

       also have "\<dots> = (\<integral>\<^isup>+ x. ereal (D x) * indicator {x\<in>space M. D x \<noteq> 0} x \<partial>M)"

       also have "\<dots> = (\<integral>\<^isup>+ x. ereal (D x) \<partial>M)"

       also have "\<dots> = \<nu> {x\<in>space M. D x \<noteq> 0}"

       finally have "AE x in M. D x = 1"

         using D(1) D_density by auto

         using D D_pos by (intro AE_I_eq_1) auto

       also have "\<dots> = \<nu> (space M)"

         using D_density D(1) by (auto intro!: positive_integral_cong simp: indicator_def)

       finally have "AE x. D x = 1"

         using D(1) \<nu>.measure_space_1 by (intro AE_I_eq_1) auto

       also have "\<dots> = \<nu> A"

       also have "\<dots> = density M D A"

         using `A \<in> sets M` D_density by simp

         using `A \<in> sets M` D by (simp add: emeasure_density)

       finally show False using `A \<in> sets M` `\<nu> A \<noteq> \<mu> A` by simp

       finally show False using `A \<in> sets M` `emeasure (density M D) A \<noteq> emeasure M A` by simp

       using D(1) by (auto intro: sets_Collect)

       using D(1) by (auto intro: sets_Collect_conj)

     show "AE t. t \<in> {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<longrightarrow>

     show "AE t in M. t \<in> {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<longrightarrow>

       D t - indicator ?D_set t \<noteq> D t * (ln b * entropy_density b M \<nu> t)"

       D t - indicator ?D_set t \<noteq> D t * (ln b * log b (D t))"

     proof (elim AE_mp, safe intro!: AE_I2)

     proof (eventually_elim, safe)

       fix t assume Dt: "t \<in> space M" "D t \<noteq> 1" "D t \<noteq> 0"

       fix t assume Dt: "t \<in> space M" "D t \<noteq> 1" "D t \<noteq> 0" "0 \<le> D t"

         and RN: "RN_deriv M \<nu> t = ereal (D t)"

         and eq: "D t - indicator ?D_set t = D t * (ln b * log b (D t))"

         and eq: "D t - indicator ?D_set t = D t * (ln b * entropy_density b M \<nu> t)"

       also have "D t * (ln b * entropy_density b M \<nu> t) = - D t * ln (1 / D t)"

       also have "D t * (ln b * log b (D t)) = - D t * ln (1 / D t)"

         using RN b_gt_1 `D t \<noteq> 0` `0 \<le> D t`

         using b_gt_1 `D t \<noteq> 0` `0 \<le> D t`

         by (simp add: entropy_density_def log_def ln_div less_le)

         by (simp add: log_def ln_div less_le)

     show "AE t. D t - indicator ?D_set t \<le> D t * (ln b * entropy_density b M \<nu> t)"

     show "AE t in M. D t - indicator ?D_set t \<le> D t * (ln b * log b (D t))"

       using D(2)

       using D(2) AE_space

     proof (elim AE_mp, intro AE_I2 impI)

     proof eventually_elim

       fix t assume "t \<in> space M" and RN: "RN_deriv M \<nu> t = ereal (D t)"

       fix t assume "t \<in> space M" "0 \<le> D t"

       show "D t - indicator ?D_set t \<le> D t * (ln b * entropy_density b M \<nu> t)"

       show "D t - indicator ?D_set t \<le> D t * (ln b * log b (D t))"

         also have "\<dots> = D t * (ln b * entropy_density b M \<nu> t)"

         also have "\<dots> = D t * (ln b * log b (D t))"

           using `0 < D t` RN b_gt_1

           using `0 < D t` b_gt_1

           by (simp_all add: log_def ln_div entropy_density_def)

           by (simp_all add: log_def ln_div)

   also have "\<dots> = (\<integral> x. ln b * entropy_density b M \<nu> x \<partial>M\<lparr>measure := \<nu>\<rparr>)"

   also have "\<dots> = (\<integral> x. ln b * (D x * log b (D x)) \<partial>M)"

     using D D_density ln_entropy

     by (simp add: ac_simps)

     by (intro integral_translated_density[symmetric]) auto

   also have "\<dots> = ln b * (\<integral> x. D x * log b (D x) \<partial>M)"

   also have "\<dots> = ln b * (\<integral> x. entropy_density b M \<nu> x \<partial>M\<lparr>measure := \<nu>\<rparr>)"

     using int by (rule integral_cmult)

     using int by (rule \<nu>.integral_cmult)

   finally show ?thesis

   finally show "0 < KL_divergence b M \<nu>"

     using b_gt_1 D by (subst KL_density) (auto simp: zero_less_mult_iff)

     using b_gt_1 by (auto simp: KL_divergence_def zero_less_mult_iff)

 qed

 qed

 lemma (in sigma_finite_measure) KL_same_eq_0: "KL_divergence b M M = 0"

 lemma (in sigma_finite_measure) KL_eq_0:

 proof -

   assumes eq: "\<forall>A\<in>sets M. \<nu> A = measure M A"

   have "AE x in M. 1 = RN_deriv M M x"

   shows "KL_divergence b M \<nu> = 0"

 proof -

   have "AE x. 1 = RN_deriv M \<nu> x"

     show "measure_space (M\<lparr>measure := \<nu>\<rparr>)"

     show "(\<lambda>x. 1) \<in> borel_measurable M" "AE x in M. 0 \<le> (1 :: ereal)" by auto

       using eq by (intro measure_space_cong) auto

     show "density M (\<lambda>x. 1) = M"

     show "absolutely_continuous \<nu>"

       apply (auto intro!: measure_eqI emeasure_density)

       unfolding absolutely_continuous_def using eq by auto

       apply (subst emeasure_density)

     show "(\<lambda>x. 1) \<in> borel_measurable M" "AE x. 0 \<le> (1 :: ereal)" by auto

       apply auto

     fix A assume "A \<in> sets M"

       done

     with eq show "\<nu> A = \<integral>\<^isup>+ x. 1 * indicator A x \<partial>M" by simp

   then have "AE x. log b (real (RN_deriv M \<nu> x)) = 0"

   then have "AE x in M. log b (real (RN_deriv M M x)) = 0"

   have "integral\<^isup>L M (entropy_density b M \<nu>) = 0"

   have "integral\<^isup>L M (entropy_density b M M) = 0"

   with eq show "KL_divergence b M \<nu> = 0"

   then show "KL_divergence b M M = 0"

     by (subst integral_cong_measure) auto

     by auto

 qed

 qed

 lemma (in information_space) KL_eq_0_imp:

 lemma (in information_space) KL_eq_0_iff_eq:

   assumes ps: "prob_space (M\<lparr>measure := \<nu>\<rparr>)"

   fixes D :: "'a \<Rightarrow> real"

   assumes ac: "absolutely_continuous \<nu>"

   assumes "prob_space (density M D)"

   assumes int: "integrable (M\<lparr> measure := \<nu> \<rparr>) (entropy_density b M \<nu>)"

   assumes D: "D \<in> borel_measurable M" "AE x in M. 0 \<le> D x"

   assumes KL: "KL_divergence b M \<nu> = 0"

   assumes int: "integrable M (\<lambda>x. D x * log b (D x))"

   shows "\<forall>A\<in>sets M. \<nu> A = \<mu> A"

   shows "KL_divergence b M (density M D) = 0 \<longleftrightarrow> density M D = M"

   by (metis less_imp_neq KL_gt_0 assms)

   using KL_same_eq_0[of b] KL_gt_0[OF assms]

   by (auto simp: less_le)

 lemma (in information_space) KL_ge_0:

   assumes ps: "prob_space (M\<lparr>measure := \<nu>\<rparr>)"

 lemma (in information_space) KL_eq_0_iff_eq_ac:

   assumes ac: "absolutely_continuous \<nu>"

   fixes D :: "'a \<Rightarrow> real"

   assumes int: "integrable (M\<lparr> measure := \<nu> \<rparr>) (entropy_density b M \<nu>)"

   assumes "prob_space N"

   shows "0 \<le> KL_divergence b M \<nu>"

   assumes ac: "absolutely_continuous M N" "sets N = sets M"

   using KL_eq_0 KL_gt_0[OF ps ac int]

   assumes int: "integrable N (entropy_density b M N)"

   by (cases "\<forall>A\<in>sets M. \<nu> A = measure M A") (auto simp: le_less)

   shows "KL_divergence b M N = 0 \<longleftrightarrow> N = M"

 proof -

   interpret N: prob_space N by fact

 lemma (in sigma_finite_measure) KL_divergence_vimage:

   have "finite_measure N" by unfold_locales

   assumes T: "T \<in> measure_preserving M M'"

   from real_RN_deriv[OF this ac] guess D . note D = this

     and T': "T' \<in> measure_preserving (M'\<lparr> measure := \<nu>' \<rparr>) (M\<lparr> measure := \<nu> \<rparr>)"

     and inv: "\<And>x. x \<in> space M \<Longrightarrow> T' (T x) = x"

   have "N = density M (RN_deriv M N)"

     and inv': "\<And>x. x \<in> space M' \<Longrightarrow> T (T' x) = x"

     using ac by (rule density_RN_deriv[symmetric])

   and \<nu>': "measure_space (M'\<lparr>measure := \<nu>'\<rparr>)" "measure_space.absolutely_continuous M' \<nu>'"

   also have "\<dots> = density M D"

   and "1 < b"

     using borel_measurable_RN_deriv[OF ac] D by (auto intro!: density_cong)

   shows "KL_divergence b M' \<nu>' = KL_divergence b M \<nu>"

   finally have N: "N = density M D" .

 proof -

   interpret \<nu>': measure_space "M'\<lparr>measure := \<nu>'\<rparr>" by fact

   from absolutely_continuous_AE[OF ac(2,1) D(2)] D b_gt_1 ac measurable_entropy_density

   have M: "measure_space (M\<lparr> measure := \<nu>\<rparr>)"

   have "integrable N (\<lambda>x. log b (D x))"

     by (rule \<nu>'.measure_space_vimage[OF _ T'], simp) default

     by (intro integrable_cong_AE[THEN iffD2, OF _ _ _ int])

   have "sigma_algebra (M'\<lparr> measure := \<nu>'\<rparr>)" by default

        (auto simp: N entropy_density_def)

   then have saM': "sigma_algebra M'" by simp

   with D b_gt_1 have "integrable M (\<lambda>x. D x * log b (D x))"

   then interpret M': measure_space M' by (rule measure_space_vimage) fact

     by (subst integral_density(2)[symmetric]) (auto simp: N[symmetric] comp_def)

   have ac: "absolutely_continuous \<nu>" unfolding absolutely_continuous_def

   with `prob_space N` D show ?thesis

   proof safe

     unfolding N

     fix N assume N: "N \<in> sets M" and N_0: "\<mu> N = 0"

     by (intro KL_eq_0_iff_eq) auto

     then have N': "T' -` N \<inter> space M' \<in> sets M'"

 qed

       using T' by (auto simp: measurable_def measure_preserving_def)

     have "T -` (T' -` N \<inter> space M') \<inter> space M = N"

 lemma (in information_space) KL_nonneg:

       using inv T N sets_into_space[OF N] by (auto simp: measurable_def measure_preserving_def)

   assumes "prob_space (density M D)"

     then have "measure M' (T' -` N \<inter> space M') = 0"

   assumes D: "D \<in> borel_measurable M" "AE x in M. 0 \<le> D x"

       using measure_preservingD[OF T N'] N_0 by auto

   assumes int: "integrable M (\<lambda>x. D x * log b (D x))"

     with \<nu>'(2) N' show "\<nu> N = 0" using measure_preservingD[OF T', of N] N

   shows "0 \<le> KL_divergence b M (density M D)"

       unfolding M'.absolutely_continuous_def measurable_def by auto

   using KL_gt_0[OF assms] by (cases "density M D = M") (auto simp: KL_same_eq_0)

 lemma (in sigma_finite_measure) KL_density_density_nonneg:

   fixes f g :: "'a \<Rightarrow> real"

   assumes "1 < b"

   assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "prob_space (density M f)"

   assumes g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x" "prob_space (density M g)"

   assumes ac: "AE x in M. f x = 0 \<longrightarrow> g x = 0"

   assumes int: "integrable M (\<lambda>x. g x * log b (g x / f x))"

   shows "0 \<le> KL_divergence b (density M f) (density M g)"

 proof -

   interpret Mf: prob_space "density M f" by fact

   interpret Mf: information_space "density M f" b by default fact

   have eq: "density (density M f) (\<lambda>x. g x / f x) = density M g" (is "?DD = _")

     using f g ac by (subst density_density_divide) simp_all

   have "0 \<le> KL_divergence b (density M f) (density (density M f) (\<lambda>x. g x / f x))"

   proof (rule Mf.KL_nonneg)

     show "prob_space ?DD" unfolding eq by fact

     from f g show "(\<lambda>x. g x / f x) \<in> borel_measurable (density M f)"

       by auto

     show "AE x in density M f. 0 \<le> g x / f x"

       using f g by (auto simp: AE_density divide_nonneg_nonneg)

     show "integrable (density M f) (\<lambda>x. g x / f x * log b (g x / f x))"

       using `1 < b` f g ac

       by (subst integral_density)

          (auto intro!: integrable_cong_AE[THEN iffD2, OF _ _ _ int] measurable_If)

   also have "\<dots> = KL_divergence b (density M f) (density M g)"

   have sa: "sigma_algebra (M\<lparr>measure := \<nu>\<rparr>)" by simp default

     using f g ac by (subst density_density_divide) simp_all

   have AE: "AE x. RN_deriv M' \<nu>' (T x) = RN_deriv M \<nu> x"

     by (rule RN_deriv_vimage[OF T T' inv \<nu>'])

   show ?thesis

     unfolding KL_divergence_def entropy_density_def comp_def

   proof (subst \<nu>'.integral_vimage[OF sa T'])

     show "(\<lambda>x. log b (real (RN_deriv M \<nu> x))) \<in> borel_measurable (M\<lparr>measure := \<nu>\<rparr>)"

       by (auto intro!: RN_deriv[OF M ac] borel_measurable_log[OF _ `1 < b`])

     have "(\<integral> x. log b (real (RN_deriv M' \<nu>' x)) \<partial>M'\<lparr>measure := \<nu>'\<rparr>) =

       (\<integral> x. log b (real (RN_deriv M' \<nu>' (T (T' x)))) \<partial>M'\<lparr>measure := \<nu>'\<rparr>)" (is "?l = _")

       using inv' by (auto intro!: \<nu>'.integral_cong)

     also have "\<dots> = (\<integral> x. log b (real (RN_deriv M \<nu> (T' x))) \<partial>M'\<lparr>measure := \<nu>'\<rparr>)" (is "_ = ?r")

       using M ac AE

       by (intro \<nu>'.integral_cong_AE \<nu>'.almost_everywhere_vimage[OF sa T'] absolutely_continuous_AE[OF M])

          (auto elim!: AE_mp)

     finally show "?l = ?r" .

   qed

 qed

 lemma (in sigma_finite_measure) KL_divergence_cong:

   assumes "measure_space (M\<lparr>measure := \<nu>\<rparr>)" (is "measure_space ?\<nu>")

   assumes [simp]: "sets N = sets M" "space N = space M"

     "\<And>A. A \<in> sets M \<Longrightarrow> measure N A = \<mu> A"

     "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = \<nu>' A"

   shows "KL_divergence b M \<nu> = KL_divergence b N \<nu>'"

 proof -

   interpret \<nu>: measure_space ?\<nu> by fact

   have "KL_divergence b M \<nu> = \<integral>x. log b (real (RN_deriv N \<nu>' x)) \<partial>?\<nu>"

     by (simp cong: RN_deriv_cong \<nu>.integral_cong add: KL_divergence_def entropy_density_def)

   also have "\<dots> = KL_divergence b N \<nu>'"

     by (auto intro!: \<nu>.integral_cong_measure[symmetric] simp: KL_divergence_def entropy_density_def comp_def)

     KL_divergence b (S\<lparr>measure := ereal\<circ>distribution X\<rparr> \<Otimes>\<^isub>M T\<lparr>measure := ereal\<circ>distribution Y\<rparr>)

     KL_divergence b (distr M S X \<Otimes>\<^isub>M distr M T Y) (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)))"

       (ereal\<circ>joint_distribution X Y)"

 lemma (in information_space) mutual_information_indep_vars:

 lemma (in information_space)

   defines "P \<equiv> S\<lparr>measure := ereal\<circ>distribution X\<rparr> \<Otimes>\<^isub>M T\<lparr>measure := ereal\<circ>distribution Y\<rparr>"

   defines "P \<equiv> distr M S X \<Otimes>\<^isub>M distr M T Y"

   defines "Q \<equiv> distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"

       measure_space.absolutely_continuous P (ereal\<circ>joint_distribution X Y) \<and>

       absolutely_continuous P Q \<and> integrable Q (entropy_density b P Q) \<and>

       integrable (P\<lparr>measure := (ereal\<circ>joint_distribution X Y)\<rparr>)

       mutual_information b S T X Y = 0)"

         (entropy_density b P (ereal\<circ>joint_distribution X Y)) \<and>

   unfolding indep_var_distribution_eq

      mutual_information b S T X Y = 0)"

   assume indep: "indep_var S X T Y"

   assume rv: "random_variable S X" "random_variable T Y"

   then have "random_variable S X" "random_variable T Y"

     by (blast dest: indep_var_rv1 indep_var_rv2)+

   interpret X: prob_space "distr M S X"

   then show "sigma_algebra S" "X \<in> measurable M S" "sigma_algebra T" "Y \<in> measurable M T"

     by (rule prob_space_distr) fact

     by blast+

   interpret Y: prob_space "distr M T Y"

     by (rule prob_space_distr) fact

   interpret X: prob_space "S\<lparr>measure := ereal\<circ>distribution X\<rparr>"

   interpret XY: pair_prob_space "distr M S X" "distr M T Y" by default

     by (rule distribution_prob_space) fact

   interpret P: information_space P b unfolding P_def by default (rule b_gt_1)

   interpret Y: prob_space "T\<lparr>measure := ereal\<circ>distribution Y\<rparr>"

     by (rule distribution_prob_space) fact

   interpret Q: prob_space Q unfolding Q_def

   interpret XY: pair_prob_space "S\<lparr>measure := ereal\<circ>distribution X\<rparr>" "T\<lparr>measure := ereal\<circ>distribution Y\<rparr>" by default

     by (rule prob_space_distr) (simp add: comp_def measurable_pair_iff rv)

   interpret XY: information_space XY.P b by default (rule b_gt_1)

   { assume "distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"

   let ?J = "XY.P\<lparr> measure := (ereal\<circ>joint_distribution X Y) \<rparr>"

     then have [simp]: "Q = P"  unfolding Q_def P_def by simp

   { fix A assume "A \<in> sets XY.P"

     then have "ereal (joint_distribution X Y A) = XY.\<mu> A"

     show ac: "absolutely_continuous P Q" by (simp add: absolutely_continuous_def)

       using indep_var_distributionD[OF indep]

     then have ed: "entropy_density b P Q \<in> borel_measurable P"

       by (simp add: XY.P.finite_measure_eq) }

       by (rule P.measurable_entropy_density) simp

   note j_eq = this

     have "AE x in P. 1 = RN_deriv P Q x"

   interpret J: prob_space ?J

     proof (rule P.RN_deriv_unique)

     using j_eq by (intro XY.prob_space_cong) auto

       show "density P (\<lambda>x. 1) = Q"

         unfolding `Q = P` by (intro measure_eqI) (auto simp: emeasure_density)

   have ac: "XY.absolutely_continuous (ereal\<circ>joint_distribution X Y)"

     qed auto

     by (simp add: XY.absolutely_continuous_def j_eq)

     then have ae_0: "AE x in P. entropy_density b P Q x = 0"

   then show "measure_space.absolutely_continuous P (ereal\<circ>joint_distribution X Y)"

       by eventually_elim (auto simp: entropy_density_def)

     unfolding P_def .

     then have "integrable P (entropy_density b P Q) \<longleftrightarrow> integrable Q (\<lambda>x. 0)"

       using ed unfolding `Q = P` by (intro integrable_cong_AE) auto

   have ed: "entropy_density b XY.P (ereal\<circ>joint_distribution X Y) \<in> borel_measurable XY.P"

     then show "integrable Q (entropy_density b P Q)" by simp

     by (rule XY.measurable_entropy_density) (default | fact)+

     show "mutual_information b S T X Y = 0"

   have "AE x in XY.P. 1 = RN_deriv XY.P (ereal\<circ>joint_distribution X Y) x"

       unfolding mutual_information_def KL_divergence_def P_def[symmetric] Q_def[symmetric] `Q = P`

   proof (rule XY.RN_deriv_unique[OF _ ac])

       using ae_0 by (simp cong: integral_cong_AE) }

     show "measure_space ?J" by default

     fix A assume "A \<in> sets XY.P"

   { assume ac: "absolutely_continuous P Q"

     then show "(ereal\<circ>joint_distribution X Y) A = (\<integral>\<^isup>+ x. 1 * indicator A x \<partial>XY.P)"

     assume int: "integrable Q (entropy_density b P Q)"

       by (simp add: j_eq)

     assume I_eq_0: "mutual_information b S T X Y = 0"

   qed (insert XY.measurable_const[of 1 borel], auto)

   then have ae_XY: "AE x in XY.P. entropy_density b XY.P (ereal\<circ>joint_distribution X Y) x = 0"

     have eq: "Q = P"

     by (elim XY.AE_mp) (simp add: entropy_density_def)

     proof (rule P.KL_eq_0_iff_eq_ac[THEN iffD1])

   have ae_J: "AE x in ?J. entropy_density b XY.P (ereal\<circ>joint_distribution X Y) x = 0"

       show "prob_space Q" by unfold_locales

   proof (rule XY.absolutely_continuous_AE)

       show "absolutely_continuous P Q" by fact

     show "measure_space ?J" by default

       show "integrable Q (entropy_density b P Q)" by fact

     show "XY.absolutely_continuous (measure ?J)"

       show "sets Q = sets P" by (simp add: P_def Q_def sets_pair_measure)

       using ac by simp

       show "KL_divergence b P Q = 0"

   qed (insert ae_XY, simp_all)

         using I_eq_0 unfolding mutual_information_def by (simp add: P_def Q_def)

   then show "integrable (P\<lparr>measure := (ereal\<circ>joint_distribution X Y)\<rparr>)

         (entropy_density b P (ereal\<circ>joint_distribution X Y))"

     unfolding P_def

     using ed XY.measurable_const[of 0 borel]

     by (subst J.integrable_cong_AE) auto

   show "mutual_information b S T X Y = 0"

     unfolding mutual_information_def KL_divergence_def P_def

     by (subst J.integral_cong_AE[OF ae_J]) simp

 next

   assume "sigma_algebra S" "X \<in> measurable M S" "sigma_algebra T" "Y \<in> measurable M T"

   then have rvs: "random_variable S X" "random_variable T Y" by blast+

   interpret X: prob_space "S\<lparr>measure := ereal\<circ>distribution X\<rparr>"

     by (rule distribution_prob_space) fact

   interpret Y: prob_space "T\<lparr>measure := ereal\<circ>distribution Y\<rparr>"

     by (rule distribution_prob_space) fact

   interpret XY: pair_prob_space "S\<lparr>measure := ereal\<circ>distribution X\<rparr>" "T\<lparr>measure := ereal\<circ>distribution Y\<rparr>" by default

   interpret XY: information_space XY.P b by default (rule b_gt_1)

   let ?J = "XY.P\<lparr> measure := (ereal\<circ>joint_distribution X Y) \<rparr>"

   interpret J: prob_space ?J

     using rvs by (intro joint_distribution_prob_space) auto

   assume ac: "measure_space.absolutely_continuous P (ereal\<circ>joint_distribution X Y)"

   assume int: "integrable (P\<lparr>measure := (ereal\<circ>joint_distribution X Y)\<rparr>)

         (entropy_density b P (ereal\<circ>joint_distribution X Y))"

   assume I_eq_0: "mutual_information b S T X Y = 0"

   have eq: "\<forall>A\<in>sets XY.P. (ereal \<circ> joint_distribution X Y) A = XY.\<mu> A"

   proof (rule XY.KL_eq_0_imp)

     show "prob_space ?J" by unfold_locales

     show "XY.absolutely_continuous (ereal\<circ>joint_distribution X Y)"

       using ac by (simp add: P_def)

     show "integrable ?J (entropy_density b XY.P (ereal\<circ>joint_distribution X Y))"

       using int by (simp add: P_def)

     show "KL_divergence b XY.P (ereal\<circ>joint_distribution X Y) = 0"

       using I_eq_0 unfolding mutual_information_def by (simp add: P_def)

   qed

   { fix S X assume "sigma_algebra S"

     interpret S: sigma_algebra S by fact

     have "Int_stable \<lparr>space = space M, sets = {X -` A \<inter> space M |A. A \<in> sets S}\<rparr>"

     proof (safe intro!: Int_stableI)

       fix A B assume "A \<in> sets S" "B \<in> sets S"

       then show "\<exists>C. (X -` A \<inter> space M) \<inter> (X -` B \<inter> space M) = (X -` C \<inter> space M) \<and> C \<in> sets S"

         by (intro exI[of _ "A \<inter> B"]) auto

     qed }

   note Int_stable = this

   show "indep_var S X T Y" unfolding indep_var_eq

   proof (intro conjI indep_set_sigma_sets Int_stable)

     show "indep_set {X -` A \<inter> space M |A. A \<in> sets S} {Y -` A \<inter> space M |A. A \<in> sets T}"

     proof (safe intro!: indep_setI)

       { fix A assume "A \<in> sets S" then show "X -` A \<inter> space M \<in> sets M"

         using `X \<in> measurable M S` by (auto intro: measurable_sets) }

       { fix A assume "A \<in> sets T" then show "Y -` A \<inter> space M \<in> sets M"

         using `Y \<in> measurable M T` by (auto intro: measurable_sets) }

     next

       fix A B assume ab: "A \<in> sets S" "B \<in> sets T"

       have "ereal (prob ((X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M))) =

         ereal (joint_distribution X Y (A \<times> B))"

         unfolding distribution_def

         by (intro arg_cong[where f="\<lambda>C. ereal (prob C)"]) auto

       also have "\<dots> = XY.\<mu> (A \<times> B)"

         using ab eq by (auto simp: XY.finite_measure_eq)

       also have "\<dots> = ereal (distribution X A) * ereal (distribution Y B)"

         using ab by (simp add: XY.pair_measure_times)

       finally show "prob ((X -` A \<inter> space M) \<inter> (Y -` B \<inter> space M)) =

         prob (X -` A \<inter> space M) * prob (Y -` B \<inter> space M)"

         unfolding distribution_def by simp

   qed fact+

     then show "distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"

 qed

       unfolding P_def Q_def .. }

 qed

 lemma (in information_space) mutual_information_commute_generic:

   assumes X: "random_variable S X" and Y: "random_variable T Y"

   assumes ac: "measure_space.absolutely_continuous

     (S\<lparr>measure := ereal\<circ>distribution X\<rparr> \<Otimes>\<^isub>M T\<lparr>measure := ereal\<circ>distribution Y\<rparr>) (ereal\<circ>joint_distribution X Y)"

   shows "mutual_information b S T X Y = mutual_information b T S Y X"

 proof -

   let ?S = "S\<lparr>measure := ereal\<circ>distribution X\<rparr>" and ?T = "T\<lparr>measure := ereal\<circ>distribution Y\<rparr>"

   interpret S: prob_space ?S using X by (rule distribution_prob_space)

   interpret T: prob_space ?T using Y by (rule distribution_prob_space)

   interpret P: pair_prob_space ?S ?T ..

   interpret Q: pair_prob_space ?T ?S ..

   show ?thesis

     unfolding mutual_information_def

   proof (intro Q.KL_divergence_vimage[OF Q.measure_preserving_swap _ _ _ _ ac b_gt_1])

     show "(\<lambda>(x,y). (y,x)) \<in> measure_preserving

       (P.P \<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>) (Q.P \<lparr> measure := ereal\<circ>joint_distribution Y X\<rparr>)"

       using X Y unfolding measurable_def

       unfolding measure_preserving_def using P.pair_sigma_algebra_swap_measurable

       by (auto simp add: space_pair_measure distribution_def intro!: arg_cong[where f=\<mu>'])

     have "prob_space (P.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)"

       using X Y by (auto intro!: distribution_prob_space random_variable_pairI)

     then show "measure_space (P.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)"

       unfolding prob_space_def finite_measure_def sigma_finite_measure_def by simp

   qed auto

 qed

 definition (in prob_space)

   "entropy b s X = mutual_information b s s X X"

   "\<I>(X ; Y) \<equiv> mutual_information b

   "\<I>(X ; Y) \<equiv> mutual_information b (count_space (X`space M)) (count_space (Y`space M)) X Y"

     \<lparr> space = X`space M, sets = Pow (X`space M), measure = ereal\<circ>distribution X \<rparr>

     \<lparr> space = Y`space M, sets = Pow (Y`space M), measure = ereal\<circ>distribution Y \<rparr> X Y"

 lemma (in information_space)

   fixes Pxy :: "'b \<times> 'c \<Rightarrow> real" and Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"

 lemma (in prob_space) finite_variables_absolutely_continuous:

   assumes "sigma_finite_measure S" "sigma_finite_measure T"

   assumes X: "finite_random_variable S X" and Y: "finite_random_variable T Y"

   assumes Px: "distributed M S X Px" and Py: "distributed M T Y Py"

   shows "measure_space.absolutely_continuous

   assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"

     (S\<lparr>measure := ereal\<circ>distribution X\<rparr> \<Otimes>\<^isub>M T\<lparr>measure := ereal\<circ>distribution Y\<rparr>)

   defines "f \<equiv> \<lambda>x. Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x)))"

     (ereal\<circ>joint_distribution X Y)"

   shows mutual_information_distr: "mutual_information b S T X Y = integral\<^isup>L (S \<Otimes>\<^isub>M T) f" (is "?M = ?R")

 proof -

     and mutual_information_nonneg: "integrable (S \<Otimes>\<^isub>M T) f \<Longrightarrow> 0 \<le> mutual_information b S T X Y"

   interpret X: finite_prob_space "S\<lparr>measure := ereal\<circ>distribution X\<rparr>"

 proof -

     using X by (rule distribution_finite_prob_space)

   have X: "random_variable S X"

   interpret Y: finite_prob_space "T\<lparr>measure := ereal\<circ>distribution Y\<rparr>"

     using Px by (auto simp: distributed_def)

     using Y by (rule distribution_finite_prob_space)

   have Y: "random_variable T Y"

   interpret XY: pair_finite_prob_space

     using Py by (auto simp: distributed_def)

     "S\<lparr>measure := ereal\<circ>distribution X\<rparr>" "T\<lparr> measure := ereal\<circ>distribution Y\<rparr>" by default

   interpret S: sigma_finite_measure S by fact

   interpret P: finite_prob_space "XY.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>"

   interpret T: sigma_finite_measure T by fact

     using assms by (auto intro!: joint_distribution_finite_prob_space)

   interpret ST: pair_sigma_finite S T ..

   note rv = assms[THEN finite_random_variableD]

   interpret X: prob_space "distr M S X" using X by (rule prob_space_distr)

   show "XY.absolutely_continuous (ereal\<circ>joint_distribution X Y)"

   interpret Y: prob_space "distr M T Y" using Y by (rule prob_space_distr)

   proof (rule XY.absolutely_continuousI)

   interpret XY: pair_prob_space "distr M S X" "distr M T Y" ..

     show "finite_measure_space (XY.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)" by unfold_locales

   let ?P = "S \<Otimes>\<^isub>M T"

     fix x assume "x \<in> space XY.P" and "XY.\<mu> {x} = 0"

   let ?D = "distr M ?P (\<lambda>x. (X x, Y x))"

     then obtain a b where "x = (a, b)"

       and "distribution X {a} = 0 \<or> distribution Y {b} = 0"

   { fix A assume "A \<in> sets S"

       by (cases x) (auto simp: space_pair_measure)

     with X Y have "emeasure (distr M S X) A = emeasure ?D (A \<times> space T)"

     with finite_distribution_order(5,6)[OF X Y]

       by (auto simp: emeasure_distr measurable_Pair measurable_space

     show "(ereal \<circ> joint_distribution X Y) {x} = 0" by auto

                intro!: arg_cong[where f="emeasure M"]) }

   note marginal_eq1 = this

   { fix A assume "A \<in> sets T"

     with X Y have "emeasure (distr M T Y) A = emeasure ?D (space S \<times> A)"

       by (auto simp: emeasure_distr measurable_Pair measurable_space

                intro!: arg_cong[where f="emeasure M"]) }

   note marginal_eq2 = this

   have eq: "(\<lambda>x. ereal (Px (fst x) * Py (snd x))) = (\<lambda>(x, y). ereal (Px x) * ereal (Py y))"

     by auto

   have distr_eq: "distr M S X \<Otimes>\<^isub>M distr M T Y = density ?P (\<lambda>x. ereal (Px (fst x) * Py (snd x)))"

     unfolding Px(1)[THEN distributed_distr_eq_density] Py(1)[THEN distributed_distr_eq_density] eq

   proof (subst pair_measure_density)

     show "(\<lambda>x. ereal (Px x)) \<in> borel_measurable S" "(\<lambda>y. ereal (Py y)) \<in> borel_measurable T"

       "AE x in S. 0 \<le> ereal (Px x)" "AE y in T. 0 \<le> ereal (Py y)"

       using Px Py by (auto simp: distributed_def)

     show "sigma_finite_measure (density S Px)" unfolding Px(1)[THEN distributed_distr_eq_density, symmetric] ..

     show "sigma_finite_measure (density T Py)" unfolding Py(1)[THEN distributed_distr_eq_density, symmetric] ..

   qed (fact | simp)+

   have M: "?M = KL_divergence b (density ?P (\<lambda>x. ereal (Px (fst x) * Py (snd x)))) (density ?P (\<lambda>x. ereal (Pxy x)))"

     unfolding mutual_information_def distr_eq Pxy(1)[THEN distributed_distr_eq_density] ..

   from Px Py have f: "(\<lambda>x. Px (fst x) * Py (snd x)) \<in> borel_measurable ?P"

     by (intro borel_measurable_times) (auto intro: distributed_real_measurable measurable_fst'' measurable_snd'')

   have PxPy_nonneg: "AE x in ?P. 0 \<le> Px (fst x) * Py (snd x)"

   proof (rule ST.AE_pair_measure)

     show "{x \<in> space ?P. 0 \<le> Px (fst x) * Py (snd x)} \<in> sets ?P"

       using f by auto

     show "AE x in S. AE y in T. 0 \<le> Px (fst (x, y)) * Py (snd (x, y))"

       using Px Py by (auto simp: zero_le_mult_iff dest!: distributed_real_AE)

   assumes MX: "finite_random_variable MX X"

   fixes Pxy :: "'b \<times> 'c \<Rightarrow> real" and Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"

   assumes MY: "finite_random_variable MY Y"

   assumes "sigma_finite_measure S" "sigma_finite_measure T"

   shows mutual_information_generic_eq:

   assumes Px: "distributed M S X Px" and Py: "distributed M T Y Py"

     "mutual_information b MX MY X Y = (\<Sum> (x,y) \<in> space MX \<times> space MY.

   assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"

       joint_distribution X Y {(x,y)} *

   assumes ae: "AE x in S. AE y in T. Pxy (x, y) = Px x * Py y"

       log b (joint_distribution X Y {(x,y)} /

   shows mutual_information_eq_0: "mutual_information b S T X Y = 0"

       (distribution X {x} * distribution Y {y})))"

 proof -

     (is ?sum)

   interpret S: sigma_finite_measure S by fact

   and mutual_information_positive_generic:

   interpret T: sigma_finite_measure T by fact

      "0 \<le> mutual_information b MX MY X Y" (is ?positive)

   interpret ST: pair_sigma_finite S T ..

 proof -

   interpret X: finite_prob_space "MX\<lparr>measure := ereal\<circ>distribution X\<rparr>"

   have "AE x in S \<Otimes>\<^isub>M T. Px (fst x) = 0 \<longrightarrow> Pxy x = 0"

     using MX by (rule distribution_finite_prob_space)

     by (rule subdensity_real[OF measurable_fst Pxy Px]) auto

   interpret Y: finite_prob_space "MY\<lparr>measure := ereal\<circ>distribution Y\<rparr>"

   moreover

     using MY by (rule distribution_finite_prob_space)

   have "AE x in S \<Otimes>\<^isub>M T. Py (snd x) = 0 \<longrightarrow> Pxy x = 0"

   interpret XY: pair_finite_prob_space "MX\<lparr>measure := ereal\<circ>distribution X\<rparr>" "MY\<lparr>measure := ereal\<circ>distribution Y\<rparr>" by default

     by (rule subdensity_real[OF measurable_snd Pxy Py]) auto

   interpret P: finite_prob_space "XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>"

   moreover 

     using assms by (auto intro!: joint_distribution_finite_prob_space)

   have "AE x in S \<Otimes>\<^isub>M T. Pxy x = Px (fst x) * Py (snd x)"

     using distributed_real_measurable[OF Px] distributed_real_measurable[OF Py] distributed_real_measurable[OF Pxy]

   have P_ms: "finite_measure_space (XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>)" by unfold_locales

     by (intro ST.AE_pair_measure) (auto simp: ae intro!: measurable_snd'' measurable_fst'')

   have P_ps: "finite_prob_space (XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>)" by unfold_locales

   ultimately have "AE x in S \<Otimes>\<^isub>M T. Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x))) = 0"

     by eventually_elim simp

   show ?sum

   then have "(\<integral>x. Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x))) \<partial>(S \<Otimes>\<^isub>M T)) = (\<integral>x. 0 \<partial>(S \<Otimes>\<^isub>M T))"

     unfolding Let_def mutual_information_def

     by (rule integral_cong_AE)

     by (subst XY.KL_divergence_eq_finite[OF P_ms finite_variables_absolutely_continuous[OF MX MY]])

   then show ?thesis

        (auto simp add: space_pair_measure setsum_cartesian_product')

     by (subst mutual_information_distr[OF assms(1-5)]) simp

 qed

   show ?positive

     using XY.KL_divergence_positive_finite[OF P_ps finite_variables_absolutely_continuous[OF MX MY] b_gt_1]

 lemma (in information_space) mutual_information_simple_distributed:

     unfolding mutual_information_def .

   assumes X: "simple_distributed M X Px" and Y: "simple_distributed M Y Py"

 qed

   assumes XY: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"

   shows "\<I>(X ; Y) = (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x))`space M. Pxy (x, y) * log b (Pxy (x, y) / (Px x * Py y)))"

 lemma (in information_space) mutual_information_commute:

 proof (subst mutual_information_distr[OF _ _ simple_distributed[OF X] simple_distributed[OF Y] simple_distributed_joint[OF XY]])

   assumes X: "finite_random_variable S X" and Y: "finite_random_variable T Y"

   note fin = simple_distributed_joint_finite[OF XY, simp]

   shows "mutual_information b S T X Y = mutual_information b T S Y X"

   show "sigma_finite_measure (count_space (X ` space M))"

   unfolding mutual_information_generic_eq[OF X Y] mutual_information_generic_eq[OF Y X]

     by (simp add: sigma_finite_measure_count_space_finite)

   unfolding joint_distribution_commute_singleton[of X Y]

   show "sigma_finite_measure (count_space (Y ` space M))"

   by (auto simp add: ac_simps intro!: setsum_reindex_cong[OF swap_inj_on])

     by (simp add: sigma_finite_measure_count_space_finite)

   let ?Pxy = "\<lambda>x. (if x \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy x else 0)"

 lemma (in information_space) mutual_information_commute_simple:

   let ?f = "\<lambda>x. ?Pxy x * log b (?Pxy x / (Px (fst x) * Py (snd x)))"

   assumes X: "simple_function M X" and Y: "simple_function M Y"

   have "\<And>x. ?f x = (if x \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x))) else 0)"

   shows "\<I>(X;Y) = \<I>(Y;X)"

     by auto

   by (intro mutual_information_commute X Y simple_function_imp_finite_random_variable)

   with fin show "(\<integral> x. ?f x \<partial>(count_space (X ` space M) \<Otimes>\<^isub>M count_space (Y ` space M))) =

     (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / (Px x * Py y)))"

 lemma (in information_space) mutual_information_eq:

     by (auto simp add: pair_measure_count_space lebesgue_integral_count_space_finite setsum_cases split_beta'

   assumes "simple_function M X" "simple_function M Y"

              intro!: setsum_cong)

   shows "\<I>(X;Y) = (\<Sum> (x,y) \<in> X ` space M \<times> Y ` space M.

 qed

     distribution (\<lambda>x. (X x, Y x)) {(x,y)} * log b (distribution (\<lambda>x. (X x, Y x)) {(x,y)} /

                                                    (distribution X {x} * distribution Y {y})))"

 lemma (in information_space)

   using assms by (simp add: mutual_information_generic_eq)

   fixes Pxy :: "'b \<times> 'c \<Rightarrow> real" and Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"

   assumes Px: "simple_distributed M X Px" and Py: "simple_distributed M Y Py"

 lemma (in information_space) mutual_information_generic_cong:

   assumes Pxy: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"

   assumes X: "\<And>x. x \<in> space M \<Longrightarrow> X x = X' x"

   assumes ae: "\<forall>x\<in>space M. Pxy (X x, Y x) = Px (X x) * Py (Y x)"

   assumes Y: "\<And>x. x \<in> space M \<Longrightarrow> Y x = Y' x"

   shows mutual_information_eq_0_simple: "\<I>(X ; Y) = 0"

   shows "mutual_information b MX MY X Y = mutual_information b MX MY X' Y'"

 proof (subst mutual_information_simple_distributed[OF Px Py Pxy])

   unfolding mutual_information_def using X Y

   have "(\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / (Px x * Py y))) =

   by (simp cong: distribution_cong)

     (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. 0)"

     by (intro setsum_cong) (auto simp: ae)

 lemma (in information_space) mutual_information_cong:

   then show "(\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M.

   assumes X: "\<And>x. x \<in> space M \<Longrightarrow> X x = X' x"

     Pxy (x, y) * log b (Pxy (x, y) / (Px x * Py y))) = 0" by simp

   assumes Y: "\<And>x. x \<in> space M \<Longrightarrow> Y x = Y' x"

 qed

   shows "\<I>(X; Y) = \<I>(X'; Y')"

   unfolding mutual_information_def using X Y

   by (simp cong: distribution_cong image_cong)

 lemma (in information_space) mutual_information_positive:

   assumes "simple_function M X" "simple_function M Y"

   shows "0 \<le> \<I>(X;Y)"

   using assms by (simp add: mutual_information_positive_generic)

   "\<H>(X) \<equiv> entropy b \<lparr> space = X`space M, sets = Pow (X`space M), measure = ereal\<circ>distribution X \<rparr> X"

   "\<H>(X) \<equiv> entropy b (count_space (X`space M)) X"

 lemma (in information_space) entropy_generic_eq:

 lemma (in information_space) entropy_distr:

   fixes X :: "'a \<Rightarrow> 'c"

   fixes X :: "'a \<Rightarrow> 'b"

   assumes MX: "finite_random_variable MX X"

   assumes "sigma_finite_measure MX" and X: "distributed M MX X f"

   shows "entropy b MX X = -(\<Sum> x \<in> space MX. distribution X {x} * log b (distribution X {x}))"

   shows "entropy b MX X = - (\<integral>x. f x * log b (f x) \<partial>MX)"

 proof -

 proof -

   interpret MX: finite_prob_space "MX\<lparr>measure := ereal\<circ>distribution X\<rparr>"

   interpret MX: sigma_finite_measure MX by fact

     using MX by (rule distribution_finite_prob_space)

   from X show ?thesis

   let ?X = "\<lambda>x. distribution X {x}"

     unfolding entropy_def X[THEN distributed_distr_eq_density]

   let ?XX = "\<lambda>x y. joint_distribution X X {(x, y)}"

     by (subst MX.KL_density[OF b_gt_1]) (simp_all add: distributed_real_AE distributed_real_measurable)

 qed

   { fix x y :: 'c

     { assume "x \<noteq> y"

 lemma (in information_space) entropy_uniform:

       then have "(\<lambda>x. (X x, X x)) -` {(x,y)} \<inter> space M = {}" by auto

   assumes "sigma_finite_measure MX"

       then have "joint_distribution X X {(x, y)} = 0" by (simp add: distribution_def) }

   assumes A: "A \<in> sets MX" "emeasure MX A \<noteq> 0" "emeasure MX A \<noteq> \<infinity>"

     then have "?XX x y * log b (?XX x y / (?X x * ?X y)) =

   assumes X: "distributed M MX X (\<lambda>x. 1 / measure MX A * indicator A x)"

         (if x = y then - ?X y * log b (?X y) else 0)"

   shows "entropy b MX X = log b (measure MX A)"

       by (auto simp: log_simps zero_less_mult_iff) }

 proof (subst entropy_distr[OF _ X])

   note remove_XX = this

   let ?f = "\<lambda>x. 1 / measure MX A * indicator A x"

   have "- (\<integral>x. ?f x * log b (?f x) \<partial>MX) = 

   show ?thesis

     - (\<integral>x. (log b (1 / measure MX A) / measure MX A) * indicator A x \<partial>MX)"

     unfolding entropy_def mutual_information_generic_eq[OF MX MX]

     by (auto intro!: integral_cong simp: indicator_def)

     unfolding setsum_cartesian_product[symmetric] setsum_negf[symmetric] remove_XX

   also have "\<dots> = - log b (inverse (measure MX A))"

     using MX.finite_space by (auto simp: setsum_cases)

     using A by (subst integral_cmult(2))

 qed

                (simp_all add: measure_def real_of_ereal_eq_0 integral_cmult inverse_eq_divide)

   also have "\<dots> = log b (measure MX A)"

 lemma (in information_space) entropy_eq:

     using b_gt_1 A by (subst log_inverse) (auto simp add: measure_def less_le real_of_ereal_eq_0

   assumes "simple_function M X"

                                                           emeasure_nonneg real_of_ereal_pos)

   shows "\<H>(X) = -(\<Sum> x \<in> X ` space M. distribution X {x} * log b (distribution X {x}))"

   finally show "- (\<integral>x. ?f x * log b (?f x) \<partial>MX) = log b (measure MX A)" by simp

   using assms by (simp add: entropy_generic_eq)

 qed fact+

 lemma (in information_space) entropy_positive:

 lemma (in information_space) entropy_simple_distributed:

   "simple_function M X \<Longrightarrow> 0 \<le> \<H>(X)"

   fixes X :: "'a \<Rightarrow> 'b"

   unfolding entropy_def by (simp add: mutual_information_positive)

   assumes X: "simple_distributed M X f"

   shows "\<H>(X) = - (\<Sum>x\<in>X`space M. f x * log b (f x))"

 lemma (in information_space) entropy_certainty_eq_0:

 proof (subst entropy_distr[OF _ simple_distributed[OF X]])

   assumes X: "simple_function M X" and "x \<in> X ` space M" and "distribution X {x} = 1"

   show "sigma_finite_measure (count_space (X ` space M))"

   shows "\<H>(X) = 0"

     using X by (simp add: sigma_finite_measure_count_space_finite simple_distributed_def)

 proof -

   show "- (\<integral>x. f x * log b (f x) \<partial>(count_space (X`space M))) = - (\<Sum>x\<in>X ` space M. f x * log b (f x))"

   let ?X = "\<lparr> space = X ` space M, sets = Pow (X ` space M), measure = ereal\<circ>distribution X\<rparr>"

     using X by (auto simp add: lebesgue_integral_count_space_finite)

   note simple_function_imp_finite_random_variable[OF `simple_function M X`]

   from distribution_finite_prob_space[OF this, of "\<lparr> measure = ereal\<circ>distribution X \<rparr>"]

   interpret X: finite_prob_space ?X by simp

   have "distribution X (X ` space M - {x}) = distribution X (X ` space M) - distribution X {x}"

     using X.measure_compl[of "{x}"] assms by auto

   also have "\<dots> = 0" using X.prob_space assms by auto

   finally have X0: "distribution X (X ` space M - {x}) = 0" by auto

   { fix y assume *: "y \<in> X ` space M"

     { assume asm: "y \<noteq> x"

       with * have "{y} \<subseteq> X ` space M - {x}" by auto

       from X.measure_mono[OF this] X0 asm *

       have "distribution X {y} = 0"  by (auto intro: antisym) }

     then have "distribution X {y} = (if x = y then 1 else 0)"

       using assms by auto }

   note fi = this

   have y: "\<And>y. (if x = y then 1 else 0) * log b (if x = y then 1 else 0) = 0" by simp

   show ?thesis unfolding entropy_eq[OF `simple_function M X`] by (auto simp: y fi)

   assumes X: "simple_function M X"

   assumes X: "simple_distributed M X f"

   shows "\<H>(X) \<le> log b (card (X ` space M \<inter> {x. distribution X {x} \<noteq> 0}))"

   shows "\<H>(X) \<le> log b (card (X ` space M \<inter> {x. f x \<noteq> 0}))"

 proof -

 proof -

   let ?p = "\<lambda>x. distribution X {x}"

   have "\<H>(X) = (\<Sum>x\<in>X`space M. f x * log b (1 / f x))"

   have "\<H>(X) = (\<Sum>x\<in>X`space M. ?p x * log b (1 / ?p x))"

     unfolding entropy_simple_distributed[OF X] setsum_negf[symmetric]

     unfolding entropy_eq[OF X] setsum_negf[symmetric]

     using X by (auto dest: simple_distributed_nonneg intro!: setsum_cong simp: log_simps less_le)

     by (auto intro!: setsum_cong simp: log_simps)

   also have "\<dots> \<le> log b (\<Sum>x\<in>X`space M. f x * (1 / f x))"

   also have "\<dots> \<le> log b (\<Sum>x\<in>X`space M. ?p x * (1 / ?p x))"

     using not_empty b_gt_1 `simple_distributed M X f`

     using not_empty b_gt_1 `simple_function M X` sum_over_space_real_distribution[OF X]

     by (intro log_setsum') (auto simp: simple_distributed_nonneg simple_distributed_setsum_space)

     by (intro log_setsum') (auto simp: simple_function_def)

   also have "\<dots> = log b (\<Sum>x\<in>X`space M. if f x \<noteq> 0 then 1 else 0)"

   also have "\<dots> = log b (\<Sum>x\<in>X`space M. if ?p x \<noteq> 0 then 1 else 0)"

     using `simple_function M X` by (auto simp: setsum_cases real_eq_of_nat simple_function_def)

     using `simple_distributed M X f` by (auto simp: setsum_cases real_eq_of_nat)

 qed

 lemma (in prob_space) measure'_translate:

   assumes X: "random_variable S X" and A: "A \<in> sets S"

   shows "finite_measure.\<mu>' (S\<lparr> measure := ereal\<circ>distribution X \<rparr>) A = distribution X A"

 proof -

   interpret S: prob_space "S\<lparr> measure := ereal\<circ>distribution X \<rparr>"

     using distribution_prob_space[OF X] .

   from A show "S.\<mu>' A = distribution X A"

     unfolding S.\<mu>'_def by (simp add: distribution_def [abs_def] \<mu>'_def)

 qed

 lemma (in information_space) entropy_uniform_max:

   assumes X: "simple_function M X"

   assumes "\<And>x y. \<lbrakk> x \<in> X ` space M ; y \<in> X ` space M \<rbrakk> \<Longrightarrow> distribution X {x} = distribution X {y}"

   shows "\<H>(X) = log b (real (card (X ` space M)))"

 proof -

   let ?X = "\<lparr> space = X ` space M, sets = Pow (X ` space M), measure = undefined\<rparr>\<lparr> measure := ereal\<circ>distribution X\<rparr>"

   note frv = simple_function_imp_finite_random_variable[OF X]

   from distribution_finite_prob_space[OF this, of "\<lparr> measure = ereal\<circ>distribution X \<rparr>"]

   interpret X: finite_prob_space ?X by simp

   note rv = finite_random_variableD[OF frv]

   have card_gt0: "0 < card (X ` space M)" unfolding card_gt_0_iff

     using `simple_function M X` not_empty by (auto simp: simple_function_def)

   { fix x assume "x \<in> space ?X"

     moreover then have "X.\<mu>' {x} = 1 / card (space ?X)"

     proof (rule X.uniform_prob)

       fix x y assume "x \<in> space ?X" "y \<in> space ?X"

       with assms(2)[of x y] show "X.\<mu>' {x} = X.\<mu>' {y}"

         by (subst (1 2) measure'_translate[OF rv]) auto

     qed

     ultimately have "distribution X {x} = 1 / card (space ?X)"

       by (subst (asm) measure'_translate[OF rv]) auto }

   thus ?thesis

     using not_empty X.finite_space b_gt_1 card_gt0

     by (simp add: entropy_eq[OF `simple_function M X`] real_eq_of_nat[symmetric] log_simps)

   assumes "simple_function M X"

   assumes "simple_distributed M X f"

   assume "X ` space M \<inter> {x. distribution X {x} \<noteq> 0} = {}"

   assume "X ` space M \<inter> {x. f x \<noteq> 0} = {}"

   then have "\<And>x. x\<in>X`space M \<Longrightarrow> distribution X {x} = 0" by auto

   then have "\<And>x. x\<in>X`space M \<Longrightarrow> f x = 0" by auto

     using `simple_function M X` not_empty

     using `simple_distributed M X f` not_empty by (auto simp: card_gt_0_iff)

     by (auto simp: card_gt_0_iff simple_function_def)

   ultimately show ?thesis using assms by (simp add: entropy_eq)

   ultimately show ?thesis using assms by (simp add: entropy_simple_distributed)

   assume False: "X ` space M \<inter> {x. distribution X {x} \<noteq> 0} \<noteq> {}"

   assume False: "X ` space M \<inter> {x. f x \<noteq> 0} \<noteq> {}"

   have "card (X ` space M \<inter> {x. distribution X {x} \<noteq> 0}) \<le> card (X ` space M)"

   have "card (X ` space M \<inter> {x. f x \<noteq> 0}) \<le> card (X ` space M)"

     (is "?A \<le> ?B") using assms not_empty by (auto intro!: card_mono simp: simple_function_def)

     (is "?A \<le> ?B") using assms not_empty

     by (auto intro!: card_mono simp: simple_function_def simple_distributed_def)

     by (auto intro!: log_le simp: card_gt_0_iff simp: simple_function_def)

     by (auto intro!: log_le simp: card_gt_0_iff simp: simple_distributed_def)

     \<lparr> space = X`space M, sets = Pow (X`space M), measure = ereal\<circ>distribution X \<rparr>

     (count_space (X ` space M)) (count_space (Y ` space M)) (count_space (Z ` space M)) X Y Z"

     \<lparr> space = Y`space M, sets = Pow (Y`space M), measure = ereal\<circ>distribution Y \<rparr>

     \<lparr> space = Z`space M, sets = Pow (Z`space M), measure = ereal\<circ>distribution Z \<rparr>

     X Y Z"

   assumes MX: "finite_random_variable MX X"

   assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" and P: "sigma_finite_measure P"

     and MY: "finite_random_variable MY Y"

   assumes Px: "distributed M S X Px"

     and MZ: "finite_random_variable MZ Z"

   assumes Pz: "distributed M P Z Pz"

   shows "conditional_mutual_information b MX MY MZ X Y Z = (\<Sum>(x, y, z) \<in> space MX \<times> space MY \<times> space MZ.

   assumes Pyz: "distributed M (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x)) Pyz"

              distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)} *

   assumes Pxz: "distributed M (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) Pxz"

              log b (distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)} /

   assumes Pxyz: "distributed M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Y x, Z x)) Pxyz"

     (joint_distribution X Z {(x, z)} * (joint_distribution Y Z {(y,z)} / distribution Z {z}))))"

   assumes I1: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Px x * Pyz (y, z))))"

   (is "_ = (\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * log b (?XYZ x y z / (?XZ x z * (?YZ y z / ?Z z))))")

   assumes I2: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxz (x, z) / (Px x * Pz z)))"

 proof -

   shows "conditional_mutual_information b S T P X Y Z

   let ?X = "\<lambda>x. distribution X {x}"

     = (\<integral>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"

   note finite_var = MX MY MZ

 proof -

   note YZ = finite_random_variable_pairI[OF finite_var(2,3)]

   interpret S: sigma_finite_measure S by fact

   note XYZ = finite_random_variable_pairI[OF MX YZ]

   interpret T: sigma_finite_measure T by fact

   note XZ = finite_random_variable_pairI[OF finite_var(1,3)]

   interpret P: sigma_finite_measure P by fact

   note ZX = finite_random_variable_pairI[OF finite_var(3,1)]

   interpret TP: pair_sigma_finite T P ..

   note YZX = finite_random_variable_pairI[OF finite_var(2) ZX]

   interpret SP: pair_sigma_finite S P ..

   note order1 =

   interpret SPT: pair_sigma_finite "S \<Otimes>\<^isub>M P" T ..

     finite_distribution_order(5,6)[OF finite_var(1) YZ]

   interpret STP: pair_sigma_finite S "T \<Otimes>\<^isub>M P" ..

     finite_distribution_order(5,6)[OF finite_var(1,3)]

   have TP: "sigma_finite_measure (T \<Otimes>\<^isub>M P)" ..

   have SP: "sigma_finite_measure (S \<Otimes>\<^isub>M P)" ..

   note random_var = finite_var[THEN finite_random_variableD]

   have YZ: "random_variable (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x))"

   note finite = finite_var(1) YZ finite_var(3) XZ YZX

     using Pyz by (simp add: distributed_measurable)

   have order2: "\<And>x y z. \<lbrakk>x \<in> space MX; y \<in> space MY; z \<in> space MZ; joint_distribution X Z {(x, z)} = 0\<rbrakk>

   have Pxyz_f: "\<And>M f. f \<in> measurable M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) \<Longrightarrow> (\<lambda>x. Pxyz (f x)) \<in> borel_measurable M"

           \<Longrightarrow> joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)} = 0"

     using measurable_comp[OF _ Pxyz[THEN distributed_real_measurable]] by (auto simp: comp_def)

     unfolding joint_distribution_commute_singleton[of X]

     unfolding joint_distribution_assoc_singleton[symmetric]

   { fix f g h M

     using finite_distribution_order(6)[OF finite_var(2) ZX]

     assume f: "f \<in> measurable M S" and g: "g \<in> measurable M P" and h: "h \<in> measurable M (S \<Otimes>\<^isub>M P)"

     by auto

     from measurable_comp[OF h Pxz[THEN distributed_real_measurable]]

          measurable_comp[OF f Px[THEN distributed_real_measurable]]

   have "(\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * log b (?XYZ x y z / (?XZ x z * (?YZ y z / ?Z z)))) =

          measurable_comp[OF g Pz[THEN distributed_real_measurable]]

     (\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * (log b (?XYZ x y z / (?X x * ?YZ y z)) - log b (?XZ x z / (?X x * ?Z z))))"

     have "(\<lambda>x. log b (Pxz (h x) / (Px (f x) * Pz (g x)))) \<in> borel_measurable M"

     (is "(\<Sum>(x, y, z)\<in>?S. ?L x y z) = (\<Sum>(x, y, z)\<in>?S. ?R x y z)")

       by (simp add: comp_def b_gt_1) }

   proof (safe intro!: setsum_cong)

   note borel_log = this

     fix x y z assume space: "x \<in> space MX" "y \<in> space MY" "z \<in> space MZ"

     show "?L x y z = ?R x y z"

   have measurable_cut: "(\<lambda>(x, y, z). (x, z)) \<in> measurable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (S \<Otimes>\<^isub>M P)"

     by (auto simp add: split_beta' comp_def intro!: measurable_Pair measurable_snd')

   from Pxz Pxyz have distr_eq: "distr M (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) =

     distr (distr M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Y x, Z x))) (S \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). (x, z))"

     by (subst distr_distr[OF measurable_cut]) (auto dest: distributed_measurable simp: comp_def)

   have "mutual_information b S P X Z =

     (\<integral>x. Pxz x * log b (Pxz x / (Px (fst x) * Pz (snd x))) \<partial>(S \<Otimes>\<^isub>M P))"

     by (rule mutual_information_distr[OF S P Px Pz Pxz])

   also have "\<dots> = (\<integral>(x,y,z). Pxyz (x,y,z) * log b (Pxz (x,z) / (Px x * Pz z)) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"

     using b_gt_1 Pxz Px Pz

     by (subst distributed_transform_integral[OF Pxyz Pxz, where T="\<lambda>(x, y, z). (x, z)"])

        (auto simp: split_beta' intro!: measurable_Pair measurable_snd' measurable_snd'' measurable_fst'' borel_measurable_times

              dest!: distributed_real_measurable)

   finally have mi_eq:

     "mutual_information b S P X Z = (\<integral>(x,y,z). Pxyz (x,y,z) * log b (Pxz (x,z) / (Px x * Pz z)) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))" .

   have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Px (fst x) = 0 \<longrightarrow> Pxyz x = 0"

     by (intro subdensity_real[of fst, OF _ Pxyz Px]) auto

   moreover have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pz (snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"

     by (intro subdensity_real[of "\<lambda>x. snd (snd x)", OF _ Pxyz Pz]) (auto intro: measurable_snd')

   moreover have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pxz (fst x, snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"

     by (intro subdensity_real[of "\<lambda>x. (fst x, snd (snd x))", OF _ Pxyz Pxz]) (auto intro: measurable_Pair measurable_snd')

   moreover have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pyz (snd x) = 0 \<longrightarrow> Pxyz x = 0"

     by (intro subdensity_real[of snd, OF _ Pxyz Pyz]) (auto intro: measurable_Pair)

   moreover have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Px (fst x)"

     using Px by (intro STP.AE_pair_measure) (auto simp: comp_def intro!: measurable_fst'' dest: distributed_real_AE distributed_real_measurable)

   moreover have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pyz (snd x)"

     using Pyz by (intro STP.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)

   moreover have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pz (snd (snd x))"

     using Pz Pz[THEN distributed_real_measurable] by (auto intro!: measurable_snd'' TP.AE_pair_measure STP.AE_pair_measure AE_I2[of S] dest: distributed_real_AE)

   moreover have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pxz (fst x, snd (snd x))"

     using Pxz[THEN distributed_real_AE, THEN SP.AE_pair]

     using measurable_comp[OF measurable_Pair[OF measurable_fst measurable_comp[OF measurable_snd measurable_snd]] Pxz[THEN distributed_real_measurable], of T]

     using measurable_comp[OF measurable_snd measurable_Pair2[OF Pxz[THEN distributed_real_measurable]], of _ T]

     by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure simp: comp_def)

   moreover note Pxyz[THEN distributed_real_AE]

   ultimately have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P.

     Pxyz x * log b (Pxyz x / (Px (fst x) * Pyz (snd x))) -

     Pxyz x * log b (Pxz (fst x, snd (snd x)) / (Px (fst x) * Pz (snd (snd x)))) =

     Pxyz x * log b (Pxyz x * Pz (snd (snd x)) / (Pxz (fst x, snd (snd x)) * Pyz (snd x))) "

   proof eventually_elim

     case (goal1 x)

     show ?case

       assume "?XYZ x y z \<noteq> 0"

       assume "Pxyz x \<noteq> 0"

       with space have "0 < ?X x" "0 < ?Z z" "0 < ?XZ x z" "0 < ?YZ y z" "0 < ?XYZ x y z"

       with goal1 have "0 < Px (fst x)" "0 < Pz (snd (snd x))" "0 < Pxz (fst x, snd (snd x))" "0 < Pyz (snd x)" "0 < Pxyz x"

         using order1 order2 by (auto simp: less_le)

         by auto

       with b_gt_1 show ?thesis

       then show ?thesis

         by (simp add: log_mult log_divide zero_less_mult_iff zero_less_divide_iff)

         using b_gt_1 by (simp add: log_simps mult_pos_pos less_imp_le field_simps)

   also have "\<dots> = (\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * log b (?XYZ x y z / (?X x * ?YZ y z))) -

   with I1 I2 show ?thesis

                   (\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * log b (?XZ x z / (?X x * ?Z z)))"

     by (auto simp add: setsum_subtractf[symmetric] field_simps intro!: setsum_cong)

   also have "(\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * log b (?XZ x z / (?X x * ?Z z))) =

              (\<Sum>(x, z)\<in>space MX \<times> space MZ. ?XZ x z * log b (?XZ x z / (?X x * ?Z z)))"

     unfolding setsum_cartesian_product[symmetric] setsum_commute[of _ _ "space MY"]

               setsum_left_distrib[symmetric]

     unfolding joint_distribution_commute_singleton[of X]

     unfolding joint_distribution_assoc_singleton[symmetric]

     using setsum_joint_distribution_singleton[OF finite_var(2) ZX]

     by (intro setsum_cong refl) (simp add: space_pair_measure)

   also have "(\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * log b (?XYZ x y z / (?X x * ?YZ y z))) -

              (\<Sum>(x, z)\<in>space MX \<times> space MZ. ?XZ x z * log b (?XZ x z / (?X x * ?Z z))) =

              conditional_mutual_information b MX MY MZ X Y Z"

     unfolding mutual_information_generic_eq[OF finite_var(1,3)]

     apply (subst mi_eq)

     unfolding mutual_information_generic_eq[OF finite_var(1) YZ]

     apply (subst mutual_information_distr[OF S TP Px Pyz Pxyz])

     by (simp add: space_sigma space_pair_measure setsum_cartesian_product')

     apply (subst integral_diff(2)[symmetric])

   finally show ?thesis by simp

     apply (auto intro!: integral_cong_AE simp: split_beta' simp del: integral_diff)

     done

   assumes "simple_function M X" "simple_function M Y" "simple_function M Z"

   assumes Pz: "simple_distributed M Z Pz"

   shows "\<I>(X;Y|Z) = (\<Sum>(x, y, z) \<in> X`space M \<times> Y`space M \<times> Z`space M.

   assumes Pyz: "simple_distributed M (\<lambda>x. (Y x, Z x)) Pyz"

              distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)} *

   assumes Pxz: "simple_distributed M (\<lambda>x. (X x, Z x)) Pxz"

              log b (distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)} /

   assumes Pxyz: "simple_distributed M (\<lambda>x. (X x, Y x, Z x)) Pxyz"

     (joint_distribution X Z {(x, z)} * joint_distribution Y Z {(y,z)} / distribution Z {z})))"

   shows "\<I>(X ; Y | Z) =

   by (subst conditional_mutual_information_generic_eq[OF assms[THEN simple_function_imp_finite_random_variable]])

    (\<Sum>(x, y, z)\<in>(\<lambda>x. (X x, Y x, Z x))`space M. Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"

      simp

 proof (subst conditional_mutual_information_generic_eq[OF _ _ _ _

     simple_distributed[OF Pz] simple_distributed_joint[OF Pyz] simple_distributed_joint[OF Pxz]

 lemma (in information_space) conditional_mutual_information_eq_mutual_information:

     simple_distributed_joint2[OF Pxyz]])

   assumes X: "simple_function M X" and Y: "simple_function M Y"

   note simple_distributed_joint2_finite[OF Pxyz, simp]

   shows "\<I>(X ; Y) = \<I>(X ; Y | (\<lambda>x. ()))"

   show "sigma_finite_measure (count_space (X ` space M))"

 proof -

     by (simp add: sigma_finite_measure_count_space_finite)

   have [simp]: "(\<lambda>x. ()) ` space M = {()}" using not_empty by auto

   show "sigma_finite_measure (count_space (Y ` space M))"

   have C: "simple_function M (\<lambda>x. ())" by auto

     by (simp add: sigma_finite_measure_count_space_finite)

   show ?thesis

   show "sigma_finite_measure (count_space (Z ` space M))"

     unfolding conditional_mutual_information_eq[OF X Y C]

     by (simp add: sigma_finite_measure_count_space_finite)

     unfolding mutual_information_eq[OF X Y]

   have "count_space (X ` space M) \<Otimes>\<^isub>M count_space (Y ` space M) \<Otimes>\<^isub>M count_space (Z ` space M) =

     by (simp add: setsum_cartesian_product' distribution_remove_const)

       count_space (X`space M \<times> Y`space M \<times> Z`space M)"

 qed

     (is "?P = ?C")

     by (simp add: pair_measure_count_space)

 lemma (in information_space) conditional_mutual_information_generic_positive:

   assumes X: "finite_random_variable MX X" and Y: "finite_random_variable MY Y" and Z: "finite_random_variable MZ Z"

   let ?Px = "\<lambda>x. measure M (X -` {x} \<inter> space M)"

   shows "0 \<le> conditional_mutual_information b MX MY MZ X Y Z"

   have "(\<lambda>x. (X x, Z x)) \<in> measurable M (count_space (X ` space M) \<Otimes>\<^isub>M count_space (Z ` space M))"

 proof (cases "space MX \<times> space MY \<times> space MZ = {}")

     using simple_distributed_joint[OF Pxz] by (rule distributed_measurable)

   case True show ?thesis

   from measurable_comp[OF this measurable_fst]

     unfolding conditional_mutual_information_generic_eq[OF assms] True

   have "random_variable (count_space (X ` space M)) X"

     by simp

     by (simp add: comp_def)

 next

   then have "simple_function M X"    

   case False

     unfolding simple_function_def by auto

   let ?dXYZ = "distribution (\<lambda>x. (X x, Y x, Z x))"

   then have "simple_distributed M X ?Px"

   let ?dXZ = "joint_distribution X Z"

     by (rule simple_distributedI) auto

   let ?dYZ = "joint_distribution Y Z"

   then show "distributed M (count_space (X ` space M)) X ?Px"

   let ?dX = "distribution X"

     by (rule simple_distributed)

   let ?dZ = "distribution Z"

   let ?M = "space MX \<times> space MY \<times> space MZ"

   let ?f = "(\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x, Z x)) ` space M then Pxyz x else 0)"

   let ?g = "(\<lambda>x. if x \<in> (\<lambda>x. (Y x, Z x)) ` space M then Pyz x else 0)"

   note YZ = finite_random_variable_pairI[OF Y Z]

   let ?h = "(\<lambda>x. if x \<in> (\<lambda>x. (X x, Z x)) ` space M then Pxz x else 0)"

   note XZ = finite_random_variable_pairI[OF X Z]

   show

   note ZX = finite_random_variable_pairI[OF Z X]

       "integrable ?P (\<lambda>(x, y, z). ?f (x, y, z) * log b (?f (x, y, z) / (?Px x * ?g (y, z))))"

   note YZ = finite_random_variable_pairI[OF Y Z]

       "integrable ?P (\<lambda>(x, y, z). ?f (x, y, z) * log b (?h (x, z) / (?Px x * Pz z)))"

   note XYZ = finite_random_variable_pairI[OF X YZ]

     by (auto intro!: integrable_count_space simp: pair_measure_count_space)

   note finite = Z YZ XZ XYZ

   let ?i = "\<lambda>x y z. ?f (x, y, z) * log b (?f (x, y, z) / (?h (x, z) * (?g (y, z) / Pz z)))"

   have order: "\<And>x y z. \<lbrakk>x \<in> space MX; y \<in> space MY; z \<in> space MZ; joint_distribution X Z {(x, z)} = 0\<rbrakk>

   let ?j = "\<lambda>x y z. Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z)))"

           \<Longrightarrow> joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)} = 0"

   have "(\<lambda>(x, y, z). ?i x y z) = (\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x, Z x)) ` space M then ?j (fst x) (fst (snd x)) (snd (snd x)) else 0)"

     unfolding joint_distribution_commute_singleton[of X]

     by (auto intro!: ext)

     unfolding joint_distribution_assoc_singleton[symmetric]

   then show "(\<integral> (x, y, z). ?i x y z \<partial>?P) = (\<Sum>(x, y, z)\<in>(\<lambda>x. (X x, Y x, Z x)) ` space M. ?j x y z)"

     using finite_distribution_order(6)[OF Y ZX]

     by (auto intro!: setsum_cong simp add: `?P = ?C` lebesgue_integral_count_space_finite simple_distributed_finite setsum_cases split_beta')

     by auto

 qed

   note order = order

 lemma (in information_space) conditional_mutual_information_nonneg:

     finite_distribution_order(5,6)[OF X YZ]

   assumes X: "simple_function M X" and Y: "simple_function M Y" and Z: "simple_function M Z"

     finite_distribution_order(5,6)[OF Y Z]

   shows "0 \<le> \<I>(X ; Y | Z)"

 proof -

   have "- conditional_mutual_information b MX MY MZ X Y Z = - (\<Sum>(x, y, z) \<in> ?M. ?dXYZ {(x, y, z)} *

   def Pz \<equiv> "\<lambda>x. if x \<in> Z`space M then measure M (Z -` {x} \<inter> space M) else 0"

     log b (?dXYZ {(x, y, z)} / (?dXZ {(x, z)} * ?dYZ {(y,z)} / ?dZ {z})))"

   def Pxz \<equiv> "\<lambda>x. if x \<in> (\<lambda>x. (X x, Z x))`space M then measure M ((\<lambda>x. (X x, Z x)) -` {x} \<inter> space M) else 0"

     unfolding conditional_mutual_information_generic_eq[OF assms] neg_equal_iff_equal by auto

   def Pyz \<equiv> "\<lambda>x. if x \<in> (\<lambda>x. (Y x, Z x))`space M then measure M ((\<lambda>x. (Y x, Z x)) -` {x} \<inter> space M) else 0"

   also have "\<dots> \<le> log b (\<Sum>(x, y, z) \<in> ?M. ?dXZ {(x, z)} * ?dYZ {(y,z)} / ?dZ {z})"

   def Pxyz \<equiv> "\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x, Z x))`space M then measure M ((\<lambda>x. (X x, Y x, Z x)) -` {x} \<inter> space M) else 0"

   let ?M = "X`space M \<times> Y`space M \<times> Z`space M"

   note XZ = simple_function_Pair[OF X Z]

   note YZ = simple_function_Pair[OF Y Z]

   note XYZ = simple_function_Pair[OF X simple_function_Pair[OF Y Z]]

   have Pz: "simple_distributed M Z Pz"

     using Z by (rule simple_distributedI) (auto simp: Pz_def)

   have Pxz: "simple_distributed M (\<lambda>x. (X x, Z x)) Pxz"

     using XZ by (rule simple_distributedI) (auto simp: Pxz_def)

   have Pyz: "simple_distributed M (\<lambda>x. (Y x, Z x)) Pyz"

     using YZ by (rule simple_distributedI) (auto simp: Pyz_def)

   have Pxyz: "simple_distributed M (\<lambda>x. (X x, Y x, Z x)) Pxyz"

     using XYZ by (rule simple_distributedI) (auto simp: Pxyz_def)

   { fix z assume z: "z \<in> Z ` space M" then have "(\<Sum>x\<in>X ` space M. Pxz (x, z)) = Pz z"

       using distributed_marginal_eq_joint_simple[OF X Pz Pxz z]

       by (auto intro!: setsum_cong simp: Pxz_def) }

   note marginal1 = this

   { fix z assume z: "z \<in> Z ` space M" then have "(\<Sum>y\<in>Y ` space M. Pyz (y, z)) = Pz z"

       using distributed_marginal_eq_joint_simple[OF Y Pz Pyz z]

       by (auto intro!: setsum_cong simp: Pyz_def) }

   note marginal2 = this

   have "- \<I>(X ; Y | Z) = - (\<Sum>(x, y, z) \<in> ?M. Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"

     unfolding conditional_mutual_information_eq[OF Pz Pyz Pxz Pxyz]

     using X Y Z by (auto intro!: setsum_mono_zero_left simp: Pxyz_def simple_functionD)

   also have "\<dots> \<le> log b (\<Sum>(x, y, z) \<in> ?M. Pxz (x, z) * (Pyz (y,z) / Pz z))"

     show "?M \<noteq> {}" using False by simp

     show "?M \<noteq> {}" using not_empty by simp

     show "finite ?M" using assms

     show "finite ?M" using X Y Z by (auto simp: simple_functionD)

       unfolding finite_sigma_algebra_def finite_sigma_algebra_axioms_def by auto

     then show "(\<Sum>x\<in>?M. Pxyz (fst x, fst (snd x), snd (snd x))) = 1"

     show "(\<Sum>x\<in>?M. ?dXYZ {(fst x, fst (snd x), snd (snd x))}) = 1"

       apply (subst Pxyz[THEN simple_distributed_setsum_space, symmetric])

       unfolding setsum_cartesian_product'

       apply simp

       unfolding setsum_commute[of _ "space MY"]

       apply (intro setsum_mono_zero_right)

       unfolding setsum_commute[of _ "space MZ"]

       apply (auto simp: Pxyz_def)

       by (simp_all add: space_pair_measure

       done

                         setsum_joint_distribution_singleton[OF X YZ]

     let ?N = "(\<lambda>x. (X x, Y x, Z x)) ` space M"

                         setsum_joint_distribution_singleton[OF Y Z]

     fix x assume x: "x \<in> ?M"

                         setsum_distribution[OF Z])

     let ?Q = "Pxyz (fst x, fst (snd x), snd (snd x))"

     let ?P = "Pxz (fst x, snd (snd x)) * (Pyz (fst (snd x), snd (snd x)) / Pz (snd (snd x)))"

     fix x assume "x \<in> ?M"

     from x show "0 \<le> ?Q" "0 \<le> ?P"

     let ?x = "(fst x, fst (snd x), snd (snd x))"

       using Pxyz[THEN simple_distributed, THEN distributed_real_AE]

       using Pxz[THEN simple_distributed, THEN distributed_real_AE]

     show "0 \<le> ?dXYZ {?x}"

       using Pyz[THEN simple_distributed, THEN distributed_real_AE]

       "0 \<le> ?dXZ {(fst x, snd (snd x))} * ?dYZ {(fst (snd x), snd (snd x))} / ?dZ {snd (snd x)}"

       using Pz[THEN simple_distributed, THEN distributed_real_AE]

      by (simp_all add: mult_nonneg_nonneg divide_nonneg_nonneg)

       by (auto intro!: mult_nonneg_nonneg divide_nonneg_nonneg simp: AE_count_space Pxyz_def Pxz_def Pyz_def Pz_def)

     moreover assume "0 < ?Q"

     assume *: "0 < ?dXYZ {?x}"

     moreover have "AE x in count_space ?N. Pz (snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"

     with `x \<in> ?M` finite order show "0 < ?dXZ {(fst x, snd (snd x))} * ?dYZ {(fst (snd x), snd (snd x))} / ?dZ {snd (snd x)}"

       by (intro subdensity_real[of "\<lambda>x. snd (snd x)", OF _ Pxyz[THEN simple_distributed] Pz[THEN simple_distributed]]) (auto intro: measurable_snd')

       by (cases x) (auto simp add: zero_le_mult_iff zero_le_divide_iff less_le)

     then have "\<And>x. Pz (snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"

       by (auto simp: Pz_def Pxyz_def AE_count_space)

     moreover have "AE x in count_space ?N. Pxz (fst x, snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"

       by (intro subdensity_real[of "\<lambda>x. (fst x, snd (snd x))", OF _ Pxyz[THEN simple_distributed] Pxz[THEN simple_distributed]]) (auto intro: measurable_Pair measurable_snd')

     then have "\<And>x. Pxz (fst x, snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"

       by (auto simp: Pz_def Pxyz_def AE_count_space)

     moreover have "AE x in count_space ?N. Pyz (snd x) = 0 \<longrightarrow> Pxyz x = 0"

       by (intro subdensity_real[of snd, OF _ Pxyz[THEN simple_distributed] Pyz[THEN simple_distributed]]) (auto intro: measurable_Pair)

     then have "\<And>x. Pyz (snd x) = 0 \<longrightarrow> Pxyz x = 0"

       by (auto simp: Pz_def Pxyz_def AE_count_space)

     ultimately show "0 < ?P" using x by (auto intro!: divide_pos_pos mult_pos_pos simp: less_le)

   also have "(\<Sum>(x, y, z) \<in> ?M. ?dXZ {(x, z)} * ?dYZ {(y,z)} / ?dZ {z}) = (\<Sum>z\<in>space MZ. ?dZ {z})"

   also have "(\<Sum>(x, y, z) \<in> ?M. Pxz (x, z) * (Pyz (y,z) / Pz z)) = (\<Sum>z\<in>Z`space M. Pz z)"

     by (auto simp: setsum_divide_distrib[symmetric] setsum_product[symmetric]

     apply (auto simp: setsum_divide_distrib[symmetric] setsum_product[symmetric] marginal1 marginal2

                    setsum_joint_distribution_singleton[OF X Z]

                    setsum_joint_distribution_singleton[OF Y Z]

   also have "log b (\<Sum>z\<in>space MZ. ?dZ {z}) = 0"

     done

     unfolding setsum_distribution[OF Z] by simp

   also have "log b (\<Sum>z\<in>Z`space M. Pz z) = 0"

     using Pz[THEN simple_distributed_setsum_space] by simp