src/HOL/Probability/Information.thy
author hoelzl
Wed Oct 10 12:12:36 2012 +0200 (2012-10-10)
changeset 49802 dd8dffaf84b9
parent 49792 43f49922811d
child 49803 2f076e377703
permissions -rw-r--r--
continuous version of mutual_information_eq_entropy_conditional_entropy
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
hoelzl@42067
     6
header {*Information theory*}
hoelzl@42067
     7
hoelzl@36080
     8
theory Information
wenzelm@41413
     9
imports
hoelzl@43340
    10
  Independent_Family
hoelzl@43556
    11
  Radon_Nikodym
wenzelm@41413
    12
  "~~/src/HOL/Library/Convex"
hoelzl@36080
    13
begin
hoelzl@36080
    14
hoelzl@39097
    15
lemma log_le: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> x \<le> y \<Longrightarrow> log a x \<le> log a y"
hoelzl@39097
    16
  by (subst log_le_cancel_iff) auto
hoelzl@39097
    17
hoelzl@39097
    18
lemma log_less: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> x < y \<Longrightarrow> log a x < log a y"
hoelzl@39097
    19
  by (subst log_less_cancel_iff) auto
hoelzl@39097
    20
hoelzl@39097
    21
lemma setsum_cartesian_product':
hoelzl@39097
    22
  "(\<Sum>x\<in>A \<times> B. f x) = (\<Sum>x\<in>A. setsum (\<lambda>y. f (x, y)) B)"
hoelzl@39097
    23
  unfolding setsum_cartesian_product by simp
hoelzl@39097
    24
hoelzl@39097
    25
lemma split_pairs:
hoelzl@40859
    26
  "((A, B) = X) \<longleftrightarrow> (fst X = A \<and> snd X = B)" and
hoelzl@40859
    27
  "(X = (A, B)) \<longleftrightarrow> (fst X = A \<and> snd X = B)" by auto
hoelzl@38656
    28
hoelzl@38656
    29
section "Information theory"
hoelzl@38656
    30
hoelzl@40859
    31
locale information_space = prob_space +
hoelzl@38656
    32
  fixes b :: real assumes b_gt_1: "1 < b"
hoelzl@38656
    33
hoelzl@40859
    34
context information_space
hoelzl@38656
    35
begin
hoelzl@38656
    36
hoelzl@40859
    37
text {* Introduce some simplification rules for logarithm of base @{term b}. *}
hoelzl@40859
    38
hoelzl@40859
    39
lemma log_neg_const:
hoelzl@40859
    40
  assumes "x \<le> 0"
hoelzl@40859
    41
  shows "log b x = log b 0"
hoelzl@36624
    42
proof -
hoelzl@40859
    43
  { fix u :: real
hoelzl@40859
    44
    have "x \<le> 0" by fact
hoelzl@40859
    45
    also have "0 < exp u"
hoelzl@40859
    46
      using exp_gt_zero .
hoelzl@40859
    47
    finally have "exp u \<noteq> x"
hoelzl@40859
    48
      by auto }
hoelzl@40859
    49
  then show "log b x = log b 0"
hoelzl@40859
    50
    by (simp add: log_def ln_def)
hoelzl@38656
    51
qed
hoelzl@38656
    52
hoelzl@40859
    53
lemma log_mult_eq:
hoelzl@40859
    54
  "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
    55
  using log_mult[of b "\<bar>A\<bar>" "\<bar>B\<bar>"] b_gt_1 log_neg_const[of "A * B"]
hoelzl@40859
    56
  by (auto simp: zero_less_mult_iff mult_le_0_iff)
hoelzl@38656
    57
hoelzl@40859
    58
lemma log_inverse_eq:
hoelzl@40859
    59
  "log b (inverse B) = (if 0 < B then - log b B else log b 0)"
hoelzl@40859
    60
  using log_inverse[of b B] log_neg_const[of "inverse B"] b_gt_1 by simp
hoelzl@36080
    61
hoelzl@40859
    62
lemma log_divide_eq:
hoelzl@40859
    63
  "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
    64
  unfolding divide_inverse log_mult_eq log_inverse_eq abs_inverse
hoelzl@40859
    65
  by (auto simp: zero_less_mult_iff mult_le_0_iff)
hoelzl@38656
    66
hoelzl@40859
    67
lemmas log_simps = log_mult_eq log_inverse_eq log_divide_eq
hoelzl@38656
    68
hoelzl@38656
    69
end
hoelzl@38656
    70
hoelzl@39097
    71
subsection "Kullback$-$Leibler divergence"
hoelzl@36080
    72
hoelzl@39097
    73
text {* The Kullback$-$Leibler divergence is also known as relative entropy or
hoelzl@39097
    74
Kullback$-$Leibler distance. *}
hoelzl@39097
    75
hoelzl@39097
    76
definition
hoelzl@47694
    77
  "entropy_density b M N = log b \<circ> real \<circ> RN_deriv M N"
hoelzl@43340
    78
hoelzl@43340
    79
definition
hoelzl@47694
    80
  "KL_divergence b M N = integral\<^isup>L N (entropy_density b M N)"
hoelzl@43340
    81
hoelzl@43340
    82
lemma (in information_space) measurable_entropy_density:
hoelzl@47694
    83
  assumes ac: "absolutely_continuous M N" "sets N = events"
hoelzl@47694
    84
  shows "entropy_density b M N \<in> borel_measurable M"
hoelzl@43340
    85
proof -
hoelzl@47694
    86
  from borel_measurable_RN_deriv[OF ac] b_gt_1 show ?thesis
hoelzl@43340
    87
    unfolding entropy_density_def
hoelzl@43340
    88
    by (intro measurable_comp) auto
hoelzl@43340
    89
qed
hoelzl@43340
    90
hoelzl@47694
    91
lemma (in sigma_finite_measure) KL_density:
hoelzl@47694
    92
  fixes f :: "'a \<Rightarrow> real"
hoelzl@47694
    93
  assumes "1 < b"
hoelzl@47694
    94
  assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
hoelzl@47694
    95
  shows "KL_divergence b M (density M f) = (\<integral>x. f x * log b (f x) \<partial>M)"
hoelzl@47694
    96
  unfolding KL_divergence_def
hoelzl@47694
    97
proof (subst integral_density)
hoelzl@47694
    98
  show "entropy_density b M (density M (\<lambda>x. ereal (f x))) \<in> borel_measurable M"
hoelzl@49776
    99
    using f
hoelzl@47694
   100
    by (auto simp: comp_def entropy_density_def intro!: borel_measurable_log borel_measurable_RN_deriv_density)
hoelzl@47694
   101
  have "density M (RN_deriv M (density M f)) = density M f"
hoelzl@47694
   102
    using f by (intro density_RN_deriv_density) auto
hoelzl@47694
   103
  then have eq: "AE x in M. RN_deriv M (density M f) x = f x"
hoelzl@47694
   104
    using f
hoelzl@47694
   105
    by (intro density_unique)
hoelzl@47694
   106
       (auto intro!: borel_measurable_log borel_measurable_RN_deriv_density simp: RN_deriv_density_nonneg)
hoelzl@47694
   107
  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
   108
    apply (intro integral_cong_AE)
hoelzl@47694
   109
    using eq
hoelzl@47694
   110
    apply eventually_elim
hoelzl@47694
   111
    apply (auto simp: entropy_density_def)
hoelzl@47694
   112
    done
hoelzl@47694
   113
qed fact+
hoelzl@43340
   114
hoelzl@47694
   115
lemma (in sigma_finite_measure) KL_density_density:
hoelzl@47694
   116
  fixes f g :: "'a \<Rightarrow> real"
hoelzl@47694
   117
  assumes "1 < b"
hoelzl@47694
   118
  assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
hoelzl@47694
   119
  assumes g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
hoelzl@47694
   120
  assumes ac: "AE x in M. f x = 0 \<longrightarrow> g x = 0"
hoelzl@47694
   121
  shows "KL_divergence b (density M f) (density M g) = (\<integral>x. g x * log b (g x / f x) \<partial>M)"
hoelzl@47694
   122
proof -
hoelzl@47694
   123
  interpret Mf: sigma_finite_measure "density M f"
hoelzl@47694
   124
    using f by (subst sigma_finite_iff_density_finite) auto
hoelzl@47694
   125
  have "KL_divergence b (density M f) (density M g) =
hoelzl@47694
   126
    KL_divergence b (density M f) (density (density M f) (\<lambda>x. g x / f x))"
hoelzl@47694
   127
    using f g ac by (subst density_density_divide) simp_all
hoelzl@47694
   128
  also have "\<dots> = (\<integral>x. (g x / f x) * log b (g x / f x) \<partial>density M f)"
hoelzl@47694
   129
    using f g `1 < b` by (intro Mf.KL_density) (auto simp: AE_density divide_nonneg_nonneg)
hoelzl@47694
   130
  also have "\<dots> = (\<integral>x. g x * log b (g x / f x) \<partial>M)"
hoelzl@47694
   131
    using ac f g `1 < b` by (subst integral_density) (auto intro!: integral_cong_AE)
hoelzl@47694
   132
  finally show ?thesis .
hoelzl@47694
   133
qed
hoelzl@43340
   134
hoelzl@47694
   135
lemma (in information_space) KL_gt_0:
hoelzl@47694
   136
  fixes D :: "'a \<Rightarrow> real"
hoelzl@47694
   137
  assumes "prob_space (density M D)"
hoelzl@47694
   138
  assumes D: "D \<in> borel_measurable M" "AE x in M. 0 \<le> D x"
hoelzl@47694
   139
  assumes int: "integrable M (\<lambda>x. D x * log b (D x))"
hoelzl@47694
   140
  assumes A: "density M D \<noteq> M"
hoelzl@47694
   141
  shows "0 < KL_divergence b M (density M D)"
hoelzl@47694
   142
proof -
hoelzl@47694
   143
  interpret N: prob_space "density M D" by fact
hoelzl@43340
   144
hoelzl@47694
   145
  obtain A where "A \<in> sets M" "emeasure (density M D) A \<noteq> emeasure M A"
hoelzl@47694
   146
    using measure_eqI[of "density M D" M] `density M D \<noteq> M` by auto
hoelzl@47694
   147
hoelzl@47694
   148
  let ?D_set = "{x\<in>space M. D x \<noteq> 0}"
hoelzl@47694
   149
  have [simp, intro]: "?D_set \<in> sets M"
hoelzl@47694
   150
    using D by auto
hoelzl@43340
   151
hoelzl@43920
   152
  have D_neg: "(\<integral>\<^isup>+ x. ereal (- D x) \<partial>M) = 0"
hoelzl@43340
   153
    using D by (subst positive_integral_0_iff_AE) auto
hoelzl@43340
   154
hoelzl@47694
   155
  have "(\<integral>\<^isup>+ x. ereal (D x) \<partial>M) = emeasure (density M D) (space M)"
hoelzl@47694
   156
    using D by (simp add: emeasure_density cong: positive_integral_cong)
hoelzl@43920
   157
  then have D_pos: "(\<integral>\<^isup>+ x. ereal (D x) \<partial>M) = 1"
hoelzl@47694
   158
    using N.emeasure_space_1 by simp
hoelzl@43340
   159
hoelzl@47694
   160
  have "integrable M D" "integral\<^isup>L M D = 1"
hoelzl@47694
   161
    using D D_pos D_neg unfolding integrable_def lebesgue_integral_def by simp_all
hoelzl@43340
   162
hoelzl@47694
   163
  have "0 \<le> 1 - measure M ?D_set"
hoelzl@43340
   164
    using prob_le_1 by (auto simp: field_simps)
hoelzl@43340
   165
  also have "\<dots> = (\<integral> x. D x - indicator ?D_set x \<partial>M)"
hoelzl@43340
   166
    using `integrable M D` `integral\<^isup>L M D = 1`
hoelzl@47694
   167
    by (simp add: emeasure_eq_measure)
hoelzl@47694
   168
  also have "\<dots> < (\<integral> x. D x * (ln b * log b (D x)) \<partial>M)"
hoelzl@43340
   169
  proof (rule integral_less_AE)
hoelzl@43340
   170
    show "integrable M (\<lambda>x. D x - indicator ?D_set x)"
hoelzl@43340
   171
      using `integrable M D`
hoelzl@43340
   172
      by (intro integral_diff integral_indicator) auto
hoelzl@43340
   173
  next
hoelzl@47694
   174
    from integral_cmult(1)[OF int, of "ln b"]
hoelzl@47694
   175
    show "integrable M (\<lambda>x. D x * (ln b * log b (D x)))" 
hoelzl@47694
   176
      by (simp add: ac_simps)
hoelzl@43340
   177
  next
hoelzl@47694
   178
    show "emeasure M {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<noteq> 0"
hoelzl@43340
   179
    proof
hoelzl@47694
   180
      assume eq_0: "emeasure M {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} = 0"
hoelzl@47694
   181
      then have disj: "AE x in M. D x = 1 \<or> D x = 0"
hoelzl@43340
   182
        using D(1) by (auto intro!: AE_I[OF subset_refl] sets_Collect)
hoelzl@43340
   183
hoelzl@47694
   184
      have "emeasure M {x\<in>space M. D x = 1} = (\<integral>\<^isup>+ x. indicator {x\<in>space M. D x = 1} x \<partial>M)"
hoelzl@43340
   185
        using D(1) by auto
hoelzl@47694
   186
      also have "\<dots> = (\<integral>\<^isup>+ x. ereal (D x) \<partial>M)"
hoelzl@43920
   187
        using disj by (auto intro!: positive_integral_cong_AE simp: indicator_def one_ereal_def)
hoelzl@47694
   188
      finally have "AE x in M. D x = 1"
hoelzl@47694
   189
        using D D_pos by (intro AE_I_eq_1) auto
hoelzl@43920
   190
      then have "(\<integral>\<^isup>+x. indicator A x\<partial>M) = (\<integral>\<^isup>+x. ereal (D x) * indicator A x\<partial>M)"
hoelzl@43920
   191
        by (intro positive_integral_cong_AE) (auto simp: one_ereal_def[symmetric])
hoelzl@47694
   192
      also have "\<dots> = density M D A"
hoelzl@47694
   193
        using `A \<in> sets M` D by (simp add: emeasure_density)
hoelzl@47694
   194
      finally show False using `A \<in> sets M` `emeasure (density M D) A \<noteq> emeasure M A` by simp
hoelzl@43340
   195
    qed
hoelzl@43340
   196
    show "{x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<in> sets M"
hoelzl@47694
   197
      using D(1) by (auto intro: sets_Collect_conj)
hoelzl@43340
   198
hoelzl@47694
   199
    show "AE t in M. t \<in> {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<longrightarrow>
hoelzl@47694
   200
      D t - indicator ?D_set t \<noteq> D t * (ln b * log b (D t))"
hoelzl@43340
   201
      using D(2)
hoelzl@47694
   202
    proof (eventually_elim, safe)
hoelzl@47694
   203
      fix t assume Dt: "t \<in> space M" "D t \<noteq> 1" "D t \<noteq> 0" "0 \<le> D t"
hoelzl@47694
   204
        and eq: "D t - indicator ?D_set t = D t * (ln b * log b (D t))"
hoelzl@43340
   205
hoelzl@43340
   206
      have "D t - 1 = D t - indicator ?D_set t"
hoelzl@43340
   207
        using Dt by simp
hoelzl@43340
   208
      also note eq
hoelzl@47694
   209
      also have "D t * (ln b * log b (D t)) = - D t * ln (1 / D t)"
hoelzl@47694
   210
        using b_gt_1 `D t \<noteq> 0` `0 \<le> D t`
hoelzl@47694
   211
        by (simp add: log_def ln_div less_le)
hoelzl@43340
   212
      finally have "ln (1 / D t) = 1 / D t - 1"
hoelzl@43340
   213
        using `D t \<noteq> 0` by (auto simp: field_simps)
hoelzl@43340
   214
      from ln_eq_minus_one[OF _ this] `D t \<noteq> 0` `0 \<le> D t` `D t \<noteq> 1`
hoelzl@43340
   215
      show False by auto
hoelzl@43340
   216
    qed
hoelzl@43340
   217
hoelzl@47694
   218
    show "AE t in M. D t - indicator ?D_set t \<le> D t * (ln b * log b (D t))"
hoelzl@47694
   219
      using D(2) AE_space
hoelzl@47694
   220
    proof eventually_elim
hoelzl@47694
   221
      fix t assume "t \<in> space M" "0 \<le> D t"
hoelzl@47694
   222
      show "D t - indicator ?D_set t \<le> D t * (ln b * log b (D t))"
hoelzl@43340
   223
      proof cases
hoelzl@43340
   224
        assume asm: "D t \<noteq> 0"
hoelzl@43340
   225
        then have "0 < D t" using `0 \<le> D t` by auto
hoelzl@43340
   226
        then have "0 < 1 / D t" by auto
hoelzl@43340
   227
        have "D t - indicator ?D_set t \<le> - D t * (1 / D t - 1)"
hoelzl@43340
   228
          using asm `t \<in> space M` by (simp add: field_simps)
hoelzl@43340
   229
        also have "- D t * (1 / D t - 1) \<le> - D t * ln (1 / D t)"
hoelzl@43340
   230
          using ln_le_minus_one `0 < 1 / D t` by (intro mult_left_mono_neg) auto
hoelzl@47694
   231
        also have "\<dots> = D t * (ln b * log b (D t))"
hoelzl@47694
   232
          using `0 < D t` b_gt_1
hoelzl@47694
   233
          by (simp_all add: log_def ln_div)
hoelzl@43340
   234
        finally show ?thesis by simp
hoelzl@43340
   235
      qed simp
hoelzl@43340
   236
    qed
hoelzl@43340
   237
  qed
hoelzl@47694
   238
  also have "\<dots> = (\<integral> x. ln b * (D x * log b (D x)) \<partial>M)"
hoelzl@47694
   239
    by (simp add: ac_simps)
hoelzl@47694
   240
  also have "\<dots> = ln b * (\<integral> x. D x * log b (D x) \<partial>M)"
hoelzl@47694
   241
    using int by (rule integral_cmult)
hoelzl@47694
   242
  finally show ?thesis
hoelzl@47694
   243
    using b_gt_1 D by (subst KL_density) (auto simp: zero_less_mult_iff)
hoelzl@43340
   244
qed
hoelzl@43340
   245
hoelzl@47694
   246
lemma (in sigma_finite_measure) KL_same_eq_0: "KL_divergence b M M = 0"
hoelzl@43340
   247
proof -
hoelzl@47694
   248
  have "AE x in M. 1 = RN_deriv M M x"
hoelzl@43340
   249
  proof (rule RN_deriv_unique)
hoelzl@47694
   250
    show "(\<lambda>x. 1) \<in> borel_measurable M" "AE x in M. 0 \<le> (1 :: ereal)" by auto
hoelzl@47694
   251
    show "density M (\<lambda>x. 1) = M"
hoelzl@47694
   252
      apply (auto intro!: measure_eqI emeasure_density)
hoelzl@47694
   253
      apply (subst emeasure_density)
hoelzl@47694
   254
      apply auto
hoelzl@47694
   255
      done
hoelzl@43340
   256
  qed
hoelzl@47694
   257
  then have "AE x in M. log b (real (RN_deriv M M x)) = 0"
hoelzl@43340
   258
    by (elim AE_mp) simp
hoelzl@43340
   259
  from integral_cong_AE[OF this]
hoelzl@47694
   260
  have "integral\<^isup>L M (entropy_density b M M) = 0"
hoelzl@43340
   261
    by (simp add: entropy_density_def comp_def)
hoelzl@47694
   262
  then show "KL_divergence b M M = 0"
hoelzl@43340
   263
    unfolding KL_divergence_def
hoelzl@47694
   264
    by auto
hoelzl@43340
   265
qed
hoelzl@43340
   266
hoelzl@47694
   267
lemma (in information_space) KL_eq_0_iff_eq:
hoelzl@47694
   268
  fixes D :: "'a \<Rightarrow> real"
hoelzl@47694
   269
  assumes "prob_space (density M D)"
hoelzl@47694
   270
  assumes D: "D \<in> borel_measurable M" "AE x in M. 0 \<le> D x"
hoelzl@47694
   271
  assumes int: "integrable M (\<lambda>x. D x * log b (D x))"
hoelzl@47694
   272
  shows "KL_divergence b M (density M D) = 0 \<longleftrightarrow> density M D = M"
hoelzl@47694
   273
  using KL_same_eq_0[of b] KL_gt_0[OF assms]
hoelzl@47694
   274
  by (auto simp: less_le)
hoelzl@43340
   275
hoelzl@47694
   276
lemma (in information_space) KL_eq_0_iff_eq_ac:
hoelzl@47694
   277
  fixes D :: "'a \<Rightarrow> real"
hoelzl@47694
   278
  assumes "prob_space N"
hoelzl@47694
   279
  assumes ac: "absolutely_continuous M N" "sets N = sets M"
hoelzl@47694
   280
  assumes int: "integrable N (entropy_density b M N)"
hoelzl@47694
   281
  shows "KL_divergence b M N = 0 \<longleftrightarrow> N = M"
hoelzl@41833
   282
proof -
hoelzl@47694
   283
  interpret N: prob_space N by fact
hoelzl@47694
   284
  have "finite_measure N" by unfold_locales
hoelzl@47694
   285
  from real_RN_deriv[OF this ac] guess D . note D = this
hoelzl@47694
   286
  
hoelzl@47694
   287
  have "N = density M (RN_deriv M N)"
hoelzl@47694
   288
    using ac by (rule density_RN_deriv[symmetric])
hoelzl@47694
   289
  also have "\<dots> = density M D"
hoelzl@47694
   290
    using borel_measurable_RN_deriv[OF ac] D by (auto intro!: density_cong)
hoelzl@47694
   291
  finally have N: "N = density M D" .
hoelzl@41833
   292
hoelzl@47694
   293
  from absolutely_continuous_AE[OF ac(2,1) D(2)] D b_gt_1 ac measurable_entropy_density
hoelzl@47694
   294
  have "integrable N (\<lambda>x. log b (D x))"
hoelzl@47694
   295
    by (intro integrable_cong_AE[THEN iffD2, OF _ _ _ int])
hoelzl@47694
   296
       (auto simp: N entropy_density_def)
hoelzl@47694
   297
  with D b_gt_1 have "integrable M (\<lambda>x. D x * log b (D x))"
hoelzl@47694
   298
    by (subst integral_density(2)[symmetric]) (auto simp: N[symmetric] comp_def)
hoelzl@47694
   299
  with `prob_space N` D show ?thesis
hoelzl@47694
   300
    unfolding N
hoelzl@47694
   301
    by (intro KL_eq_0_iff_eq) auto
hoelzl@41833
   302
qed
hoelzl@41833
   303
hoelzl@47694
   304
lemma (in information_space) KL_nonneg:
hoelzl@47694
   305
  assumes "prob_space (density M D)"
hoelzl@47694
   306
  assumes D: "D \<in> borel_measurable M" "AE x in M. 0 \<le> D x"
hoelzl@47694
   307
  assumes int: "integrable M (\<lambda>x. D x * log b (D x))"
hoelzl@47694
   308
  shows "0 \<le> KL_divergence b M (density M D)"
hoelzl@47694
   309
  using KL_gt_0[OF assms] by (cases "density M D = M") (auto simp: KL_same_eq_0)
hoelzl@40859
   310
hoelzl@47694
   311
lemma (in sigma_finite_measure) KL_density_density_nonneg:
hoelzl@47694
   312
  fixes f g :: "'a \<Rightarrow> real"
hoelzl@47694
   313
  assumes "1 < b"
hoelzl@47694
   314
  assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "prob_space (density M f)"
hoelzl@47694
   315
  assumes g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x" "prob_space (density M g)"
hoelzl@47694
   316
  assumes ac: "AE x in M. f x = 0 \<longrightarrow> g x = 0"
hoelzl@47694
   317
  assumes int: "integrable M (\<lambda>x. g x * log b (g x / f x))"
hoelzl@47694
   318
  shows "0 \<le> KL_divergence b (density M f) (density M g)"
hoelzl@47694
   319
proof -
hoelzl@47694
   320
  interpret Mf: prob_space "density M f" by fact
hoelzl@47694
   321
  interpret Mf: information_space "density M f" b by default fact
hoelzl@47694
   322
  have eq: "density (density M f) (\<lambda>x. g x / f x) = density M g" (is "?DD = _")
hoelzl@47694
   323
    using f g ac by (subst density_density_divide) simp_all
hoelzl@36080
   324
hoelzl@47694
   325
  have "0 \<le> KL_divergence b (density M f) (density (density M f) (\<lambda>x. g x / f x))"
hoelzl@47694
   326
  proof (rule Mf.KL_nonneg)
hoelzl@47694
   327
    show "prob_space ?DD" unfolding eq by fact
hoelzl@47694
   328
    from f g show "(\<lambda>x. g x / f x) \<in> borel_measurable (density M f)"
hoelzl@47694
   329
      by auto
hoelzl@47694
   330
    show "AE x in density M f. 0 \<le> g x / f x"
hoelzl@47694
   331
      using f g by (auto simp: AE_density divide_nonneg_nonneg)
hoelzl@47694
   332
    show "integrable (density M f) (\<lambda>x. g x / f x * log b (g x / f x))"
hoelzl@47694
   333
      using `1 < b` f g ac
hoelzl@47694
   334
      by (subst integral_density)
hoelzl@47694
   335
         (auto intro!: integrable_cong_AE[THEN iffD2, OF _ _ _ int] measurable_If)
hoelzl@47694
   336
  qed
hoelzl@47694
   337
  also have "\<dots> = KL_divergence b (density M f) (density M g)"
hoelzl@47694
   338
    using f g ac by (subst density_density_divide) simp_all
hoelzl@47694
   339
  finally show ?thesis .
hoelzl@36080
   340
qed
hoelzl@36080
   341
hoelzl@39097
   342
subsection {* Mutual Information *}
hoelzl@39097
   343
hoelzl@36080
   344
definition (in prob_space)
hoelzl@38656
   345
  "mutual_information b S T X Y =
hoelzl@47694
   346
    KL_divergence b (distr M S X \<Otimes>\<^isub>M distr M T Y) (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)))"
hoelzl@36080
   347
hoelzl@47694
   348
lemma (in information_space) mutual_information_indep_vars:
hoelzl@43340
   349
  fixes S T X Y
hoelzl@47694
   350
  defines "P \<equiv> distr M S X \<Otimes>\<^isub>M distr M T Y"
hoelzl@47694
   351
  defines "Q \<equiv> distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
hoelzl@43340
   352
  shows "indep_var S X T Y \<longleftrightarrow>
hoelzl@43340
   353
    (random_variable S X \<and> random_variable T Y \<and>
hoelzl@47694
   354
      absolutely_continuous P Q \<and> integrable Q (entropy_density b P Q) \<and>
hoelzl@47694
   355
      mutual_information b S T X Y = 0)"
hoelzl@47694
   356
  unfolding indep_var_distribution_eq
hoelzl@43340
   357
proof safe
hoelzl@47694
   358
  assume rv: "random_variable S X" "random_variable T Y"
hoelzl@43340
   359
hoelzl@47694
   360
  interpret X: prob_space "distr M S X"
hoelzl@47694
   361
    by (rule prob_space_distr) fact
hoelzl@47694
   362
  interpret Y: prob_space "distr M T Y"
hoelzl@47694
   363
    by (rule prob_space_distr) fact
hoelzl@47694
   364
  interpret XY: pair_prob_space "distr M S X" "distr M T Y" by default
hoelzl@47694
   365
  interpret P: information_space P b unfolding P_def by default (rule b_gt_1)
hoelzl@43340
   366
hoelzl@47694
   367
  interpret Q: prob_space Q unfolding Q_def
hoelzl@47694
   368
    by (rule prob_space_distr) (simp add: comp_def measurable_pair_iff rv)
hoelzl@43340
   369
hoelzl@47694
   370
  { assume "distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
hoelzl@47694
   371
    then have [simp]: "Q = P"  unfolding Q_def P_def by simp
hoelzl@43340
   372
hoelzl@47694
   373
    show ac: "absolutely_continuous P Q" by (simp add: absolutely_continuous_def)
hoelzl@47694
   374
    then have ed: "entropy_density b P Q \<in> borel_measurable P"
hoelzl@47694
   375
      by (rule P.measurable_entropy_density) simp
hoelzl@43340
   376
hoelzl@47694
   377
    have "AE x in P. 1 = RN_deriv P Q x"
hoelzl@47694
   378
    proof (rule P.RN_deriv_unique)
hoelzl@47694
   379
      show "density P (\<lambda>x. 1) = Q"
hoelzl@47694
   380
        unfolding `Q = P` by (intro measure_eqI) (auto simp: emeasure_density)
hoelzl@47694
   381
    qed auto
hoelzl@47694
   382
    then have ae_0: "AE x in P. entropy_density b P Q x = 0"
hoelzl@47694
   383
      by eventually_elim (auto simp: entropy_density_def)
hoelzl@47694
   384
    then have "integrable P (entropy_density b P Q) \<longleftrightarrow> integrable Q (\<lambda>x. 0)"
hoelzl@47694
   385
      using ed unfolding `Q = P` by (intro integrable_cong_AE) auto
hoelzl@47694
   386
    then show "integrable Q (entropy_density b P Q)" by simp
hoelzl@43340
   387
hoelzl@47694
   388
    show "mutual_information b S T X Y = 0"
hoelzl@47694
   389
      unfolding mutual_information_def KL_divergence_def P_def[symmetric] Q_def[symmetric] `Q = P`
hoelzl@47694
   390
      using ae_0 by (simp cong: integral_cong_AE) }
hoelzl@43340
   391
hoelzl@47694
   392
  { assume ac: "absolutely_continuous P Q"
hoelzl@47694
   393
    assume int: "integrable Q (entropy_density b P Q)"
hoelzl@47694
   394
    assume I_eq_0: "mutual_information b S T X Y = 0"
hoelzl@43340
   395
hoelzl@47694
   396
    have eq: "Q = P"
hoelzl@47694
   397
    proof (rule P.KL_eq_0_iff_eq_ac[THEN iffD1])
hoelzl@47694
   398
      show "prob_space Q" by unfold_locales
hoelzl@47694
   399
      show "absolutely_continuous P Q" by fact
hoelzl@47694
   400
      show "integrable Q (entropy_density b P Q)" by fact
hoelzl@47694
   401
      show "sets Q = sets P" by (simp add: P_def Q_def sets_pair_measure)
hoelzl@47694
   402
      show "KL_divergence b P Q = 0"
hoelzl@47694
   403
        using I_eq_0 unfolding mutual_information_def by (simp add: P_def Q_def)
hoelzl@47694
   404
    qed
hoelzl@47694
   405
    then show "distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
hoelzl@47694
   406
      unfolding P_def Q_def .. }
hoelzl@43340
   407
qed
hoelzl@43340
   408
hoelzl@40859
   409
abbreviation (in information_space)
hoelzl@40859
   410
  mutual_information_Pow ("\<I>'(_ ; _')") where
hoelzl@47694
   411
  "\<I>(X ; Y) \<equiv> mutual_information b (count_space (X`space M)) (count_space (Y`space M)) X Y"
hoelzl@41689
   412
hoelzl@47694
   413
lemma (in information_space)
hoelzl@47694
   414
  fixes Pxy :: "'b \<times> 'c \<Rightarrow> real" and Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
hoelzl@47694
   415
  assumes "sigma_finite_measure S" "sigma_finite_measure T"
hoelzl@47694
   416
  assumes Px: "distributed M S X Px" and Py: "distributed M T Y Py"
hoelzl@47694
   417
  assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
hoelzl@47694
   418
  defines "f \<equiv> \<lambda>x. Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x)))"
hoelzl@47694
   419
  shows mutual_information_distr: "mutual_information b S T X Y = integral\<^isup>L (S \<Otimes>\<^isub>M T) f" (is "?M = ?R")
hoelzl@47694
   420
    and mutual_information_nonneg: "integrable (S \<Otimes>\<^isub>M T) f \<Longrightarrow> 0 \<le> mutual_information b S T X Y"
hoelzl@40859
   421
proof -
hoelzl@47694
   422
  have X: "random_variable S X"
hoelzl@47694
   423
    using Px by (auto simp: distributed_def)
hoelzl@47694
   424
  have Y: "random_variable T Y"
hoelzl@47694
   425
    using Py by (auto simp: distributed_def)
hoelzl@47694
   426
  interpret S: sigma_finite_measure S by fact
hoelzl@47694
   427
  interpret T: sigma_finite_measure T by fact
hoelzl@47694
   428
  interpret ST: pair_sigma_finite S T ..
hoelzl@47694
   429
  interpret X: prob_space "distr M S X" using X by (rule prob_space_distr)
hoelzl@47694
   430
  interpret Y: prob_space "distr M T Y" using Y by (rule prob_space_distr)
hoelzl@47694
   431
  interpret XY: pair_prob_space "distr M S X" "distr M T Y" ..
hoelzl@47694
   432
  let ?P = "S \<Otimes>\<^isub>M T"
hoelzl@47694
   433
  let ?D = "distr M ?P (\<lambda>x. (X x, Y x))"
hoelzl@47694
   434
hoelzl@47694
   435
  { fix A assume "A \<in> sets S"
hoelzl@47694
   436
    with X Y have "emeasure (distr M S X) A = emeasure ?D (A \<times> space T)"
hoelzl@47694
   437
      by (auto simp: emeasure_distr measurable_Pair measurable_space
hoelzl@47694
   438
               intro!: arg_cong[where f="emeasure M"]) }
hoelzl@47694
   439
  note marginal_eq1 = this
hoelzl@47694
   440
  { fix A assume "A \<in> sets T"
hoelzl@47694
   441
    with X Y have "emeasure (distr M T Y) A = emeasure ?D (space S \<times> A)"
hoelzl@47694
   442
      by (auto simp: emeasure_distr measurable_Pair measurable_space
hoelzl@47694
   443
               intro!: arg_cong[where f="emeasure M"]) }
hoelzl@47694
   444
  note marginal_eq2 = this
hoelzl@47694
   445
hoelzl@47694
   446
  have eq: "(\<lambda>x. ereal (Px (fst x) * Py (snd x))) = (\<lambda>(x, y). ereal (Px x) * ereal (Py y))"
hoelzl@47694
   447
    by auto
hoelzl@47694
   448
hoelzl@47694
   449
  have distr_eq: "distr M S X \<Otimes>\<^isub>M distr M T Y = density ?P (\<lambda>x. ereal (Px (fst x) * Py (snd x)))"
hoelzl@47694
   450
    unfolding Px(1)[THEN distributed_distr_eq_density] Py(1)[THEN distributed_distr_eq_density] eq
hoelzl@47694
   451
  proof (subst pair_measure_density)
hoelzl@47694
   452
    show "(\<lambda>x. ereal (Px x)) \<in> borel_measurable S" "(\<lambda>y. ereal (Py y)) \<in> borel_measurable T"
hoelzl@47694
   453
      "AE x in S. 0 \<le> ereal (Px x)" "AE y in T. 0 \<le> ereal (Py y)"
hoelzl@47694
   454
      using Px Py by (auto simp: distributed_def)
hoelzl@47694
   455
    show "sigma_finite_measure (density S Px)" unfolding Px(1)[THEN distributed_distr_eq_density, symmetric] ..
hoelzl@47694
   456
    show "sigma_finite_measure (density T Py)" unfolding Py(1)[THEN distributed_distr_eq_density, symmetric] ..
hoelzl@47694
   457
  qed (fact | simp)+
hoelzl@47694
   458
  
hoelzl@47694
   459
  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
   460
    unfolding mutual_information_def distr_eq Pxy(1)[THEN distributed_distr_eq_density] ..
hoelzl@47694
   461
hoelzl@47694
   462
  from Px Py have f: "(\<lambda>x. Px (fst x) * Py (snd x)) \<in> borel_measurable ?P"
hoelzl@47694
   463
    by (intro borel_measurable_times) (auto intro: distributed_real_measurable measurable_fst'' measurable_snd'')
hoelzl@47694
   464
  have PxPy_nonneg: "AE x in ?P. 0 \<le> Px (fst x) * Py (snd x)"
hoelzl@47694
   465
  proof (rule ST.AE_pair_measure)
hoelzl@47694
   466
    show "{x \<in> space ?P. 0 \<le> Px (fst x) * Py (snd x)} \<in> sets ?P"
hoelzl@47694
   467
      using f by auto
hoelzl@47694
   468
    show "AE x in S. AE y in T. 0 \<le> Px (fst (x, y)) * Py (snd (x, y))"
hoelzl@47694
   469
      using Px Py by (auto simp: zero_le_mult_iff dest!: distributed_real_AE)
hoelzl@47694
   470
  qed
hoelzl@47694
   471
hoelzl@47694
   472
  have "(AE x in ?P. Px (fst x) = 0 \<longrightarrow> Pxy x = 0)"
hoelzl@47694
   473
    by (rule subdensity_real[OF measurable_fst Pxy Px]) auto
hoelzl@47694
   474
  moreover
hoelzl@47694
   475
  have "(AE x in ?P. Py (snd x) = 0 \<longrightarrow> Pxy x = 0)"
hoelzl@47694
   476
    by (rule subdensity_real[OF measurable_snd Pxy Py]) auto
hoelzl@47694
   477
  ultimately have ac: "AE x in ?P. Px (fst x) * Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
hoelzl@47694
   478
    by eventually_elim auto
hoelzl@47694
   479
hoelzl@47694
   480
  show "?M = ?R"
hoelzl@47694
   481
    unfolding M f_def
hoelzl@47694
   482
    using b_gt_1 f PxPy_nonneg Pxy[THEN distributed_real_measurable] Pxy[THEN distributed_real_AE] ac
hoelzl@47694
   483
    by (rule ST.KL_density_density)
hoelzl@47694
   484
hoelzl@47694
   485
  assume int: "integrable (S \<Otimes>\<^isub>M T) f"
hoelzl@47694
   486
  show "0 \<le> ?M" unfolding M
hoelzl@47694
   487
  proof (rule ST.KL_density_density_nonneg
hoelzl@47694
   488
    [OF b_gt_1 f PxPy_nonneg _ Pxy[THEN distributed_real_measurable] Pxy[THEN distributed_real_AE] _ ac int[unfolded f_def]])
hoelzl@47694
   489
    show "prob_space (density (S \<Otimes>\<^isub>M T) (\<lambda>x. ereal (Pxy x))) "
hoelzl@47694
   490
      unfolding distributed_distr_eq_density[OF Pxy, symmetric]
hoelzl@47694
   491
      using distributed_measurable[OF Pxy] by (rule prob_space_distr)
hoelzl@47694
   492
    show "prob_space (density (S \<Otimes>\<^isub>M T) (\<lambda>x. ereal (Px (fst x) * Py (snd x))))"
hoelzl@47694
   493
      unfolding distr_eq[symmetric] by unfold_locales
hoelzl@40859
   494
  qed
hoelzl@40859
   495
qed
hoelzl@40859
   496
hoelzl@40859
   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@47694
   499
  assumes "sigma_finite_measure S" "sigma_finite_measure T"
hoelzl@47694
   500
  assumes Px: "distributed M S X Px" and Py: "distributed M T Y Py"
hoelzl@47694
   501
  assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
hoelzl@47694
   502
  assumes ae: "AE x in S. AE y in T. Pxy (x, y) = Px x * Py y"
hoelzl@47694
   503
  shows mutual_information_eq_0: "mutual_information b S T X Y = 0"
hoelzl@36624
   504
proof -
hoelzl@47694
   505
  interpret S: sigma_finite_measure S by fact
hoelzl@47694
   506
  interpret T: sigma_finite_measure T by fact
hoelzl@47694
   507
  interpret ST: pair_sigma_finite S T ..
hoelzl@36080
   508
hoelzl@47694
   509
  have "AE x in S \<Otimes>\<^isub>M T. Px (fst x) = 0 \<longrightarrow> Pxy x = 0"
hoelzl@47694
   510
    by (rule subdensity_real[OF measurable_fst Pxy Px]) auto
hoelzl@47694
   511
  moreover
hoelzl@47694
   512
  have "AE x in S \<Otimes>\<^isub>M T. Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
hoelzl@47694
   513
    by (rule subdensity_real[OF measurable_snd Pxy Py]) auto
hoelzl@47694
   514
  moreover 
hoelzl@47694
   515
  have "AE x in S \<Otimes>\<^isub>M T. Pxy x = Px (fst x) * Py (snd x)"
hoelzl@47694
   516
    using distributed_real_measurable[OF Px] distributed_real_measurable[OF Py] distributed_real_measurable[OF Pxy]
hoelzl@47694
   517
    by (intro ST.AE_pair_measure) (auto simp: ae intro!: measurable_snd'' measurable_fst'')
hoelzl@47694
   518
  ultimately have "AE x in S \<Otimes>\<^isub>M T. Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x))) = 0"
hoelzl@47694
   519
    by eventually_elim simp
hoelzl@47694
   520
  then have "(\<integral>x. Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x))) \<partial>(S \<Otimes>\<^isub>M T)) = (\<integral>x. 0 \<partial>(S \<Otimes>\<^isub>M T))"
hoelzl@47694
   521
    by (rule integral_cong_AE)
hoelzl@47694
   522
  then show ?thesis
hoelzl@47694
   523
    by (subst mutual_information_distr[OF assms(1-5)]) simp
hoelzl@36080
   524
qed
hoelzl@36080
   525
hoelzl@47694
   526
lemma (in information_space) mutual_information_simple_distributed:
hoelzl@47694
   527
  assumes X: "simple_distributed M X Px" and Y: "simple_distributed M Y Py"
hoelzl@47694
   528
  assumes XY: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"
hoelzl@47694
   529
  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
   530
proof (subst mutual_information_distr[OF _ _ simple_distributed[OF X] simple_distributed[OF Y] simple_distributed_joint[OF XY]])
hoelzl@47694
   531
  note fin = simple_distributed_joint_finite[OF XY, simp]
hoelzl@47694
   532
  show "sigma_finite_measure (count_space (X ` space M))"
hoelzl@47694
   533
    by (simp add: sigma_finite_measure_count_space_finite)
hoelzl@47694
   534
  show "sigma_finite_measure (count_space (Y ` space M))"
hoelzl@47694
   535
    by (simp add: sigma_finite_measure_count_space_finite)
hoelzl@47694
   536
  let ?Pxy = "\<lambda>x. (if x \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy x else 0)"
hoelzl@47694
   537
  let ?f = "\<lambda>x. ?Pxy x * log b (?Pxy x / (Px (fst x) * Py (snd x)))"
hoelzl@47694
   538
  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
   539
    by auto
hoelzl@47694
   540
  with fin show "(\<integral> x. ?f x \<partial>(count_space (X ` space M) \<Otimes>\<^isub>M count_space (Y ` space M))) =
hoelzl@47694
   541
    (\<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
   542
    by (auto simp add: pair_measure_count_space lebesgue_integral_count_space_finite setsum_cases split_beta'
hoelzl@47694
   543
             intro!: setsum_cong)
hoelzl@47694
   544
qed
hoelzl@36080
   545
hoelzl@47694
   546
lemma (in information_space)
hoelzl@47694
   547
  fixes Pxy :: "'b \<times> 'c \<Rightarrow> real" and Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
hoelzl@47694
   548
  assumes Px: "simple_distributed M X Px" and Py: "simple_distributed M Y Py"
hoelzl@47694
   549
  assumes Pxy: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"
hoelzl@47694
   550
  assumes ae: "\<forall>x\<in>space M. Pxy (X x, Y x) = Px (X x) * Py (Y x)"
hoelzl@47694
   551
  shows mutual_information_eq_0_simple: "\<I>(X ; Y) = 0"
hoelzl@47694
   552
proof (subst mutual_information_simple_distributed[OF Px Py Pxy])
hoelzl@47694
   553
  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
   554
    (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. 0)"
hoelzl@47694
   555
    by (intro setsum_cong) (auto simp: ae)
hoelzl@47694
   556
  then show "(\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M.
hoelzl@47694
   557
    Pxy (x, y) * log b (Pxy (x, y) / (Px x * Py y))) = 0" by simp
hoelzl@47694
   558
qed
hoelzl@36080
   559
hoelzl@39097
   560
subsection {* Entropy *}
hoelzl@39097
   561
hoelzl@47694
   562
definition (in prob_space) entropy :: "real \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> real" where
hoelzl@47694
   563
  "entropy b S X = - KL_divergence b S (distr M S X)"
hoelzl@47694
   564
hoelzl@40859
   565
abbreviation (in information_space)
hoelzl@40859
   566
  entropy_Pow ("\<H>'(_')") where
hoelzl@47694
   567
  "\<H>(X) \<equiv> entropy b (count_space (X`space M)) X"
hoelzl@41981
   568
hoelzl@49791
   569
lemma (in prob_space) distributed_RN_deriv:
hoelzl@49791
   570
  assumes X: "distributed M S X Px"
hoelzl@49791
   571
  shows "AE x in S. RN_deriv S (density S Px) x = Px x"
hoelzl@49791
   572
proof -
hoelzl@49791
   573
  note D = distributed_measurable[OF X] distributed_borel_measurable[OF X] distributed_AE[OF X]
hoelzl@49791
   574
  interpret X: prob_space "distr M S X"
hoelzl@49791
   575
    using D(1) by (rule prob_space_distr)
hoelzl@49791
   576
hoelzl@49791
   577
  have sf: "sigma_finite_measure (distr M S X)" by default
hoelzl@49791
   578
  show ?thesis
hoelzl@49791
   579
    using D
hoelzl@49791
   580
    apply (subst eq_commute)
hoelzl@49791
   581
    apply (intro RN_deriv_unique_sigma_finite)
hoelzl@49791
   582
    apply (auto intro: divide_nonneg_nonneg measure_nonneg
hoelzl@49791
   583
             simp: distributed_distr_eq_density[symmetric, OF X] sf)
hoelzl@49791
   584
    done
hoelzl@49791
   585
qed
hoelzl@49791
   586
hoelzl@49788
   587
lemma (in information_space)
hoelzl@47694
   588
  fixes X :: "'a \<Rightarrow> 'b"
hoelzl@49785
   589
  assumes X: "distributed M MX X f"
hoelzl@49788
   590
  shows entropy_distr: "entropy b MX X = - (\<integral>x. f x * log b (f x) \<partial>MX)" (is ?eq)
hoelzl@49788
   591
proof -
hoelzl@49785
   592
  note D = distributed_measurable[OF X] distributed_borel_measurable[OF X] distributed_AE[OF X]
hoelzl@49791
   593
  note ae = distributed_RN_deriv[OF X]
hoelzl@49788
   594
hoelzl@49788
   595
  have ae_eq: "AE x in distr M MX X. log b (real (RN_deriv MX (distr M MX X) x)) =
hoelzl@49785
   596
    log b (f x)"
hoelzl@49785
   597
    unfolding distributed_distr_eq_density[OF X]
hoelzl@49785
   598
    apply (subst AE_density)
hoelzl@49785
   599
    using D apply simp
hoelzl@49785
   600
    using ae apply eventually_elim
hoelzl@49785
   601
    apply auto
hoelzl@49785
   602
    done
hoelzl@49788
   603
hoelzl@49788
   604
  have int_eq: "- (\<integral> x. log b (f x) \<partial>distr M MX X) = - (\<integral> x. f x * log b (f x) \<partial>MX)"
hoelzl@49785
   605
    unfolding distributed_distr_eq_density[OF X]
hoelzl@49785
   606
    using D
hoelzl@49785
   607
    by (subst integral_density)
hoelzl@49785
   608
       (auto simp: borel_measurable_ereal_iff)
hoelzl@49788
   609
hoelzl@49788
   610
  show ?eq
hoelzl@49788
   611
    unfolding entropy_def KL_divergence_def entropy_density_def comp_def
hoelzl@49788
   612
    apply (subst integral_cong_AE)
hoelzl@49788
   613
    apply (rule ae_eq)
hoelzl@49788
   614
    apply (rule int_eq)
hoelzl@49788
   615
    done
hoelzl@49788
   616
qed
hoelzl@49785
   617
hoelzl@49786
   618
lemma (in prob_space) distributed_imp_emeasure_nonzero:
hoelzl@49786
   619
  assumes X: "distributed M MX X Px"
hoelzl@49786
   620
  shows "emeasure MX {x \<in> space MX. Px x \<noteq> 0} \<noteq> 0"
hoelzl@49786
   621
proof
hoelzl@49786
   622
  note Px = distributed_borel_measurable[OF X] distributed_AE[OF X]
hoelzl@49786
   623
  interpret X: prob_space "distr M MX X"
hoelzl@49786
   624
    using distributed_measurable[OF X] by (rule prob_space_distr)
hoelzl@49786
   625
hoelzl@49786
   626
  assume "emeasure MX {x \<in> space MX. Px x \<noteq> 0} = 0"
hoelzl@49786
   627
  with Px have "AE x in MX. Px x = 0"
hoelzl@49786
   628
    by (intro AE_I[OF subset_refl]) (auto simp: borel_measurable_ereal_iff)
hoelzl@49786
   629
  moreover
hoelzl@49786
   630
  from X.emeasure_space_1 have "(\<integral>\<^isup>+x. Px x \<partial>MX) = 1"
hoelzl@49786
   631
    unfolding distributed_distr_eq_density[OF X] using Px
hoelzl@49786
   632
    by (subst (asm) emeasure_density)
hoelzl@49786
   633
       (auto simp: borel_measurable_ereal_iff intro!: integral_cong cong: positive_integral_cong)
hoelzl@49786
   634
  ultimately show False
hoelzl@49786
   635
    by (simp add: positive_integral_cong_AE)
hoelzl@49786
   636
qed
hoelzl@49786
   637
hoelzl@49786
   638
lemma (in information_space) entropy_le:
hoelzl@49786
   639
  fixes Px :: "'b \<Rightarrow> real" and MX :: "'b measure"
hoelzl@49786
   640
  assumes X: "distributed M MX X Px"
hoelzl@49786
   641
  and fin: "emeasure MX {x \<in> space MX. Px x \<noteq> 0} \<noteq> \<infinity>"
hoelzl@49786
   642
  and int: "integrable MX (\<lambda>x. - Px x * log b (Px x))"
hoelzl@49786
   643
  shows "entropy b MX X \<le> log b (measure MX {x \<in> space MX. Px x \<noteq> 0})"
hoelzl@49786
   644
proof -
hoelzl@49786
   645
  note Px = distributed_borel_measurable[OF X] distributed_AE[OF X]
hoelzl@49786
   646
  interpret X: prob_space "distr M MX X"
hoelzl@49786
   647
    using distributed_measurable[OF X] by (rule prob_space_distr)
hoelzl@49786
   648
hoelzl@49786
   649
  have " - log b (measure MX {x \<in> space MX. Px x \<noteq> 0}) = 
hoelzl@49786
   650
    - log b (\<integral> x. indicator {x \<in> space MX. Px x \<noteq> 0} x \<partial>MX)"
hoelzl@49786
   651
    using Px fin
hoelzl@49786
   652
    by (subst integral_indicator) (auto simp: measure_def borel_measurable_ereal_iff)
hoelzl@49786
   653
  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
   654
    unfolding distributed_distr_eq_density[OF X] using Px
hoelzl@49786
   655
    apply (intro arg_cong[where f="log b"] arg_cong[where f=uminus])
hoelzl@49786
   656
    by (subst integral_density) (auto simp: borel_measurable_ereal_iff intro!: integral_cong)
hoelzl@49786
   657
  also have "\<dots> \<le> (\<integral> x. - log b (1 / Px x) \<partial>distr M MX X)"
hoelzl@49786
   658
  proof (rule X.jensens_inequality[of "\<lambda>x. 1 / Px x" "{0<..}" 0 1 "\<lambda>x. - log b x"])
hoelzl@49786
   659
    show "AE x in distr M MX X. 1 / Px x \<in> {0<..}"
hoelzl@49786
   660
      unfolding distributed_distr_eq_density[OF X]
hoelzl@49786
   661
      using Px by (auto simp: AE_density)
hoelzl@49786
   662
    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
   663
      by (auto simp: one_ereal_def)
hoelzl@49786
   664
    have "(\<integral>\<^isup>+ x. max 0 (ereal (- (if Px x = 0 then 0 else 1))) \<partial>MX) = (\<integral>\<^isup>+ x. 0 \<partial>MX)"
hoelzl@49786
   665
      by (intro positive_integral_cong) (auto split: split_max)
hoelzl@49786
   666
    then show "integrable (distr M MX X) (\<lambda>x. 1 / Px x)"
hoelzl@49786
   667
      unfolding distributed_distr_eq_density[OF X] using Px
hoelzl@49786
   668
      by (auto simp: positive_integral_density integrable_def borel_measurable_ereal_iff fin positive_integral_max_0
hoelzl@49786
   669
              cong: positive_integral_cong)
hoelzl@49786
   670
    have "integrable MX (\<lambda>x. Px x * log b (1 / Px x)) =
hoelzl@49786
   671
      integrable MX (\<lambda>x. - Px x * log b (Px x))"
hoelzl@49786
   672
      using Px
hoelzl@49786
   673
      by (intro integrable_cong_AE)
hoelzl@49786
   674
         (auto simp: borel_measurable_ereal_iff log_divide_eq
hoelzl@49786
   675
                  intro!: measurable_If)
hoelzl@49786
   676
    then show "integrable (distr M MX X) (\<lambda>x. - log b (1 / Px x))"
hoelzl@49786
   677
      unfolding distributed_distr_eq_density[OF X]
hoelzl@49786
   678
      using Px int
hoelzl@49786
   679
      by (subst integral_density) (auto simp: borel_measurable_ereal_iff)
hoelzl@49786
   680
  qed (auto simp: minus_log_convex[OF b_gt_1])
hoelzl@49786
   681
  also have "\<dots> = (\<integral> x. log b (Px x) \<partial>distr M MX X)"
hoelzl@49786
   682
    unfolding distributed_distr_eq_density[OF X] using Px
hoelzl@49786
   683
    by (intro integral_cong_AE) (auto simp: AE_density log_divide_eq)
hoelzl@49786
   684
  also have "\<dots> = - entropy b MX X"
hoelzl@49786
   685
    unfolding distributed_distr_eq_density[OF X] using Px
hoelzl@49786
   686
    by (subst entropy_distr[OF X]) (auto simp: borel_measurable_ereal_iff integral_density)
hoelzl@49786
   687
  finally show ?thesis
hoelzl@49786
   688
    by simp
hoelzl@49786
   689
qed
hoelzl@49786
   690
hoelzl@49786
   691
lemma (in information_space) entropy_le_space:
hoelzl@49786
   692
  fixes Px :: "'b \<Rightarrow> real" and MX :: "'b measure"
hoelzl@49786
   693
  assumes X: "distributed M MX X Px"
hoelzl@49786
   694
  and fin: "finite_measure MX"
hoelzl@49786
   695
  and int: "integrable MX (\<lambda>x. - Px x * log b (Px x))"
hoelzl@49786
   696
  shows "entropy b MX X \<le> log b (measure MX (space MX))"
hoelzl@49786
   697
proof -
hoelzl@49786
   698
  note Px = distributed_borel_measurable[OF X] distributed_AE[OF X]
hoelzl@49786
   699
  interpret finite_measure MX by fact
hoelzl@49786
   700
  have "entropy b MX X \<le> log b (measure MX {x \<in> space MX. Px x \<noteq> 0})"
hoelzl@49786
   701
    using int X by (intro entropy_le) auto
hoelzl@49786
   702
  also have "\<dots> \<le> log b (measure MX (space MX))"
hoelzl@49786
   703
    using Px distributed_imp_emeasure_nonzero[OF X]
hoelzl@49786
   704
    by (intro log_le)
hoelzl@49786
   705
       (auto intro!: borel_measurable_ereal_iff finite_measure_mono b_gt_1
hoelzl@49786
   706
                     less_le[THEN iffD2] measure_nonneg simp: emeasure_eq_measure)
hoelzl@49786
   707
  finally show ?thesis .
hoelzl@49786
   708
qed
hoelzl@49786
   709
hoelzl@49785
   710
lemma (in prob_space) uniform_distributed_params:
hoelzl@49785
   711
  assumes X: "distributed M MX X (\<lambda>x. indicator A x / measure MX A)"
hoelzl@49785
   712
  shows "A \<in> sets MX" "measure MX A \<noteq> 0"
hoelzl@47694
   713
proof -
hoelzl@49785
   714
  interpret X: prob_space "distr M MX X"
hoelzl@49785
   715
    using distributed_measurable[OF X] by (rule prob_space_distr)
hoelzl@49785
   716
hoelzl@49785
   717
  show "measure MX A \<noteq> 0"
hoelzl@49785
   718
  proof
hoelzl@49785
   719
    assume "measure MX A = 0"
hoelzl@49785
   720
    with X.emeasure_space_1 X.prob_space distributed_distr_eq_density[OF X]
hoelzl@49785
   721
    show False
hoelzl@49785
   722
      by (simp add: emeasure_density zero_ereal_def[symmetric])
hoelzl@49785
   723
  qed
hoelzl@49785
   724
  with measure_notin_sets[of A MX] show "A \<in> sets MX"
hoelzl@49785
   725
    by blast
hoelzl@39097
   726
qed
hoelzl@36624
   727
hoelzl@47694
   728
lemma (in information_space) entropy_uniform:
hoelzl@49785
   729
  assumes X: "distributed M MX X (\<lambda>x. indicator A x / measure MX A)" (is "distributed _ _ _ ?f")
hoelzl@47694
   730
  shows "entropy b MX X = log b (measure MX A)"
hoelzl@49785
   731
proof (subst entropy_distr[OF X])
hoelzl@49785
   732
  have [simp]: "emeasure MX A \<noteq> \<infinity>"
hoelzl@49785
   733
    using uniform_distributed_params[OF X] by (auto simp add: measure_def)
hoelzl@49785
   734
  have eq: "(\<integral> x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \<partial>MX) =
hoelzl@49785
   735
    (\<integral> x. (- log b (measure MX A) / measure MX A) * indicator A x \<partial>MX)"
hoelzl@49785
   736
    using measure_nonneg[of MX A] uniform_distributed_params[OF X]
hoelzl@49785
   737
    by (auto intro!: integral_cong split: split_indicator simp: log_divide_eq)
hoelzl@49785
   738
  show "- (\<integral> x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \<partial>MX) =
hoelzl@49785
   739
    log b (measure MX A)"
hoelzl@49785
   740
    unfolding eq using uniform_distributed_params[OF X]
hoelzl@49785
   741
    by (subst lebesgue_integral_cmult) (auto simp: measure_def)
hoelzl@49785
   742
qed
hoelzl@36080
   743
hoelzl@47694
   744
lemma (in information_space) entropy_simple_distributed:
hoelzl@49786
   745
  "simple_distributed M X f \<Longrightarrow> \<H>(X) = - (\<Sum>x\<in>X`space M. f x * log b (f x))"
hoelzl@49786
   746
  by (subst entropy_distr[OF simple_distributed])
hoelzl@49786
   747
     (auto simp add: lebesgue_integral_count_space_finite)
hoelzl@39097
   748
hoelzl@40859
   749
lemma (in information_space) entropy_le_card_not_0:
hoelzl@47694
   750
  assumes X: "simple_distributed M X f"
hoelzl@47694
   751
  shows "\<H>(X) \<le> log b (card (X ` space M \<inter> {x. f x \<noteq> 0}))"
hoelzl@39097
   752
proof -
hoelzl@49787
   753
  let ?X = "count_space (X`space M)"
hoelzl@49787
   754
  have "\<H>(X) \<le> log b (measure ?X {x \<in> space ?X. f x \<noteq> 0})"
hoelzl@49787
   755
    by (rule entropy_le[OF simple_distributed[OF X]])
hoelzl@49787
   756
       (simp_all add: simple_distributed_finite[OF X] subset_eq integrable_count_space emeasure_count_space)
hoelzl@49787
   757
  also have "measure ?X {x \<in> space ?X. f x \<noteq> 0} = card (X ` space M \<inter> {x. f x \<noteq> 0})"
hoelzl@49787
   758
    by (simp_all add: simple_distributed_finite[OF X] subset_eq emeasure_count_space measure_def Int_def)
hoelzl@49787
   759
  finally show ?thesis .
hoelzl@39097
   760
qed
hoelzl@39097
   761
hoelzl@40859
   762
lemma (in information_space) entropy_le_card:
hoelzl@49787
   763
  assumes X: "simple_distributed M X f"
hoelzl@40859
   764
  shows "\<H>(X) \<le> log b (real (card (X ` space M)))"
hoelzl@49787
   765
proof -
hoelzl@49787
   766
  let ?X = "count_space (X`space M)"
hoelzl@49787
   767
  have "\<H>(X) \<le> log b (measure ?X (space ?X))"
hoelzl@49787
   768
    by (rule entropy_le_space[OF simple_distributed[OF X]])
hoelzl@49787
   769
       (simp_all add: simple_distributed_finite[OF X] subset_eq integrable_count_space emeasure_count_space finite_measure_count_space)
hoelzl@49787
   770
  also have "measure ?X (space ?X) = card (X ` space M)"
hoelzl@49787
   771
    by (simp_all add: simple_distributed_finite[OF X] subset_eq emeasure_count_space measure_def)
hoelzl@39097
   772
  finally show ?thesis .
hoelzl@39097
   773
qed
hoelzl@39097
   774
hoelzl@39097
   775
subsection {* Conditional Mutual Information *}
hoelzl@39097
   776
hoelzl@36080
   777
definition (in prob_space)
hoelzl@41689
   778
  "conditional_mutual_information b MX MY MZ X Y Z \<equiv>
hoelzl@41689
   779
    mutual_information b MX (MY \<Otimes>\<^isub>M MZ) X (\<lambda>x. (Y x, Z x)) -
hoelzl@41689
   780
    mutual_information b MX MZ X Z"
hoelzl@36080
   781
hoelzl@40859
   782
abbreviation (in information_space)
hoelzl@40859
   783
  conditional_mutual_information_Pow ("\<I>'( _ ; _ | _ ')") where
hoelzl@36624
   784
  "\<I>(X ; Y | Z) \<equiv> conditional_mutual_information b
hoelzl@47694
   785
    (count_space (X ` space M)) (count_space (Y ` space M)) (count_space (Z ` space M)) X Y Z"
hoelzl@36080
   786
hoelzl@49787
   787
lemma (in pair_sigma_finite) borel_measurable_positive_integral_fst:
hoelzl@49787
   788
  "(\<lambda>(x, y). f x y) \<in> borel_measurable (M1 \<Otimes>\<^isub>M M2) \<Longrightarrow> (\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M2) \<in> borel_measurable M1"
hoelzl@49787
   789
  using positive_integral_fst_measurable(1)[of "\<lambda>(x, y). f x y"] by simp
hoelzl@49787
   790
hoelzl@49787
   791
lemma (in pair_sigma_finite) borel_measurable_positive_integral_snd:
hoelzl@49787
   792
  assumes "(\<lambda>(x, y). f x y) \<in> borel_measurable (M2 \<Otimes>\<^isub>M M1)" shows "(\<lambda>x. \<integral>\<^isup>+ y. f x y \<partial>M1) \<in> borel_measurable M2"
hoelzl@49787
   793
proof -
hoelzl@49787
   794
  interpret Q: pair_sigma_finite M2 M1 by default
hoelzl@49787
   795
  from Q.borel_measurable_positive_integral_fst assms show ?thesis by simp
hoelzl@49787
   796
qed
hoelzl@49787
   797
hoelzl@49787
   798
lemma (in information_space)
hoelzl@47694
   799
  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" and P: "sigma_finite_measure P"
hoelzl@47694
   800
  assumes Px: "distributed M S X Px"
hoelzl@47694
   801
  assumes Pz: "distributed M P Z Pz"
hoelzl@47694
   802
  assumes Pyz: "distributed M (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x)) Pyz"
hoelzl@47694
   803
  assumes Pxz: "distributed M (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) Pxz"
hoelzl@47694
   804
  assumes Pxyz: "distributed M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Y x, Z x)) Pxyz"
hoelzl@47694
   805
  assumes I1: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Px x * Pyz (y, z))))"
hoelzl@47694
   806
  assumes I2: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxz (x, z) / (Px x * Pz z)))"
hoelzl@49787
   807
  shows conditional_mutual_information_generic_eq: "conditional_mutual_information b S T P X Y Z
hoelzl@49787
   808
    = (\<integral>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))" (is "?eq")
hoelzl@49787
   809
    and conditional_mutual_information_generic_nonneg: "0 \<le> conditional_mutual_information b S T P X Y Z" (is "?nonneg")
hoelzl@40859
   810
proof -
hoelzl@47694
   811
  interpret S: sigma_finite_measure S by fact
hoelzl@47694
   812
  interpret T: sigma_finite_measure T by fact
hoelzl@47694
   813
  interpret P: sigma_finite_measure P by fact
hoelzl@47694
   814
  interpret TP: pair_sigma_finite T P ..
hoelzl@47694
   815
  interpret SP: pair_sigma_finite S P ..
hoelzl@49787
   816
  interpret ST: pair_sigma_finite S T ..
hoelzl@47694
   817
  interpret SPT: pair_sigma_finite "S \<Otimes>\<^isub>M P" T ..
hoelzl@47694
   818
  interpret STP: pair_sigma_finite S "T \<Otimes>\<^isub>M P" ..
hoelzl@49787
   819
  interpret TPS: pair_sigma_finite "T \<Otimes>\<^isub>M P" S ..
hoelzl@47694
   820
  have TP: "sigma_finite_measure (T \<Otimes>\<^isub>M P)" ..
hoelzl@47694
   821
  have SP: "sigma_finite_measure (S \<Otimes>\<^isub>M P)" ..
hoelzl@47694
   822
  have YZ: "random_variable (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x))"
hoelzl@47694
   823
    using Pyz by (simp add: distributed_measurable)
hoelzl@47694
   824
hoelzl@47694
   825
  have Pxyz_f: "\<And>M f. f \<in> measurable M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) \<Longrightarrow> (\<lambda>x. Pxyz (f x)) \<in> borel_measurable M"
hoelzl@47694
   826
    using measurable_comp[OF _ Pxyz[THEN distributed_real_measurable]] by (auto simp: comp_def)
hoelzl@47694
   827
hoelzl@47694
   828
  { fix f g h M
hoelzl@47694
   829
    assume f: "f \<in> measurable M S" and g: "g \<in> measurable M P" and h: "h \<in> measurable M (S \<Otimes>\<^isub>M P)"
hoelzl@47694
   830
    from measurable_comp[OF h Pxz[THEN distributed_real_measurable]]
hoelzl@47694
   831
         measurable_comp[OF f Px[THEN distributed_real_measurable]]
hoelzl@47694
   832
         measurable_comp[OF g Pz[THEN distributed_real_measurable]]
hoelzl@47694
   833
    have "(\<lambda>x. log b (Pxz (h x) / (Px (f x) * Pz (g x)))) \<in> borel_measurable M"
hoelzl@47694
   834
      by (simp add: comp_def b_gt_1) }
hoelzl@47694
   835
  note borel_log = this
hoelzl@47694
   836
hoelzl@47694
   837
  have measurable_cut: "(\<lambda>(x, y, z). (x, z)) \<in> measurable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (S \<Otimes>\<^isub>M P)"
hoelzl@47694
   838
    by (auto simp add: split_beta' comp_def intro!: measurable_Pair measurable_snd')
hoelzl@47694
   839
  
hoelzl@47694
   840
  from Pxz Pxyz have distr_eq: "distr M (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) =
hoelzl@47694
   841
    distr (distr M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Y x, Z x))) (S \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). (x, z))"
hoelzl@47694
   842
    by (subst distr_distr[OF measurable_cut]) (auto dest: distributed_measurable simp: comp_def)
hoelzl@40859
   843
hoelzl@47694
   844
  have "mutual_information b S P X Z =
hoelzl@47694
   845
    (\<integral>x. Pxz x * log b (Pxz x / (Px (fst x) * Pz (snd x))) \<partial>(S \<Otimes>\<^isub>M P))"
hoelzl@47694
   846
    by (rule mutual_information_distr[OF S P Px Pz Pxz])
hoelzl@47694
   847
  also have "\<dots> = (\<integral>(x,y,z). Pxyz (x,y,z) * log b (Pxz (x,z) / (Px x * Pz z)) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"
hoelzl@47694
   848
    using b_gt_1 Pxz Px Pz
hoelzl@47694
   849
    by (subst distributed_transform_integral[OF Pxyz Pxz, where T="\<lambda>(x, y, z). (x, z)"])
hoelzl@47694
   850
       (auto simp: split_beta' intro!: measurable_Pair measurable_snd' measurable_snd'' measurable_fst'' borel_measurable_times
hoelzl@47694
   851
             dest!: distributed_real_measurable)
hoelzl@47694
   852
  finally have mi_eq:
hoelzl@47694
   853
    "mutual_information b S P X Z = (\<integral>(x,y,z). Pxyz (x,y,z) * log b (Pxz (x,z) / (Px x * Pz z)) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))" .
hoelzl@47694
   854
  
hoelzl@49787
   855
  have ae1: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Px (fst x) = 0 \<longrightarrow> Pxyz x = 0"
hoelzl@47694
   856
    by (intro subdensity_real[of fst, OF _ Pxyz Px]) auto
hoelzl@49787
   857
  moreover have ae2: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pz (snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
hoelzl@47694
   858
    by (intro subdensity_real[of "\<lambda>x. snd (snd x)", OF _ Pxyz Pz]) (auto intro: measurable_snd')
hoelzl@49787
   859
  moreover have ae3: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pxz (fst x, snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
hoelzl@47694
   860
    by (intro subdensity_real[of "\<lambda>x. (fst x, snd (snd x))", OF _ Pxyz Pxz]) (auto intro: measurable_Pair measurable_snd')
hoelzl@49787
   861
  moreover have ae4: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pyz (snd x) = 0 \<longrightarrow> Pxyz x = 0"
hoelzl@47694
   862
    by (intro subdensity_real[of snd, OF _ Pxyz Pyz]) (auto intro: measurable_Pair)
hoelzl@49787
   863
  moreover have ae5: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Px (fst x)"
hoelzl@47694
   864
    using Px by (intro STP.AE_pair_measure) (auto simp: comp_def intro!: measurable_fst'' dest: distributed_real_AE distributed_real_measurable)
hoelzl@49787
   865
  moreover have ae6: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pyz (snd x)"
hoelzl@47694
   866
    using Pyz by (intro STP.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
hoelzl@49787
   867
  moreover have ae7: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pz (snd (snd x))"
hoelzl@47694
   868
    using Pz Pz[THEN distributed_real_measurable] by (auto intro!: measurable_snd'' TP.AE_pair_measure STP.AE_pair_measure AE_I2[of S] dest: distributed_real_AE)
hoelzl@49787
   869
  moreover have ae8: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pxz (fst x, snd (snd x))"
hoelzl@47694
   870
    using Pxz[THEN distributed_real_AE, THEN SP.AE_pair]
hoelzl@47694
   871
    using measurable_comp[OF measurable_Pair[OF measurable_fst measurable_comp[OF measurable_snd measurable_snd]] Pxz[THEN distributed_real_measurable], of T]
hoelzl@47694
   872
    using measurable_comp[OF measurable_snd measurable_Pair2[OF Pxz[THEN distributed_real_measurable]], of _ T]
hoelzl@47694
   873
    by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure simp: comp_def)
hoelzl@47694
   874
  moreover note Pxyz[THEN distributed_real_AE]
hoelzl@49787
   875
  ultimately have ae: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P.
hoelzl@47694
   876
    Pxyz x * log b (Pxyz x / (Px (fst x) * Pyz (snd x))) -
hoelzl@47694
   877
    Pxyz x * log b (Pxz (fst x, snd (snd x)) / (Px (fst x) * Pz (snd (snd x)))) =
hoelzl@47694
   878
    Pxyz x * log b (Pxyz x * Pz (snd (snd x)) / (Pxz (fst x, snd (snd x)) * Pyz (snd x))) "
hoelzl@47694
   879
  proof eventually_elim
hoelzl@47694
   880
    case (goal1 x)
hoelzl@47694
   881
    show ?case
hoelzl@40859
   882
    proof cases
hoelzl@47694
   883
      assume "Pxyz x \<noteq> 0"
hoelzl@47694
   884
      with goal1 have "0 < Px (fst x)" "0 < Pz (snd (snd x))" "0 < Pxz (fst x, snd (snd x))" "0 < Pyz (snd x)" "0 < Pxyz x"
hoelzl@47694
   885
        by auto
hoelzl@47694
   886
      then show ?thesis
hoelzl@47694
   887
        using b_gt_1 by (simp add: log_simps mult_pos_pos less_imp_le field_simps)
hoelzl@40859
   888
    qed simp
hoelzl@40859
   889
  qed
hoelzl@49787
   890
  with I1 I2 show ?eq
hoelzl@40859
   891
    unfolding conditional_mutual_information_def
hoelzl@47694
   892
    apply (subst mi_eq)
hoelzl@47694
   893
    apply (subst mutual_information_distr[OF S TP Px Pyz Pxyz])
hoelzl@47694
   894
    apply (subst integral_diff(2)[symmetric])
hoelzl@47694
   895
    apply (auto intro!: integral_cong_AE simp: split_beta' simp del: integral_diff)
hoelzl@47694
   896
    done
hoelzl@49787
   897
hoelzl@49787
   898
  let ?P = "density (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) Pxyz"
hoelzl@49787
   899
  interpret P: prob_space ?P
hoelzl@49787
   900
    unfolding distributed_distr_eq_density[OF Pxyz, symmetric]
hoelzl@49787
   901
    using distributed_measurable[OF Pxyz] by (rule prob_space_distr)
hoelzl@49787
   902
hoelzl@49787
   903
  let ?Q = "density (T \<Otimes>\<^isub>M P) Pyz"
hoelzl@49787
   904
  interpret Q: prob_space ?Q
hoelzl@49787
   905
    unfolding distributed_distr_eq_density[OF Pyz, symmetric]
hoelzl@49787
   906
    using distributed_measurable[OF Pyz] by (rule prob_space_distr)
hoelzl@49787
   907
hoelzl@49787
   908
  let ?f = "\<lambda>(x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) / Pxyz (x, y, z)"
hoelzl@49787
   909
hoelzl@49787
   910
  from subdensity_real[of snd, OF _ Pyz Pz]
hoelzl@49787
   911
  have aeX1: "AE x in T \<Otimes>\<^isub>M P. Pz (snd x) = 0 \<longrightarrow> Pyz x = 0" by (auto simp: comp_def)
hoelzl@49787
   912
  have aeX2: "AE x in T \<Otimes>\<^isub>M P. 0 \<le> Pz (snd x)"
hoelzl@49787
   913
    using Pz by (intro TP.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
hoelzl@49787
   914
hoelzl@49787
   915
  have aeX3: "AE y in T \<Otimes>\<^isub>M P. (\<integral>\<^isup>+ x. ereal (Pxz (x, snd y)) \<partial>S) = ereal (Pz (snd y))"
hoelzl@49788
   916
    using Pz distributed_marginal_eq_joint2[OF P S Pz Pxz]
hoelzl@49787
   917
    apply (intro TP.AE_pair_measure)
hoelzl@49787
   918
    apply (auto simp: comp_def measurable_split_conv
hoelzl@49787
   919
                intro!: measurable_snd'' borel_measurable_ereal_eq borel_measurable_ereal
hoelzl@49787
   920
                        SP.borel_measurable_positive_integral_snd measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
hoelzl@49787
   921
                        measurable_Pair
hoelzl@49787
   922
                dest: distributed_real_AE distributed_real_measurable)
hoelzl@49787
   923
    done
hoelzl@49787
   924
hoelzl@49787
   925
  note M = borel_measurable_divide borel_measurable_diff borel_measurable_times borel_measurable_ereal
hoelzl@49787
   926
           measurable_compose[OF _ measurable_snd]
hoelzl@49787
   927
           measurable_Pair
hoelzl@49787
   928
           measurable_compose[OF _ Pxyz[THEN distributed_real_measurable]]
hoelzl@49787
   929
           measurable_compose[OF _ Pxz[THEN distributed_real_measurable]]
hoelzl@49787
   930
           measurable_compose[OF _ Pyz[THEN distributed_real_measurable]]
hoelzl@49787
   931
           measurable_compose[OF _ Pz[THEN distributed_real_measurable]]
hoelzl@49787
   932
           measurable_compose[OF _ Px[THEN distributed_real_measurable]]
hoelzl@49787
   933
           STP.borel_measurable_positive_integral_snd
hoelzl@49787
   934
  have "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<le> (\<integral>\<^isup>+ (x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"
hoelzl@49787
   935
    apply (subst positive_integral_density)
hoelzl@49787
   936
    apply (rule distributed_borel_measurable[OF Pxyz])
hoelzl@49787
   937
    apply (rule distributed_AE[OF Pxyz])
hoelzl@49787
   938
    apply (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M) []
hoelzl@49787
   939
    apply (rule positive_integral_mono_AE)
hoelzl@49787
   940
    using ae5 ae6 ae7 ae8
hoelzl@49787
   941
    apply eventually_elim
hoelzl@49787
   942
    apply (auto intro!: divide_nonneg_nonneg mult_nonneg_nonneg)
hoelzl@49787
   943
    done
hoelzl@49787
   944
  also have "\<dots> = (\<integral>\<^isup>+(y, z). \<integral>\<^isup>+ x. ereal (Pxz (x, z)) * ereal (Pyz (y, z) / Pz z) \<partial>S \<partial>T \<Otimes>\<^isub>M P)"
hoelzl@49787
   945
    by (subst STP.positive_integral_snd_measurable[symmetric])
hoelzl@49787
   946
       (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M)
hoelzl@49787
   947
  also have "\<dots> = (\<integral>\<^isup>+x. ereal (Pyz x) * 1 \<partial>T \<Otimes>\<^isub>M P)"
hoelzl@49787
   948
    apply (rule positive_integral_cong_AE)
hoelzl@49787
   949
    using aeX1 aeX2 aeX3 distributed_AE[OF Pyz] AE_space
hoelzl@49787
   950
    apply eventually_elim
hoelzl@49787
   951
  proof (case_tac x, simp del: times_ereal.simps add: space_pair_measure)
hoelzl@49787
   952
    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"
hoelzl@49787
   953
      "(\<integral>\<^isup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)" 
hoelzl@49787
   954
    then show "(\<integral>\<^isup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
hoelzl@49787
   955
      apply (subst positive_integral_multc)
hoelzl@49787
   956
      apply (auto intro!: borel_measurable_ereal divide_nonneg_nonneg
hoelzl@49787
   957
                          measurable_compose[OF _ Pxz[THEN distributed_real_measurable]] measurable_Pair
hoelzl@49787
   958
                  split: prod.split)
hoelzl@49787
   959
      done
hoelzl@49787
   960
  qed
hoelzl@49787
   961
  also have "\<dots> = 1"
hoelzl@49787
   962
    using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
hoelzl@49787
   963
    by (subst positive_integral_density[symmetric]) (auto intro!: M)
hoelzl@49787
   964
  finally have le1: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<le> 1" .
hoelzl@49787
   965
  also have "\<dots> < \<infinity>" by simp
hoelzl@49787
   966
  finally have fin: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<noteq> \<infinity>" by simp
hoelzl@49787
   967
hoelzl@49787
   968
  have pos: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<noteq> 0"
hoelzl@49787
   969
    apply (subst positive_integral_density)
hoelzl@49787
   970
    apply (rule distributed_borel_measurable[OF Pxyz])
hoelzl@49787
   971
    apply (rule distributed_AE[OF Pxyz])
hoelzl@49787
   972
    apply (auto simp add: borel_measurable_ereal_iff split_beta' intro!: M) []
hoelzl@49787
   973
    apply (simp add: split_beta')
hoelzl@49787
   974
  proof
hoelzl@49787
   975
    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@49787
   976
    assume "(\<integral>\<^isup>+ x. ?g x \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P)) = 0"
hoelzl@49787
   977
    then have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. ?g x \<le> 0"
hoelzl@49787
   978
      by (intro positive_integral_0_iff_AE[THEN iffD1]) (auto intro!: M borel_measurable_ereal measurable_If)
hoelzl@49787
   979
    then have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pxyz x = 0"
hoelzl@49787
   980
      using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
hoelzl@49787
   981
      by eventually_elim (auto split: split_if_asm simp: mult_le_0_iff divide_le_0_iff)
hoelzl@49787
   982
    then have "(\<integral>\<^isup>+ x. ereal (Pxyz x) \<partial>S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) = 0"
hoelzl@49787
   983
      by (subst positive_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
hoelzl@49787
   984
    with P.emeasure_space_1 show False
hoelzl@49787
   985
      by (subst (asm) emeasure_density) (auto intro!: M cong: positive_integral_cong)
hoelzl@49787
   986
  qed
hoelzl@49787
   987
hoelzl@49787
   988
  have neg: "(\<integral>\<^isup>+ x. - ?f x \<partial>?P) = 0"
hoelzl@49787
   989
    apply (rule positive_integral_0_iff_AE[THEN iffD2])
hoelzl@49787
   990
    apply (auto intro!: M simp: split_beta') []
hoelzl@49787
   991
    apply (subst AE_density)
hoelzl@49787
   992
    apply (auto intro!: M simp: split_beta') []
hoelzl@49787
   993
    using ae5 ae6 ae7 ae8
hoelzl@49787
   994
    apply eventually_elim
hoelzl@49787
   995
    apply (auto intro!: mult_nonneg_nonneg divide_nonneg_nonneg)
hoelzl@49787
   996
    done
hoelzl@49787
   997
hoelzl@49787
   998
  have I3: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>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@49787
   999
    apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ integral_diff(1)[OF I1 I2]])
hoelzl@49787
  1000
    using ae
hoelzl@49787
  1001
    apply (auto intro!: M simp: split_beta')
hoelzl@49787
  1002
    done
hoelzl@49787
  1003
hoelzl@49787
  1004
  have "- log b 1 \<le> - log b (integral\<^isup>L ?P ?f)"
hoelzl@49787
  1005
  proof (intro le_imp_neg_le log_le[OF b_gt_1])
hoelzl@49787
  1006
    show "0 < integral\<^isup>L ?P ?f"
hoelzl@49787
  1007
      using neg pos fin positive_integral_positive[of ?P ?f]
hoelzl@49787
  1008
      by (cases "(\<integral>\<^isup>+ x. ?f x \<partial>?P)") (auto simp add: lebesgue_integral_def less_le split_beta')
hoelzl@49787
  1009
    show "integral\<^isup>L ?P ?f \<le> 1"
hoelzl@49787
  1010
      using neg le1 fin positive_integral_positive[of ?P ?f]
hoelzl@49787
  1011
      by (cases "(\<integral>\<^isup>+ x. ?f x \<partial>?P)") (auto simp add: lebesgue_integral_def split_beta' one_ereal_def)
hoelzl@49787
  1012
  qed
hoelzl@49787
  1013
  also have "- log b (integral\<^isup>L ?P ?f) \<le> (\<integral> x. - log b (?f x) \<partial>?P)"
hoelzl@49787
  1014
  proof (rule P.jensens_inequality[where a=0 and b=1 and I="{0<..}"])
hoelzl@49787
  1015
    show "AE x in ?P. ?f x \<in> {0<..}"
hoelzl@49787
  1016
      unfolding AE_density[OF distributed_borel_measurable[OF Pxyz]]
hoelzl@49787
  1017
      using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
hoelzl@49787
  1018
      by eventually_elim (auto simp: divide_pos_pos mult_pos_pos)
hoelzl@49787
  1019
    show "integrable ?P ?f"
hoelzl@49787
  1020
      unfolding integrable_def 
hoelzl@49787
  1021
      using fin neg by (auto intro!: M simp: split_beta')
hoelzl@49787
  1022
    show "integrable ?P (\<lambda>x. - log b (?f x))"
hoelzl@49787
  1023
      apply (subst integral_density)
hoelzl@49787
  1024
      apply (auto intro!: M) []
hoelzl@49787
  1025
      apply (auto intro!: M distributed_real_AE[OF Pxyz]) []
hoelzl@49787
  1026
      apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
hoelzl@49787
  1027
      apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ I3])
hoelzl@49787
  1028
      apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
hoelzl@49787
  1029
      apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
hoelzl@49787
  1030
      using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
hoelzl@49787
  1031
      apply eventually_elim
hoelzl@49787
  1032
      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
  1033
      done
hoelzl@49787
  1034
  qed (auto simp: b_gt_1 minus_log_convex)
hoelzl@49787
  1035
  also have "\<dots> = conditional_mutual_information b S T P X Y Z"
hoelzl@49787
  1036
    unfolding `?eq`
hoelzl@49787
  1037
    apply (subst integral_density)
hoelzl@49787
  1038
    apply (auto intro!: M) []
hoelzl@49787
  1039
    apply (auto intro!: M distributed_real_AE[OF Pxyz]) []
hoelzl@49787
  1040
    apply (auto intro!: M borel_measurable_uminus borel_measurable_log simp: split_beta') []
hoelzl@49787
  1041
    apply (intro integral_cong_AE)
hoelzl@49787
  1042
    using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
hoelzl@49787
  1043
    apply eventually_elim
hoelzl@49787
  1044
    apply (auto simp: log_divide_eq zero_less_mult_iff zero_less_divide_iff field_simps)
hoelzl@49787
  1045
    done
hoelzl@49787
  1046
  finally show ?nonneg
hoelzl@49787
  1047
    by simp
hoelzl@40859
  1048
qed
hoelzl@40859
  1049
hoelzl@40859
  1050
lemma (in information_space) conditional_mutual_information_eq:
hoelzl@47694
  1051
  assumes Pz: "simple_distributed M Z Pz"
hoelzl@47694
  1052
  assumes Pyz: "simple_distributed M (\<lambda>x. (Y x, Z x)) Pyz"
hoelzl@47694
  1053
  assumes Pxz: "simple_distributed M (\<lambda>x. (X x, Z x)) Pxz"
hoelzl@47694
  1054
  assumes Pxyz: "simple_distributed M (\<lambda>x. (X x, Y x, Z x)) Pxyz"
hoelzl@47694
  1055
  shows "\<I>(X ; Y | Z) =
hoelzl@47694
  1056
   (\<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
  1057
proof (subst conditional_mutual_information_generic_eq[OF _ _ _ _
hoelzl@47694
  1058
    simple_distributed[OF Pz] simple_distributed_joint[OF Pyz] simple_distributed_joint[OF Pxz]
hoelzl@47694
  1059
    simple_distributed_joint2[OF Pxyz]])
hoelzl@47694
  1060
  note simple_distributed_joint2_finite[OF Pxyz, simp]
hoelzl@47694
  1061
  show "sigma_finite_measure (count_space (X ` space M))"
hoelzl@47694
  1062
    by (simp add: sigma_finite_measure_count_space_finite)
hoelzl@47694
  1063
  show "sigma_finite_measure (count_space (Y ` space M))"
hoelzl@47694
  1064
    by (simp add: sigma_finite_measure_count_space_finite)
hoelzl@47694
  1065
  show "sigma_finite_measure (count_space (Z ` space M))"
hoelzl@47694
  1066
    by (simp add: sigma_finite_measure_count_space_finite)
hoelzl@47694
  1067
  have "count_space (X ` space M) \<Otimes>\<^isub>M count_space (Y ` space M) \<Otimes>\<^isub>M count_space (Z ` space M) =
hoelzl@47694
  1068
      count_space (X`space M \<times> Y`space M \<times> Z`space M)"
hoelzl@47694
  1069
    (is "?P = ?C")
hoelzl@47694
  1070
    by (simp add: pair_measure_count_space)
hoelzl@40859
  1071
hoelzl@47694
  1072
  let ?Px = "\<lambda>x. measure M (X -` {x} \<inter> space M)"
hoelzl@47694
  1073
  have "(\<lambda>x. (X x, Z x)) \<in> measurable M (count_space (X ` space M) \<Otimes>\<^isub>M count_space (Z ` space M))"
hoelzl@47694
  1074
    using simple_distributed_joint[OF Pxz] by (rule distributed_measurable)
hoelzl@47694
  1075
  from measurable_comp[OF this measurable_fst]
hoelzl@47694
  1076
  have "random_variable (count_space (X ` space M)) X"
hoelzl@47694
  1077
    by (simp add: comp_def)
hoelzl@47694
  1078
  then have "simple_function M X"    
hoelzl@47694
  1079
    unfolding simple_function_def by auto
hoelzl@47694
  1080
  then have "simple_distributed M X ?Px"
hoelzl@47694
  1081
    by (rule simple_distributedI) auto
hoelzl@47694
  1082
  then show "distributed M (count_space (X ` space M)) X ?Px"
hoelzl@47694
  1083
    by (rule simple_distributed)
hoelzl@47694
  1084
hoelzl@47694
  1085
  let ?f = "(\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x, Z x)) ` space M then Pxyz x else 0)"
hoelzl@47694
  1086
  let ?g = "(\<lambda>x. if x \<in> (\<lambda>x. (Y x, Z x)) ` space M then Pyz x else 0)"
hoelzl@47694
  1087
  let ?h = "(\<lambda>x. if x \<in> (\<lambda>x. (X x, Z x)) ` space M then Pxz x else 0)"
hoelzl@47694
  1088
  show
hoelzl@47694
  1089
      "integrable ?P (\<lambda>(x, y, z). ?f (x, y, z) * log b (?f (x, y, z) / (?Px x * ?g (y, z))))"
hoelzl@47694
  1090
      "integrable ?P (\<lambda>(x, y, z). ?f (x, y, z) * log b (?h (x, z) / (?Px x * Pz z)))"
hoelzl@47694
  1091
    by (auto intro!: integrable_count_space simp: pair_measure_count_space)
hoelzl@47694
  1092
  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
  1093
  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
  1094
  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
  1095
    by (auto intro!: ext)
hoelzl@47694
  1096
  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)"
hoelzl@47694
  1097
    by (auto intro!: setsum_cong simp add: `?P = ?C` lebesgue_integral_count_space_finite simple_distributed_finite setsum_cases split_beta')
hoelzl@36624
  1098
qed
hoelzl@36624
  1099
hoelzl@47694
  1100
lemma (in information_space) conditional_mutual_information_nonneg:
hoelzl@47694
  1101
  assumes X: "simple_function M X" and Y: "simple_function M Y" and Z: "simple_function M Z"
hoelzl@47694
  1102
  shows "0 \<le> \<I>(X ; Y | Z)"
hoelzl@47694
  1103
proof -
hoelzl@49787
  1104
  have [simp]: "count_space (X ` space M) \<Otimes>\<^isub>M count_space (Y ` space M) \<Otimes>\<^isub>M count_space (Z ` space M) =
hoelzl@49787
  1105
      count_space (X`space M \<times> Y`space M \<times> Z`space M)"
hoelzl@49787
  1106
    by (simp add: pair_measure_count_space X Y Z simple_functionD)
hoelzl@49787
  1107
  note sf = sigma_finite_measure_count_space_finite[OF simple_functionD(1)]
hoelzl@49787
  1108
  note sd = simple_distributedI[OF _ refl]
hoelzl@49787
  1109
  note sp = simple_function_Pair
hoelzl@49787
  1110
  show ?thesis
hoelzl@49787
  1111
   apply (rule conditional_mutual_information_generic_nonneg[OF sf[OF X] sf[OF Y] sf[OF Z]])
hoelzl@49787
  1112
   apply (rule simple_distributed[OF sd[OF X]])
hoelzl@49787
  1113
   apply (rule simple_distributed[OF sd[OF Z]])
hoelzl@49787
  1114
   apply (rule simple_distributed_joint[OF sd[OF sp[OF Y Z]]])
hoelzl@49787
  1115
   apply (rule simple_distributed_joint[OF sd[OF sp[OF X Z]]])
hoelzl@49787
  1116
   apply (rule simple_distributed_joint2[OF sd[OF sp[OF X sp[OF Y Z]]]])
hoelzl@49787
  1117
   apply (auto intro!: integrable_count_space simp: X Y Z simple_functionD)
hoelzl@49787
  1118
   done
hoelzl@36080
  1119
qed
hoelzl@36080
  1120
hoelzl@39097
  1121
subsection {* Conditional Entropy *}
hoelzl@39097
  1122
hoelzl@36080
  1123
definition (in prob_space)
hoelzl@49791
  1124
  "conditional_entropy b S T X Y = - (\<integral>(x, y). log b (real (RN_deriv (S \<Otimes>\<^isub>M T) (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))) (x, y)) / 
hoelzl@49791
  1125
    real (RN_deriv T (distr M T Y) y)) \<partial>distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)))"
hoelzl@36080
  1126
hoelzl@40859
  1127
abbreviation (in information_space)
hoelzl@40859
  1128
  conditional_entropy_Pow ("\<H>'(_ | _')") where
hoelzl@47694
  1129
  "\<H>(X | Y) \<equiv> conditional_entropy b (count_space (X`space M)) (count_space (Y`space M)) X Y"
hoelzl@36080
  1130
hoelzl@49791
  1131
lemma (in information_space) conditional_entropy_generic_eq:
hoelzl@49791
  1132
  fixes Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
hoelzl@49791
  1133
  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
hoelzl@49791
  1134
  assumes Py: "distributed M T Y Py"
hoelzl@49791
  1135
  assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
hoelzl@49791
  1136
  shows "conditional_entropy b S T X Y = - (\<integral>(x, y). Pxy (x, y) * log b (Pxy (x, y) / Py y) \<partial>(S \<Otimes>\<^isub>M T))"
hoelzl@49791
  1137
proof -
hoelzl@49791
  1138
  interpret S: sigma_finite_measure S by fact
hoelzl@49791
  1139
  interpret T: sigma_finite_measure T by fact
hoelzl@49791
  1140
  interpret ST: pair_sigma_finite S T ..
hoelzl@49791
  1141
hoelzl@49791
  1142
  have "AE x in density (S \<Otimes>\<^isub>M T) (\<lambda>x. ereal (Pxy x)). Pxy x = real (RN_deriv (S \<Otimes>\<^isub>M T) (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))) x)"
hoelzl@49791
  1143
    unfolding AE_density[OF distributed_borel_measurable, OF Pxy]
hoelzl@49791
  1144
    unfolding distributed_distr_eq_density[OF Pxy]
hoelzl@49791
  1145
    using distributed_RN_deriv[OF Pxy]
hoelzl@49791
  1146
    by auto
hoelzl@49791
  1147
  moreover
hoelzl@49791
  1148
  have "AE x in density (S \<Otimes>\<^isub>M T) (\<lambda>x. ereal (Pxy x)). Py (snd x) = real (RN_deriv T (distr M T Y) (snd x))"
hoelzl@49791
  1149
    unfolding AE_density[OF distributed_borel_measurable, OF Pxy]
hoelzl@49791
  1150
    unfolding distributed_distr_eq_density[OF Py]
hoelzl@49791
  1151
    apply (rule ST.AE_pair_measure)
hoelzl@49791
  1152
    apply (auto intro!: sets_Collect borel_measurable_eq measurable_compose[OF _ distributed_real_measurable[OF Py]]
hoelzl@49791
  1153
                        distributed_real_measurable[OF Pxy] distributed_real_AE[OF Py]
hoelzl@49791
  1154
                        borel_measurable_real_of_ereal measurable_compose[OF _ borel_measurable_RN_deriv_density])
hoelzl@49791
  1155
    using distributed_RN_deriv[OF Py]
hoelzl@49791
  1156
    apply auto
hoelzl@49791
  1157
    done    
hoelzl@49791
  1158
  ultimately
hoelzl@49791
  1159
  have "conditional_entropy b S T X Y = - (\<integral>x. Pxy x * log b (Pxy x / Py (snd x)) \<partial>(S \<Otimes>\<^isub>M T))"
hoelzl@49791
  1160
    unfolding conditional_entropy_def neg_equal_iff_equal
hoelzl@49791
  1161
    apply (subst integral_density(1)[symmetric])
hoelzl@49791
  1162
    apply (auto simp: distributed_real_measurable[OF Pxy] distributed_real_AE[OF Pxy]
hoelzl@49791
  1163
                      measurable_compose[OF _ distributed_real_measurable[OF Py]]
hoelzl@49791
  1164
                      distributed_distr_eq_density[OF Pxy]
hoelzl@49791
  1165
                intro!: integral_cong_AE)
hoelzl@49791
  1166
    done
hoelzl@49791
  1167
  then show ?thesis by (simp add: split_beta')
hoelzl@49791
  1168
qed
hoelzl@49791
  1169
hoelzl@49791
  1170
lemma (in information_space) conditional_entropy_eq_entropy:
hoelzl@47694
  1171
  fixes Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
hoelzl@47694
  1172
  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
hoelzl@47694
  1173
  assumes Py: "distributed M T Y Py"
hoelzl@47694
  1174
  assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
hoelzl@47694
  1175
  assumes I1: "integrable (S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Pxy x))"
hoelzl@47694
  1176
  assumes I2: "integrable (S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Py (snd x)))"
hoelzl@49791
  1177
  shows "conditional_entropy b S T X Y = entropy b (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) - entropy b T Y"
hoelzl@40859
  1178
proof -
hoelzl@47694
  1179
  interpret S: sigma_finite_measure S by fact
hoelzl@47694
  1180
  interpret T: sigma_finite_measure T by fact
hoelzl@47694
  1181
  interpret ST: pair_sigma_finite S T ..
hoelzl@47694
  1182
hoelzl@47694
  1183
  have "entropy b T Y = - (\<integral>y. Py y * log b (Py y) \<partial>T)"
hoelzl@49786
  1184
    by (rule entropy_distr[OF Py])
hoelzl@47694
  1185
  also have "\<dots> = - (\<integral>(x,y). Pxy (x,y) * log b (Py y) \<partial>(S \<Otimes>\<^isub>M T))"
hoelzl@47694
  1186
    using b_gt_1 Py[THEN distributed_real_measurable]
hoelzl@47694
  1187
    by (subst distributed_transform_integral[OF Pxy Py, where T=snd]) (auto intro!: integral_cong)
hoelzl@47694
  1188
  finally have e_eq: "entropy b T Y = - (\<integral>(x,y). Pxy (x,y) * log b (Py y) \<partial>(S \<Otimes>\<^isub>M T))" .
hoelzl@49791
  1189
hoelzl@49790
  1190
  have ae2: "AE x in S \<Otimes>\<^isub>M T. Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
hoelzl@47694
  1191
    by (intro subdensity_real[of snd, OF _ Pxy Py]) (auto intro: measurable_Pair)
hoelzl@49788
  1192
  moreover have ae4: "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Py (snd x)"
hoelzl@47694
  1193
    using Py by (intro ST.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
hoelzl@49788
  1194
  moreover note ae5 = Pxy[THEN distributed_real_AE]
hoelzl@49791
  1195
  ultimately have "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Pxy x \<and> 0 \<le> Py (snd x) \<and>
hoelzl@49790
  1196
    (Pxy x = 0 \<or> (Pxy x \<noteq> 0 \<longrightarrow> 0 < Pxy x \<and> 0 < Py (snd x)))"
hoelzl@47694
  1197
    by eventually_elim auto
hoelzl@49791
  1198
  then have ae: "AE x in S \<Otimes>\<^isub>M T.
hoelzl@47694
  1199
     Pxy x * log b (Pxy x) - Pxy x * log b (Py (snd x)) = Pxy x * log b (Pxy x / Py (snd x))"
hoelzl@47694
  1200
    by eventually_elim (auto simp: log_simps mult_pos_pos field_simps b_gt_1)
hoelzl@49791
  1201
  have "conditional_entropy b S T X Y = 
hoelzl@49791
  1202
    - (\<integral>x. Pxy x * log b (Pxy x) - Pxy x * log b (Py (snd x)) \<partial>(S \<Otimes>\<^isub>M T))"
hoelzl@49791
  1203
    unfolding conditional_entropy_generic_eq[OF S T Py Pxy] neg_equal_iff_equal
hoelzl@49791
  1204
    apply (intro integral_cong_AE)
hoelzl@49791
  1205
    using ae
hoelzl@49791
  1206
    apply eventually_elim
hoelzl@49791
  1207
    apply auto
hoelzl@47694
  1208
    done
hoelzl@49791
  1209
  also have "\<dots> = - (\<integral>x. Pxy x * log b (Pxy x) \<partial>(S \<Otimes>\<^isub>M T)) - - (\<integral>x.  Pxy x * log b (Py (snd x)) \<partial>(S \<Otimes>\<^isub>M T))"
hoelzl@49791
  1210
    by (simp add: integral_diff[OF I1 I2])
hoelzl@49791
  1211
  finally show ?thesis 
hoelzl@49791
  1212
    unfolding conditional_entropy_generic_eq[OF S T Py Pxy] entropy_distr[OF Pxy] e_eq
hoelzl@49791
  1213
    by (simp add: split_beta')
hoelzl@49791
  1214
qed
hoelzl@49791
  1215
hoelzl@49791
  1216
lemma (in information_space) conditional_entropy_eq_entropy_simple:
hoelzl@49791
  1217
  assumes X: "simple_function M X" and Y: "simple_function M Y"
hoelzl@49791
  1218
  shows "\<H>(X | Y) = entropy b (count_space (X`space M) \<Otimes>\<^isub>M count_space (Y`space M)) (\<lambda>x. (X x, Y x)) - \<H>(Y)"
hoelzl@49791
  1219
proof -
hoelzl@49791
  1220
  have "count_space (X ` space M) \<Otimes>\<^isub>M count_space (Y ` space M) = count_space (X`space M \<times> Y`space M)"
hoelzl@49791
  1221
    (is "?P = ?C") using X Y by (simp add: simple_functionD pair_measure_count_space)
hoelzl@49791
  1222
  show ?thesis
hoelzl@49791
  1223
    by (rule conditional_entropy_eq_entropy sigma_finite_measure_count_space_finite
hoelzl@49791
  1224
                 simple_functionD  X Y simple_distributed simple_distributedI[OF _ refl]
hoelzl@49791
  1225
                 simple_distributed_joint simple_function_Pair integrable_count_space)+
hoelzl@49791
  1226
       (auto simp: `?P = ?C` intro!: integrable_count_space simple_functionD  X Y)
hoelzl@39097
  1227
qed
hoelzl@39097
  1228
hoelzl@40859
  1229
lemma (in information_space) conditional_entropy_eq:
hoelzl@49792
  1230
  assumes Y: "simple_distributed M Y Py"
hoelzl@47694
  1231
  assumes XY: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"
hoelzl@47694
  1232
    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
  1233
proof (subst conditional_entropy_generic_eq[OF _ _
hoelzl@49790
  1234
  simple_distributed[OF Y] simple_distributed_joint[OF XY]])
hoelzl@49792
  1235
  have "finite ((\<lambda>x. (X x, Y x))`space M)"
hoelzl@49792
  1236
    using XY unfolding simple_distributed_def by auto
hoelzl@49792
  1237
  from finite_imageI[OF this, of fst]
hoelzl@49792
  1238
  have [simp]: "finite (X`space M)"
hoelzl@49792
  1239
    by (simp add: image_compose[symmetric] comp_def)
hoelzl@47694
  1240
  note Y[THEN simple_distributed_finite, simp]
hoelzl@47694
  1241
  show "sigma_finite_measure (count_space (X ` space M))"
hoelzl@47694
  1242
    by (simp add: sigma_finite_measure_count_space_finite)
hoelzl@47694
  1243
  show "sigma_finite_measure (count_space (Y ` space M))"
hoelzl@47694
  1244
    by (simp add: sigma_finite_measure_count_space_finite)
hoelzl@47694
  1245
  let ?f = "(\<lambda>x. if x \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy x else 0)"
hoelzl@47694
  1246
  have "count_space (X ` space M) \<Otimes>\<^isub>M count_space (Y ` space M) = count_space (X`space M \<times> Y`space M)"
hoelzl@47694
  1247
    (is "?P = ?C")
hoelzl@49792
  1248
    using Y by (simp add: simple_distributed_finite pair_measure_count_space)
hoelzl@47694
  1249
  have eq: "(\<lambda>(x, y). ?f (x, y) * log b (?f (x, y) / Py y)) =
hoelzl@47694
  1250
    (\<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
  1251
    by auto
hoelzl@49792
  1252
  from Y show "- (\<integral> (x, y). ?f (x, y) * log b (?f (x, y) / Py y) \<partial>?P) =
hoelzl@47694
  1253
    - (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / Py y))"
hoelzl@47694
  1254
    by (auto intro!: setsum_cong simp add: `?P = ?C` lebesgue_integral_count_space_finite simple_distributed_finite eq setsum_cases split_beta')
hoelzl@47694
  1255
qed
hoelzl@39097
  1256
hoelzl@47694
  1257
lemma (in information_space) conditional_mutual_information_eq_conditional_entropy:
hoelzl@41689
  1258
  assumes X: "simple_function M X" and Y: "simple_function M Y"
hoelzl@47694
  1259
  shows "\<I>(X ; X | Y) = \<H>(X | Y)"
hoelzl@47694
  1260
proof -
hoelzl@47694
  1261
  def Py \<equiv> "\<lambda>x. if x \<in> Y`space M then measure M (Y -` {x} \<inter> space M) else 0"
hoelzl@47694
  1262
  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
  1263
  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
  1264
  let ?M = "X`space M \<times> X`space M \<times> Y`space M"
hoelzl@39097
  1265
hoelzl@47694
  1266
  note XY = simple_function_Pair[OF X Y]
hoelzl@47694
  1267
  note XXY = simple_function_Pair[OF X XY]
hoelzl@47694
  1268
  have Py: "simple_distributed M Y Py"
hoelzl@47694
  1269
    using Y by (rule simple_distributedI) (auto simp: Py_def)
hoelzl@47694
  1270
  have Pxy: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"
hoelzl@47694
  1271
    using XY by (rule simple_distributedI) (auto simp: Pxy_def)
hoelzl@47694
  1272
  have Pxxy: "simple_distributed M (\<lambda>x. (X x, X x, Y x)) Pxxy"
hoelzl@47694
  1273
    using XXY by (rule simple_distributedI) (auto simp: Pxxy_def)
hoelzl@47694
  1274
  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
  1275
    by auto
hoelzl@47694
  1276
  have inj: "\<And>A. inj_on (\<lambda>(x, y). (x, x, y)) A"
hoelzl@47694
  1277
    by (auto simp: inj_on_def)
hoelzl@47694
  1278
  have Pxxy_eq: "\<And>x y. Pxxy (x, x, y) = Pxy (x, y)"
hoelzl@47694
  1279
    by (auto simp: Pxxy_def Pxy_def intro!: arg_cong[where f=prob])
hoelzl@47694
  1280
  have "AE x in count_space ((\<lambda>x. (X x, Y x))`space M). Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
hoelzl@47694
  1281
    by (intro subdensity_real[of snd, OF _ Pxy[THEN simple_distributed] Py[THEN simple_distributed]]) (auto intro: measurable_Pair)
hoelzl@47694
  1282
  then show ?thesis
hoelzl@47694
  1283
    apply (subst conditional_mutual_information_eq[OF Py Pxy Pxy Pxxy])
hoelzl@49792
  1284
    apply (subst conditional_entropy_eq[OF Py Pxy])
hoelzl@47694
  1285
    apply (auto intro!: setsum_cong simp: Pxxy_eq setsum_negf[symmetric] eq setsum_reindex[OF inj]
hoelzl@47694
  1286
                log_simps zero_less_mult_iff zero_le_mult_iff field_simps mult_less_0_iff AE_count_space)
hoelzl@47694
  1287
    using Py[THEN simple_distributed, THEN distributed_real_AE] Pxy[THEN simple_distributed, THEN distributed_real_AE]
hoelzl@49790
  1288
  apply (auto simp add: not_le[symmetric] AE_count_space)
hoelzl@47694
  1289
    done
hoelzl@47694
  1290
qed
hoelzl@47694
  1291
hoelzl@47694
  1292
lemma (in information_space) conditional_entropy_nonneg:
hoelzl@47694
  1293
  assumes X: "simple_function M X" and Y: "simple_function M Y" shows "0 \<le> \<H>(X | Y)"
hoelzl@47694
  1294
  using conditional_mutual_information_eq_conditional_entropy[OF X Y] conditional_mutual_information_nonneg[OF X X Y]
hoelzl@47694
  1295
  by simp
hoelzl@36080
  1296
hoelzl@39097
  1297
subsection {* Equalities *}
hoelzl@39097
  1298
hoelzl@47694
  1299
lemma (in information_space) mutual_information_eq_entropy_conditional_entropy_distr:
hoelzl@47694
  1300
  fixes Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real" and Pxy :: "('b \<times> 'c) \<Rightarrow> real"
hoelzl@47694
  1301
  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
hoelzl@47694
  1302
  assumes Px: "distributed M S X Px" and Py: "distributed M T Y Py"
hoelzl@47694
  1303
  assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
hoelzl@47694
  1304
  assumes Ix: "integrable(S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Px (fst x)))"
hoelzl@47694
  1305
  assumes Iy: "integrable(S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Py (snd x)))"
hoelzl@47694
  1306
  assumes Ixy: "integrable(S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Pxy x))"
hoelzl@47694
  1307
  shows  "mutual_information b S T X Y = entropy b S X + entropy b T Y - entropy b (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
hoelzl@40859
  1308
proof -
hoelzl@47694
  1309
  have X: "entropy b S X = - (\<integral>x. Pxy x * log b (Px (fst x)) \<partial>(S \<Otimes>\<^isub>M T))"
hoelzl@47694
  1310
    using b_gt_1 Px[THEN distributed_real_measurable]
hoelzl@49786
  1311
    apply (subst entropy_distr[OF Px])
hoelzl@47694
  1312
    apply (subst distributed_transform_integral[OF Pxy Px, where T=fst])
hoelzl@47694
  1313
    apply (auto intro!: integral_cong)
hoelzl@47694
  1314
    done
hoelzl@47694
  1315
hoelzl@47694
  1316
  have Y: "entropy b T Y = - (\<integral>x. Pxy x * log b (Py (snd x)) \<partial>(S \<Otimes>\<^isub>M T))"
hoelzl@47694
  1317
    using b_gt_1 Py[THEN distributed_real_measurable]
hoelzl@49786
  1318
    apply (subst entropy_distr[OF Py])
hoelzl@47694
  1319
    apply (subst distributed_transform_integral[OF Pxy Py, where T=snd])
hoelzl@47694
  1320
    apply (auto intro!: integral_cong)
hoelzl@47694
  1321
    done
hoelzl@47694
  1322
hoelzl@47694
  1323
  interpret S: sigma_finite_measure S by fact
hoelzl@47694
  1324
  interpret T: sigma_finite_measure T by fact
hoelzl@47694
  1325
  interpret ST: pair_sigma_finite S T ..
hoelzl@47694
  1326
  have ST: "sigma_finite_measure (S \<Otimes>\<^isub>M T)" ..
hoelzl@47694
  1327
hoelzl@47694
  1328
  have XY: "entropy b (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) = - (\<integral>x. Pxy x * log b (Pxy x) \<partial>(S \<Otimes>\<^isub>M T))"
hoelzl@49786
  1329
    by (subst entropy_distr[OF Pxy]) (auto intro!: integral_cong)
hoelzl@47694
  1330
  
hoelzl@47694
  1331
  have "AE x in S \<Otimes>\<^isub>M T. Px (fst x) = 0 \<longrightarrow> Pxy x = 0"
hoelzl@47694
  1332
    by (intro subdensity_real[of fst, OF _ Pxy Px]) (auto intro: measurable_Pair)
hoelzl@47694
  1333
  moreover have "AE x in S \<Otimes>\<^isub>M T. Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
hoelzl@47694
  1334
    by (intro subdensity_real[of snd, OF _ Pxy Py]) (auto intro: measurable_Pair)
hoelzl@47694
  1335
  moreover have "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Px (fst x)"
hoelzl@47694
  1336
    using Px by (intro ST.AE_pair_measure) (auto simp: comp_def intro!: measurable_fst'' dest: distributed_real_AE distributed_real_measurable)
hoelzl@47694
  1337
  moreover have "AE x in S \<Otimes>\<^isub>M T. 0 \<le> Py (snd x)"
hoelzl@47694
  1338
    using Py by (intro ST.AE_pair_measure) (auto simp: comp_def intro!: measurable_snd'' dest: distributed_real_AE distributed_real_measurable)
hoelzl@47694
  1339
  moreover note Pxy[THEN distributed_real_AE]
hoelzl@47694
  1340
  ultimately have "AE x in S \<Otimes>\<^isub>M T. Pxy x * log b (Pxy x) - Pxy x * log b (Px (fst x)) - Pxy x * log b (Py (snd x)) = 
hoelzl@47694
  1341
    Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x)))"
hoelzl@47694
  1342
    (is "AE x in _. ?f x = ?g x")
hoelzl@47694
  1343
  proof eventually_elim
hoelzl@47694
  1344
    case (goal1 x)
hoelzl@47694
  1345
    show ?case
hoelzl@47694
  1346
    proof cases
hoelzl@47694
  1347
      assume "Pxy x \<noteq> 0"
hoelzl@47694
  1348
      with goal1 have "0 < Px (fst x)" "0 < Py (snd x)" "0 < Pxy x"
hoelzl@47694
  1349
        by auto
hoelzl@47694
  1350
      then show ?thesis
hoelzl@47694
  1351
        using b_gt_1 by (simp add: log_simps mult_pos_pos less_imp_le field_simps)
hoelzl@47694
  1352
    qed simp
hoelzl@47694
  1353
  qed
hoelzl@47694
  1354
hoelzl@47694
  1355
  have "entropy b S X + entropy b T Y - entropy b (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) = integral\<^isup>L (S \<Otimes>\<^isub>M T) ?f"
hoelzl@47694
  1356
    unfolding X Y XY
hoelzl@47694
  1357
    apply (subst integral_diff)
hoelzl@47694
  1358
    apply (intro integral_diff Ixy Ix Iy)+
hoelzl@47694
  1359
    apply (subst integral_diff)
hoelzl@47694
  1360
    apply (intro integral_diff Ixy Ix Iy)+
hoelzl@47694
  1361
    apply (simp add: field_simps)
hoelzl@47694
  1362
    done
hoelzl@47694
  1363
  also have "\<dots> = integral\<^isup>L (S \<Otimes>\<^isub>M T) ?g"
hoelzl@47694
  1364
    using `AE x in _. ?f x = ?g x` by (rule integral_cong_AE)
hoelzl@47694
  1365
  also have "\<dots> = mutual_information b S T X Y"
hoelzl@47694
  1366
    by (rule mutual_information_distr[OF S T Px Py Pxy, symmetric])
hoelzl@47694
  1367
  finally show ?thesis ..
hoelzl@47694
  1368
qed
hoelzl@47694
  1369
hoelzl@49802
  1370
lemma (in information_space) mutual_information_eq_entropy_conditional_entropy':
hoelzl@49802
  1371
  fixes Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real" and Pxy :: "('b \<times> 'c) \<Rightarrow> real"
hoelzl@49802
  1372
  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
hoelzl@49802
  1373
  assumes Px: "distributed M S X Px" and Py: "distributed M T Y Py"
hoelzl@49802
  1374
  assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
hoelzl@49802
  1375
  assumes Ix: "integrable(S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Px (fst x)))"
hoelzl@49802
  1376
  assumes Iy: "integrable(S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Py (snd x)))"
hoelzl@49802
  1377
  assumes Ixy: "integrable(S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Pxy x))"
hoelzl@49802
  1378
  shows  "mutual_information b S T X Y = entropy b S X - conditional_entropy b S T X Y"
hoelzl@49802
  1379
  using
hoelzl@49802
  1380
    mutual_information_eq_entropy_conditional_entropy_distr[OF S T Px Py Pxy Ix Iy Ixy]
hoelzl@49802
  1381
    conditional_entropy_eq_entropy[OF S T Py Pxy Ixy Iy]
hoelzl@49802
  1382
  by simp
hoelzl@49802
  1383
hoelzl@47694
  1384
lemma (in information_space) mutual_information_eq_entropy_conditional_entropy:
hoelzl@47694
  1385
  assumes sf_X: "simple_function M X" and sf_Y: "simple_function M Y"
hoelzl@47694
  1386
  shows  "\<I>(X ; Y) = \<H>(X) - \<H>(X | Y)"
hoelzl@47694
  1387
proof -
hoelzl@47694
  1388
  have X: "simple_distributed M X (\<lambda>x. measure M (X -` {x} \<inter> space M))"
hoelzl@47694
  1389
    using sf_X by (rule simple_distributedI) auto
hoelzl@47694
  1390
  have Y: "simple_distributed M Y (\<lambda>x. measure M (Y -` {x} \<inter> space M))"
hoelzl@47694
  1391
    using sf_Y by (rule simple_distributedI) auto
hoelzl@47694
  1392
  have sf_XY: "simple_function M (\<lambda>x. (X x, Y x))"
hoelzl@47694
  1393
    using sf_X sf_Y by (rule simple_function_Pair)
hoelzl@47694
  1394
  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
  1395
    by (rule simple_distributedI) auto
hoelzl@47694
  1396
  from simple_distributed_joint_finite[OF this, simp]
hoelzl@47694
  1397
  have eq: "count_space (X ` space M) \<Otimes>\<^isub>M count_space (Y ` space M) = count_space (X ` space M \<times> Y ` space M)"
hoelzl@47694
  1398
    by (simp add: pair_measure_count_space)
hoelzl@47694
  1399
hoelzl@47694
  1400
  have "\<I>(X ; Y) = \<H>(X) + \<H>(Y) - entropy b (count_space (X`space M) \<Otimes>\<^isub>M count_space (Y`space M)) (\<lambda>x. (X x, Y x))"
hoelzl@47694
  1401
    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
  1402
    by (rule mutual_information_eq_entropy_conditional_entropy_distr) (auto simp: eq integrable_count_space)
hoelzl@47694
  1403
  then show ?thesis
hoelzl@49791
  1404
    unfolding conditional_entropy_eq_entropy_simple[OF sf_X sf_Y] by simp
hoelzl@47694
  1405
qed
hoelzl@47694
  1406
hoelzl@47694
  1407
lemma (in information_space) mutual_information_nonneg_simple:
hoelzl@47694
  1408
  assumes sf_X: "simple_function M X" and sf_Y: "simple_function M Y"
hoelzl@47694
  1409
  shows  "0 \<le> \<I>(X ; Y)"
hoelzl@47694
  1410
proof -
hoelzl@47694
  1411
  have X: "simple_distributed M X (\<lambda>x. measure M (X -` {x} \<inter> space M))"
hoelzl@47694
  1412
    using sf_X by (rule simple_distributedI) auto
hoelzl@47694
  1413
  have Y: "simple_distributed M Y (\<lambda>x. measure M (Y -` {x} \<inter> space M))"
hoelzl@47694
  1414
    using sf_Y by (rule simple_distributedI) auto
hoelzl@47694
  1415
hoelzl@47694
  1416
  have sf_XY: "simple_function M (\<lambda>x. (X x, Y x))"
hoelzl@47694
  1417
    using sf_X sf_Y by (rule simple_function_Pair)
hoelzl@47694
  1418
  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
  1419
    by (rule simple_distributedI) auto
hoelzl@47694
  1420
hoelzl@47694
  1421
  from simple_distributed_joint_finite[OF this, simp]
hoelzl@47694
  1422
  have eq: "count_space (X ` space M) \<Otimes>\<^isub>M count_space (Y ` space M) = count_space (X ` space M \<times> Y ` space M)"
hoelzl@47694
  1423
    by (simp add: pair_measure_count_space)
hoelzl@47694
  1424
hoelzl@40859
  1425
  show ?thesis
hoelzl@47694
  1426
    by (rule mutual_information_nonneg[OF _ _ simple_distributed[OF X] simple_distributed[OF Y] simple_distributed_joint[OF XY]])
hoelzl@47694
  1427
       (simp_all add: eq integrable_count_space sigma_finite_measure_count_space_finite)
hoelzl@40859
  1428
qed
hoelzl@36080
  1429
hoelzl@40859
  1430
lemma (in information_space) conditional_entropy_less_eq_entropy:
hoelzl@41689
  1431
  assumes X: "simple_function M X" and Z: "simple_function M Z"
hoelzl@40859
  1432
  shows "\<H>(X | Z) \<le> \<H>(X)"
hoelzl@36624
  1433
proof -
hoelzl@47694
  1434
  have "0 \<le> \<I>(X ; Z)" using X Z by (rule mutual_information_nonneg_simple)
hoelzl@47694
  1435
  also have "\<I>(X ; Z) = \<H>(X) - \<H>(X | Z)" using mutual_information_eq_entropy_conditional_entropy[OF assms] .
hoelzl@47694
  1436
  finally show ?thesis by auto
hoelzl@36080
  1437
qed
hoelzl@36080
  1438
hoelzl@40859
  1439
lemma (in information_space) entropy_chain_rule:
hoelzl@41689
  1440
  assumes X: "simple_function M X" and Y: "simple_function M Y"
hoelzl@40859
  1441
  shows  "\<H>(\<lambda>x. (X x, Y x)) = \<H>(X) + \<H>(Y|X)"
hoelzl@40859
  1442
proof -
hoelzl@47694
  1443
  note XY = simple_distributedI[OF simple_function_Pair[OF X Y] refl]
hoelzl@47694
  1444
  note YX = simple_distributedI[OF simple_function_Pair[OF Y X] refl]
hoelzl@47694
  1445
  note simple_distributed_joint_finite[OF this, simp]
hoelzl@47694
  1446
  let ?f = "\<lambda>x. prob ((\<lambda>x. (X x, Y x)) -` {x} \<inter> space M)"
hoelzl@47694
  1447
  let ?g = "\<lambda>x. prob ((\<lambda>x. (Y x, X x)) -` {x} \<inter> space M)"
hoelzl@47694
  1448
  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
  1449
  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
  1450
    using XY by (rule entropy_simple_distributed)
hoelzl@47694
  1451
  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))"
hoelzl@47694
  1452
    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
  1453
  also have "\<dots> = - (\<Sum>x\<in>(\<lambda>x. (Y x, X x)) ` space M. ?h x * log b (?h x))"
hoelzl@47694
  1454
    by (auto intro!: setsum_cong)
hoelzl@47694
  1455
  also have "\<dots> = entropy b (count_space (Y ` space M) \<Otimes>\<^isub>M count_space (X ` space M)) (\<lambda>x. (Y x, X x))"
hoelzl@49786
  1456
    by (subst entropy_distr[OF simple_distributed_joint[OF YX]])
hoelzl@47694
  1457
       (auto simp: pair_measure_count_space sigma_finite_measure_count_space_finite lebesgue_integral_count_space_finite
hoelzl@47694
  1458
             cong del: setsum_cong  intro!: setsum_mono_zero_left)
hoelzl@47694
  1459
  finally have "\<H>(\<lambda>x. (X x, Y x)) = entropy b (count_space (Y ` space M) \<Otimes>\<^isub>M count_space (X ` space M)) (\<lambda>x. (Y x, X x))" .
hoelzl@47694
  1460
  then show ?thesis
hoelzl@49791
  1461
    unfolding conditional_entropy_eq_entropy_simple[OF Y X] by simp
hoelzl@36624
  1462
qed
hoelzl@36624
  1463
hoelzl@40859
  1464
lemma (in information_space) entropy_partition:
hoelzl@47694
  1465
  assumes X: "simple_function M X"
hoelzl@47694
  1466
  shows "\<H>(X) = \<H>(f \<circ> X) + \<H>(X|f \<circ> X)"
hoelzl@36624
  1467
proof -
hoelzl@47694
  1468
  note fX = simple_function_compose[OF X, of f]  
hoelzl@47694
  1469
  have eq: "(\<lambda>x. ((f \<circ> X) x, X x)) ` space M = (\<lambda>x. (f x, x)) ` X ` space M" by auto
hoelzl@47694
  1470
  have inj: "\<And>A. inj_on (\<lambda>x. (f x, x)) A"
hoelzl@47694
  1471
    by (auto simp: inj_on_def)
hoelzl@47694
  1472
  show ?thesis
hoelzl@47694
  1473
    apply (subst entropy_chain_rule[symmetric, OF fX X])
hoelzl@47694
  1474
    apply (subst entropy_simple_distributed[OF simple_distributedI[OF simple_function_Pair[OF fX X] refl]])
hoelzl@47694
  1475
    apply (subst entropy_simple_distributed[OF simple_distributedI[OF X refl]])
hoelzl@47694
  1476
    unfolding eq
hoelzl@47694
  1477
    apply (subst setsum_reindex[OF inj])
hoelzl@47694
  1478
    apply (auto intro!: setsum_cong arg_cong[where f="\<lambda>A. prob A * log b (prob A)"])
hoelzl@47694
  1479
    done
hoelzl@36624
  1480
qed
hoelzl@36624
  1481
hoelzl@40859
  1482
corollary (in information_space) entropy_data_processing:
hoelzl@41689
  1483
  assumes X: "simple_function M X" shows "\<H>(f \<circ> X) \<le> \<H>(X)"
hoelzl@40859
  1484
proof -
hoelzl@47694
  1485
  note fX = simple_function_compose[OF X, of f]
hoelzl@47694
  1486
  from X have "\<H>(X) = \<H>(f\<circ>X) + \<H>(X|f\<circ>X)" by (rule entropy_partition)
hoelzl@40859
  1487
  then show "\<H>(f \<circ> X) \<le> \<H>(X)"
hoelzl@47694
  1488
    by (auto intro: conditional_entropy_nonneg[OF X fX])
hoelzl@40859
  1489
qed
hoelzl@36624
  1490
hoelzl@40859
  1491
corollary (in information_space) entropy_of_inj:
hoelzl@41689
  1492
  assumes X: "simple_function M X" and inj: "inj_on f (X`space M)"
hoelzl@36624
  1493
  shows "\<H>(f \<circ> X) = \<H>(X)"
hoelzl@36624
  1494
proof (rule antisym)
hoelzl@40859
  1495
  show "\<H>(f \<circ> X) \<le> \<H>(X)" using entropy_data_processing[OF X] .
hoelzl@36624
  1496
next
hoelzl@41689
  1497
  have sf: "simple_function M (f \<circ> X)"
hoelzl@40859
  1498
    using X by auto
hoelzl@36624
  1499
  have "\<H>(X) = \<H>(the_inv_into (X`space M) f \<circ> (f \<circ> X))"
hoelzl@47694
  1500
    unfolding o_assoc
hoelzl@47694
  1501
    apply (subst entropy_simple_distributed[OF simple_distributedI[OF X refl]])
hoelzl@47694
  1502
    apply (subst entropy_simple_distributed[OF simple_distributedI[OF simple_function_compose[OF X]], where f="\<lambda>x. prob (X -` {x} \<inter> space M)"])
hoelzl@47694
  1503
    apply (auto intro!: setsum_cong arg_cong[where f=prob] image_eqI simp: the_inv_into_f_f[OF inj] comp_def)
hoelzl@47694
  1504
    done
hoelzl@36624
  1505
  also have "... \<le> \<H>(f \<circ> X)"
hoelzl@40859
  1506
    using entropy_data_processing[OF sf] .
hoelzl@36624
  1507
  finally show "\<H>(X) \<le> \<H>(f \<circ> X)" .
hoelzl@36624
  1508
qed
hoelzl@36624
  1509
hoelzl@36080
  1510
end