src/HOL/Probability/Information.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 61808 fc1556774cfe
child 62390 842917225d56
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
hoelzl@42067
     1
(*  Title:      HOL/Probability/Information.thy
hoelzl@42067
     2
    Author:     Johannes Hölzl, TU München
hoelzl@42067
     3
    Author:     Armin Heller, TU München
hoelzl@42067
     4
*)
hoelzl@42067
     5
wenzelm@61808
     6
section \<open>Information theory\<close>
hoelzl@42067
     7
hoelzl@36080
     8
theory Information
wenzelm@41413
     9
imports
hoelzl@43340
    10
  Independent_Family
wenzelm@41413
    11
  "~~/src/HOL/Library/Convex"
hoelzl@36080
    12
begin
hoelzl@36080
    13
hoelzl@39097
    14
lemma log_le: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> x \<le> y \<Longrightarrow> log a x \<le> log a y"
hoelzl@39097
    15
  by (subst log_le_cancel_iff) auto
hoelzl@39097
    16
hoelzl@39097
    17
lemma log_less: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> x < y \<Longrightarrow> log a x < log a y"
hoelzl@39097
    18
  by (subst log_less_cancel_iff) auto
hoelzl@39097
    19
hoelzl@39097
    20
lemma setsum_cartesian_product':
hoelzl@39097
    21
  "(\<Sum>x\<in>A \<times> B. f x) = (\<Sum>x\<in>A. setsum (\<lambda>y. f (x, y)) B)"
haftmann@57418
    22
  unfolding setsum.cartesian_product by simp
hoelzl@39097
    23
hoelzl@39097
    24
lemma split_pairs:
hoelzl@40859
    25
  "((A, B) = X) \<longleftrightarrow> (fst X = A \<and> snd X = B)" and
hoelzl@40859
    26
  "(X = (A, B)) \<longleftrightarrow> (fst X = A \<and> snd X = B)" by auto
hoelzl@38656
    27
hoelzl@56994
    28
subsection "Information theory"
hoelzl@38656
    29
hoelzl@40859
    30
locale information_space = prob_space +
hoelzl@38656
    31
  fixes b :: real assumes b_gt_1: "1 < b"
hoelzl@38656
    32
hoelzl@40859
    33
context information_space
hoelzl@38656
    34
begin
hoelzl@38656
    35
wenzelm@61808
    36
text \<open>Introduce some simplification rules for logarithm of base @{term b}.\<close>
hoelzl@40859
    37
hoelzl@40859
    38
lemma log_neg_const:
hoelzl@40859
    39
  assumes "x \<le> 0"
hoelzl@40859
    40
  shows "log b x = log b 0"
hoelzl@36624
    41
proof -
hoelzl@40859
    42
  { fix u :: real
hoelzl@40859
    43
    have "x \<le> 0" by fact
hoelzl@40859
    44
    also have "0 < exp u"
hoelzl@40859
    45
      using exp_gt_zero .
hoelzl@40859
    46
    finally have "exp u \<noteq> x"
hoelzl@40859
    47
      by auto }
hoelzl@40859
    48
  then show "log b x = log b 0"
lp15@60017
    49
    by (simp add: log_def ln_real_def)
hoelzl@38656
    50
qed
hoelzl@38656
    51
hoelzl@40859
    52
lemma log_mult_eq:
hoelzl@40859
    53
  "log b (A * B) = (if 0 < A * B then log b \<bar>A\<bar> + log b \<bar>B\<bar> else log b 0)"
hoelzl@40859
    54
  using log_mult[of b "\<bar>A\<bar>" "\<bar>B\<bar>"] b_gt_1 log_neg_const[of "A * B"]
hoelzl@40859
    55
  by (auto simp: zero_less_mult_iff mult_le_0_iff)
hoelzl@38656
    56
hoelzl@40859
    57
lemma log_inverse_eq:
hoelzl@40859
    58
  "log b (inverse B) = (if 0 < B then - log b B else log b 0)"
hoelzl@40859
    59
  using log_inverse[of b B] log_neg_const[of "inverse B"] b_gt_1 by simp
hoelzl@36080
    60
hoelzl@40859
    61
lemma log_divide_eq:
hoelzl@40859
    62
  "log b (A / B) = (if 0 < A * B then log b \<bar>A\<bar> - log b \<bar>B\<bar> else log b 0)"
hoelzl@40859
    63
  unfolding divide_inverse log_mult_eq log_inverse_eq abs_inverse
hoelzl@40859
    64
  by (auto simp: zero_less_mult_iff mult_le_0_iff)
hoelzl@38656
    65
hoelzl@40859
    66
lemmas log_simps = log_mult_eq log_inverse_eq log_divide_eq
hoelzl@38656
    67
hoelzl@38656
    68
end
hoelzl@38656
    69
hoelzl@39097
    70
subsection "Kullback$-$Leibler divergence"
hoelzl@36080
    71
wenzelm@61808
    72
text \<open>The Kullback$-$Leibler divergence is also known as relative entropy or
wenzelm@61808
    73
Kullback$-$Leibler distance.\<close>
hoelzl@39097
    74
hoelzl@39097
    75
definition
lp15@61609
    76
  "entropy_density b M N = log b \<circ> real_of_ereal \<circ> RN_deriv M N"
hoelzl@43340
    77
hoelzl@43340
    78
definition
wenzelm@53015
    79
  "KL_divergence b M N = integral\<^sup>L N (entropy_density b M N)"
hoelzl@43340
    80
hoelzl@56993
    81
lemma measurable_entropy_density[measurable]: "entropy_density b M N \<in> borel_measurable M"
hoelzl@56993
    82
  unfolding entropy_density_def by auto
hoelzl@50003
    83
hoelzl@47694
    84
lemma (in sigma_finite_measure) KL_density:
hoelzl@47694
    85
  fixes f :: "'a \<Rightarrow> real"
hoelzl@47694
    86
  assumes "1 < b"
hoelzl@56993
    87
  assumes f[measurable]: "f \<in> borel_measurable M" and nn: "AE x in M. 0 \<le> f x"
hoelzl@47694
    88
  shows "KL_divergence b M (density M f) = (\<integral>x. f x * log b (f x) \<partial>M)"
hoelzl@47694
    89
  unfolding KL_divergence_def
hoelzl@56993
    90
proof (subst integral_real_density)
hoelzl@56993
    91
  show [measurable]: "entropy_density b M (density M (\<lambda>x. ereal (f x))) \<in> borel_measurable M"
hoelzl@49776
    92
    using f
hoelzl@50003
    93
    by (auto simp: comp_def entropy_density_def)
hoelzl@47694
    94
  have "density M (RN_deriv M (density M f)) = density M f"
hoelzl@56993
    95
    using f nn by (intro density_RN_deriv_density) auto
hoelzl@47694
    96
  then have eq: "AE x in M. RN_deriv M (density M f) x = f x"
hoelzl@56993
    97
    using f nn by (intro density_unique) (auto simp: RN_deriv_nonneg)
hoelzl@47694
    98
  show "(\<integral>x. f x * entropy_density b M (density M (\<lambda>x. ereal (f x))) x \<partial>M) = (\<integral>x. f x * log b (f x) \<partial>M)"
hoelzl@47694
    99
    apply (intro integral_cong_AE)
hoelzl@56993
   100
    apply measurable
hoelzl@47694
   101
    using eq
hoelzl@47694
   102
    apply eventually_elim
hoelzl@47694
   103
    apply (auto simp: entropy_density_def)
hoelzl@47694
   104
    done
hoelzl@47694
   105
qed fact+
hoelzl@43340
   106
hoelzl@47694
   107
lemma (in sigma_finite_measure) KL_density_density:
hoelzl@47694
   108
  fixes f g :: "'a \<Rightarrow> real"
hoelzl@47694
   109
  assumes "1 < b"
hoelzl@47694
   110
  assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
hoelzl@47694
   111
  assumes g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
hoelzl@47694
   112
  assumes ac: "AE x in M. f x = 0 \<longrightarrow> g x = 0"
hoelzl@47694
   113
  shows "KL_divergence b (density M f) (density M g) = (\<integral>x. g x * log b (g x / f x) \<partial>M)"
hoelzl@47694
   114
proof -
hoelzl@47694
   115
  interpret Mf: sigma_finite_measure "density M f"
hoelzl@47694
   116
    using f by (subst sigma_finite_iff_density_finite) auto
hoelzl@47694
   117
  have "KL_divergence b (density M f) (density M g) =
hoelzl@47694
   118
    KL_divergence b (density M f) (density (density M f) (\<lambda>x. g x / f x))"
hoelzl@47694
   119
    using f g ac by (subst density_density_divide) simp_all
hoelzl@47694
   120
  also have "\<dots> = (\<integral>x. (g x / f x) * log b (g x / f x) \<partial>density M f)"
wenzelm@61808
   121
    using f g \<open>1 < b\<close> by (intro Mf.KL_density) (auto simp: AE_density)
hoelzl@47694
   122
  also have "\<dots> = (\<integral>x. g x * log b (g x / f x) \<partial>M)"
wenzelm@61808
   123
    using ac f g \<open>1 < b\<close> by (subst integral_density) (auto intro!: integral_cong_AE)
hoelzl@47694
   124
  finally show ?thesis .
hoelzl@47694
   125
qed
hoelzl@43340
   126
hoelzl@47694
   127
lemma (in information_space) KL_gt_0:
hoelzl@47694
   128
  fixes D :: "'a \<Rightarrow> real"
hoelzl@47694
   129
  assumes "prob_space (density M D)"
hoelzl@47694
   130
  assumes D: "D \<in> borel_measurable M" "AE x in M. 0 \<le> D x"
hoelzl@47694
   131
  assumes int: "integrable M (\<lambda>x. D x * log b (D x))"
hoelzl@47694
   132
  assumes A: "density M D \<noteq> M"
hoelzl@47694
   133
  shows "0 < KL_divergence b M (density M D)"
hoelzl@47694
   134
proof -
hoelzl@47694
   135
  interpret N: prob_space "density M D" by fact
hoelzl@43340
   136
hoelzl@47694
   137
  obtain A where "A \<in> sets M" "emeasure (density M D) A \<noteq> emeasure M A"
wenzelm@61808
   138
    using measure_eqI[of "density M D" M] \<open>density M D \<noteq> M\<close> by auto
hoelzl@47694
   139
hoelzl@47694
   140
  let ?D_set = "{x\<in>space M. D x \<noteq> 0}"
hoelzl@47694
   141
  have [simp, intro]: "?D_set \<in> sets M"
hoelzl@47694
   142
    using D by auto
hoelzl@43340
   143
wenzelm@53015
   144
  have D_neg: "(\<integral>\<^sup>+ x. ereal (- D x) \<partial>M) = 0"
hoelzl@56996
   145
    using D by (subst nn_integral_0_iff_AE) auto
hoelzl@43340
   146
wenzelm@53015
   147
  have "(\<integral>\<^sup>+ x. ereal (D x) \<partial>M) = emeasure (density M D) (space M)"
hoelzl@56996
   148
    using D by (simp add: emeasure_density cong: nn_integral_cong)
wenzelm@53015
   149
  then have D_pos: "(\<integral>\<^sup>+ x. ereal (D x) \<partial>M) = 1"
hoelzl@47694
   150
    using N.emeasure_space_1 by simp
hoelzl@43340
   151
hoelzl@56993
   152
  have "integrable M D"
hoelzl@56993
   153
    using D D_pos D_neg unfolding real_integrable_def real_lebesgue_integral_def by simp_all
hoelzl@56993
   154
  then have "integral\<^sup>L M D = 1"
hoelzl@56993
   155
    using D D_pos D_neg by (simp add: real_lebesgue_integral_def)
hoelzl@43340
   156
hoelzl@47694
   157
  have "0 \<le> 1 - measure M ?D_set"
hoelzl@43340
   158
    using prob_le_1 by (auto simp: field_simps)
hoelzl@43340
   159
  also have "\<dots> = (\<integral> x. D x - indicator ?D_set x \<partial>M)"
wenzelm@61808
   160
    using \<open>integrable M D\<close> \<open>integral\<^sup>L M D = 1\<close>
hoelzl@47694
   161
    by (simp add: emeasure_eq_measure)
hoelzl@47694
   162
  also have "\<dots> < (\<integral> x. D x * (ln b * log b (D x)) \<partial>M)"
hoelzl@43340
   163
  proof (rule integral_less_AE)
hoelzl@43340
   164
    show "integrable M (\<lambda>x. D x - indicator ?D_set x)"
wenzelm@61808
   165
      using \<open>integrable M D\<close> by auto
hoelzl@43340
   166
  next
hoelzl@56993
   167
    from integrable_mult_left(1)[OF int, of "ln b"]
hoelzl@47694
   168
    show "integrable M (\<lambda>x. D x * (ln b * log b (D x)))" 
hoelzl@47694
   169
      by (simp add: ac_simps)
hoelzl@43340
   170
  next
hoelzl@47694
   171
    show "emeasure M {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<noteq> 0"
hoelzl@43340
   172
    proof
hoelzl@47694
   173
      assume eq_0: "emeasure M {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} = 0"
hoelzl@47694
   174
      then have disj: "AE x in M. D x = 1 \<or> D x = 0"
immler@50244
   175
        using D(1) by (auto intro!: AE_I[OF subset_refl] sets.sets_Collect)
hoelzl@43340
   176
wenzelm@53015
   177
      have "emeasure M {x\<in>space M. D x = 1} = (\<integral>\<^sup>+ x. indicator {x\<in>space M. D x = 1} x \<partial>M)"
hoelzl@43340
   178
        using D(1) by auto
wenzelm@53015
   179
      also have "\<dots> = (\<integral>\<^sup>+ x. ereal (D x) \<partial>M)"
hoelzl@56996
   180
        using disj by (auto intro!: nn_integral_cong_AE simp: indicator_def one_ereal_def)
hoelzl@47694
   181
      finally have "AE x in M. D x = 1"
hoelzl@47694
   182
        using D D_pos by (intro AE_I_eq_1) auto
wenzelm@53015
   183
      then have "(\<integral>\<^sup>+x. indicator A x\<partial>M) = (\<integral>\<^sup>+x. ereal (D x) * indicator A x\<partial>M)"
hoelzl@56996
   184
        by (intro nn_integral_cong_AE) (auto simp: one_ereal_def[symmetric])
hoelzl@47694
   185
      also have "\<dots> = density M D A"
wenzelm@61808
   186
        using \<open>A \<in> sets M\<close> D by (simp add: emeasure_density)
wenzelm@61808
   187
      finally show False using \<open>A \<in> sets M\<close> \<open>emeasure (density M D) A \<noteq> emeasure M A\<close> by simp
hoelzl@43340
   188
    qed
hoelzl@43340
   189
    show "{x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<in> sets M"
immler@50244
   190
      using D(1) by (auto intro: sets.sets_Collect_conj)
hoelzl@43340
   191
hoelzl@47694
   192
    show "AE t in M. t \<in> {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<longrightarrow>
hoelzl@47694
   193
      D t - indicator ?D_set t \<noteq> D t * (ln b * log b (D t))"
hoelzl@43340
   194
      using D(2)
hoelzl@47694
   195
    proof (eventually_elim, safe)
hoelzl@47694
   196
      fix t assume Dt: "t \<in> space M" "D t \<noteq> 1" "D t \<noteq> 0" "0 \<le> D t"
hoelzl@47694
   197
        and eq: "D t - indicator ?D_set t = D t * (ln b * log b (D t))"
hoelzl@43340
   198
hoelzl@43340
   199
      have "D t - 1 = D t - indicator ?D_set t"
hoelzl@43340
   200
        using Dt by simp
hoelzl@43340
   201
      also note eq
hoelzl@47694
   202
      also have "D t * (ln b * log b (D t)) = - D t * ln (1 / D t)"
wenzelm@61808
   203
        using b_gt_1 \<open>D t \<noteq> 0\<close> \<open>0 \<le> D t\<close>
hoelzl@47694
   204
        by (simp add: log_def ln_div less_le)
hoelzl@43340
   205
      finally have "ln (1 / D t) = 1 / D t - 1"
wenzelm@61808
   206
        using \<open>D t \<noteq> 0\<close> by (auto simp: field_simps)
wenzelm@61808
   207
      from ln_eq_minus_one[OF _ this] \<open>D t \<noteq> 0\<close> \<open>0 \<le> D t\<close> \<open>D t \<noteq> 1\<close>
hoelzl@43340
   208
      show False by auto
hoelzl@43340
   209
    qed
hoelzl@43340
   210
hoelzl@47694
   211
    show "AE t in M. D t - indicator ?D_set t \<le> D t * (ln b * log b (D t))"
hoelzl@47694
   212
      using D(2) AE_space
hoelzl@47694
   213
    proof eventually_elim
hoelzl@47694
   214
      fix t assume "t \<in> space M" "0 \<le> D t"
hoelzl@47694
   215
      show "D t - indicator ?D_set t \<le> D t * (ln b * log b (D t))"
hoelzl@43340
   216
      proof cases
hoelzl@43340
   217
        assume asm: "D t \<noteq> 0"
wenzelm@61808
   218
        then have "0 < D t" using \<open>0 \<le> D t\<close> by auto
hoelzl@43340
   219
        then have "0 < 1 / D t" by auto
hoelzl@43340
   220
        have "D t - indicator ?D_set t \<le> - D t * (1 / D t - 1)"
wenzelm@61808
   221
          using asm \<open>t \<in> space M\<close> by (simp add: field_simps)
hoelzl@43340
   222
        also have "- D t * (1 / D t - 1) \<le> - D t * ln (1 / D t)"
wenzelm@61808
   223
          using ln_le_minus_one \<open>0 < 1 / D t\<close> by (intro mult_left_mono_neg) auto
hoelzl@47694
   224
        also have "\<dots> = D t * (ln b * log b (D t))"
wenzelm@61808
   225
          using \<open>0 < D t\<close> b_gt_1
hoelzl@47694
   226
          by (simp_all add: log_def ln_div)
hoelzl@43340
   227
        finally show ?thesis by simp
hoelzl@43340
   228
      qed simp
hoelzl@43340
   229
    qed
hoelzl@43340
   230
  qed
hoelzl@47694
   231
  also have "\<dots> = (\<integral> x. ln b * (D x * log b (D x)) \<partial>M)"
hoelzl@47694
   232
    by (simp add: ac_simps)
hoelzl@47694
   233
  also have "\<dots> = ln b * (\<integral> x. D x * log b (D x) \<partial>M)"
hoelzl@56993
   234
    using int by simp
hoelzl@47694
   235
  finally show ?thesis
hoelzl@47694
   236
    using b_gt_1 D by (subst KL_density) (auto simp: zero_less_mult_iff)
hoelzl@43340
   237
qed
hoelzl@43340
   238
hoelzl@47694
   239
lemma (in sigma_finite_measure) KL_same_eq_0: "KL_divergence b M M = 0"
hoelzl@43340
   240
proof -
hoelzl@47694
   241
  have "AE x in M. 1 = RN_deriv M M x"
hoelzl@43340
   242
  proof (rule RN_deriv_unique)
hoelzl@47694
   243
    show "(\<lambda>x. 1) \<in> borel_measurable M" "AE x in M. 0 \<le> (1 :: ereal)" by auto
hoelzl@47694
   244
    show "density M (\<lambda>x. 1) = M"
hoelzl@47694
   245
      apply (auto intro!: measure_eqI emeasure_density)
hoelzl@47694
   246
      apply (subst emeasure_density)
hoelzl@47694
   247
      apply auto
hoelzl@47694
   248
      done
hoelzl@43340
   249
  qed
lp15@61609
   250
  then have "AE x in M. log b (real_of_ereal (RN_deriv M M x)) = 0"
hoelzl@43340
   251
    by (elim AE_mp) simp
hoelzl@56993
   252
  from integral_cong_AE[OF _ _ this]
wenzelm@53015
   253
  have "integral\<^sup>L M (entropy_density b M M) = 0"
hoelzl@43340
   254
    by (simp add: entropy_density_def comp_def)
hoelzl@47694
   255
  then show "KL_divergence b M M = 0"
hoelzl@43340
   256
    unfolding KL_divergence_def
hoelzl@47694
   257
    by auto
hoelzl@43340
   258
qed
hoelzl@43340
   259
hoelzl@47694
   260
lemma (in information_space) KL_eq_0_iff_eq:
hoelzl@47694
   261
  fixes D :: "'a \<Rightarrow> real"
hoelzl@47694
   262
  assumes "prob_space (density M D)"
hoelzl@47694
   263
  assumes D: "D \<in> borel_measurable M" "AE x in M. 0 \<le> D x"
hoelzl@47694
   264
  assumes int: "integrable M (\<lambda>x. D x * log b (D x))"
hoelzl@47694
   265
  shows "KL_divergence b M (density M D) = 0 \<longleftrightarrow> density M D = M"
hoelzl@47694
   266
  using KL_same_eq_0[of b] KL_gt_0[OF assms]
hoelzl@47694
   267
  by (auto simp: less_le)
hoelzl@43340
   268
hoelzl@47694
   269
lemma (in information_space) KL_eq_0_iff_eq_ac:
hoelzl@47694
   270
  fixes D :: "'a \<Rightarrow> real"
hoelzl@47694
   271
  assumes "prob_space N"
hoelzl@47694
   272
  assumes ac: "absolutely_continuous M N" "sets N = sets M"
hoelzl@47694
   273
  assumes int: "integrable N (entropy_density b M N)"
hoelzl@47694
   274
  shows "KL_divergence b M N = 0 \<longleftrightarrow> N = M"
hoelzl@41833
   275
proof -
hoelzl@47694
   276
  interpret N: prob_space N by fact
hoelzl@47694
   277
  have "finite_measure N" by unfold_locales
hoelzl@47694
   278
  from real_RN_deriv[OF this ac] guess D . note D = this
hoelzl@47694
   279
  
hoelzl@47694
   280
  have "N = density M (RN_deriv M N)"
hoelzl@47694
   281
    using ac by (rule density_RN_deriv[symmetric])
hoelzl@47694
   282
  also have "\<dots> = density M D"
hoelzl@56993
   283
    using D by (auto intro!: density_cong)
hoelzl@47694
   284
  finally have N: "N = density M D" .
hoelzl@41833
   285
hoelzl@47694
   286
  from absolutely_continuous_AE[OF ac(2,1) D(2)] D b_gt_1 ac measurable_entropy_density
hoelzl@47694
   287
  have "integrable N (\<lambda>x. log b (D x))"
hoelzl@47694
   288
    by (intro integrable_cong_AE[THEN iffD2, OF _ _ _ int])
hoelzl@47694
   289
       (auto simp: N entropy_density_def)
hoelzl@47694
   290
  with D b_gt_1 have "integrable M (\<lambda>x. D x * log b (D x))"
hoelzl@56993
   291
    by (subst integrable_real_density[symmetric]) (auto simp: N[symmetric] comp_def)
wenzelm@61808
   292
  with \<open>prob_space N\<close> D show ?thesis
hoelzl@47694
   293
    unfolding N
hoelzl@47694
   294
    by (intro KL_eq_0_iff_eq) auto
hoelzl@41833
   295
qed
hoelzl@41833
   296
hoelzl@47694
   297
lemma (in information_space) KL_nonneg:
hoelzl@47694
   298
  assumes "prob_space (density M D)"
hoelzl@47694
   299
  assumes D: "D \<in> borel_measurable M" "AE x in M. 0 \<le> D x"
hoelzl@47694
   300
  assumes int: "integrable M (\<lambda>x. D x * log b (D x))"
hoelzl@47694
   301
  shows "0 \<le> KL_divergence b M (density M D)"
hoelzl@47694
   302
  using KL_gt_0[OF assms] by (cases "density M D = M") (auto simp: KL_same_eq_0)
hoelzl@40859
   303
hoelzl@47694
   304
lemma (in sigma_finite_measure) KL_density_density_nonneg:
hoelzl@47694
   305
  fixes f g :: "'a \<Rightarrow> real"
hoelzl@47694
   306
  assumes "1 < b"
hoelzl@47694
   307
  assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "prob_space (density M f)"
hoelzl@47694
   308
  assumes g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x" "prob_space (density M g)"
hoelzl@47694
   309
  assumes ac: "AE x in M. f x = 0 \<longrightarrow> g x = 0"
hoelzl@47694
   310
  assumes int: "integrable M (\<lambda>x. g x * log b (g x / f x))"
hoelzl@47694
   311
  shows "0 \<le> KL_divergence b (density M f) (density M g)"
hoelzl@47694
   312
proof -
hoelzl@47694
   313
  interpret Mf: prob_space "density M f" by fact
wenzelm@61169
   314
  interpret Mf: information_space "density M f" b by standard fact
hoelzl@47694
   315
  have eq: "density (density M f) (\<lambda>x. g x / f x) = density M g" (is "?DD = _")
hoelzl@47694
   316
    using f g ac by (subst density_density_divide) simp_all
hoelzl@36080
   317
hoelzl@47694
   318
  have "0 \<le> KL_divergence b (density M f) (density (density M f) (\<lambda>x. g x / f x))"
hoelzl@47694
   319
  proof (rule Mf.KL_nonneg)
hoelzl@47694
   320
    show "prob_space ?DD" unfolding eq by fact
hoelzl@47694
   321
    from f g show "(\<lambda>x. g x / f x) \<in> borel_measurable (density M f)"
hoelzl@47694
   322
      by auto
hoelzl@47694
   323
    show "AE x in density M f. 0 \<le> g x / f x"
hoelzl@56571
   324
      using f g by (auto simp: AE_density)
hoelzl@47694
   325
    show "integrable (density M f) (\<lambda>x. g x / f x * log b (g x / f x))"
wenzelm@61808
   326
      using \<open>1 < b\<close> f g ac
hoelzl@56993
   327
      by (subst integrable_density)
hoelzl@47694
   328
         (auto intro!: integrable_cong_AE[THEN iffD2, OF _ _ _ int] measurable_If)
hoelzl@47694
   329
  qed
hoelzl@47694
   330
  also have "\<dots> = KL_divergence b (density M f) (density M g)"
hoelzl@47694
   331
    using f g ac by (subst density_density_divide) simp_all
hoelzl@47694
   332
  finally show ?thesis .
hoelzl@36080
   333
qed
hoelzl@36080
   334
wenzelm@61808
   335
subsection \<open>Finite Entropy\<close>
hoelzl@49803
   336
hoelzl@49803
   337
definition (in information_space) 
hoelzl@49803
   338
  "finite_entropy S X f \<longleftrightarrow> distributed M S X f \<and> integrable S (\<lambda>x. f x * log b (f x))"
hoelzl@49803
   339
hoelzl@49803
   340
lemma (in information_space) finite_entropy_simple_function:
hoelzl@49803
   341
  assumes X: "simple_function M X"
hoelzl@49803
   342
  shows "finite_entropy (count_space (X`space M)) X (\<lambda>a. measure M {x \<in> space M. X x = a})"
hoelzl@49803
   343
  unfolding finite_entropy_def
hoelzl@49803
   344
proof
hoelzl@49803
   345
  have [simp]: "finite (X ` space M)"
hoelzl@49803
   346
    using X by (auto simp: simple_function_def)
hoelzl@49803
   347
  then show "integrable (count_space (X ` space M))
hoelzl@49803
   348
     (\<lambda>x. prob {xa \<in> space M. X xa = x} * log b (prob {xa \<in> space M. X xa = x}))"
hoelzl@49803
   349
    by (rule integrable_count_space)
hoelzl@49803
   350
  have d: "distributed M (count_space (X ` space M)) X (\<lambda>x. ereal (if x \<in> X`space M then prob {xa \<in> space M. X xa = x} else 0))"
hoelzl@49803
   351
    by (rule distributed_simple_function_superset[OF X]) (auto intro!: arg_cong[where f=prob])
hoelzl@49803
   352
  show "distributed M (count_space (X ` space M)) X (\<lambda>x. ereal (prob {xa \<in> space M. X xa = x}))"
hoelzl@49803
   353
    by (rule distributed_cong_density[THEN iffD1, OF _ _ _ d]) auto
hoelzl@49803
   354
qed
hoelzl@49803
   355
hoelzl@49803
   356
lemma distributed_transform_AE:
hoelzl@49803
   357
  assumes T: "T \<in> measurable P Q" "absolutely_continuous Q (distr P Q T)"
hoelzl@49803
   358
  assumes g: "distributed M Q Y g"
hoelzl@49803
   359
  shows "AE x in P. 0 \<le> g (T x)"
hoelzl@49803
   360
  using g
hoelzl@49803
   361
  apply (subst AE_distr_iff[symmetric, OF T(1)])
hoelzl@50003
   362
  apply simp
hoelzl@49803
   363
  apply (rule absolutely_continuous_AE[OF _ T(2)])
hoelzl@49803
   364
  apply simp
hoelzl@49803
   365
  apply (simp add: distributed_AE)
hoelzl@49803
   366
  done
hoelzl@49803
   367
hoelzl@49803
   368
lemma ac_fst:
hoelzl@49803
   369
  assumes "sigma_finite_measure T"
wenzelm@53015
   370
  shows "absolutely_continuous S (distr (S \<Otimes>\<^sub>M T) S fst)"
hoelzl@49803
   371
proof -
hoelzl@49803
   372
  interpret sigma_finite_measure T by fact
wenzelm@53374
   373
  { fix A assume A: "A \<in> sets S" "emeasure S A = 0"
wenzelm@53374
   374
    then have "fst -` A \<inter> space (S \<Otimes>\<^sub>M T) = A \<times> space T"
immler@50244
   375
      by (auto simp: space_pair_measure dest!: sets.sets_into_space)
wenzelm@53374
   376
    with A have "emeasure (S \<Otimes>\<^sub>M T) (fst -` A \<inter> space (S \<Otimes>\<^sub>M T)) = 0"
hoelzl@49803
   377
      by (simp add: emeasure_pair_measure_Times) }
hoelzl@49803
   378
  then show ?thesis
hoelzl@49803
   379
    unfolding absolutely_continuous_def
hoelzl@49803
   380
    apply (auto simp: null_sets_distr_iff)
hoelzl@49803
   381
    apply (auto simp: null_sets_def intro!: measurable_sets)
hoelzl@49803
   382
    done
hoelzl@49803
   383
qed
hoelzl@49803
   384
hoelzl@49803
   385
lemma ac_snd:
hoelzl@49803
   386
  assumes "sigma_finite_measure T"
wenzelm@53015
   387
  shows "absolutely_continuous T (distr (S \<Otimes>\<^sub>M T) T snd)"
hoelzl@49803
   388
proof -
hoelzl@49803
   389
  interpret sigma_finite_measure T by fact
wenzelm@53374
   390
  { fix A assume A: "A \<in> sets T" "emeasure T A = 0"
wenzelm@53374
   391
    then have "snd -` A \<inter> space (S \<Otimes>\<^sub>M T) = space S \<times> A"
immler@50244
   392
      by (auto simp: space_pair_measure dest!: sets.sets_into_space)
wenzelm@53374
   393
    with A have "emeasure (S \<Otimes>\<^sub>M T) (snd -` A \<inter> space (S \<Otimes>\<^sub>M T)) = 0"
hoelzl@49803
   394
      by (simp add: emeasure_pair_measure_Times) }
hoelzl@49803
   395
  then show ?thesis
hoelzl@49803
   396
    unfolding absolutely_continuous_def
hoelzl@49803
   397
    apply (auto simp: null_sets_distr_iff)
hoelzl@49803
   398
    apply (auto simp: null_sets_def intro!: measurable_sets)
hoelzl@49803
   399
    done
hoelzl@49803
   400
qed
hoelzl@49803
   401
hoelzl@56993
   402
lemma integrable_cong_AE_imp:
hoelzl@56993
   403
  "integrable M g \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> (AE x in M. g x = f x) \<Longrightarrow> integrable M f"
hoelzl@56993
   404
  using integrable_cong_AE[of f M g] by (auto simp: eq_commute)
hoelzl@49803
   405
hoelzl@49803
   406
lemma (in information_space) finite_entropy_integrable:
hoelzl@49803
   407
  "finite_entropy S X Px \<Longrightarrow> integrable S (\<lambda>x. Px x * log b (Px x))"
hoelzl@49803
   408
  unfolding finite_entropy_def by auto
hoelzl@49803
   409
hoelzl@49803
   410
lemma (in information_space) finite_entropy_distributed:
hoelzl@49803
   411
  "finite_entropy S X Px \<Longrightarrow> distributed M S X Px"
hoelzl@49803
   412
  unfolding finite_entropy_def by auto
hoelzl@49803
   413
hoelzl@49803
   414
lemma (in information_space) finite_entropy_integrable_transform:
hoelzl@49803
   415
  assumes Fx: "finite_entropy S X Px"
hoelzl@49803
   416
  assumes Fy: "distributed M T Y Py"
hoelzl@49803
   417
    and "X = (\<lambda>x. f (Y x))"
hoelzl@49803
   418
    and "f \<in> measurable T S"
hoelzl@49803
   419
  shows "integrable T (\<lambda>x. Py x * log b (Px (f x)))"
hoelzl@49803
   420
  using assms unfolding finite_entropy_def
hoelzl@49803
   421
  using distributed_transform_integrable[of M T Y Py S X Px f "\<lambda>x. log b (Px x)"]
hoelzl@50003
   422
  by auto
hoelzl@49803
   423
wenzelm@61808
   424
subsection \<open>Mutual Information\<close>
hoelzl@39097
   425
hoelzl@36080
   426
definition (in prob_space)
hoelzl@38656
   427
  "mutual_information b S T X Y =
wenzelm@53015
   428
    KL_divergence b (distr M S X \<Otimes>\<^sub>M distr M T Y) (distr M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)))"
hoelzl@36080
   429
hoelzl@47694
   430
lemma (in information_space) mutual_information_indep_vars:
hoelzl@43340
   431
  fixes S T X Y
wenzelm@53015
   432
  defines "P \<equiv> distr M S X \<Otimes>\<^sub>M distr M T Y"
wenzelm@53015
   433
  defines "Q \<equiv> distr M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x))"
hoelzl@43340
   434
  shows "indep_var S X T Y \<longleftrightarrow>
hoelzl@43340
   435
    (random_variable S X \<and> random_variable T Y \<and>
hoelzl@47694
   436
      absolutely_continuous P Q \<and> integrable Q (entropy_density b P Q) \<and>
hoelzl@47694
   437
      mutual_information b S T X Y = 0)"
hoelzl@47694
   438
  unfolding indep_var_distribution_eq
hoelzl@43340
   439
proof safe
hoelzl@50003
   440
  assume rv[measurable]: "random_variable S X" "random_variable T Y"
hoelzl@43340
   441
hoelzl@47694
   442
  interpret X: prob_space "distr M S X"
hoelzl@47694
   443
    by (rule prob_space_distr) fact
hoelzl@47694
   444
  interpret Y: prob_space "distr M T Y"
hoelzl@47694
   445
    by (rule prob_space_distr) fact
wenzelm@61169
   446
  interpret XY: pair_prob_space "distr M S X" "distr M T Y" by standard
wenzelm@61169
   447
  interpret P: information_space P b unfolding P_def by standard (rule b_gt_1)
hoelzl@43340
   448
hoelzl@47694
   449
  interpret Q: prob_space Q unfolding Q_def
hoelzl@50003
   450
    by (rule prob_space_distr) simp
hoelzl@43340
   451
wenzelm@53015
   452
  { assume "distr M S X \<Otimes>\<^sub>M distr M T Y = distr M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x))"
hoelzl@47694
   453
    then have [simp]: "Q = P"  unfolding Q_def P_def by simp
hoelzl@43340
   454
hoelzl@47694
   455
    show ac: "absolutely_continuous P Q" by (simp add: absolutely_continuous_def)
hoelzl@47694
   456
    then have ed: "entropy_density b P Q \<in> borel_measurable P"
hoelzl@56993
   457
      by simp
hoelzl@43340
   458
hoelzl@47694
   459
    have "AE x in P. 1 = RN_deriv P Q x"
hoelzl@47694
   460
    proof (rule P.RN_deriv_unique)
hoelzl@47694
   461
      show "density P (\<lambda>x. 1) = Q"
wenzelm@61808
   462
        unfolding \<open>Q = P\<close> by (intro measure_eqI) (auto simp: emeasure_density)
hoelzl@47694
   463
    qed auto
hoelzl@47694
   464
    then have ae_0: "AE x in P. entropy_density b P Q x = 0"
hoelzl@47694
   465
      by eventually_elim (auto simp: entropy_density_def)
hoelzl@56993
   466
    then have "integrable P (entropy_density b P Q) \<longleftrightarrow> integrable Q (\<lambda>x. 0::real)"
wenzelm@61808
   467
      using ed unfolding \<open>Q = P\<close> by (intro integrable_cong_AE) auto
hoelzl@47694
   468
    then show "integrable Q (entropy_density b P Q)" by simp
hoelzl@43340
   469
hoelzl@56993
   470
    from ae_0 have "mutual_information b S T X Y = (\<integral>x. 0 \<partial>P)"
wenzelm@61808
   471
      unfolding mutual_information_def KL_divergence_def P_def[symmetric] Q_def[symmetric] \<open>Q = P\<close>
hoelzl@56993
   472
      by (intro integral_cong_AE) auto
hoelzl@56993
   473
    then show "mutual_information b S T X Y = 0"
hoelzl@56993
   474
      by simp }
hoelzl@43340
   475
hoelzl@47694
   476
  { assume ac: "absolutely_continuous P Q"
hoelzl@47694
   477
    assume int: "integrable Q (entropy_density b P Q)"
hoelzl@47694
   478
    assume I_eq_0: "mutual_information b S T X Y = 0"
hoelzl@43340
   479
hoelzl@47694
   480
    have eq: "Q = P"
hoelzl@47694
   481
    proof (rule P.KL_eq_0_iff_eq_ac[THEN iffD1])
hoelzl@47694
   482
      show "prob_space Q" by unfold_locales
hoelzl@47694
   483
      show "absolutely_continuous P Q" by fact
hoelzl@47694
   484
      show "integrable Q (entropy_density b P Q)" by fact
hoelzl@47694
   485
      show "sets Q = sets P" by (simp add: P_def Q_def sets_pair_measure)
hoelzl@47694
   486
      show "KL_divergence b P Q = 0"
hoelzl@47694
   487
        using I_eq_0 unfolding mutual_information_def by (simp add: P_def Q_def)
hoelzl@47694
   488
    qed
wenzelm@53015
   489
    then show "distr M S X \<Otimes>\<^sub>M distr M T Y = distr M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x))"
hoelzl@47694
   490
      unfolding P_def Q_def .. }
hoelzl@43340
   491
qed
hoelzl@43340
   492
hoelzl@40859
   493
abbreviation (in information_space)
hoelzl@40859
   494
  mutual_information_Pow ("\<I>'(_ ; _')") where
hoelzl@47694
   495
  "\<I>(X ; Y) \<equiv> mutual_information b (count_space (X`space M)) (count_space (Y`space M)) X Y"
hoelzl@41689
   496
hoelzl@47694
   497
lemma (in information_space)
hoelzl@47694
   498
  fixes Pxy :: "'b \<times> 'c \<Rightarrow> real" and Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
hoelzl@49803
   499
  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
hoelzl@49803
   500
  assumes Fx: "finite_entropy S X Px" and Fy: "finite_entropy T Y Py"
wenzelm@53015
   501
  assumes Fxy: "finite_entropy (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) Pxy"
hoelzl@49803
   502
  defines "f \<equiv> \<lambda>x. Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x)))"
wenzelm@53015
   503
  shows mutual_information_distr': "mutual_information b S T X Y = integral\<^sup>L (S \<Otimes>\<^sub>M T) f" (is "?M = ?R")
hoelzl@49803
   504
    and mutual_information_nonneg': "0 \<le> mutual_information b S T X Y"
hoelzl@49803
   505
proof -
hoelzl@49803
   506
  have Px: "distributed M S X Px"
hoelzl@49803
   507
    using Fx by (auto simp: finite_entropy_def)
hoelzl@49803
   508
  have Py: "distributed M T Y Py"
hoelzl@49803
   509
    using Fy by (auto simp: finite_entropy_def)
wenzelm@53015
   510
  have Pxy: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) Pxy"
hoelzl@49803
   511
    using Fxy by (auto simp: finite_entropy_def)
hoelzl@49803
   512
hoelzl@49803
   513
  have X: "random_variable S X"
hoelzl@50003
   514
    using Px by auto
hoelzl@49803
   515
  have Y: "random_variable T Y"
hoelzl@50003
   516
    using Py by auto
hoelzl@49803
   517
  interpret S: sigma_finite_measure S by fact
hoelzl@49803
   518
  interpret T: sigma_finite_measure T by fact
hoelzl@49803
   519
  interpret ST: pair_sigma_finite S T ..
hoelzl@49803
   520
  interpret X: prob_space "distr M S X" using X by (rule prob_space_distr)
hoelzl@49803
   521
  interpret Y: prob_space "distr M T Y" using Y by (rule prob_space_distr)
hoelzl@49803
   522
  interpret XY: pair_prob_space "distr M S X" "distr M T Y" ..
wenzelm@53015
   523
  let ?P = "S \<Otimes>\<^sub>M T"
hoelzl@49803
   524
  let ?D = "distr M ?P (\<lambda>x. (X x, Y x))"
hoelzl@49803
   525
hoelzl@49803
   526
  { fix A assume "A \<in> sets S"
hoelzl@49803
   527
    with X Y have "emeasure (distr M S X) A = emeasure ?D (A \<times> space T)"
hoelzl@49803
   528
      by (auto simp: emeasure_distr measurable_Pair measurable_space
hoelzl@49803
   529
               intro!: arg_cong[where f="emeasure M"]) }
hoelzl@49803
   530
  note marginal_eq1 = this
hoelzl@49803
   531
  { fix A assume "A \<in> sets T"
hoelzl@49803
   532
    with X Y have "emeasure (distr M T Y) A = emeasure ?D (space S \<times> A)"
hoelzl@49803
   533
      by (auto simp: emeasure_distr measurable_Pair measurable_space
hoelzl@49803
   534
               intro!: arg_cong[where f="emeasure M"]) }
hoelzl@49803
   535
  note marginal_eq2 = this
hoelzl@49803
   536
hoelzl@49803
   537
  have eq: "(\<lambda>x. ereal (Px (fst x) * Py (snd x))) = (\<lambda>(x, y). ereal (Px x) * ereal (Py y))"
hoelzl@49803
   538
    by auto
hoelzl@49803
   539
wenzelm@53015
   540
  have distr_eq: "distr M S X \<Otimes>\<^sub>M distr M T Y = density ?P (\<lambda>x. ereal (Px (fst x) * Py (snd x)))"
hoelzl@49803
   541
    unfolding Px(1)[THEN distributed_distr_eq_density] Py(1)[THEN distributed_distr_eq_density] eq
hoelzl@49803
   542
  proof (subst pair_measure_density)
hoelzl@49803
   543
    show "(\<lambda>x. ereal (Px x)) \<in> borel_measurable S" "(\<lambda>y. ereal (Py y)) \<in> borel_measurable T"
hoelzl@49803
   544
      "AE x in S. 0 \<le> ereal (Px x)" "AE y in T. 0 \<le> ereal (Py y)"
hoelzl@49803
   545
      using Px Py by (auto simp: distributed_def)
hoelzl@49803
   546
    show "sigma_finite_measure (density T Py)" unfolding Py(1)[THEN distributed_distr_eq_density, symmetric] ..
hoelzl@49803
   547
  qed (fact | simp)+
hoelzl@49803
   548
  
hoelzl@49803
   549
  have M: "?M = KL_divergence b (density ?P (\<lambda>x. ereal (Px (fst x) * Py (snd x)))) (density ?P (\<lambda>x. ereal (Pxy x)))"
hoelzl@49803
   550
    unfolding mutual_information_def distr_eq Pxy(1)[THEN distributed_distr_eq_density] ..
hoelzl@49803
   551
hoelzl@49803
   552
  from Px Py have f: "(\<lambda>x. Px (fst x) * Py (snd x)) \<in> borel_measurable ?P"
hoelzl@49803
   553
    by (intro borel_measurable_times) (auto intro: distributed_real_measurable measurable_fst'' measurable_snd'')
hoelzl@49803
   554
  have PxPy_nonneg: "AE x in ?P. 0 \<le> Px (fst x) * Py (snd x)"
hoelzl@49803
   555
  proof (rule ST.AE_pair_measure)
hoelzl@49803
   556
    show "{x \<in> space ?P. 0 \<le> Px (fst x) * Py (snd x)} \<in> sets ?P"
hoelzl@49803
   557
      using f by auto
hoelzl@49803
   558
    show "AE x in S. AE y in T. 0 \<le> Px (fst (x, y)) * Py (snd (x, y))"
hoelzl@49803
   559
      using Px Py by (auto simp: zero_le_mult_iff dest!: distributed_real_AE)
hoelzl@49803
   560
  qed
hoelzl@49803
   561
hoelzl@49803
   562
  have "(AE x in ?P. Px (fst x) = 0 \<longrightarrow> Pxy x = 0)"
hoelzl@49803
   563
    by (rule subdensity_real[OF measurable_fst Pxy Px]) auto
hoelzl@49803
   564
  moreover
hoelzl@49803
   565
  have "(AE x in ?P. Py (snd x) = 0 \<longrightarrow> Pxy x = 0)"
hoelzl@49803
   566
    by (rule subdensity_real[OF measurable_snd Pxy Py]) auto
hoelzl@49803
   567
  ultimately have ac: "AE x in ?P. Px (fst x) * Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
hoelzl@49803
   568
    by eventually_elim auto
hoelzl@49803
   569
hoelzl@49803
   570
  show "?M = ?R"
hoelzl@49803
   571
    unfolding M f_def
hoelzl@49803
   572
    using b_gt_1 f PxPy_nonneg Pxy[THEN distributed_real_measurable] Pxy[THEN distributed_real_AE] ac
hoelzl@49803
   573
    by (rule ST.KL_density_density)
hoelzl@49803
   574
hoelzl@49803
   575
  have X: "X = fst \<circ> (\<lambda>x. (X x, Y x))" and Y: "Y = snd \<circ> (\<lambda>x. (X x, Y x))"
hoelzl@49803
   576
    by auto
hoelzl@49803
   577
wenzelm@53015
   578
  have "integrable (S \<Otimes>\<^sub>M T) (\<lambda>x. Pxy x * log b (Pxy x) - Pxy x * log b (Px (fst x)) - Pxy x * log b (Py (snd x)))"
hoelzl@49803
   579
    using finite_entropy_integrable[OF Fxy]
hoelzl@49803
   580
    using finite_entropy_integrable_transform[OF Fx Pxy, of fst]
hoelzl@49803
   581
    using finite_entropy_integrable_transform[OF Fy Pxy, of snd]
hoelzl@49803
   582
    by simp
wenzelm@53015
   583
  moreover have "f \<in> borel_measurable (S \<Otimes>\<^sub>M T)"
hoelzl@49803
   584
    unfolding f_def using Px Py Pxy
hoelzl@49803
   585
    by (auto intro: distributed_real_measurable measurable_fst'' measurable_snd''
hoelzl@49803
   586
      intro!: borel_measurable_times borel_measurable_log borel_measurable_divide)
wenzelm@53015
   587
  ultimately have int: "integrable (S \<Otimes>\<^sub>M T) f"
hoelzl@49803
   588
    apply (rule integrable_cong_AE_imp)
hoelzl@49803
   589
    using
hoelzl@49803
   590
      distributed_transform_AE[OF measurable_fst ac_fst, of T, OF T Px]
hoelzl@49803
   591
      distributed_transform_AE[OF measurable_snd ac_snd, of _ _ _ _ S, OF T Py]
hoelzl@49803
   592
      subdensity_real[OF measurable_fst Pxy Px X]
hoelzl@49803
   593
      subdensity_real[OF measurable_snd Pxy Py Y]
hoelzl@49803
   594
      distributed_real_AE[OF Pxy]
hoelzl@49803
   595
    by eventually_elim
nipkow@56536
   596
       (auto simp: f_def log_divide_eq log_mult_eq field_simps zero_less_mult_iff)
hoelzl@49803
   597
hoelzl@49803
   598
  show "0 \<le> ?M" unfolding M
hoelzl@49803
   599
  proof (rule ST.KL_density_density_nonneg
hoelzl@49803
   600
    [OF b_gt_1 f PxPy_nonneg _ Pxy[THEN distributed_real_measurable] Pxy[THEN distributed_real_AE] _ ac int[unfolded f_def]])
wenzelm@53015
   601
    show "prob_space (density (S \<Otimes>\<^sub>M T) (\<lambda>x. ereal (Pxy x))) "
hoelzl@49803
   602
      unfolding distributed_distr_eq_density[OF Pxy, symmetric]
hoelzl@49803
   603
      using distributed_measurable[OF Pxy] by (rule prob_space_distr)
wenzelm@53015
   604
    show "prob_space (density (S \<Otimes>\<^sub>M T) (\<lambda>x. ereal (Px (fst x) * Py (snd x))))"
hoelzl@49803
   605
      unfolding distr_eq[symmetric] by unfold_locales
hoelzl@49803
   606
  qed
hoelzl@49803
   607
qed
hoelzl@49803
   608
hoelzl@49803
   609
hoelzl@49803
   610
lemma (in information_space)
hoelzl@49803
   611
  fixes Pxy :: "'b \<times> 'c \<Rightarrow> real" and Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
hoelzl@47694
   612
  assumes "sigma_finite_measure S" "sigma_finite_measure T"
hoelzl@47694
   613
  assumes Px: "distributed M S X Px" and Py: "distributed M T Y Py"
wenzelm@53015
   614
  assumes Pxy: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) Pxy"
hoelzl@47694
   615
  defines "f \<equiv> \<lambda>x. Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x)))"
wenzelm@53015
   616
  shows mutual_information_distr: "mutual_information b S T X Y = integral\<^sup>L (S \<Otimes>\<^sub>M T) f" (is "?M = ?R")
wenzelm@53015
   617
    and mutual_information_nonneg: "integrable (S \<Otimes>\<^sub>M T) f \<Longrightarrow> 0 \<le> mutual_information b S T X Y"
hoelzl@40859
   618
proof -
hoelzl@47694
   619
  have X: "random_variable S X"
hoelzl@47694
   620
    using Px by (auto simp: distributed_def)
hoelzl@47694
   621
  have Y: "random_variable T Y"
hoelzl@47694
   622
    using Py by (auto simp: distributed_def)
hoelzl@47694
   623
  interpret S: sigma_finite_measure S by fact
hoelzl@47694
   624
  interpret T: sigma_finite_measure T by fact
hoelzl@47694
   625
  interpret ST: pair_sigma_finite S T ..
hoelzl@47694
   626
  interpret X: prob_space "distr M S X" using X by (rule prob_space_distr)
hoelzl@47694
   627
  interpret Y: prob_space "distr M T Y" using Y by (rule prob_space_distr)
hoelzl@47694
   628
  interpret XY: pair_prob_space "distr M S X" "distr M T Y" ..
wenzelm@53015
   629
  let ?P = "S \<Otimes>\<^sub>M T"
hoelzl@47694
   630
  let ?D = "distr M ?P (\<lambda>x. (X x, Y x))"
hoelzl@47694
   631
hoelzl@47694
   632
  { fix A assume "A \<in> sets S"
hoelzl@47694
   633
    with X Y have "emeasure (distr M S X) A = emeasure ?D (A \<times> space T)"
hoelzl@47694
   634
      by (auto simp: emeasure_distr measurable_Pair measurable_space
hoelzl@47694
   635
               intro!: arg_cong[where f="emeasure M"]) }
hoelzl@47694
   636
  note marginal_eq1 = this
hoelzl@47694
   637
  { fix A assume "A \<in> sets T"
hoelzl@47694
   638
    with X Y have "emeasure (distr M T Y) A = emeasure ?D (space S \<times> A)"
hoelzl@47694
   639
      by (auto simp: emeasure_distr measurable_Pair measurable_space
hoelzl@47694
   640
               intro!: arg_cong[where f="emeasure M"]) }
hoelzl@47694
   641
  note marginal_eq2 = this
hoelzl@47694
   642
hoelzl@47694
   643
  have eq: "(\<lambda>x. ereal (Px (fst x) * Py (snd x))) = (\<lambda>(x, y). ereal (Px x) * ereal (Py y))"
hoelzl@47694
   644
    by auto
hoelzl@47694
   645
wenzelm@53015
   646
  have distr_eq: "distr M S X \<Otimes>\<^sub>M distr M T Y = density ?P (\<lambda>x. ereal (Px (fst x) * Py (snd x)))"
hoelzl@47694
   647
    unfolding Px(1)[THEN distributed_distr_eq_density] Py(1)[THEN distributed_distr_eq_density] eq
hoelzl@47694
   648
  proof (subst pair_measure_density)
hoelzl@47694
   649
    show "(\<lambda>x. ereal (Px x)) \<in> borel_measurable S" "(\<lambda>y. ereal (Py y)) \<in> borel_measurable T"
hoelzl@47694
   650
      "AE x in S. 0 \<le> ereal (Px x)" "AE y in T. 0 \<le> ereal (Py y)"
hoelzl@47694
   651
      using Px Py by (auto simp: distributed_def)
hoelzl@47694
   652
    show "sigma_finite_measure (density T Py)" unfolding Py(1)[THEN distributed_distr_eq_density, symmetric] ..
hoelzl@47694
   653
  qed (fact | simp)+
hoelzl@47694
   654
  
hoelzl@47694
   655
  have M: "?M = KL_divergence b (density ?P (\<lambda>x. ereal (Px (fst x) * Py (snd x)))) (density ?P (\<lambda>x. ereal (Pxy x)))"
hoelzl@47694
   656
    unfolding mutual_information_def distr_eq Pxy(1)[THEN distributed_distr_eq_density] ..
hoelzl@47694
   657
hoelzl@47694
   658
  from Px Py have f: "(\<lambda>x. Px (fst x) * Py (snd x)) \<in> borel_measurable ?P"
hoelzl@47694
   659
    by (intro borel_measurable_times) (auto intro: distributed_real_measurable measurable_fst'' measurable_snd'')
hoelzl@47694
   660
  have PxPy_nonneg: "AE x in ?P. 0 \<le> Px (fst x) * Py (snd x)"
hoelzl@47694
   661
  proof (rule ST.AE_pair_measure)
hoelzl@47694
   662
    show "{x \<in> space ?P. 0 \<le> Px (fst x) * Py (snd x)} \<in> sets ?P"
hoelzl@47694
   663
      using f by auto
hoelzl@47694
   664
    show "AE x in S. AE y in T. 0 \<le> Px (fst (x, y)) * Py (snd (x, y))"
hoelzl@47694
   665
      using Px Py by (auto simp: zero_le_mult_iff dest!: distributed_real_AE)
hoelzl@47694
   666
  qed
hoelzl@47694
   667
hoelzl@47694
   668
  have "(AE x in ?P. Px (fst x) = 0 \<longrightarrow> Pxy x = 0)"
hoelzl@47694
   669
    by (rule subdensity_real[OF measurable_fst Pxy Px]) auto
hoelzl@47694
   670
  moreover
hoelzl@47694
   671
  have "(AE x in ?P. Py (snd x) = 0 \<longrightarrow> Pxy x = 0)"
hoelzl@47694
   672
    by (rule subdensity_real[OF measurable_snd Pxy Py]) auto
hoelzl@47694
   673
  ultimately have ac: "AE x in ?P. Px (fst x) * Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
hoelzl@47694
   674
    by eventually_elim auto
hoelzl@47694
   675
hoelzl@47694
   676
  show "?M = ?R"
hoelzl@47694
   677
    unfolding M f_def
hoelzl@47694
   678
    using b_gt_1 f PxPy_nonneg Pxy[THEN distributed_real_measurable] Pxy[THEN distributed_real_AE] ac
hoelzl@47694
   679
    by (rule ST.KL_density_density)
hoelzl@47694
   680
wenzelm@53015
   681
  assume int: "integrable (S \<Otimes>\<^sub>M T) f"
hoelzl@47694
   682
  show "0 \<le> ?M" unfolding M
hoelzl@47694
   683
  proof (rule ST.KL_density_density_nonneg
hoelzl@47694
   684
    [OF b_gt_1 f PxPy_nonneg _ Pxy[THEN distributed_real_measurable] Pxy[THEN distributed_real_AE] _ ac int[unfolded f_def]])
wenzelm@53015
   685
    show "prob_space (density (S \<Otimes>\<^sub>M T) (\<lambda>x. ereal (Pxy x))) "
hoelzl@47694
   686
      unfolding distributed_distr_eq_density[OF Pxy, symmetric]
hoelzl@47694
   687
      using distributed_measurable[OF Pxy] by (rule prob_space_distr)
wenzelm@53015
   688
    show "prob_space (density (S \<Otimes>\<^sub>M T) (\<lambda>x. ereal (Px (fst x) * Py (snd x))))"
hoelzl@47694
   689
      unfolding distr_eq[symmetric] by unfold_locales
hoelzl@40859
   690
  qed
hoelzl@40859
   691
qed
hoelzl@40859
   692
hoelzl@40859
   693
lemma (in information_space)
hoelzl@47694
   694
  fixes Pxy :: "'b \<times> 'c \<Rightarrow> real" and Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
hoelzl@47694
   695
  assumes "sigma_finite_measure S" "sigma_finite_measure T"
hoelzl@56993
   696
  assumes Px[measurable]: "distributed M S X Px" and Py[measurable]: "distributed M T Y Py"
hoelzl@56993
   697
  assumes Pxy[measurable]: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) Pxy"
hoelzl@47694
   698
  assumes ae: "AE x in S. AE y in T. Pxy (x, y) = Px x * Py y"
hoelzl@47694
   699
  shows mutual_information_eq_0: "mutual_information b S T X Y = 0"
hoelzl@36624
   700
proof -
hoelzl@47694
   701
  interpret S: sigma_finite_measure S by fact
hoelzl@47694
   702
  interpret T: sigma_finite_measure T by fact
hoelzl@47694
   703
  interpret ST: pair_sigma_finite S T ..
hoelzl@36080
   704
wenzelm@53015
   705
  have "AE x in S \<Otimes>\<^sub>M T. Px (fst x) = 0 \<longrightarrow> Pxy x = 0"
hoelzl@47694
   706
    by (rule subdensity_real[OF measurable_fst Pxy Px]) auto
hoelzl@47694
   707
  moreover
wenzelm@53015
   708
  have "AE x in S \<Otimes>\<^sub>M T. Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
hoelzl@47694
   709
    by (rule subdensity_real[OF measurable_snd Pxy Py]) auto
hoelzl@47694
   710
  moreover 
wenzelm@53015
   711
  have "AE x in S \<Otimes>\<^sub>M T. Pxy x = Px (fst x) * Py (snd x)"
hoelzl@47694
   712
    using distributed_real_measurable[OF Px] distributed_real_measurable[OF Py] distributed_real_measurable[OF Pxy]
hoelzl@47694
   713
    by (intro ST.AE_pair_measure) (auto simp: ae intro!: measurable_snd'' measurable_fst'')
wenzelm@53015
   714
  ultimately have "AE x in S \<Otimes>\<^sub>M T. Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x))) = 0"
hoelzl@47694
   715
    by eventually_elim simp
wenzelm@53015
   716
  then have "(\<integral>x. Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x))) \<partial>(S \<Otimes>\<^sub>M T)) = (\<integral>x. 0 \<partial>(S \<Otimes>\<^sub>M T))"
hoelzl@56993
   717
    by (intro integral_cong_AE) auto
hoelzl@47694
   718
  then show ?thesis
hoelzl@47694
   719
    by (subst mutual_information_distr[OF assms(1-5)]) simp
hoelzl@36080
   720
qed
hoelzl@36080
   721
hoelzl@47694
   722
lemma (in information_space) mutual_information_simple_distributed:
hoelzl@47694
   723
  assumes X: "simple_distributed M X Px" and Y: "simple_distributed M Y Py"
hoelzl@47694
   724
  assumes XY: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"
hoelzl@47694
   725
  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)))"
hoelzl@47694
   726
proof (subst mutual_information_distr[OF _ _ simple_distributed[OF X] simple_distributed[OF Y] simple_distributed_joint[OF XY]])
hoelzl@47694
   727
  note fin = simple_distributed_joint_finite[OF XY, simp]
hoelzl@47694
   728
  show "sigma_finite_measure (count_space (X ` space M))"
hoelzl@47694
   729
    by (simp add: sigma_finite_measure_count_space_finite)
hoelzl@47694
   730
  show "sigma_finite_measure (count_space (Y ` space M))"
hoelzl@47694
   731
    by (simp add: sigma_finite_measure_count_space_finite)
hoelzl@47694
   732
  let ?Pxy = "\<lambda>x. (if x \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy x else 0)"
hoelzl@47694
   733
  let ?f = "\<lambda>x. ?Pxy x * log b (?Pxy x / (Px (fst x) * Py (snd x)))"
hoelzl@47694
   734
  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)"
hoelzl@47694
   735
    by auto
wenzelm@53015
   736
  with fin show "(\<integral> x. ?f x \<partial>(count_space (X ` space M) \<Otimes>\<^sub>M count_space (Y ` space M))) =
hoelzl@47694
   737
    (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / (Px x * Py y)))"
haftmann@57418
   738
    by (auto simp add: pair_measure_count_space lebesgue_integral_count_space_finite setsum.If_cases split_beta'
haftmann@57418
   739
             intro!: setsum.cong)
hoelzl@47694
   740
qed
hoelzl@36080
   741
hoelzl@47694
   742
lemma (in information_space)
hoelzl@47694
   743
  fixes Pxy :: "'b \<times> 'c \<Rightarrow> real" and Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
hoelzl@47694
   744
  assumes Px: "simple_distributed M X Px" and Py: "simple_distributed M Y Py"
hoelzl@47694
   745
  assumes Pxy: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"
hoelzl@47694
   746
  assumes ae: "\<forall>x\<in>space M. Pxy (X x, Y x) = Px (X x) * Py (Y x)"
hoelzl@47694
   747
  shows mutual_information_eq_0_simple: "\<I>(X ; Y) = 0"
hoelzl@47694
   748
proof (subst mutual_information_simple_distributed[OF Px Py Pxy])
hoelzl@47694
   749
  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))) =
hoelzl@47694
   750
    (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. 0)"
haftmann@57418
   751
    by (intro setsum.cong) (auto simp: ae)
hoelzl@47694
   752
  then show "(\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M.
hoelzl@47694
   753
    Pxy (x, y) * log b (Pxy (x, y) / (Px x * Py y))) = 0" by simp
hoelzl@47694
   754
qed
hoelzl@36080
   755
wenzelm@61808
   756
subsection \<open>Entropy\<close>
hoelzl@39097
   757
hoelzl@47694
   758
definition (in prob_space) entropy :: "real \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> real" where
hoelzl@47694
   759
  "entropy b S X = - KL_divergence b S (distr M S X)"
hoelzl@47694
   760
hoelzl@40859
   761
abbreviation (in information_space)
hoelzl@40859
   762
  entropy_Pow ("\<H>'(_')") where
hoelzl@47694
   763
  "\<H>(X) \<equiv> entropy b (count_space (X`space M)) X"
hoelzl@41981
   764
hoelzl@49791
   765
lemma (in prob_space) distributed_RN_deriv:
hoelzl@49791
   766
  assumes X: "distributed M S X Px"
hoelzl@49791
   767
  shows "AE x in S. RN_deriv S (density S Px) x = Px x"
hoelzl@49791
   768
proof -
hoelzl@49791
   769
  note D = distributed_measurable[OF X] distributed_borel_measurable[OF X] distributed_AE[OF X]
hoelzl@49791
   770
  interpret X: prob_space "distr M S X"
hoelzl@49791
   771
    using D(1) by (rule prob_space_distr)
hoelzl@49791
   772
wenzelm@61169
   773
  have sf: "sigma_finite_measure (distr M S X)" by standard
hoelzl@49791
   774
  show ?thesis
hoelzl@49791
   775
    using D
hoelzl@49791
   776
    apply (subst eq_commute)
hoelzl@49791
   777
    apply (intro RN_deriv_unique_sigma_finite)
hoelzl@56571
   778
    apply (auto simp: distributed_distr_eq_density[symmetric, OF X] sf measure_nonneg)
hoelzl@49791
   779
    done
hoelzl@49791
   780
qed
hoelzl@49791
   781
hoelzl@49788
   782
lemma (in information_space)
hoelzl@47694
   783
  fixes X :: "'a \<Rightarrow> 'b"
hoelzl@56993
   784
  assumes X[measurable]: "distributed M MX X f"
hoelzl@49788
   785
  shows entropy_distr: "entropy b MX X = - (\<integral>x. f x * log b (f x) \<partial>MX)" (is ?eq)
hoelzl@49788
   786
proof -
hoelzl@49785
   787
  note D = distributed_measurable[OF X] distributed_borel_measurable[OF X] distributed_AE[OF X]
hoelzl@49791
   788
  note ae = distributed_RN_deriv[OF X]
hoelzl@49788
   789
lp15@61609
   790
  have ae_eq: "AE x in distr M MX X. log b (real_of_ereal (RN_deriv MX (distr M MX X) x)) =
hoelzl@49785
   791
    log b (f x)"
hoelzl@49785
   792
    unfolding distributed_distr_eq_density[OF X]
hoelzl@49785
   793
    apply (subst AE_density)
hoelzl@49785
   794
    using D apply simp
hoelzl@49785
   795
    using ae apply eventually_elim
hoelzl@49785
   796
    apply auto
hoelzl@49785
   797
    done
hoelzl@49788
   798
hoelzl@56993
   799
  have int_eq: "(\<integral> x. f x * log b (f x) \<partial>MX) = (\<integral> x. log b (f x) \<partial>distr M MX X)"
hoelzl@49785
   800
    unfolding distributed_distr_eq_density[OF X]
hoelzl@49785
   801
    using D
hoelzl@49785
   802
    by (subst integral_density)
hoelzl@49785
   803
       (auto simp: borel_measurable_ereal_iff)
hoelzl@49788
   804
hoelzl@49788
   805
  show ?eq
hoelzl@56993
   806
    unfolding entropy_def KL_divergence_def entropy_density_def comp_def int_eq neg_equal_iff_equal
hoelzl@56993
   807
    using ae_eq by (intro integral_cong_AE) auto
hoelzl@49788
   808
qed
hoelzl@49785
   809
hoelzl@49786
   810
lemma (in prob_space) distributed_imp_emeasure_nonzero:
hoelzl@49786
   811
  assumes X: "distributed M MX X Px"
hoelzl@49786
   812
  shows "emeasure MX {x \<in> space MX. Px x \<noteq> 0} \<noteq> 0"
hoelzl@49786
   813
proof
hoelzl@49786
   814
  note Px = distributed_borel_measurable[OF X] distributed_AE[OF X]
hoelzl@49786
   815
  interpret X: prob_space "distr M MX X"
hoelzl@49786
   816
    using distributed_measurable[OF X] by (rule prob_space_distr)
hoelzl@49786
   817
hoelzl@49786
   818
  assume "emeasure MX {x \<in> space MX. Px x \<noteq> 0} = 0"
hoelzl@49786
   819
  with Px have "AE x in MX. Px x = 0"
hoelzl@49786
   820
    by (intro AE_I[OF subset_refl]) (auto simp: borel_measurable_ereal_iff)
hoelzl@49786
   821
  moreover
wenzelm@53015
   822
  from X.emeasure_space_1 have "(\<integral>\<^sup>+x. Px x \<partial>MX) = 1"
hoelzl@49786
   823
    unfolding distributed_distr_eq_density[OF X] using Px
hoelzl@49786
   824
    by (subst (asm) emeasure_density)
hoelzl@56996
   825
       (auto simp: borel_measurable_ereal_iff intro!: integral_cong cong: nn_integral_cong)
hoelzl@49786
   826
  ultimately show False
hoelzl@56996
   827
    by (simp add: nn_integral_cong_AE)
hoelzl@49786
   828
qed
hoelzl@49786
   829
hoelzl@49786
   830
lemma (in information_space) entropy_le:
hoelzl@49786
   831
  fixes Px :: "'b \<Rightarrow> real" and MX :: "'b measure"
hoelzl@56993
   832
  assumes X[measurable]: "distributed M MX X Px"
hoelzl@49786
   833
  and fin: "emeasure MX {x \<in> space MX. Px x \<noteq> 0} \<noteq> \<infinity>"
hoelzl@49786
   834
  and int: "integrable MX (\<lambda>x. - Px x * log b (Px x))"
hoelzl@49786
   835
  shows "entropy b MX X \<le> log b (measure MX {x \<in> space MX. Px x \<noteq> 0})"
hoelzl@49786
   836
proof -
hoelzl@49786
   837
  note Px = distributed_borel_measurable[OF X] distributed_AE[OF X]
hoelzl@49786
   838
  interpret X: prob_space "distr M MX X"
hoelzl@49786
   839
    using distributed_measurable[OF X] by (rule prob_space_distr)
hoelzl@49786
   840
hoelzl@49786
   841
  have " - log b (measure MX {x \<in> space MX. Px x \<noteq> 0}) = 
hoelzl@49786
   842
    - log b (\<integral> x. indicator {x \<in> space MX. Px x \<noteq> 0} x \<partial>MX)"
hoelzl@49786
   843
    using Px fin
hoelzl@57166
   844
    by (auto simp: measure_def borel_measurable_ereal_iff)
hoelzl@49786
   845
  also have "- log b (\<integral> x. indicator {x \<in> space MX. Px x \<noteq> 0} x \<partial>MX) = - log b (\<integral> x. 1 / Px x \<partial>distr M MX X)"
hoelzl@49786
   846
    unfolding distributed_distr_eq_density[OF X] using Px
hoelzl@49786
   847
    apply (intro arg_cong[where f="log b"] arg_cong[where f=uminus])
hoelzl@57166
   848
    by (subst integral_density) (auto simp: borel_measurable_ereal_iff simp del: integral_indicator intro!: integral_cong)
hoelzl@49786
   849
  also have "\<dots> \<le> (\<integral> x. - log b (1 / Px x) \<partial>distr M MX X)"
hoelzl@49786
   850
  proof (rule X.jensens_inequality[of "\<lambda>x. 1 / Px x" "{0<..}" 0 1 "\<lambda>x. - log b x"])
hoelzl@49786
   851
    show "AE x in distr M MX X. 1 / Px x \<in> {0<..}"
hoelzl@49786
   852
      unfolding distributed_distr_eq_density[OF X]
hoelzl@49786
   853
      using Px by (auto simp: AE_density)
hoelzl@49786
   854
    have [simp]: "\<And>x. x \<in> space MX \<Longrightarrow> ereal (if Px x = 0 then 0 else 1) = indicator {x \<in> space MX. Px x \<noteq> 0} x"
hoelzl@49786
   855
      by (auto simp: one_ereal_def)
wenzelm@53015
   856
    have "(\<integral>\<^sup>+ x. max 0 (ereal (- (if Px x = 0 then 0 else 1))) \<partial>MX) = (\<integral>\<^sup>+ x. 0 \<partial>MX)"
hoelzl@56996
   857
      by (intro nn_integral_cong) (auto split: split_max)
hoelzl@49786
   858
    then show "integrable (distr M MX X) (\<lambda>x. 1 / Px x)"
hoelzl@49786
   859
      unfolding distributed_distr_eq_density[OF X] using Px
hoelzl@56996
   860
      by (auto simp: nn_integral_density real_integrable_def borel_measurable_ereal_iff fin nn_integral_max_0
hoelzl@56996
   861
              cong: nn_integral_cong)
hoelzl@49786
   862
    have "integrable MX (\<lambda>x. Px x * log b (1 / Px x)) =
hoelzl@49786
   863
      integrable MX (\<lambda>x. - Px x * log b (Px x))"
hoelzl@49786
   864
      using Px
hoelzl@49786
   865
      by (intro integrable_cong_AE)
hoelzl@49786
   866
         (auto simp: borel_measurable_ereal_iff log_divide_eq
hoelzl@49786
   867
                  intro!: measurable_If)
hoelzl@49786
   868
    then show "integrable (distr M MX X) (\<lambda>x. - log b (1 / Px x))"
hoelzl@49786
   869
      unfolding distributed_distr_eq_density[OF X]
hoelzl@49786
   870
      using Px int
hoelzl@56993
   871
      by (subst integrable_real_density) (auto simp: borel_measurable_ereal_iff)
hoelzl@49786
   872
  qed (auto simp: minus_log_convex[OF b_gt_1])
hoelzl@49786
   873
  also have "\<dots> = (\<integral> x. log b (Px x) \<partial>distr M MX X)"
hoelzl@49786
   874
    unfolding distributed_distr_eq_density[OF X] using Px
hoelzl@49786
   875
    by (intro integral_cong_AE) (auto simp: AE_density log_divide_eq)
hoelzl@49786
   876
  also have "\<dots> = - entropy b MX X"
hoelzl@49786
   877
    unfolding distributed_distr_eq_density[OF X] using Px
hoelzl@49786
   878
    by (subst entropy_distr[OF X]) (auto simp: borel_measurable_ereal_iff integral_density)
hoelzl@49786
   879
  finally show ?thesis
hoelzl@49786
   880
    by simp
hoelzl@49786
   881
qed
hoelzl@49786
   882
hoelzl@49786
   883
lemma (in information_space) entropy_le_space:
hoelzl@49786
   884
  fixes Px :: "'b \<Rightarrow> real" and MX :: "'b measure"
hoelzl@49786
   885
  assumes X: "distributed M MX X Px"
hoelzl@49786
   886
  and fin: "finite_measure MX"
hoelzl@49786
   887
  and int: "integrable MX (\<lambda>x. - Px x * log b (Px x))"
hoelzl@49786
   888
  shows "entropy b MX X \<le> log b (measure MX (space MX))"
hoelzl@49786
   889
proof -
hoelzl@49786
   890
  note Px = distributed_borel_measurable[OF X] distributed_AE[OF X]
hoelzl@49786
   891
  interpret finite_measure MX by fact
hoelzl@49786
   892
  have "entropy b MX X \<le> log b (measure MX {x \<in> space MX. Px x \<noteq> 0})"
hoelzl@49786
   893
    using int X by (intro entropy_le) auto
hoelzl@49786
   894
  also have "\<dots> \<le> log b (measure MX (space MX))"
hoelzl@49786
   895
    using Px distributed_imp_emeasure_nonzero[OF X]
hoelzl@49786
   896
    by (intro log_le)
hoelzl@49786
   897
       (auto intro!: borel_measurable_ereal_iff finite_measure_mono b_gt_1
hoelzl@49786
   898
                     less_le[THEN iffD2] measure_nonneg simp: emeasure_eq_measure)
hoelzl@49786
   899
  finally show ?thesis .
hoelzl@49786
   900
qed
hoelzl@49786
   901
hoelzl@47694
   902
lemma (in information_space) entropy_uniform:
hoelzl@49785
   903
  assumes X: "distributed M MX X (\<lambda>x. indicator A x / measure MX A)" (is "distributed _ _ _ ?f")
hoelzl@47694
   904
  shows "entropy b MX X = log b (measure MX A)"
hoelzl@49785
   905
proof (subst entropy_distr[OF X])
hoelzl@49785
   906
  have [simp]: "emeasure MX A \<noteq> \<infinity>"
hoelzl@49785
   907
    using uniform_distributed_params[OF X] by (auto simp add: measure_def)
hoelzl@49785
   908
  have eq: "(\<integral> x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \<partial>MX) =
hoelzl@49785
   909
    (\<integral> x. (- log b (measure MX A) / measure MX A) * indicator A x \<partial>MX)"
hoelzl@49785
   910
    using measure_nonneg[of MX A] uniform_distributed_params[OF X]
hoelzl@56993
   911
    by (intro integral_cong) (auto split: split_indicator simp: log_divide_eq)
hoelzl@49785
   912
  show "- (\<integral> x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \<partial>MX) =
hoelzl@49785
   913
    log b (measure MX A)"
hoelzl@49785
   914
    unfolding eq using uniform_distributed_params[OF X]
hoelzl@56993
   915
    by (subst integral_mult_right) (auto simp: measure_def)
hoelzl@49785
   916
qed
hoelzl@36080
   917
hoelzl@47694
   918
lemma (in information_space) entropy_simple_distributed:
hoelzl@49786
   919
  "simple_distributed M X f \<Longrightarrow> \<H>(X) = - (\<Sum>x\<in>X`space M. f x * log b (f x))"
hoelzl@49786
   920
  by (subst entropy_distr[OF simple_distributed])
hoelzl@49786
   921
     (auto simp add: lebesgue_integral_count_space_finite)
hoelzl@39097
   922
hoelzl@40859
   923
lemma (in information_space) entropy_le_card_not_0:
hoelzl@47694
   924
  assumes X: "simple_distributed M X f"
hoelzl@47694
   925
  shows "\<H>(X) \<le> log b (card (X ` space M \<inter> {x. f x \<noteq> 0}))"
hoelzl@39097
   926
proof -
hoelzl@49787
   927
  let ?X = "count_space (X`space M)"
hoelzl@49787
   928
  have "\<H>(X) \<le> log b (measure ?X {x \<in> space ?X. f x \<noteq> 0})"
hoelzl@49787
   929
    by (rule entropy_le[OF simple_distributed[OF X]])
hoelzl@49787
   930
       (simp_all add: simple_distributed_finite[OF X] subset_eq integrable_count_space emeasure_count_space)
hoelzl@49787
   931
  also have "measure ?X {x \<in> space ?X. f x \<noteq> 0} = card (X ` space M \<inter> {x. f x \<noteq> 0})"
hoelzl@49787
   932
    by (simp_all add: simple_distributed_finite[OF X] subset_eq emeasure_count_space measure_def Int_def)
hoelzl@49787
   933
  finally show ?thesis .
hoelzl@39097
   934
qed
hoelzl@39097
   935
hoelzl@40859
   936
lemma (in information_space) entropy_le_card:
hoelzl@49787
   937
  assumes X: "simple_distributed M X f"
hoelzl@40859
   938
  shows "\<H>(X) \<le> log b (real (card (X ` space M)))"
hoelzl@49787
   939
proof -
hoelzl@49787
   940
  let ?X = "count_space (X`space M)"
hoelzl@49787
   941
  have "\<H>(X) \<le> log b (measure ?X (space ?X))"
hoelzl@49787
   942
    by (rule entropy_le_space[OF simple_distributed[OF X]])
hoelzl@49787
   943
       (simp_all add: simple_distributed_finite[OF X] subset_eq integrable_count_space emeasure_count_space finite_measure_count_space)
hoelzl@49787
   944
  also have "measure ?X (space ?X) = card (X ` space M)"
hoelzl@49787
   945
    by (simp_all add: simple_distributed_finite[OF X] subset_eq emeasure_count_space measure_def)
hoelzl@39097
   946
  finally show ?thesis .
hoelzl@39097
   947
qed
hoelzl@39097
   948
wenzelm@61808
   949
subsection \<open>Conditional Mutual Information\<close>
hoelzl@39097
   950
hoelzl@36080
   951
definition (in prob_space)
hoelzl@41689
   952
  "conditional_mutual_information b MX MY MZ X Y Z \<equiv>
wenzelm@53015
   953
    mutual_information b MX (MY \<Otimes>\<^sub>M MZ) X (\<lambda>x. (Y x, Z x)) -
hoelzl@41689
   954
    mutual_information b MX MZ X Z"
hoelzl@36080
   955
hoelzl@40859
   956
abbreviation (in information_space)
hoelzl@40859
   957
  conditional_mutual_information_Pow ("\<I>'( _ ; _ | _ ')") where
hoelzl@36624
   958
  "\<I>(X ; Y | Z) \<equiv> conditional_mutual_information b
hoelzl@47694
   959
    (count_space (X ` space M)) (count_space (Y ` space M)) (count_space (Z ` space M)) X Y Z"
hoelzl@36080
   960
hoelzl@49787
   961
lemma (in information_space)
hoelzl@47694
   962
  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" and P: "sigma_finite_measure P"
hoelzl@50003
   963
  assumes Px[measurable]: "distributed M S X Px"
hoelzl@50003
   964
  assumes Pz[measurable]: "distributed M P Z Pz"
wenzelm@53015
   965
  assumes Pyz[measurable]: "distributed M (T \<Otimes>\<^sub>M P) (\<lambda>x. (Y x, Z x)) Pyz"
wenzelm@53015
   966
  assumes Pxz[measurable]: "distributed M (S \<Otimes>\<^sub>M P) (\<lambda>x. (X x, Z x)) Pxz"
wenzelm@53015
   967
  assumes Pxyz[measurable]: "distributed M (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>x. (X x, Y x, Z x)) Pxyz"
wenzelm@53015
   968
  assumes I1: "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Px x * Pyz (y, z))))"
wenzelm@53015
   969
  assumes I2: "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxz (x, z) / (Px x * Pz z)))"
hoelzl@49787
   970
  shows conditional_mutual_information_generic_eq: "conditional_mutual_information b S T P X Y Z
wenzelm@53015
   971
    = (\<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>\<^sub>M T \<Otimes>\<^sub>M P))" (is "?eq")
hoelzl@49787
   972
    and conditional_mutual_information_generic_nonneg: "0 \<le> conditional_mutual_information b S T P X Y Z" (is "?nonneg")
hoelzl@40859
   973
proof -
hoelzl@47694
   974
  interpret S: sigma_finite_measure S by fact
hoelzl@47694
   975
  interpret T: sigma_finite_measure T by fact
hoelzl@47694
   976
  interpret P: sigma_finite_measure P by fact
hoelzl@47694
   977
  interpret TP: pair_sigma_finite T P ..
hoelzl@47694
   978
  interpret SP: pair_sigma_finite S P ..
hoelzl@49787
   979
  interpret ST: pair_sigma_finite S T ..
wenzelm@53015
   980
  interpret SPT: pair_sigma_finite "S \<Otimes>\<^sub>M P" T ..
wenzelm@53015
   981
  interpret STP: pair_sigma_finite S "T \<Otimes>\<^sub>M P" ..
wenzelm@53015
   982
  interpret TPS: pair_sigma_finite "T \<Otimes>\<^sub>M P" S ..
wenzelm@53015
   983
  have TP: "sigma_finite_measure (T \<Otimes>\<^sub>M P)" ..
wenzelm@53015
   984
  have SP: "sigma_finite_measure (S \<Otimes>\<^sub>M P)" ..
wenzelm@53015
   985
  have YZ: "random_variable (T \<Otimes>\<^sub>M P) (\<lambda>x. (Y x, Z x))"
hoelzl@47694
   986
    using Pyz by (simp add: distributed_measurable)
hoelzl@47694
   987
  
wenzelm@53015
   988
  from Pxz Pxyz have distr_eq: "distr M (S \<Otimes>\<^sub>M P) (\<lambda>x. (X x, Z x)) =
wenzelm@53015
   989
    distr (distr M (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>x. (X x, Y x, Z x))) (S \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). (x, z))"
hoelzl@50003
   990
    by (simp add: comp_def distr_distr)
hoelzl@40859
   991
hoelzl@47694
   992
  have "mutual_information b S P X Z =
wenzelm@53015
   993
    (\<integral>x. Pxz x * log b (Pxz x / (Px (fst x) * Pz (snd x))) \<partial>(S \<Otimes>\<^sub>M P))"
hoelzl@47694
   994
    by (rule mutual_information_distr[OF S P Px Pz Pxz])
wenzelm@53015
   995
  also have "\<dots> = (\<integral>(x,y,z). Pxyz (x,y,z) * log b (Pxz (x,z) / (Px x * Pz z)) \<partial>(S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P))"
hoelzl@47694
   996
    using b_gt_1 Pxz Px Pz
hoelzl@50003
   997
    by (subst distributed_transform_integral[OF Pxyz Pxz, where T="\<lambda>(x, y, z). (x, z)"]) (auto simp: split_beta')
hoelzl@47694
   998
  finally have mi_eq:
wenzelm@53015
   999
    "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>\<^sub>M T \<Otimes>\<^sub>M P))" .
hoelzl@47694
  1000
  
wenzelm@53015
  1001
  have ae1: "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. Px (fst x) = 0 \<longrightarrow> Pxyz x = 0"
hoelzl@47694
  1002
    by (intro subdensity_real[of fst, OF _ Pxyz Px]) auto
wenzelm@53015
  1003
  moreover have ae2: "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. Pz (snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
hoelzl@50003
  1004
    by (intro subdensity_real[of "\<lambda>x. snd (snd x)", OF _ Pxyz Pz]) auto
wenzelm@53015
  1005
  moreover have ae3: "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. Pxz (fst x, snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
hoelzl@50003
  1006
    by (intro subdensity_real[of "\<lambda>x. (fst x, snd (snd x))", OF _ Pxyz Pxz]) auto
wenzelm@53015
  1007
  moreover have ae4: "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. Pyz (snd x) = 0 \<longrightarrow> Pxyz x = 0"
hoelzl@50003
  1008
    by (intro subdensity_real[of snd, OF _ Pxyz Pyz]) auto
wenzelm@53015
  1009
  moreover have ae5: "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. 0 \<le> Px (fst x)"
hoelzl@50003
  1010
    using Px by (intro STP.AE_pair_measure) (auto simp: comp_def dest: distributed_real_AE)
wenzelm@53015
  1011
  moreover have ae6: "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. 0 \<le> Pyz (snd x)"
hoelzl@50003
  1012
    using Pyz by (intro STP.AE_pair_measure) (auto simp: comp_def dest: distributed_real_AE)
wenzelm@53015
  1013
  moreover have ae7: "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. 0 \<le> Pz (snd (snd x))"
hoelzl@50003
  1014
    using Pz Pz[THEN distributed_real_measurable]
hoelzl@50003
  1015
    by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure AE_I2[of S] dest: distributed_real_AE)
wenzelm@53015
  1016
  moreover have ae8: "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. 0 \<le> Pxz (fst x, snd (snd x))"
hoelzl@47694
  1017
    using Pxz[THEN distributed_real_AE, THEN SP.AE_pair]
hoelzl@50003
  1018
    by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure)
hoelzl@47694
  1019
  moreover note Pxyz[THEN distributed_real_AE]
wenzelm@53015
  1020
  ultimately have ae: "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P.
hoelzl@47694
  1021
    Pxyz x * log b (Pxyz x / (Px (fst x) * Pyz (snd x))) -
hoelzl@47694
  1022
    Pxyz x * log b (Pxz (fst x, snd (snd x)) / (Px (fst x) * Pz (snd (snd x)))) =
hoelzl@47694
  1023
    Pxyz x * log b (Pxyz x * Pz (snd (snd x)) / (Pxz (fst x, snd (snd x)) * Pyz (snd x))) "
hoelzl@47694
  1024
  proof eventually_elim
wenzelm@60580
  1025
    case (elim x)
hoelzl@47694
  1026
    show ?case
hoelzl@40859
  1027
    proof cases
hoelzl@47694
  1028
      assume "Pxyz x \<noteq> 0"
wenzelm@60580
  1029
      with elim have "0 < Px (fst x)" "0 < Pz (snd (snd x))" "0 < Pxz (fst x, snd (snd x))"
wenzelm@60580
  1030
        "0 < Pyz (snd x)" "0 < Pxyz x"
hoelzl@47694
  1031
        by auto
hoelzl@47694
  1032
      then show ?thesis
nipkow@56544
  1033
        using b_gt_1 by (simp add: log_simps less_imp_le field_simps)
hoelzl@40859
  1034
    qed simp
hoelzl@40859
  1035
  qed
hoelzl@49787
  1036
  with I1 I2 show ?eq
hoelzl@40859
  1037
    unfolding conditional_mutual_information_def
hoelzl@47694
  1038
    apply (subst mi_eq)
hoelzl@47694
  1039
    apply (subst mutual_information_distr[OF S TP Px Pyz Pxyz])
hoelzl@56993
  1040
    apply (subst integral_diff[symmetric])
hoelzl@47694
  1041
    apply (auto intro!: integral_cong_AE simp: split_beta' simp del: integral_diff)
hoelzl@47694
  1042
    done
hoelzl@49787
  1043
wenzelm@53015
  1044
  let ?P = "density (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) Pxyz"
hoelzl@49787
  1045
  interpret P: prob_space ?P
hoelzl@49787
  1046
    unfolding distributed_distr_eq_density[OF Pxyz, symmetric]
hoelzl@50003
  1047
    by (rule prob_space_distr) simp
hoelzl@49787
  1048
wenzelm@53015
  1049
  let ?Q = "density (T \<Otimes>\<^sub>M P) Pyz"
hoelzl@49787
  1050
  interpret Q: prob_space ?Q
hoelzl@49787
  1051
    unfolding distributed_distr_eq_density[OF Pyz, symmetric]
hoelzl@50003
  1052
    by (rule prob_space_distr) simp
hoelzl@49787
  1053
hoelzl@49787
  1054
  let ?f = "\<lambda>(x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) / Pxyz (x, y, z)"
hoelzl@49787
  1055
hoelzl@49787
  1056
  from subdensity_real[of snd, OF _ Pyz Pz]
wenzelm@53015
  1057
  have aeX1: "AE x in T \<Otimes>\<^sub>M P. Pz (snd x) = 0 \<longrightarrow> Pyz x = 0" by (auto simp: comp_def)
wenzelm@53015
  1058
  have aeX2: "AE x in T \<Otimes>\<^sub>M P. 0 \<le> Pz (snd x)"
hoelzl@50003
  1059
    using Pz by (intro TP.AE_pair_measure) (auto simp: comp_def dest: distributed_real_AE)
hoelzl@49787
  1060
wenzelm@53015
  1061
  have aeX3: "AE y in T \<Otimes>\<^sub>M P. (\<integral>\<^sup>+ x. ereal (Pxz (x, snd y)) \<partial>S) = ereal (Pz (snd y))"
hoelzl@49788
  1062
    using Pz distributed_marginal_eq_joint2[OF P S Pz Pxz]
hoelzl@50003
  1063
    by (intro TP.AE_pair_measure) (auto dest: distributed_real_AE)
hoelzl@49787
  1064
wenzelm@53015
  1065
  have "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<le> (\<integral>\<^sup>+ (x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) \<partial>(S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P))"
hoelzl@56996
  1066
    apply (subst nn_integral_density)
hoelzl@50003
  1067
    apply simp
hoelzl@49787
  1068
    apply (rule distributed_AE[OF Pxyz])
hoelzl@50003
  1069
    apply auto []
hoelzl@56996
  1070
    apply (rule nn_integral_mono_AE)
hoelzl@49787
  1071
    using ae5 ae6 ae7 ae8
hoelzl@49787
  1072
    apply eventually_elim
hoelzl@56571
  1073
    apply auto
hoelzl@49787
  1074
    done
wenzelm@53015
  1075
  also have "\<dots> = (\<integral>\<^sup>+(y, z). \<integral>\<^sup>+ x. ereal (Pxz (x, z)) * ereal (Pyz (y, z) / Pz z) \<partial>S \<partial>T \<Otimes>\<^sub>M P)"
hoelzl@56996
  1076
    by (subst STP.nn_integral_snd[symmetric]) (auto simp add: split_beta')
wenzelm@53015
  1077
  also have "\<dots> = (\<integral>\<^sup>+x. ereal (Pyz x) * 1 \<partial>T \<Otimes>\<^sub>M P)"
hoelzl@56996
  1078
    apply (rule nn_integral_cong_AE)
hoelzl@49787
  1079
    using aeX1 aeX2 aeX3 distributed_AE[OF Pyz] AE_space
hoelzl@49787
  1080
    apply eventually_elim
hoelzl@49787
  1081
  proof (case_tac x, simp del: times_ereal.simps add: space_pair_measure)
hoelzl@49787
  1082
    fix a b assume "Pz b = 0 \<longrightarrow> Pyz (a, b) = 0" "0 \<le> Pz b" "a \<in> space T \<and> b \<in> space P"
wenzelm@53015
  1083
      "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)" 
wenzelm@53015
  1084
    then show "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
hoelzl@56996
  1085
      by (subst nn_integral_multc)
hoelzl@56571
  1086
         (auto split: prod.split)
hoelzl@49787
  1087
  qed
hoelzl@49787
  1088
  also have "\<dots> = 1"
hoelzl@49787
  1089
    using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
hoelzl@56996
  1090
    by (subst nn_integral_density[symmetric]) auto
wenzelm@53015
  1091
  finally have le1: "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<le> 1" .
hoelzl@49787
  1092
  also have "\<dots> < \<infinity>" by simp
wenzelm@53015
  1093
  finally have fin: "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<noteq> \<infinity>" by simp
hoelzl@49787
  1094
hoelzl@56993
  1095
  have pos: "(\<integral>\<^sup>+x. ?f x \<partial>?P) \<noteq> 0"
hoelzl@56996
  1096
    apply (subst nn_integral_density)
hoelzl@50003
  1097
    apply simp
hoelzl@49787
  1098
    apply (rule distributed_AE[OF Pxyz])
hoelzl@50003
  1099
    apply auto []
hoelzl@49787
  1100
    apply (simp add: split_beta')
hoelzl@49787
  1101
  proof
hoelzl@49787
  1102
    let ?g = "\<lambda>x. ereal (if Pxyz x = 0 then 0 else Pxz (fst x, snd (snd x)) * Pyz (snd x) / Pz (snd (snd x)))"
hoelzl@56993
  1103
    assume "(\<integral>\<^sup>+x. ?g x \<partial>(S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P)) = 0"
wenzelm@53015
  1104
    then have "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. ?g x \<le> 0"
hoelzl@56996
  1105
      by (intro nn_integral_0_iff_AE[THEN iffD1]) auto
wenzelm@53015
  1106
    then have "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. Pxyz x = 0"
hoelzl@49787
  1107
      using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
hoelzl@49787
  1108
      by eventually_elim (auto split: split_if_asm simp: mult_le_0_iff divide_le_0_iff)
wenzelm@53015
  1109
    then have "(\<integral>\<^sup>+ x. ereal (Pxyz x) \<partial>S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) = 0"
hoelzl@56996
  1110
      by (subst nn_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
hoelzl@49787
  1111
    with P.emeasure_space_1 show False
hoelzl@56996
  1112
      by (subst (asm) emeasure_density) (auto cong: nn_integral_cong)
hoelzl@49787
  1113
  qed
hoelzl@49787
  1114
wenzelm@53015
  1115
  have neg: "(\<integral>\<^sup>+ x. - ?f x \<partial>?P) = 0"
hoelzl@56996
  1116
    apply (rule nn_integral_0_iff_AE[THEN iffD2])
hoelzl@50003
  1117
    apply simp
hoelzl@49787
  1118
    apply (subst AE_density)
hoelzl@50003
  1119
    apply simp
hoelzl@49787
  1120
    using ae5 ae6 ae7 ae8
hoelzl@49787
  1121
    apply eventually_elim
hoelzl@56571
  1122
    apply auto
hoelzl@49787
  1123
    done
hoelzl@49787
  1124
wenzelm@53015
  1125
  have I3: "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"
hoelzl@56993
  1126
    apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ integrable_diff[OF I1 I2]])
hoelzl@49787
  1127
    using ae
hoelzl@50003
  1128
    apply (auto simp: split_beta')
hoelzl@49787
  1129
    done
hoelzl@49787
  1130
wenzelm@53015
  1131
  have "- log b 1 \<le> - log b (integral\<^sup>L ?P ?f)"
hoelzl@49787
  1132
  proof (intro le_imp_neg_le log_le[OF b_gt_1])
hoelzl@56993
  1133
    have If: "integrable ?P ?f"
hoelzl@56993
  1134
      unfolding real_integrable_def
hoelzl@56993
  1135
    proof (intro conjI)
hoelzl@56993
  1136
      from neg show "(\<integral>\<^sup>+ x. - ?f x \<partial>?P) \<noteq> \<infinity>"
hoelzl@56993
  1137
        by simp
hoelzl@56993
  1138
      from fin show "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<noteq> \<infinity>"
hoelzl@56993
  1139
        by simp
hoelzl@56993
  1140
    qed simp
hoelzl@56993
  1141
    then have "(\<integral>\<^sup>+ x. ?f x \<partial>?P) = (\<integral>x. ?f x \<partial>?P)"
hoelzl@56996
  1142
      apply (rule nn_integral_eq_integral)
hoelzl@56993
  1143
      apply (subst AE_density)
hoelzl@56993
  1144
      apply simp
hoelzl@56993
  1145
      using ae5 ae6 ae7 ae8
hoelzl@56993
  1146
      apply eventually_elim
hoelzl@56993
  1147
      apply auto
hoelzl@56993
  1148
      done
hoelzl@56996
  1149
    with nn_integral_nonneg[of ?P ?f] pos le1
hoelzl@56993
  1150
    show "0 < (\<integral>x. ?f x \<partial>?P)" "(\<integral>x. ?f x \<partial>?P) \<le> 1"
hoelzl@56993
  1151
      by (simp_all add: one_ereal_def)
hoelzl@49787
  1152
  qed
wenzelm@53015
  1153
  also have "- log b (integral\<^sup>L ?P ?f) \<le> (\<integral> x. - log b (?f x) \<partial>?P)"
hoelzl@49787
  1154
  proof (rule P.jensens_inequality[where a=0 and b=1 and I="{0<..}"])
hoelzl@49787
  1155
    show "AE x in ?P. ?f x \<in> {0<..}"
hoelzl@49787
  1156
      unfolding AE_density[OF distributed_borel_measurable[OF Pxyz]]
hoelzl@49787
  1157
      using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
nipkow@56544
  1158
      by eventually_elim (auto)
hoelzl@49787
  1159
    show "integrable ?P ?f"
hoelzl@56993
  1160
      unfolding real_integrable_def 
hoelzl@50003
  1161
      using fin neg by (auto simp: split_beta')
hoelzl@49787
  1162
    show "integrable ?P (\<lambda>x. - log b (?f x))"
hoelzl@56993
  1163
      apply (subst integrable_real_density)
hoelzl@50003
  1164
      apply simp
hoelzl@50003
  1165
      apply (auto intro!: distributed_real_AE[OF Pxyz]) []
hoelzl@50003
  1166
      apply simp
hoelzl@49787
  1167
      apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ I3])
hoelzl@50003
  1168
      apply simp
hoelzl@50003
  1169
      apply simp
hoelzl@49787
  1170
      using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
hoelzl@49787
  1171
      apply eventually_elim
hoelzl@49787
  1172
      apply (auto simp: log_divide_eq log_mult_eq zero_le_mult_iff zero_less_mult_iff zero_less_divide_iff field_simps)
hoelzl@49787
  1173
      done
hoelzl@49787
  1174
  qed (auto simp: b_gt_1 minus_log_convex)
hoelzl@49787
  1175
  also have "\<dots> = conditional_mutual_information b S T P X Y Z"
wenzelm@61808
  1176
    unfolding \<open>?eq\<close>
hoelzl@56993
  1177
    apply (subst integral_real_density)
hoelzl@50003
  1178
    apply simp
hoelzl@50003
  1179
    apply (auto intro!: distributed_real_AE[OF Pxyz]) []
hoelzl@50003
  1180
    apply simp
hoelzl@49787
  1181
    apply (intro integral_cong_AE)
hoelzl@49787
  1182
    using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
hoelzl@49787
  1183
    apply (auto simp: log_divide_eq zero_less_mult_iff zero_less_divide_iff field_simps)
hoelzl@49787
  1184
    done
hoelzl@49787
  1185
  finally show ?nonneg
hoelzl@49787
  1186
    by simp
hoelzl@40859
  1187
qed
hoelzl@40859
  1188
hoelzl@49803
  1189
lemma (in information_space)
hoelzl@49803
  1190
  fixes Px :: "_ \<Rightarrow> real"
hoelzl@49803
  1191
  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" and P: "sigma_finite_measure P"
hoelzl@49803
  1192
  assumes Fx: "finite_entropy S X Px"
hoelzl@49803
  1193
  assumes Fz: "finite_entropy P Z Pz"
wenzelm@53015
  1194
  assumes Fyz: "finite_entropy (T \<Otimes>\<^sub>M P) (\<lambda>x. (Y x, Z x)) Pyz"
wenzelm@53015
  1195
  assumes Fxz: "finite_entropy (S \<Otimes>\<^sub>M P) (\<lambda>x. (X x, Z x)) Pxz"
wenzelm@53015
  1196
  assumes Fxyz: "finite_entropy (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>x. (X x, Y x, Z x)) Pxyz"
hoelzl@49803
  1197
  shows conditional_mutual_information_generic_eq': "conditional_mutual_information b S T P X Y Z
wenzelm@53015
  1198
    = (\<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>\<^sub>M T \<Otimes>\<^sub>M P))" (is "?eq")
hoelzl@49803
  1199
    and conditional_mutual_information_generic_nonneg': "0 \<le> conditional_mutual_information b S T P X Y Z" (is "?nonneg")
hoelzl@49803
  1200
proof -
hoelzl@50003
  1201
  note Px = Fx[THEN finite_entropy_distributed, measurable]
hoelzl@50003
  1202
  note Pz = Fz[THEN finite_entropy_distributed, measurable]
hoelzl@50003
  1203
  note Pyz = Fyz[THEN finite_entropy_distributed, measurable]
hoelzl@50003
  1204
  note Pxz = Fxz[THEN finite_entropy_distributed, measurable]
hoelzl@50003
  1205
  note Pxyz = Fxyz[THEN finite_entropy_distributed, measurable]
hoelzl@49803
  1206
hoelzl@49803
  1207
  interpret S: sigma_finite_measure S by fact
hoelzl@49803
  1208
  interpret T: sigma_finite_measure T by fact
hoelzl@49803
  1209
  interpret P: sigma_finite_measure P by fact
hoelzl@49803
  1210
  interpret TP: pair_sigma_finite T P ..
hoelzl@49803
  1211
  interpret SP: pair_sigma_finite S P ..
hoelzl@49803
  1212
  interpret ST: pair_sigma_finite S T ..
wenzelm@53015
  1213
  interpret SPT: pair_sigma_finite "S \<Otimes>\<^sub>M P" T ..
wenzelm@53015
  1214
  interpret STP: pair_sigma_finite S "T \<Otimes>\<^sub>M P" ..
wenzelm@53015
  1215
  interpret TPS: pair_sigma_finite "T \<Otimes>\<^sub>M P" S ..
wenzelm@53015
  1216
  have TP: "sigma_finite_measure (T \<Otimes>\<^sub>M P)" ..
wenzelm@53015
  1217
  have SP: "sigma_finite_measure (S \<Otimes>\<^sub>M P)" ..
hoelzl@49803
  1218
wenzelm@53015
  1219
  from Pxz Pxyz have distr_eq: "distr M (S \<Otimes>\<^sub>M P) (\<lambda>x. (X x, Z x)) =
wenzelm@53015
  1220
    distr (distr M (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>x. (X x, Y x, Z x))) (S \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). (x, z))"
hoelzl@50003
  1221
    by (simp add: distr_distr comp_def)
hoelzl@49803
  1222
hoelzl@49803
  1223
  have "mutual_information b S P X Z =
wenzelm@53015
  1224
    (\<integral>x. Pxz x * log b (Pxz x / (Px (fst x) * Pz (snd x))) \<partial>(S \<Otimes>\<^sub>M P))"
hoelzl@49803
  1225
    by (rule mutual_information_distr[OF S P Px Pz Pxz])
wenzelm@53015
  1226
  also have "\<dots> = (\<integral>(x,y,z). Pxyz (x,y,z) * log b (Pxz (x,z) / (Px x * Pz z)) \<partial>(S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P))"
hoelzl@49803
  1227
    using b_gt_1 Pxz Px Pz
hoelzl@49803
  1228
    by (subst distributed_transform_integral[OF Pxyz Pxz, where T="\<lambda>(x, y, z). (x, z)"])
hoelzl@50003
  1229
       (auto simp: split_beta')
hoelzl@49803
  1230
  finally have mi_eq:
wenzelm@53015
  1231
    "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>\<^sub>M T \<Otimes>\<^sub>M P))" .
hoelzl@49803
  1232
  
wenzelm@53015
  1233
  have ae1: "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. Px (fst x) = 0 \<longrightarrow> Pxyz x = 0"
hoelzl@49803
  1234
    by (intro subdensity_real[of fst, OF _ Pxyz Px]) auto
wenzelm@53015
  1235
  moreover have ae2: "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. Pz (snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
hoelzl@50003
  1236
    by (intro subdensity_real[of "\<lambda>x. snd (snd x)", OF _ Pxyz Pz]) auto
wenzelm@53015
  1237
  moreover have ae3: "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. Pxz (fst x, snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
hoelzl@50003
  1238
    by (intro subdensity_real[of "\<lambda>x. (fst x, snd (snd x))", OF _ Pxyz Pxz]) auto
wenzelm@53015
  1239
  moreover have ae4: "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. Pyz (snd x) = 0 \<longrightarrow> Pxyz x = 0"
hoelzl@50003
  1240
    by (intro subdensity_real[of snd, OF _ Pxyz Pyz]) auto
wenzelm@53015
  1241
  moreover have ae5: "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. 0 \<le> Px (fst x)"
hoelzl@50003
  1242
    using Px by (intro STP.AE_pair_measure) (auto dest: distributed_real_AE)
wenzelm@53015
  1243
  moreover have ae6: "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. 0 \<le> Pyz (snd x)"
hoelzl@50003
  1244
    using Pyz by (intro STP.AE_pair_measure) (auto dest: distributed_real_AE)
wenzelm@53015
  1245
  moreover have ae7: "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. 0 \<le> Pz (snd (snd x))"
hoelzl@50003
  1246
    using Pz Pz[THEN distributed_real_measurable] by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure AE_I2[of S] dest: distributed_real_AE)
wenzelm@53015
  1247
  moreover have ae8: "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. 0 \<le> Pxz (fst x, snd (snd x))"
hoelzl@49803
  1248
    using Pxz[THEN distributed_real_AE, THEN SP.AE_pair]
hoelzl@49803
  1249
    by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure simp: comp_def)
hoelzl@49803
  1250
  moreover note ae9 = Pxyz[THEN distributed_real_AE]
wenzelm@53015
  1251
  ultimately have ae: "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P.
hoelzl@49803
  1252
    Pxyz x * log b (Pxyz x / (Px (fst x) * Pyz (snd x))) -
hoelzl@49803
  1253
    Pxyz x * log b (Pxz (fst x, snd (snd x)) / (Px (fst x) * Pz (snd (snd x)))) =
hoelzl@49803
  1254
    Pxyz x * log b (Pxyz x * Pz (snd (snd x)) / (Pxz (fst x, snd (snd x)) * Pyz (snd x))) "
hoelzl@49803
  1255
  proof eventually_elim
wenzelm@60580
  1256
    case (elim x)
hoelzl@49803
  1257
    show ?case
hoelzl@49803
  1258
    proof cases
hoelzl@49803
  1259
      assume "Pxyz x \<noteq> 0"
wenzelm@60580
  1260
      with elim have "0 < Px (fst x)" "0 < Pz (snd (snd x))" "0 < Pxz (fst x, snd (snd x))"
wenzelm@60580
  1261
        "0 < Pyz (snd x)" "0 < Pxyz x"
hoelzl@49803
  1262
        by auto
hoelzl@49803
  1263
      then show ?thesis
nipkow@56544
  1264
        using b_gt_1 by (simp add: log_simps less_imp_le field_simps)
hoelzl@49803
  1265
    qed simp
hoelzl@49803
  1266
  qed
hoelzl@49803
  1267
wenzelm@53015
  1268
  have "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P)
hoelzl@49803
  1269
    (\<lambda>x. Pxyz x * log b (Pxyz x) - Pxyz x * log b (Px (fst x)) - Pxyz x * log b (Pyz (snd x)))"
hoelzl@49803
  1270
    using finite_entropy_integrable[OF Fxyz]
hoelzl@49803
  1271
    using finite_entropy_integrable_transform[OF Fx Pxyz, of fst]
hoelzl@49803
  1272
    using finite_entropy_integrable_transform[OF Fyz Pxyz, of snd]
hoelzl@49803
  1273
    by simp
wenzelm@53015
  1274
  moreover have "(\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Px x * Pyz (y, z)))) \<in> borel_measurable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P)"
hoelzl@50003
  1275
    using Pxyz Px Pyz by simp
wenzelm@53015
  1276
  ultimately have I1: "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Px x * Pyz (y, z))))"
hoelzl@49803
  1277
    apply (rule integrable_cong_AE_imp)
hoelzl@49803
  1278
    using ae1 ae4 ae5 ae6 ae9
hoelzl@49803
  1279
    by eventually_elim
nipkow@56536
  1280
       (auto simp: log_divide_eq log_mult_eq field_simps zero_less_mult_iff)
hoelzl@49803
  1281
wenzelm@53015
  1282
  have "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P)
hoelzl@49803
  1283
    (\<lambda>x. Pxyz x * log b (Pxz (fst x, snd (snd x))) - Pxyz x * log b (Px (fst x)) - Pxyz x * log b (Pz (snd (snd x))))"
hoelzl@49803
  1284
    using finite_entropy_integrable_transform[OF Fxz Pxyz, of "\<lambda>x. (fst x, snd (snd x))"]
hoelzl@49803
  1285
    using finite_entropy_integrable_transform[OF Fx Pxyz, of fst]
hoelzl@49803
  1286
    using finite_entropy_integrable_transform[OF Fz Pxyz, of "snd \<circ> snd"]
hoelzl@50003
  1287
    by simp
wenzelm@53015
  1288
  moreover have "(\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxz (x, z) / (Px x * Pz z))) \<in> borel_measurable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P)"
hoelzl@49803
  1289
    using Pxyz Px Pz
hoelzl@50003
  1290
    by auto
wenzelm@53015
  1291
  ultimately have I2: "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxz (x, z) / (Px x * Pz z)))"
hoelzl@49803
  1292
    apply (rule integrable_cong_AE_imp)
hoelzl@49803
  1293
    using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 ae9
hoelzl@49803
  1294
    by eventually_elim
nipkow@56536
  1295
       (auto simp: log_divide_eq log_mult_eq field_simps zero_less_mult_iff)
hoelzl@49803
  1296
hoelzl@49803
  1297
  from ae I1 I2 show ?eq
hoelzl@49803
  1298
    unfolding conditional_mutual_information_def
hoelzl@49803
  1299
    apply (subst mi_eq)
hoelzl@49803
  1300
    apply (subst mutual_information_distr[OF S TP Px Pyz Pxyz])
hoelzl@56993
  1301
    apply (subst integral_diff[symmetric])
hoelzl@49803
  1302
    apply (auto intro!: integral_cong_AE simp: split_beta' simp del: integral_diff)
hoelzl@49803
  1303
    done
hoelzl@49803
  1304
wenzelm@53015
  1305
  let ?P = "density (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) Pxyz"
hoelzl@49803
  1306
  interpret P: prob_space ?P
hoelzl@50003
  1307
    unfolding distributed_distr_eq_density[OF Pxyz, symmetric] by (rule prob_space_distr) simp
hoelzl@49803
  1308
wenzelm@53015
  1309
  let ?Q = "density (T \<Otimes>\<^sub>M P) Pyz"
hoelzl@49803
  1310
  interpret Q: prob_space ?Q
hoelzl@50003
  1311
    unfolding distributed_distr_eq_density[OF Pyz, symmetric] by (rule prob_space_distr) simp
hoelzl@49803
  1312
hoelzl@49803
  1313
  let ?f = "\<lambda>(x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) / Pxyz (x, y, z)"
hoelzl@49803
  1314
hoelzl@49803
  1315
  from subdensity_real[of snd, OF _ Pyz Pz]
wenzelm@53015
  1316
  have aeX1: "AE x in T \<Otimes>\<^sub>M P. Pz (snd x) = 0 \<longrightarrow> Pyz x = 0" by (auto simp: comp_def)
wenzelm@53015
  1317
  have aeX2: "AE x in T \<Otimes>\<^sub>M P. 0 \<le> Pz (snd x)"
hoelzl@50003
  1318
    using Pz by (intro TP.AE_pair_measure) (auto dest: distributed_real_AE)
hoelzl@49803
  1319
wenzelm@53015
  1320
  have aeX3: "AE y in T \<Otimes>\<^sub>M P. (\<integral>\<^sup>+ x. ereal (Pxz (x, snd y)) \<partial>S) = ereal (Pz (snd y))"
hoelzl@49803
  1321
    using Pz distributed_marginal_eq_joint2[OF P S Pz Pxz]
hoelzl@50003
  1322
    by (intro TP.AE_pair_measure) (auto dest: distributed_real_AE)
wenzelm@53015
  1323
  have "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<le> (\<integral>\<^sup>+ (x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) \<partial>(S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P))"
hoelzl@56996
  1324
    apply (subst nn_integral_density)
hoelzl@49803
  1325
    apply (rule distributed_borel_measurable[OF Pxyz])
hoelzl@49803
  1326
    apply (rule distributed_AE[OF Pxyz])
hoelzl@50003
  1327
    apply simp
hoelzl@56996
  1328
    apply (rule nn_integral_mono_AE)
hoelzl@49803
  1329
    using ae5 ae6 ae7 ae8
hoelzl@49803
  1330
    apply eventually_elim
hoelzl@56571
  1331
    apply auto
hoelzl@49803
  1332
    done
wenzelm@53015
  1333
  also have "\<dots> = (\<integral>\<^sup>+(y, z). \<integral>\<^sup>+ x. ereal (Pxz (x, z)) * ereal (Pyz (y, z) / Pz z) \<partial>S \<partial>T \<Otimes>\<^sub>M P)"
hoelzl@56996
  1334
    by (subst STP.nn_integral_snd[symmetric]) (auto simp add: split_beta')
wenzelm@53015
  1335
  also have "\<dots> = (\<integral>\<^sup>+x. ereal (Pyz x) * 1 \<partial>T \<Otimes>\<^sub>M P)"
hoelzl@56996
  1336
    apply (rule nn_integral_cong_AE)
hoelzl@49803
  1337
    using aeX1 aeX2 aeX3 distributed_AE[OF Pyz] AE_space
hoelzl@49803
  1338
    apply eventually_elim
hoelzl@49803
  1339
  proof (case_tac x, simp del: times_ereal.simps add: space_pair_measure)
hoelzl@49803
  1340
    fix a b assume "Pz b = 0 \<longrightarrow> Pyz (a, b) = 0" "0 \<le> Pz b" "a \<in> space T \<and> b \<in> space P"
wenzelm@53015
  1341
      "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)" 
wenzelm@53015
  1342
    then show "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
hoelzl@56996
  1343
      by (subst nn_integral_multc) auto
hoelzl@49803
  1344
  qed
hoelzl@49803
  1345
  also have "\<dots> = 1"
hoelzl@49803
  1346
    using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
hoelzl@56996
  1347
    by (subst nn_integral_density[symmetric]) auto
wenzelm@53015
  1348
  finally have le1: "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<le> 1" .
hoelzl@49803
  1349
  also have "\<dots> < \<infinity>" by simp
wenzelm@53015
  1350
  finally have fin: "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<noteq> \<infinity>" by simp
hoelzl@49803
  1351
wenzelm@53015
  1352
  have pos: "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<noteq> 0"
hoelzl@56996
  1353
    apply (subst nn_integral_density)
hoelzl@50003
  1354
    apply simp
hoelzl@49803
  1355
    apply (rule distributed_AE[OF Pxyz])
hoelzl@50003
  1356
    apply simp
hoelzl@49803
  1357
    apply (simp add: split_beta')
hoelzl@49803
  1358
  proof
hoelzl@49803
  1359
    let ?g = "\<lambda>x. ereal (if Pxyz x = 0 then 0 else Pxz (fst x, snd (snd x)) * Pyz (snd x) / Pz (snd (snd x)))"
wenzelm@53015
  1360
    assume "(\<integral>\<^sup>+ x. ?g x \<partial>(S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P)) = 0"
wenzelm@53015
  1361
    then have "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. ?g x \<le> 0"
hoelzl@56996
  1362
      by (intro nn_integral_0_iff_AE[THEN iffD1]) (auto intro!: borel_measurable_ereal measurable_If)
wenzelm@53015
  1363
    then have "AE x in S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P. Pxyz x = 0"
hoelzl@49803
  1364
      using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
hoelzl@49803
  1365
      by eventually_elim (auto split: split_if_asm simp: mult_le_0_iff divide_le_0_iff)
wenzelm@53015
  1366
    then have "(\<integral>\<^sup>+ x. ereal (Pxyz x) \<partial>S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) = 0"
hoelzl@56996
  1367
      by (subst nn_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
hoelzl@49803
  1368
    with P.emeasure_space_1 show False
hoelzl@56996
  1369
      by (subst (asm) emeasure_density) (auto cong: nn_integral_cong)
hoelzl@49803
  1370
  qed
hoelzl@49803
  1371
wenzelm@53015
  1372
  have neg: "(\<integral>\<^sup>+ x. - ?f x \<partial>?P) = 0"
hoelzl@56996
  1373
    apply (rule nn_integral_0_iff_AE[THEN iffD2])
hoelzl@50003
  1374
    apply (auto simp: split_beta') []
hoelzl@49803
  1375
    apply (subst AE_density)
hoelzl@50003
  1376
    apply (auto simp: split_beta') []
hoelzl@49803
  1377
    using ae5 ae6 ae7 ae8
hoelzl@49803
  1378
    apply eventually_elim
hoelzl@56571
  1379
    apply auto
hoelzl@49803
  1380
    done
hoelzl@49803
  1381
wenzelm@53015
  1382
  have I3: "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"
hoelzl@56993
  1383
    apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ integrable_diff[OF I1 I2]])
hoelzl@49803
  1384
    using ae
hoelzl@50003
  1385
    apply (auto simp: split_beta')
hoelzl@49803
  1386
    done
hoelzl@49803
  1387
wenzelm@53015
  1388
  have "- log b 1 \<le> - log b (integral\<^sup>L ?P ?f)"
hoelzl@49803
  1389
  proof (intro le_imp_neg_le log_le[OF b_gt_1])
hoelzl@56993
  1390
    have If: "integrable ?P ?f"
hoelzl@56993
  1391
      unfolding real_integrable_def
hoelzl@56993
  1392
    proof (intro conjI)
hoelzl@56993
  1393
      from neg show "(\<integral>\<^sup>+ x. - ?f x \<partial>?P) \<noteq> \<infinity>"
hoelzl@56993
  1394
        by simp
hoelzl@56993
  1395
      from fin show "(\<integral>\<^sup>+ x. ?f x \<partial>?P) \<noteq> \<infinity>"
hoelzl@56993
  1396
        by simp
hoelzl@56993
  1397
    qed simp
hoelzl@56993
  1398
    then have "(\<integral>\<^sup>+ x. ?f x \<partial>?P) = (\<integral>x. ?f x \<partial>?P)"
hoelzl@56996
  1399
      apply (rule nn_integral_eq_integral)
hoelzl@56993
  1400
      apply (subst AE_density)
hoelzl@56993
  1401
      apply simp
hoelzl@56993
  1402
      using ae5 ae6 ae7 ae8
hoelzl@56993
  1403
      apply eventually_elim
hoelzl@56993
  1404
      apply auto
hoelzl@56993
  1405
      done
hoelzl@56996
  1406
    with nn_integral_nonneg[of ?P ?f] pos le1
hoelzl@56993
  1407
    show "0 < (\<integral>x. ?f x \<partial>?P)" "(\<integral>x. ?f x \<partial>?P) \<le> 1"
hoelzl@56993
  1408
      by (simp_all add: one_ereal_def)
hoelzl@49803
  1409
  qed
wenzelm@53015
  1410
  also have "- log b (integral\<^sup>L ?P ?f) \<le> (\<integral> x. - log b (?f x) \<partial>?P)"
hoelzl@49803
  1411
  proof (rule P.jensens_inequality[where a=0 and b=1 and I="{0<..}"])
hoelzl@49803
  1412
    show "AE x in ?P. ?f x \<in> {0<..}"
hoelzl@49803
  1413
      unfolding AE_density[OF distributed_borel_measurable[OF Pxyz]]
hoelzl@49803
  1414
      using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
nipkow@56544
  1415
      by eventually_elim (auto)
hoelzl@49803
  1416
    show "integrable ?P ?f"
hoelzl@56993
  1417
      unfolding real_integrable_def
hoelzl@50003
  1418
      using fin neg by (auto simp: split_beta')
hoelzl@49803
  1419
    show "integrable ?P (\<lambda>x. - log b (?f x))"
hoelzl@56993
  1420
      apply (subst integrable_real_density)
hoelzl@50003
  1421
      apply simp
hoelzl@50003
  1422
      apply (auto intro!: distributed_real_AE[OF Pxyz]) []
hoelzl@50003
  1423
      apply simp
hoelzl@49803
  1424
      apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ I3])
hoelzl@50003
  1425
      apply simp
hoelzl@50003
  1426
      apply simp
hoelzl@49803
  1427
      using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
hoelzl@49803
  1428
      apply eventually_elim
hoelzl@49803
  1429
      apply (auto simp: log_divide_eq log_mult_eq zero_le_mult_iff zero_less_mult_iff zero_less_divide_iff field_simps)
hoelzl@49803
  1430
      done
hoelzl@49803
  1431
  qed (auto simp: b_gt_1 minus_log_convex)
hoelzl@49803
  1432
  also have "\<dots> = conditional_mutual_information b S T P X Y Z"
wenzelm@61808
  1433
    unfolding \<open>?eq\<close>
hoelzl@56993
  1434
    apply (subst integral_real_density)
hoelzl@50003
  1435
    apply simp
hoelzl@50003
  1436
    apply (auto intro!: distributed_real_AE[OF Pxyz]) []
hoelzl@50003
  1437
    apply simp
hoelzl@49803
  1438
    apply (intro integral_cong_AE)
hoelzl@49803
  1439
    using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
hoelzl@49803
  1440
    apply (auto simp: log_divide_eq zero_less_mult_iff zero_less_divide_iff field_simps)
hoelzl@49803
  1441
    done
hoelzl@49803
  1442
  finally show ?nonneg
hoelzl@49803
  1443
    by simp
hoelzl@49803
  1444
qed
hoelzl@49803
  1445
hoelzl@40859
  1446
lemma (in information_space) conditional_mutual_information_eq:
hoelzl@47694
  1447
  assumes Pz: "simple_distributed M Z Pz"
hoelzl@47694
  1448
  assumes Pyz: "simple_distributed M (\<lambda>x. (Y x, Z x)) Pyz"
hoelzl@47694
  1449
  assumes Pxz: "simple_distributed M (\<lambda>x. (X x, Z x)) Pxz"
hoelzl@47694
  1450
  assumes Pxyz: "simple_distributed M (\<lambda>x. (X x, Y x, Z x)) Pxyz"
hoelzl@47694
  1451
  shows "\<I>(X ; Y | Z) =
hoelzl@47694
  1452
   (\<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))))"
hoelzl@47694
  1453
proof (subst conditional_mutual_information_generic_eq[OF _ _ _ _
hoelzl@47694
  1454
    simple_distributed[OF Pz] simple_distributed_joint[OF Pyz] simple_distributed_joint[OF Pxz]
hoelzl@47694
  1455
    simple_distributed_joint2[OF Pxyz]])
hoelzl@47694
  1456
  note simple_distributed_joint2_finite[OF Pxyz, simp]
hoelzl@47694
  1457
  show "sigma_finite_measure (count_space (X ` space M))"
hoelzl@47694
  1458
    by (simp add: sigma_finite_measure_count_space_finite)
hoelzl@47694
  1459
  show "sigma_finite_measure (count_space (Y ` space M))"
hoelzl@47694
  1460
    by (simp add: sigma_finite_measure_count_space_finite)
hoelzl@47694
  1461
  show "sigma_finite_measure (count_space (Z ` space M))"
hoelzl@47694
  1462
    by (simp add: sigma_finite_measure_count_space_finite)
wenzelm@53015
  1463
  have "count_space (X ` space M) \<Otimes>\<^sub>M count_space (Y ` space M) \<Otimes>\<^sub>M count_space (Z ` space M) =
hoelzl@47694
  1464
      count_space (X`space M \<times> Y`space M \<times> Z`space M)"
hoelzl@47694
  1465
    (is "?P = ?C")
hoelzl@47694
  1466
    by (simp add: pair_measure_count_space)
hoelzl@40859
  1467
hoelzl@47694
  1468
  let ?Px = "\<lambda>x. measure M (X -` {x} \<inter> space M)"
wenzelm@53015
  1469
  have "(\<lambda>x. (X x, Z x)) \<in> measurable M (count_space (X ` space M) \<Otimes>\<^sub>M count_space (Z ` space M))"
hoelzl@47694
  1470
    using simple_distributed_joint[OF Pxz] by (rule distributed_measurable)
hoelzl@47694
  1471
  from measurable_comp[OF this measurable_fst]
hoelzl@47694
  1472
  have "random_variable (count_space (X ` space M)) X"
hoelzl@47694
  1473
    by (simp add: comp_def)
hoelzl@47694
  1474
  then have "simple_function M X"    
hoelzl@50002
  1475
    unfolding simple_function_def by (auto simp: measurable_count_space_eq2)
hoelzl@47694
  1476
  then have "simple_distributed M X ?Px"
hoelzl@47694
  1477
    by (rule simple_distributedI) auto
hoelzl@47694
  1478
  then show "distributed M (count_space (X ` space M)) X ?Px"
hoelzl@47694
  1479
    by (rule simple_distributed)
hoelzl@47694
  1480
hoelzl@47694
  1481
  let ?f = "(\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x, Z x)) ` space M then Pxyz x else 0)"
hoelzl@47694
  1482
  let ?g = "(\<lambda>x. if x \<in> (\<lambda>x. (Y x, Z x)) ` space M then Pyz x else 0)"
hoelzl@47694
  1483
  let ?h = "(\<lambda>x. if x \<in> (\<lambda>x. (X x, Z x)) ` space M then Pxz x else 0)"
hoelzl@47694
  1484
  show
hoelzl@47694
  1485
      "integrable ?P (\<lambda>(x, y, z). ?f (x, y, z) * log b (?f (x, y, z) / (?Px x * ?g (y, z))))"
hoelzl@47694
  1486
      "integrable ?P (\<lambda>(x, y, z). ?f (x, y, z) * log b (?h (x, z) / (?Px x * Pz z)))"
hoelzl@47694
  1487
    by (auto intro!: integrable_count_space simp: pair_measure_count_space)
hoelzl@47694
  1488
  let ?i = "\<lambda>x y z. ?f (x, y, z) * log b (?f (x, y, z) / (?h (x, z) * (?g (y, z) / Pz z)))"
hoelzl@47694
  1489
  let ?j = "\<lambda>x y z. Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z)))"
hoelzl@47694
  1490
  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)"
hoelzl@47694
  1491
    by (auto intro!: ext)
hoelzl@47694
  1492
  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)"
wenzelm@61808
  1493
    by (auto intro!: setsum.cong simp add: \<open>?P = ?C\<close> lebesgue_integral_count_space_finite simple_distributed_finite setsum.If_cases split_beta')
hoelzl@36624
  1494
qed
hoelzl@36624
  1495
hoelzl@47694
  1496
lemma (in information_space) conditional_mutual_information_nonneg:
hoelzl@47694
  1497
  assumes X: "simple_function M X" and Y: "simple_function M Y" and Z: "simple_function M Z"
hoelzl@47694
  1498
  shows "0 \<le> \<I>(X ; Y | Z)"
hoelzl@47694
  1499
proof -
wenzelm@53015
  1500
  have [simp]: "count_space (X ` space M) \<Otimes>\<^sub>M count_space (Y ` space M) \<Otimes>\<^sub>M count_space (Z ` space M) =
hoelzl@49787
  1501
      count_space (X`space M \<times> Y`space M \<times> Z`space M)"
hoelzl@49787
  1502
    by (simp add: pair_measure_count_space X Y Z simple_functionD)
hoelzl@49787
  1503
  note sf = sigma_finite_measure_count_space_finite[OF simple_functionD(1)]
hoelzl@49787
  1504
  note sd = simple_distributedI[OF _ refl]
hoelzl@49787
  1505
  note sp = simple_function_Pair
hoelzl@49787
  1506
  show ?thesis
hoelzl@49787
  1507
   apply (rule conditional_mutual_information_generic_nonneg[OF sf[OF X] sf[OF Y] sf[OF Z]])
hoelzl@49787
  1508
   apply (rule simple_distributed[OF sd[OF X]])
hoelzl@49787
  1509
   apply (rule simple_distributed[OF sd[OF Z]])
hoelzl@49787
  1510
   apply (rule simple_distributed_joint[OF sd[OF sp[OF Y Z]]])
hoelzl@49787
  1511
   apply (rule simple_distributed_joint[OF sd[OF sp[OF X Z]]])
hoelzl@49787
  1512
   apply (rule simple_distributed_joint2[OF sd[OF sp[OF X sp[OF Y Z]]]])
hoelzl@49787
  1513
   apply (auto intro!: integrable_count_space simp: X Y Z simple_functionD)
hoelzl@49787
  1514
   done
hoelzl@36080
  1515
qed
hoelzl@36080
  1516
wenzelm@61808
  1517
subsection \<open>Conditional Entropy\<close>
hoelzl@39097
  1518
hoelzl@36080
  1519
definition (in prob_space)
lp15@61609
  1520
  "conditional_entropy b S T X Y = - (\<integral>(x, y). log b (real_of_ereal (RN_deriv (S \<Otimes>\<^sub>M T) (distr M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x))) (x, y)) / 
lp15@61609
  1521
    real_of_ereal (RN_deriv T (distr M T Y) y)) \<partial>distr M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)))"
hoelzl@36080
  1522
hoelzl@40859
  1523
abbreviation (in information_space)
hoelzl@40859
  1524
  conditional_entropy_Pow ("\<H>'(_ | _')") where
hoelzl@47694
  1525
  "\<H>(X | Y) \<equiv> conditional_entropy b (count_space (X`space M)) (count_space (Y`space M)) X Y"
hoelzl@36080
  1526
hoelzl@49791
  1527
lemma (in information_space) conditional_entropy_generic_eq:
hoelzl@56993
  1528
  fixes Pxy :: "_ \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
hoelzl@49791
  1529
  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
hoelzl@50003
  1530
  assumes Py[measurable]: "distributed M T Y Py"
wenzelm@53015
  1531
  assumes Pxy[measurable]: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) Pxy"
wenzelm@53015
  1532
  shows "conditional_entropy b S T X Y = - (\<integral>(x, y). Pxy (x, y) * log b (Pxy (x, y) / Py y) \<partial>(S \<Otimes>\<^sub>M T))"
hoelzl@49791
  1533
proof -
hoelzl@49791
  1534
  interpret S: sigma_finite_measure S by fact
hoelzl@49791
  1535
  interpret T: sigma_finite_measure T by fact
hoelzl@49791
  1536
  interpret ST: pair_sigma_finite S T ..
hoelzl@49791
  1537
lp15@61609
  1538
  have "AE x in density (S \<Otimes>\<^sub>M T) (\<lambda>x. ereal (Pxy x)). Pxy x = real_of_ereal (RN_deriv (S \<Otimes>\<^sub>M T) (distr M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x))) x)"
hoelzl@49791
  1539
    unfolding AE_density[OF distributed_borel_measurable, OF Pxy]
hoelzl@49791
  1540
    unfolding distributed_distr_eq_density[OF Pxy]
hoelzl@49791
  1541
    using distributed_RN_deriv[OF Pxy]
hoelzl@49791
  1542
    by auto
hoelzl@49791
  1543
  moreover
lp15@61609
  1544
  have "AE x in density (S \<Otimes>\<^sub>M T) (\<lambda>x. ereal (Pxy x)). Py (snd x) = real_of_ereal (RN_deriv T (distr M T Y) (snd x))"
hoelzl@49791
  1545
    unfolding AE_density[OF distributed_borel_measurable, OF Pxy]
hoelzl@49791
  1546
    unfolding distributed_distr_eq_density[OF Py]
hoelzl@49791
  1547
    apply (rule ST.AE_pair_measure)
hoelzl@56993
  1548
    apply auto
hoelzl@49791
  1549
    using distributed_RN_deriv[OF Py]
hoelzl@49791
  1550
    apply auto
hoelzl@49791
  1551
    done    
hoelzl@49791
  1552
  ultimately
wenzelm@53015
  1553
  have "conditional_entropy b S T X Y = - (\<integral>x. Pxy x * log b (Pxy x / Py (snd x)) \<partial>(S \<Otimes>\<^sub>M T))"
hoelzl@49791
  1554
    unfolding conditional_entropy_def neg_equal_iff_equal
hoelzl@56993
  1555
    apply (subst integral_real_density[symmetric])
hoelzl@56993
  1556
    apply (auto simp: distributed_real_AE[OF Pxy] distributed_distr_eq_density[OF Pxy]
hoelzl@49791
  1557
                intro!: integral_cong_AE)
hoelzl@49791
  1558
    done
hoelzl@49791
  1559
  then show ?thesis by (simp add: split_beta')
hoelzl@49791
  1560
qed
hoelzl@49791
  1561
hoelzl@49791
  1562
lemma (in information_space) conditional_entropy_eq_entropy:
hoelzl@47694
  1563
  fixes Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
hoelzl@47694
  1564
  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
hoelzl@56993
  1565
  assumes Py[measurable]: "distributed M T Y Py"
hoelzl@56993
  1566
  assumes Pxy[measurable]: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) Pxy"
wenzelm@53015
  1567
  assumes I1: "integrable (S \<Otimes>\<^sub>M T) (\<lambda>x. Pxy x * log b (Pxy x))"
wenzelm@53015
  1568
  assumes I2: "integrable (S \<Otimes>\<^sub>M T) (\<lambda>x. Pxy x * log b (Py (snd x)))"
wenzelm@53015
  1569
  shows "conditional_entropy b S T X Y = entropy b (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) - entropy b T Y"
hoelzl@40859
  1570
proof -
hoelzl@47694
  1571
  interpret S: sigma_finite_measure S by fact
hoelzl@47694
  1572
  interpret T: sigma_finite_measure T by fact
hoelzl@47694
  1573
  interpret ST: pair_sigma_finite S T ..
hoelzl@47694
  1574
hoelzl@47694
  1575
  have "entropy b T Y = - (\<integral>y. Py y * log b (Py y) \<partial>T)"
hoelzl@49786
  1576
    by (rule entropy_distr[OF Py])
wenzelm@53015
  1577
  also have "\<dots> = - (\<integral>(x,y). Pxy (x,y) * log b (Py y) \<partial>(S \<Otimes>\<^sub>M T))"
hoelzl@47694
  1578
    using b_gt_1 Py[THEN distributed_real_measurable]
hoelzl@47694
  1579
    by (subst distributed_transform_integral[OF Pxy Py, where T=snd]) (auto intro!: integral_cong)
wenzelm@53015
  1580
  finally have e_eq: "entropy b T Y = - (\<integral>(x,y). Pxy (x,y) * log b (Py y) \<partial>(S \<Otimes>\<^sub>M T))" .
hoelzl@49791
  1581
wenzelm@53015
  1582
  have ae2: "AE x in S \<Otimes>\<^sub>M T. Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
hoelzl@47694
  1583
    by (intro subdensity_real[of snd, OF _ Pxy Py]) (auto intro: measurable_Pair)
wenzelm@53015
  1584
  moreover have ae4: "AE x in S \<Otimes>\<^sub>M T. 0 \<le> Py (snd x)"
hoelzl@47694
  1585
    using Py by (intro ST.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
hoelzl@49788
  1586
  moreover note ae5 = Pxy[THEN distributed_real_AE]
wenzelm@53015
  1587
  ultimately have "AE x in S \<Otimes>\<^sub>M T. 0 \<le> Pxy x \<and> 0 \<le> Py (snd x) \<and>
hoelzl@49790
  1588
    (Pxy x = 0 \<or> (Pxy x \<noteq> 0 \<longrightarrow> 0 < Pxy x \<and> 0 < Py (snd x)))"
hoelzl@47694
  1589
    by eventually_elim auto
wenzelm@53015
  1590
  then have ae: "AE x in S \<Otimes>\<^sub>M T.
hoelzl@47694
  1591
     Pxy x * log b (Pxy x) - Pxy x * log b (Py (snd x)) = Pxy x * log b (Pxy x / Py (snd x))"
nipkow@56544
  1592
    by eventually_elim (auto simp: log_simps field_simps b_gt_1)
hoelzl@49791
  1593
  have "conditional_entropy b S T X Y = 
wenzelm@53015
  1594
    - (\<integral>x. Pxy x * log b (Pxy x) - Pxy x * log b (Py (snd x)) \<partial>(S \<Otimes>\<^sub>M T))"
hoelzl@49791
  1595
    unfolding conditional_entropy_generic_eq[OF S T Py Pxy] neg_equal_iff_equal
hoelzl@49791
  1596
    apply (intro integral_cong_AE)
hoelzl@49791
  1597
    using ae
hoelzl@49791
  1598
    apply auto
hoelzl@47694
  1599
    done
wenzelm@53015
  1600
  also have "\<dots> = - (\<integral>x. Pxy x * log b (Pxy x) \<partial>(S \<Otimes>\<^sub>M T)) - - (\<integral>x.  Pxy x * log b (Py (snd x)) \<partial>(S \<Otimes>\<^sub>M T))"
hoelzl@49791
  1601
    by (simp add: integral_diff[OF I1 I2])
hoelzl@49791
  1602
  finally show ?thesis 
hoelzl@49791
  1603
    unfolding conditional_entropy_generic_eq[OF S T Py Pxy] entropy_distr[OF Pxy] e_eq
hoelzl@49791
  1604
    by (simp add: split_beta')
hoelzl@49791
  1605
qed
hoelzl@49791
  1606
hoelzl@49791
  1607
lemma (in information_space) conditional_entropy_eq_entropy_simple:
hoelzl@49791
  1608
  assumes X: "simple_function M X" and Y: "simple_function M Y"
wenzelm@53015
  1609
  shows "\<H>(X | Y) = entropy b (count_space (X`space M) \<Otimes>\<^sub>M count_space (Y`space M)) (\<lambda>x. (X x, Y x)) - \<H>(Y)"
hoelzl@49791
  1610
proof -
wenzelm@53015
  1611
  have "count_space (X ` space M) \<Otimes>\<^sub>M count_space (Y ` space M) = count_space (X`space M \<times> Y`space M)"
hoelzl@49791
  1612
    (is "?P = ?C") using X Y by (simp add: simple_functionD pair_measure_count_space)
hoelzl@49791
  1613
  show ?thesis
hoelzl@49791
  1614
    by (rule conditional_entropy_eq_entropy sigma_finite_measure_count_space_finite
hoelzl@49791
  1615
                 simple_functionD  X Y simple_distributed simple_distributedI[OF _ refl]
hoelzl@49791
  1616
                 simple_distributed_joint simple_function_Pair integrable_count_space)+
wenzelm@61808
  1617
       (auto simp: \<open>?P = ?C\<close> intro!: integrable_count_space simple_functionD  X Y)
hoelzl@39097
  1618
qed
hoelzl@39097
  1619
hoelzl@40859
  1620
lemma (in information_space) conditional_entropy_eq:
hoelzl@49792
  1621
  assumes Y: "simple_distributed M Y Py"
hoelzl@47694
  1622
  assumes XY: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"
hoelzl@47694
  1623
    shows "\<H>(X | Y) = - (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / Py y))"
hoelzl@47694
  1624
proof (subst conditional_entropy_generic_eq[OF _ _
hoelzl@49790
  1625
  simple_distributed[OF Y] simple_distributed_joint[OF XY]])
hoelzl@49792
  1626
  have "finite ((\<lambda>x. (X x, Y x))`space M)"
hoelzl@49792
  1627
    using XY unfolding simple_distributed_def by auto
hoelzl@49792
  1628
  from finite_imageI[OF this, of fst]
hoelzl@49792
  1629
  have [simp]: "finite (X`space M)"
haftmann@56154
  1630
    by (simp add: image_comp comp_def)
hoelzl@47694
  1631
  note Y[THEN simple_distributed_finite, simp]
hoelzl@47694
  1632
  show "sigma_finite_measure (count_space (X ` space M))"
hoelzl@47694
  1633
    by (simp add: sigma_finite_measure_count_space_finite)
hoelzl@47694
  1634
  show "sigma_finite_measure (count_space (Y ` space M))"
hoelzl@47694
  1635
    by (simp add: sigma_finite_measure_count_space_finite)
hoelzl@47694
  1636
  let ?f = "(\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy x else 0)"
wenzelm@53015
  1637
  have "count_space (X ` space M) \<Otimes>\<^sub>M count_space (Y ` space M) = count_space (X`space M \<times> Y`space M)"
hoelzl@47694
  1638
    (is "?P = ?C")
hoelzl@49792
  1639
    using Y by (simp add: simple_distributed_finite pair_measure_count_space)
hoelzl@47694
  1640
  have eq: "(\<lambda>(x, y). ?f (x, y) * log b (?f (x, y) / Py y)) =
hoelzl@47694
  1641
    (\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy x * log b (Pxy x / Py (snd x)) else 0)"
hoelzl@47694
  1642
    by auto
hoelzl@49792
  1643
  from Y show "- (\<integral> (x, y). ?f (x, y) * log b (?f (x, y) / Py y) \<partial>?P) =
hoelzl@47694
  1644
    - (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / Py y))"
wenzelm@61808
  1645
    by (auto intro!: setsum.cong simp add: \<open>?P = ?C\<close> lebesgue_integral_count_space_finite simple_distributed_finite eq setsum.If_cases split_beta')
hoelzl@47694
  1646
qed
hoelzl@39097
  1647
hoelzl@47694
  1648
lemma (in information_space) conditional_mutual_information_eq_conditional_entropy:
hoelzl@41689
  1649
  assumes X: "simple_function M X" and Y: "simple_function M Y"
hoelzl@47694
  1650
  shows "\<I>(X ; X | Y) = \<H>(X | Y)"
hoelzl@47694
  1651
proof -
hoelzl@47694
  1652
  def Py \<equiv> "\<lambda>x. if x \<in> Y`space M then measure M (Y -` {x} \<inter> space M) else 0"
hoelzl@47694
  1653
  def Pxy \<equiv> "\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x))`space M then measure M ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M) else 0"
hoelzl@47694
  1654
  def Pxxy \<equiv> "\<lambda>x. if x \<in> (\<lambda>x. (X x, X x, Y x))`space M then measure M ((\<lambda>x. (X x, X x, Y x)) -` {x} \<inter> space M) else 0"
hoelzl@47694
  1655
  let ?M = "X`space M \<times> X`space M \<times> Y`space M"
hoelzl@39097
  1656
hoelzl@47694
  1657
  note XY = simple_function_Pair[OF X Y]
hoelzl@47694
  1658
  note XXY = simple_function_Pair[OF X XY]
hoelzl@47694
  1659
  have Py: "simple_distributed M Y Py"
hoelzl@47694
  1660
    using Y by (rule simple_distributedI) (auto simp: Py_def)
hoelzl@47694
  1661
  have Pxy: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"
hoelzl@47694
  1662
    using XY by (rule simple_distributedI) (auto simp: Pxy_def)
hoelzl@47694
  1663
  have Pxxy: "simple_distributed M (\<lambda>x. (X x, X x, Y x)) Pxxy"
hoelzl@47694
  1664
    using XXY by (rule simple_distributedI) (auto simp: Pxxy_def)
hoelzl@47694
  1665
  have eq: "(\<lambda>x. (X x, X x, Y x)) ` space M = (\<lambda>(x, y). (x, x, y)) ` (\<lambda>x. (X x, Y x)) ` space M"
hoelzl@47694
  1666
    by auto
hoelzl@47694
  1667
  have inj: "\<And>A. inj_on (\<lambda>(x, y). (x, x, y)) A"
hoelzl@47694
  1668
    by (auto simp: inj_on_def)
hoelzl@47694
  1669
  have Pxxy_eq: "\<And>x y. Pxxy (x, x, y) = Pxy (x, y)"
hoelzl@47694
  1670
    by (auto simp: Pxxy_def Pxy_def intro!: arg_cong[where f=prob])
hoelzl@47694
  1671
  have "AE x in count_space ((\<lambda>x. (X x, Y x))`space M). Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
hoelzl@47694
  1672
    by (intro subdensity_real[of snd, OF _ Pxy[THEN simple_distributed] Py[THEN simple_distributed]]) (auto intro: measurable_Pair)
hoelzl@47694
  1673
  then show ?thesis
hoelzl@47694
  1674
    apply (subst conditional_mutual_information_eq[OF Py Pxy Pxy Pxxy])
hoelzl@49792
  1675
    apply (subst conditional_entropy_eq[OF Py Pxy])
haftmann@57418
  1676
    apply (auto intro!: setsum.cong simp: Pxxy_eq setsum_negf[symmetric] eq setsum.reindex[OF inj]
hoelzl@47694
  1677
                log_simps zero_less_mult_iff zero_le_mult_iff field_simps mult_less_0_iff AE_count_space)
hoelzl@47694
  1678
    using Py[THEN simple_distributed, THEN distributed_real_AE] Pxy[THEN simple_distributed, THEN distributed_real_AE]
hoelzl@49790
  1679
  apply (auto simp add: not_le[symmetric] AE_count_space)
hoelzl@47694
  1680
    done
hoelzl@47694
  1681
qed
hoelzl@47694
  1682
hoelzl@47694
  1683
lemma (in information_space) conditional_entropy_nonneg:
hoelzl@47694
  1684
  assumes X: "simple_function M X" and Y: "simple_function M Y" shows "0 \<le> \<H>(X | Y)"
hoelzl@47694
  1685
  using conditional_mutual_information_eq_conditional_entropy[OF X Y] conditional_mutual_information_nonneg[OF X X Y]
hoelzl@47694
  1686
  by simp
hoelzl@36080
  1687
wenzelm@61808
  1688
subsection \<open>Equalities\<close>
hoelzl@39097
  1689
hoelzl@47694
  1690
lemma (in information_space) mutual_information_eq_entropy_conditional_entropy_distr:
hoelzl@47694
  1691
  fixes Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real" and Pxy :: "('b \<times> 'c) \<Rightarrow> real"
hoelzl@47694
  1692
  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
hoelzl@56993
  1693
  assumes Px[measurable]: "distributed M S X Px" and Py[measurable]: "distributed M T Y Py"
hoelzl@56993
  1694
  assumes Pxy[measurable]: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) Pxy"
wenzelm@53015
  1695
  assumes Ix: "integrable(S \<Otimes>\<^sub>M T) (\<lambda>x. Pxy x * log b (Px (fst x)))"
wenzelm@53015
  1696
  assumes Iy: "integrable(S \<Otimes>\<^sub>M T) (\<lambda>x. Pxy x * log b (Py (snd x)))"
wenzelm@53015
  1697
  assumes Ixy: "integrable(S \<Otimes>\<^sub>M T) (\<lambda>x. Pxy x * log b (Pxy x))"
wenzelm@53015
  1698
  shows  "mutual_information b S T X Y = entropy b S X + entropy b T Y - entropy b (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x))"
hoelzl@40859
  1699
proof -
wenzelm@53015
  1700
  have X: "entropy b S X = - (\<integral>x. Pxy x * log b (Px (fst x)) \<partial>(S \<Otimes>\<^sub>M T))"
hoelzl@47694
  1701
    using b_gt_1 Px[THEN distributed_real_measurable]
hoelzl@49786
  1702
    apply (subst entropy_distr[OF Px])
hoelzl@47694
  1703
    apply (subst distributed_transform_integral[OF Pxy Px, where T=fst])
hoelzl@47694
  1704
    apply (auto intro!: integral_cong)
hoelzl@47694
  1705
    done
hoelzl@47694
  1706
wenzelm@53015
  1707
  have Y: "entropy b T Y = - (\<integral>x. Pxy x * log b (Py (snd x)) \<partial>(S \<Otimes>\<^sub>M T))"
hoelzl@47694
  1708
    using b_gt_1 Py[THEN distributed_real_measurable]
hoelzl@49786
  1709
    apply (subst entropy_distr[OF Py])
hoelzl@47694
  1710
    apply (subst distributed_transform_integral[OF Pxy Py, where T=snd])
hoelzl@47694
  1711
    apply (auto intro!: integral_cong)
hoelzl@47694
  1712
    done
hoelzl@47694
  1713
hoelzl@47694
  1714
  interpret S: sigma_finite_measure S by fact
hoelzl@47694
  1715
  interpret T: sigma_finite_measure T by fact
hoelzl@47694
  1716
  interpret ST: pair_sigma_finite S T ..
wenzelm@53015
  1717
  have ST: "sigma_finite_measure (S \<Otimes>\<^sub>M T)" ..
hoelzl@47694
  1718
wenzelm@53015
  1719
  have XY: "entropy b (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) = - (\<integral>x. Pxy x * log b (Pxy x) \<partial>(S \<Otimes>\<^sub>M T))"
hoelzl@49786
  1720
    by (subst entropy_distr[OF Pxy]) (auto intro!: integral_cong)
hoelzl@47694
  1721
  
wenzelm@53015
  1722
  have "AE x in S \<Otimes>\<^sub>M T. Px (fst x) = 0 \<longrightarrow> Pxy x = 0"
hoelzl@47694
  1723
    by (intro subdensity_real[of fst, OF _ Pxy Px]) (auto intro: measurable_Pair)
wenzelm@53015
  1724
  moreover have "AE x in S \<Otimes>\<^sub>M T. Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
hoelzl@47694
  1725
    by (intro subdensity_real[of snd, OF _ Pxy Py]) (auto intro: measurable_Pair)
wenzelm@53015
  1726
  moreover have "AE x in S \<Otimes>\<^sub>M T. 0 \<le> Px (fst x)"
hoelzl@47694
  1727
    using Px by (intro ST.AE_pair_measure) (auto simp: comp_def intro!: measurable_fst'' dest: distributed_real_AE distributed_real_measurable)
wenzelm@53015
  1728
  moreover have "AE x in S \<Otimes>\<^sub>M T. 0 \<le> Py (snd x)"
hoelzl@47694
  1729
    using Py by (intro ST.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
hoelzl@47694
  1730
  moreover note Pxy[THEN distributed_real_AE]
wenzelm@53015
  1731
  ultimately have "AE x in S \<Otimes>\<^sub>M T. Pxy x * log b (Pxy x) - Pxy x * log b (Px (fst x)) - Pxy x * log b (Py (snd x)) = 
hoelzl@47694
  1732
    Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x)))"
hoelzl@47694
  1733
    (is "AE x in _. ?f x = ?g x")
hoelzl@47694
  1734
  proof eventually_elim
wenzelm@60580
  1735
    case (elim x)
hoelzl@47694
  1736
    show ?case
hoelzl@47694
  1737
    proof cases
hoelzl@47694
  1738
      assume "Pxy x \<noteq> 0"
wenzelm@60580
  1739
      with elim have "0 < Px (fst x)" "0 < Py (snd x)" "0 < Pxy x"
hoelzl@47694
  1740
        by auto
hoelzl@47694
  1741
      then show ?thesis
nipkow@56544
  1742
        using b_gt_1 by (simp add: log_simps less_imp_le field_simps)
hoelzl@47694
  1743
    qed simp
hoelzl@47694
  1744
  qed
hoelzl@47694
  1745
wenzelm@53015
  1746
  have "entropy b S X + entropy b T Y - entropy b (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) = integral\<^sup>L (S \<Otimes>\<^sub>M T) ?f"
hoelzl@47694
  1747
    unfolding X Y XY
hoelzl@47694
  1748
    apply (subst integral_diff)
hoelzl@56993
  1749
    apply (intro integrable_diff Ixy Ix Iy)+
hoelzl@47694
  1750
    apply (subst integral_diff)
hoelzl@56993
  1751
    apply (intro Ixy Ix Iy)+
hoelzl@47694
  1752
    apply (simp add: field_simps)
hoelzl@47694
  1753
    done
wenzelm@53015
  1754
  also have "\<dots> = integral\<^sup>L (S \<Otimes>\<^sub>M T) ?g"
wenzelm@61808
  1755
    using \<open>AE x in _. ?f x = ?g x\<close> by (intro integral_cong_AE) auto
hoelzl@47694
  1756
  also have "\<dots> = mutual_information b S T X Y"
hoelzl@47694
  1757
    by (rule mutual_information_distr[OF S T Px Py Pxy, symmetric])
hoelzl@47694
  1758
  finally show ?thesis ..
hoelzl@47694
  1759
qed
hoelzl@47694
  1760
hoelzl@49802
  1761
lemma (in information_space) mutual_information_eq_entropy_conditional_entropy':
hoelzl@49802
  1762
  fixes Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real" and Pxy :: "('b \<times> 'c) \<Rightarrow> real"
hoelzl@49802
  1763
  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
hoelzl@49802
  1764
  assumes Px: "distributed M S X Px" and Py: "distributed M T Y Py"
wenzelm@53015
  1765
  assumes Pxy: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) Pxy"
wenzelm@53015
  1766
  assumes Ix: "integrable(S \<Otimes>\<^sub>M T) (\<lambda>x. Pxy x * log b (Px (fst x)))"
wenzelm@53015
  1767
  assumes Iy: "integrable(S \<Otimes>\<^sub>M T) (\<lambda>x. Pxy x * log b (Py (snd x)))"
wenzelm@53015
  1768
  assumes Ixy: "integrable(S \<Otimes>\<^sub>M T) (\<lambda>x. Pxy x * log b (Pxy x))"
hoelzl@49802
  1769
  shows  "mutual_information b S T X Y = entropy b S X - conditional_entropy b S T X Y"
hoelzl@49802
  1770
  using
hoelzl@49802
  1771
    mutual_information_eq_entropy_conditional_entropy_distr[OF S T Px Py Pxy Ix Iy Ixy]
hoelzl@49802
  1772
    conditional_entropy_eq_entropy[OF S T Py Pxy Ixy Iy]
hoelzl@49802
  1773
  by simp
hoelzl@49802
  1774
hoelzl@47694
  1775
lemma (in information_space) mutual_information_eq_entropy_conditional_entropy:
hoelzl@47694
  1776
  assumes sf_X: "simple_function M X" and sf_Y: "simple_function M Y"
hoelzl@47694
  1777
  shows  "\<I>(X ; Y) = \<H>(X) - \<H>(X | Y)"
hoelzl@47694
  1778
proof -
hoelzl@47694
  1779
  have X: "simple_distributed M X (\<lambda>x. measure M (X -` {x} \<inter> space M))"
hoelzl@47694
  1780
    using sf_X by (rule simple_distributedI) auto
hoelzl@47694
  1781
  have Y: "simple_distributed M Y (\<lambda>x. measure M (Y -` {x} \<inter> space M))"
hoelzl@47694
  1782
    using sf_Y by (rule simple_distributedI) auto
hoelzl@47694
  1783
  have sf_XY: "simple_function M (\<lambda>x. (X x, Y x))"
hoelzl@47694
  1784
    using sf_X sf_Y by (rule simple_function_Pair)
hoelzl@47694
  1785
  then have XY: "simple_distributed M (\<lambda>x. (X x, Y x)) (\<lambda>x. measure M ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M))"
hoelzl@47694
  1786
    by (rule simple_distributedI) auto
hoelzl@47694
  1787
  from simple_distributed_joint_finite[OF this, simp]
wenzelm@53015
  1788
  have eq: "count_space (X ` space M) \<Otimes>\<^sub>M count_space (Y ` space M) = count_space (X ` space M \<times> Y ` space M)"
hoelzl@47694
  1789
    by (simp add: pair_measure_count_space)
hoelzl@47694
  1790
wenzelm@53015
  1791
  have "\<I>(X ; Y) = \<H>(X) + \<H>(Y) - entropy b (count_space (X`space M) \<Otimes>\<^sub>M count_space (Y`space M)) (\<lambda>x. (X x, Y x))"
hoelzl@47694
  1792
    using sigma_finite_measure_count_space_finite sigma_finite_measure_count_space_finite simple_distributed[OF X] simple_distributed[OF Y] simple_distributed_joint[OF XY]
hoelzl@47694
  1793
    by (rule mutual_information_eq_entropy_conditional_entropy_distr) (auto simp: eq integrable_count_space)
hoelzl@47694
  1794
  then show ?thesis
hoelzl@49791
  1795
    unfolding conditional_entropy_eq_entropy_simple[OF sf_X sf_Y] by simp
hoelzl@47694
  1796
qed
hoelzl@47694
  1797
hoelzl@47694
  1798
lemma (in information_space) mutual_information_nonneg_simple:
hoelzl@47694
  1799
  assumes sf_X: "simple_function M X" and sf_Y: "simple_function M Y"
hoelzl@47694
  1800
  shows  "0 \<le> \<I>(X ; Y)"
hoelzl@47694
  1801
proof -
hoelzl@47694
  1802
  have X: "simple_distributed M X (\<lambda>x. measure M (X -` {x} \<inter> space M))"
hoelzl@47694
  1803
    using sf_X by (rule simple_distributedI) auto
hoelzl@47694
  1804
  have Y: "simple_distributed M Y (\<lambda>x. measure M (Y -` {x} \<inter> space M))"
hoelzl@47694
  1805
    using sf_Y by (rule simple_distributedI) auto
hoelzl@47694
  1806
hoelzl@47694
  1807
  have sf_XY: "simple_function M (\<lambda>x. (X x, Y x))"
hoelzl@47694
  1808
    using sf_X sf_Y by (rule simple_function_Pair)
hoelzl@47694
  1809
  then have XY: "simple_distributed M (\<lambda>x. (X x, Y x)) (\<lambda>x. measure M ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M))"
hoelzl@47694
  1810
    by (rule simple_distributedI) auto
hoelzl@47694
  1811
hoelzl@47694
  1812
  from simple_distributed_joint_finite[OF this, simp]
wenzelm@53015
  1813
  have eq: "count_space (X ` space M) \<Otimes>\<^sub>M count_space (Y ` space M) = count_space (X ` space M \<times> Y ` space M)"
hoelzl@47694
  1814
    by (simp add: pair_measure_count_space)
hoelzl@47694
  1815
hoelzl@40859
  1816
  show ?thesis
hoelzl@47694
  1817
    by (rule mutual_information_nonneg[OF _ _ simple_distributed[OF X] simple_distributed[OF Y] simple_distributed_joint[OF XY]])
hoelzl@47694
  1818
       (simp_all add: eq integrable_count_space sigma_finite_measure_count_space_finite)
hoelzl@40859
  1819
qed
hoelzl@36080
  1820
hoelzl@40859
  1821
lemma (in information_space) conditional_entropy_less_eq_entropy:
hoelzl@41689
  1822
  assumes X: "simple_function M X" and Z: "simple_function M Z"
hoelzl@40859
  1823
  shows "\<H>(X | Z) \<le> \<H>(X)"
hoelzl@36624
  1824
proof -
hoelzl@47694
  1825
  have "0 \<le> \<I>(X ; Z)" using X Z by (rule mutual_information_nonneg_simple)
hoelzl@47694
  1826
  also have "\<I>(X ; Z) = \<H>(X) - \<H>(X | Z)" using mutual_information_eq_entropy_conditional_entropy[OF assms] .
hoelzl@47694
  1827
  finally show ?thesis by auto
hoelzl@36080
  1828
qed
hoelzl@36080
  1829
hoelzl@49803
  1830
lemma (in information_space) 
hoelzl@49803
  1831
  fixes Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real" and Pxy :: "('b \<times> 'c) \<Rightarrow> real"
hoelzl@49803
  1832
  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
hoelzl@49803
  1833
  assumes Px: "finite_entropy S X Px" and Py: "finite_entropy T Y Py"
wenzelm@53015
  1834
  assumes Pxy: "finite_entropy (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) Pxy"
hoelzl@49803
  1835
  shows "conditional_entropy b S T X Y \<le> entropy b S X"
hoelzl@49803
  1836
proof -
hoelzl@49803
  1837
hoelzl@49803
  1838
  have "0 \<le> mutual_information b S T X Y" 
hoelzl@49803
  1839
    by (rule mutual_information_nonneg') fact+
hoelzl@49803
  1840
  also have "\<dots> = entropy b S X - conditional_entropy b S T X Y"
hoelzl@49803
  1841
    apply (rule mutual_information_eq_entropy_conditional_entropy')
hoelzl@49803
  1842
    using assms
hoelzl@49803
  1843
    by (auto intro!: finite_entropy_integrable finite_entropy_distributed
hoelzl@49803
  1844
      finite_entropy_integrable_transform[OF Px]
hoelzl@49803
  1845
      finite_entropy_integrable_transform[OF Py])
hoelzl@49803
  1846
  finally show ?thesis by auto
hoelzl@49803
  1847
qed
hoelzl@49803
  1848
hoelzl@40859
  1849
lemma (in information_space) entropy_chain_rule:
hoelzl@41689
  1850
  assumes X: "simple_function M X" and Y: "simple_function M Y"
hoelzl@40859
  1851
  shows  "\<H>(\<lambda>x. (X x, Y x)) = \<H>(X) + \<H>(Y|X)"
hoelzl@40859
  1852
proof -
hoelzl@47694
  1853
  note XY = simple_distributedI[OF simple_function_Pair[OF X Y] refl]
hoelzl@47694
  1854
  note YX = simple_distributedI[OF simple_function_Pair[OF Y X] refl]
hoelzl@47694
  1855
  note simple_distributed_joint_finite[OF this, simp]
hoelzl@47694
  1856
  let ?f = "\<lambda>x. prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)"
hoelzl@47694
  1857
  let ?g = "\<lambda>x. prob ((\<lambda>x. (Y x, X x)) -` {x} \<inter> space M)"
hoelzl@47694
  1858
  let ?h = "\<lambda>x. if x \<in> (\<lambda>x. (Y x, X x)) ` space M then prob ((\<lambda>x. (Y x, X x)) -` {x} \<inter> space M) else 0"
hoelzl@47694
  1859
  have "\<H>(\<lambda>x. (X x, Y x)) = - (\<Sum>x\<in>(\<lambda>x. (X x, Y x)) ` space M. ?f x * log b (?f x))"
hoelzl@47694
  1860
    using XY by (rule entropy_simple_distributed)
hoelzl@47694
  1861
  also have "\<dots> = - (\<Sum>x\<in>(\<lambda>(x, y). (y, x)) ` (\<lambda>x. (X x, Y x)) ` space M. ?g x * log b (?g x))"
haftmann@57418
  1862
    by (subst (2) setsum.reindex) (auto simp: inj_on_def intro!: setsum.cong arg_cong[where f="\<lambda>A. prob A * log b (prob A)"])
hoelzl@47694
  1863
  also have "\<dots> = - (\<Sum>x\<in>(\<lambda>x. (Y x, X x)) ` space M. ?h x * log b (?h x))"
haftmann@57418
  1864
    by (auto intro!: setsum.cong)
wenzelm@53015
  1865
  also have "\<dots> = entropy b (count_space (Y ` space M) \<Otimes>\<^sub>M count_space (X ` space M)) (\<lambda>x. (Y x, X x))"
hoelzl@49786
  1866
    by (subst entropy_distr[OF simple_distributed_joint[OF YX]])
hoelzl@47694
  1867
       (auto simp: pair_measure_count_space sigma_finite_measure_count_space_finite lebesgue_integral_count_space_finite
haftmann@57418
  1868
             cong del: setsum.cong  intro!: setsum.mono_neutral_left)
wenzelm@53015
  1869
  finally have "\<H>(\<lambda>x. (X x, Y x)) = entropy b (count_space (Y ` space M) \<Otimes>\<^sub>M count_space (X ` space M)) (\<lambda>x. (Y x, X x))" .
hoelzl@47694
  1870
  then show ?thesis
hoelzl@49791
  1871
    unfolding conditional_entropy_eq_entropy_simple[OF Y X] by simp
hoelzl@36624
  1872
qed
hoelzl@36624
  1873
hoelzl@40859
  1874
lemma (in information_space) entropy_partition:
hoelzl@47694
  1875
  assumes X: "simple_function M X"
hoelzl@47694
  1876
  shows "\<H>(X) = \<H>(f \<circ> X) + \<H>(X|f \<circ> X)"
hoelzl@36624
  1877
proof -
hoelzl@47694
  1878
  note fX = simple_function_compose[OF X, of f]  
hoelzl@47694
  1879
  have eq: "(\<lambda>x. ((f \<circ> X) x, X x)) ` space M = (\<lambda>x. (f x, x)) ` X ` space M" by auto
hoelzl@47694
  1880
  have inj: "\<And>A. inj_on (\<lambda>x. (f x, x)) A"
hoelzl@47694
  1881
    by (auto simp: inj_on_def)
hoelzl@47694
  1882
  show ?thesis
hoelzl@47694
  1883
    apply (subst entropy_chain_rule[symmetric, OF fX X])
hoelzl@47694
  1884
    apply (subst entropy_simple_distributed[OF simple_distributedI[OF simple_function_Pair[OF fX X] refl]])
hoelzl@47694
  1885
    apply (subst entropy_simple_distributed[OF simple_distributedI[OF X refl]])
hoelzl@47694
  1886
    unfolding eq
haftmann@57418
  1887
    apply (subst setsum.reindex[OF inj])
haftmann@57418
  1888
    apply (auto intro!: setsum.cong arg_cong[where f="\<lambda>A. prob A * log b (prob A)"])
hoelzl@47694
  1889
    done
hoelzl@36624
  1890
qed
hoelzl@36624
  1891
hoelzl@40859
  1892
corollary (in information_space) entropy_data_processing:
hoelzl@41689
  1893
  assumes X: "simple_function M X" shows "\<H>(f \<circ> X) \<le> \<H>(X)"
hoelzl@40859
  1894
proof -
hoelzl@47694
  1895
  note fX = simple_function_compose[OF X, of f]
hoelzl@47694
  1896
  from X have "\<H>(X) = \<H>(f\<circ>X) + \<H>(X|f\<circ>X)" by (rule entropy_partition)
hoelzl@40859
  1897
  then show "\<H>(f \<circ> X) \<le> \<H>(X)"
hoelzl@47694
  1898
    by (auto intro: conditional_entropy_nonneg[OF X fX])
hoelzl@40859
  1899
qed
hoelzl@36624
  1900
hoelzl@40859
  1901
corollary (in information_space) entropy_of_inj:
hoelzl@41689
  1902
  assumes X: "simple_function M X" and inj: "inj_on f (X`space M)"
hoelzl@36624
  1903
  shows "\<H>(f \<circ> X) = \<H>(X)"
hoelzl@36624
  1904
proof (rule antisym)
hoelzl@40859
  1905
  show "\<H>(f \<circ> X) \<le> \<H>(X)" using entropy_data_processing[OF X] .
hoelzl@36624
  1906
next
hoelzl@41689
  1907
  have sf: "simple_function M (f \<circ> X)"
hoelzl@40859
  1908
    using X by auto
hoelzl@36624
  1909
  have "\<H>(X) = \<H>(the_inv_into (X`space M) f \<circ> (f \<circ> X))"
hoelzl@47694
  1910
    unfolding o_assoc
hoelzl@47694
  1911
    apply (subst entropy_simple_distributed[OF simple_distributedI[OF X refl]])
hoelzl@47694
  1912
    apply (subst entropy_simple_distributed[OF simple_distributedI[OF simple_function_compose[OF X]], where f="\<lambda>x. prob (X -` {x} \<inter> space M)"])
haftmann@57418
  1913
    apply (auto intro!: setsum.cong arg_cong[where f=prob] image_eqI simp: the_inv_into_f_f[OF inj] comp_def)
hoelzl@47694
  1914
    done
hoelzl@36624
  1915
  also have "... \<le> \<H>(f \<circ> X)"
hoelzl@40859
  1916
    using entropy_data_processing[OF sf] .
hoelzl@36624
  1917
  finally show "\<H>(X) \<le> \<H>(f \<circ> X)" .
hoelzl@36624
  1918
qed
hoelzl@36624
  1919
hoelzl@36080
  1920
end