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