src/HOL/Probability/Information.thy
author hoelzl
Wed, 02 Feb 2011 12:34:45 +0100
changeset 41689 3e39b0e730d6
parent 41661 baf1964bc468
child 41833 563bea92b2c0
permissions -rw-r--r--
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; changed syntax for simple_function, simple_integral, positive_integral, integral and RN_deriv. introduced binder variants for simple_integral, positive_integral and integral.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
     1
theory Information
41413
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 41095
diff changeset
     2
imports
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 41095
diff changeset
     3
  Probability_Space
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 41095
diff changeset
     4
  "~~/src/HOL/Library/Convex"
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 41095
diff changeset
     5
  Lebesgue_Measure
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
     6
begin
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
     7
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
     8
lemma log_le: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> x \<le> y \<Longrightarrow> log a x \<le> log a y"
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
     9
  by (subst log_le_cancel_iff) auto
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
    10
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
    11
lemma log_less: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> x < y \<Longrightarrow> log a x < log a y"
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
    12
  by (subst log_less_cancel_iff) auto
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
    13
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
    14
lemma setsum_cartesian_product':
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
    15
  "(\<Sum>x\<in>A \<times> B. f x) = (\<Sum>x\<in>A. setsum (\<lambda>y. f (x, y)) B)"
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
    16
  unfolding setsum_cartesian_product by simp
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
    17
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    18
section "Convex theory"
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    19
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    20
lemma log_setsum:
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    21
  assumes "finite s" "s \<noteq> {}"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    22
  assumes "b > 1"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    23
  assumes "(\<Sum> i \<in> s. a i) = 1"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    24
  assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<ge> 0"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    25
  assumes "\<And> i. i \<in> s \<Longrightarrow> y i \<in> {0 <..}"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    26
  shows "log b (\<Sum> i \<in> s. a i * y i) \<ge> (\<Sum> i \<in> s. a i * log b (y i))"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    27
proof -
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    28
  have "convex_on {0 <..} (\<lambda> x. - log b x)"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    29
    by (rule minus_log_convex[OF `b > 1`])
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    30
  hence "- log b (\<Sum> i \<in> s. a i * y i) \<le> (\<Sum> i \<in> s. a i * - log b (y i))"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    31
    using convex_on_setsum[of _ _ "\<lambda> x. - log b x"] assms pos_is_convex by fastsimp
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    32
  thus ?thesis by (auto simp add:setsum_negf le_imp_neg_le)
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    33
qed
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    34
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    35
lemma log_setsum':
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    36
  assumes "finite s" "s \<noteq> {}"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    37
  assumes "b > 1"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    38
  assumes "(\<Sum> i \<in> s. a i) = 1"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    39
  assumes pos: "\<And> i. i \<in> s \<Longrightarrow> 0 \<le> a i"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    40
          "\<And> i. \<lbrakk> i \<in> s ; 0 < a i \<rbrakk> \<Longrightarrow> 0 < y i"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    41
  shows "log b (\<Sum> i \<in> s. a i * y i) \<ge> (\<Sum> i \<in> s. a i * log b (y i))"
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    42
proof -
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    43
  have "\<And>y. (\<Sum> i \<in> s - {i. a i = 0}. a i * y i) = (\<Sum> i \<in> s. a i * y i)"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    44
    using assms by (auto intro!: setsum_mono_zero_cong_left)
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    45
  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))"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    46
  proof (rule log_setsum)
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    47
    have "setsum a (s - {i. a i = 0}) = setsum a s"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    48
      using assms(1) by (rule setsum_mono_zero_cong_left) auto
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    49
    thus sum_1: "setsum a (s - {i. a i = 0}) = 1"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    50
      "finite (s - {i. a i = 0})" using assms by simp_all
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    51
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    52
    show "s - {i. a i = 0} \<noteq> {}"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    53
    proof
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    54
      assume *: "s - {i. a i = 0} = {}"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    55
      hence "setsum a (s - {i. a i = 0}) = 0" by (simp add: * setsum_empty)
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    56
      with sum_1 show False by simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    57
    qed
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    58
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    59
    fix i assume "i \<in> s - {i. a i = 0}"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    60
    hence "i \<in> s" "a i \<noteq> 0" by simp_all
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    61
    thus "0 \<le> a i" "y i \<in> {0<..}" using pos[of i] by auto
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    62
  qed fact+
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    63
  ultimately show ?thesis by simp
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    64
qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    65
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    66
lemma log_setsum_divide:
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    67
  assumes "finite S" and "S \<noteq> {}" and "1 < b"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    68
  assumes "(\<Sum>x\<in>S. g x) = 1"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    69
  assumes pos: "\<And>x. x \<in> S \<Longrightarrow> g x \<ge> 0" "\<And>x. x \<in> S \<Longrightarrow> f x \<ge> 0"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    70
  assumes g_pos: "\<And>x. \<lbrakk> x \<in> S ; 0 < g x \<rbrakk> \<Longrightarrow> 0 < f x"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    71
  shows "- (\<Sum>x\<in>S. g x * log b (g x / f x)) \<le> log b (\<Sum>x\<in>S. f x)"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    72
proof -
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    73
  have log_mono: "\<And>x y. 0 < x \<Longrightarrow> x \<le> y \<Longrightarrow> log b x \<le> log b y"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    74
    using `1 < b` by (subst log_le_cancel_iff) auto
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    75
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    76
  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))"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    77
  proof (unfold setsum_negf[symmetric], rule setsum_cong)
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    78
    fix x assume x: "x \<in> S"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    79
    show "- (g x * log b (g x / f x)) = g x * log b (f x / g x)"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    80
    proof (cases "g x = 0")
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    81
      case False
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    82
      with pos[OF x] g_pos[OF x] have "0 < f x" "0 < g x" by simp_all
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    83
      thus ?thesis using `1 < b` by (simp add: log_divide field_simps)
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    84
    qed simp
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    85
  qed rule
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    86
  also have "... \<le> log b (\<Sum>x\<in>S. g x * (f x / g x))"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    87
  proof (rule log_setsum')
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    88
    fix x assume x: "x \<in> S" "0 < g x"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    89
    with g_pos[OF x] show "0 < f x / g x" by (safe intro!: divide_pos_pos)
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    90
  qed fact+
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    91
  also have "... = log b (\<Sum>x\<in>S - {x. g x = 0}. f x)" using `finite S`
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    92
    by (auto intro!: setsum_mono_zero_cong_right arg_cong[where f="log b"]
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    93
        split: split_if_asm)
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    94
  also have "... \<le> log b (\<Sum>x\<in>S. f x)"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    95
  proof (rule log_mono)
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    96
    have "0 = (\<Sum>x\<in>S - {x. g x = 0}. 0)" by simp
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    97
    also have "... < (\<Sum>x\<in>S - {x. g x = 0}. f x)" (is "_ < ?sum")
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    98
    proof (rule setsum_strict_mono)
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    99
      show "finite (S - {x. g x = 0})" using `finite S` by simp
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   100
      show "S - {x. g x = 0} \<noteq> {}"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   101
      proof
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   102
        assume "S - {x. g x = 0} = {}"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   103
        hence "(\<Sum>x\<in>S. g x) = 0" by (subst setsum_0') auto
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   104
        with `(\<Sum>x\<in>S. g x) = 1` show False by simp
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   105
      qed
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   106
      fix x assume "x \<in> S - {x. g x = 0}"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   107
      thus "0 < f x" using g_pos[of x] pos(1)[of x] by auto
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   108
    qed
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   109
    finally show "0 < ?sum" .
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   110
    show "(\<Sum>x\<in>S - {x. g x = 0}. f x) \<le> (\<Sum>x\<in>S. f x)"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   111
      using `finite S` pos by (auto intro!: setsum_mono2)
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   112
  qed
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   113
  finally show ?thesis .
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   114
qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   115
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   116
lemma split_pairs:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   117
  "((A, B) = X) \<longleftrightarrow> (fst X = A \<and> snd X = B)" and
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   118
  "(X = (A, B)) \<longleftrightarrow> (fst X = A \<and> snd X = B)" by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   119
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   120
section "Information theory"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   121
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   122
locale information_space = prob_space +
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   123
  fixes b :: real assumes b_gt_1: "1 < b"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   124
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   125
context information_space
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   126
begin
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   127
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   128
text {* Introduce some simplification rules for logarithm of base @{term b}. *}
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   129
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   130
lemma log_neg_const:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   131
  assumes "x \<le> 0"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   132
  shows "log b x = log b 0"
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   133
proof -
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   134
  { fix u :: real
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   135
    have "x \<le> 0" by fact
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   136
    also have "0 < exp u"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   137
      using exp_gt_zero .
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   138
    finally have "exp u \<noteq> x"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   139
      by auto }
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   140
  then show "log b x = log b 0"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   141
    by (simp add: log_def ln_def)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   142
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   143
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   144
lemma log_mult_eq:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   145
  "log b (A * B) = (if 0 < A * B then log b \<bar>A\<bar> + log b \<bar>B\<bar> else log b 0)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   146
  using log_mult[of b "\<bar>A\<bar>" "\<bar>B\<bar>"] b_gt_1 log_neg_const[of "A * B"]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   147
  by (auto simp: zero_less_mult_iff mult_le_0_iff)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   148
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   149
lemma log_inverse_eq:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   150
  "log b (inverse B) = (if 0 < B then - log b B else log b 0)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   151
  using log_inverse[of b B] log_neg_const[of "inverse B"] b_gt_1 by simp
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   152
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   153
lemma log_divide_eq:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   154
  "log b (A / B) = (if 0 < A * B then log b \<bar>A\<bar> - log b \<bar>B\<bar> else log b 0)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   155
  unfolding divide_inverse log_mult_eq log_inverse_eq abs_inverse
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   156
  by (auto simp: zero_less_mult_iff mult_le_0_iff)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   157
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   158
lemmas log_simps = log_mult_eq log_inverse_eq log_divide_eq
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   159
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   160
end
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   161
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   162
subsection "Kullback$-$Leibler divergence"
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   163
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   164
text {* The Kullback$-$Leibler divergence is also known as relative entropy or
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   165
Kullback$-$Leibler distance. *}
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   166
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   167
definition
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   168
  "KL_divergence b M \<nu> = \<integral>x. log b (real (RN_deriv M \<nu> x)) \<partial>M\<lparr>measure := \<nu>\<rparr>"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   169
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   170
lemma (in sigma_finite_measure) KL_divergence_cong:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   171
  assumes "measure_space (M\<lparr>measure := \<nu>\<rparr>)" (is "measure_space ?\<nu>")
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   172
  assumes [simp]: "sets N = sets M" "space N = space M"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   173
    "\<And>A. A \<in> sets M \<Longrightarrow> measure N A = \<mu> A"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   174
    "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = \<nu>' A"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   175
  shows "KL_divergence b M \<nu> = KL_divergence b N \<nu>'"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   176
proof -
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   177
  interpret \<nu>: measure_space ?\<nu> by fact
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   178
  have "KL_divergence b M \<nu> = \<integral>x. log b (real (RN_deriv N \<nu>' x)) \<partial>?\<nu>"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   179
    by (simp cong: RN_deriv_cong \<nu>.integral_cong add: KL_divergence_def)
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   180
  also have "\<dots> = KL_divergence b N \<nu>'"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   181
    by (auto intro!: \<nu>.integral_cong_measure[symmetric] simp: KL_divergence_def)
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   182
  finally show ?thesis .
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   183
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   184
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   185
lemma (in finite_measure_space) KL_divergence_eq_finite:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   186
  assumes v: "finite_measure_space (M\<lparr>measure := \<nu>\<rparr>)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   187
  assumes ac: "absolutely_continuous \<nu>"
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   188
  shows "KL_divergence b M \<nu> = (\<Sum>x\<in>space M. real (\<nu> {x}) * log b (real (\<nu> {x}) / real (\<mu> {x})))" (is "_ = ?sum")
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   189
proof (simp add: KL_divergence_def finite_measure_space.integral_finite_singleton[OF v])
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   190
  interpret v: finite_measure_space "M\<lparr>measure := \<nu>\<rparr>" by fact
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   191
  have ms: "measure_space (M\<lparr>measure := \<nu>\<rparr>)" by default
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   192
  show "(\<Sum>x \<in> space M. log b (real (RN_deriv M \<nu> x)) * real (\<nu> {x})) = ?sum"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   193
    using RN_deriv_finite_measure[OF ms ac]
41023
9118eb4eb8dc it is known as the extended reals, not the infinite reals
hoelzl
parents: 40859
diff changeset
   194
    by (auto intro!: setsum_cong simp: field_simps real_of_pextreal_mult[symmetric])
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   195
qed
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   196
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   197
lemma (in finite_prob_space) KL_divergence_positive_finite:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   198
  assumes v: "finite_prob_space (M\<lparr>measure := \<nu>\<rparr>)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   199
  assumes ac: "absolutely_continuous \<nu>"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   200
  and "1 < b"
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   201
  shows "0 \<le> KL_divergence b M \<nu>"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   202
proof -
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   203
  interpret v: finite_prob_space "M\<lparr>measure := \<nu>\<rparr>" by fact
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   204
  have ms: "finite_measure_space (M\<lparr>measure := \<nu>\<rparr>)" by default
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   205
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   206
  have "- (KL_divergence b M \<nu>) \<le> log b (\<Sum>x\<in>space M. real (\<mu> {x}))"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   207
  proof (subst KL_divergence_eq_finite[OF ms ac], safe intro!: log_setsum_divide not_empty)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   208
    show "finite (space M)" using finite_space by simp
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   209
    show "1 < b" by fact
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   210
    show "(\<Sum>x\<in>space M. real (\<nu> {x})) = 1" using v.finite_sum_over_space_eq_1 by simp
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   211
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   212
    fix x assume "x \<in> space M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   213
    then have x: "{x} \<in> sets M" unfolding sets_eq_Pow by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   214
    { assume "0 < real (\<nu> {x})"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   215
      then have "\<nu> {x} \<noteq> 0" by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   216
      then have "\<mu> {x} \<noteq> 0"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   217
        using ac[unfolded absolutely_continuous_def, THEN bspec, of "{x}"] x by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   218
      thus "0 < prob {x}" using finite_measure[of "{x}"] x by auto }
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   219
  qed auto
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   220
  thus "0 \<le> KL_divergence b M \<nu>" using finite_sum_over_space_eq_1 by simp
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   221
qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   222
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   223
subsection {* Mutual Information *}
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   224
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   225
definition (in prob_space)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   226
  "mutual_information b S T X Y =
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   227
    KL_divergence b (S\<lparr>measure := distribution X\<rparr> \<Otimes>\<^isub>M T\<lparr>measure := distribution Y\<rparr>)
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   228
      (joint_distribution X Y)"
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   229
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   230
definition (in prob_space)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   231
  "entropy b s X = mutual_information b s s X X"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   232
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   233
abbreviation (in information_space)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   234
  mutual_information_Pow ("\<I>'(_ ; _')") where
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   235
  "\<I>(X ; Y) \<equiv> mutual_information b
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   236
    \<lparr> space = X`space M, sets = Pow (X`space M), measure = distribution X \<rparr>
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   237
    \<lparr> space = Y`space M, sets = Pow (Y`space M), measure = distribution Y \<rparr> X Y"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   238
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   239
lemma algebra_measure_update[simp]:
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   240
  "algebra (M'\<lparr>measure := m\<rparr>) \<longleftrightarrow> algebra M'"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   241
  unfolding algebra_def by simp
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   242
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   243
lemma sigma_algebra_measure_update[simp]:
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   244
  "sigma_algebra (M'\<lparr>measure := m\<rparr>) \<longleftrightarrow> sigma_algebra M'"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   245
  unfolding sigma_algebra_def sigma_algebra_axioms_def by simp
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   246
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   247
lemma finite_sigma_algebra_measure_update[simp]:
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   248
  "finite_sigma_algebra (M'\<lparr>measure := m\<rparr>) \<longleftrightarrow> finite_sigma_algebra M'"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   249
  unfolding finite_sigma_algebra_def finite_sigma_algebra_axioms_def by simp
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   250
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   251
lemma (in prob_space) finite_variables_absolutely_continuous:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   252
  assumes X: "finite_random_variable S X" and Y: "finite_random_variable T Y"
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   253
  shows "measure_space.absolutely_continuous
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   254
    (S\<lparr>measure := distribution X\<rparr> \<Otimes>\<^isub>M T\<lparr>measure := distribution Y\<rparr>)
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   255
    (joint_distribution X Y)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   256
proof -
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   257
  interpret X: finite_prob_space "S\<lparr>measure := distribution X\<rparr>"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   258
    using X by (rule distribution_finite_prob_space)
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   259
  interpret Y: finite_prob_space "T\<lparr>measure := distribution Y\<rparr>"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   260
    using Y by (rule distribution_finite_prob_space)
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   261
  interpret XY: pair_finite_prob_space
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   262
    "S\<lparr>measure := distribution X\<rparr>" "T\<lparr> measure := distribution Y\<rparr>" by default
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   263
  interpret P: finite_prob_space "XY.P\<lparr> measure := joint_distribution X Y\<rparr>"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   264
    using assms by (auto intro!: joint_distribution_finite_prob_space)
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   265
  note rv = assms[THEN finite_random_variableD]
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   266
  show "XY.absolutely_continuous (joint_distribution X Y)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   267
  proof (rule XY.absolutely_continuousI)
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   268
    show "finite_measure_space (XY.P\<lparr> measure := joint_distribution X Y\<rparr>)" by default
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   269
    fix x assume "x \<in> space XY.P" and "XY.\<mu> {x} = 0"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   270
    then obtain a b where "(a, b) = x" and "a \<in> space S" "b \<in> space T"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   271
      and distr: "distribution X {a} * distribution Y {b} = 0"
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   272
      by (cases x) (auto simp: space_pair_measure)
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   273
    with X.sets_eq_Pow Y.sets_eq_Pow
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   274
      joint_distribution_Times_le_fst[OF rv, of "{a}" "{b}"]
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   275
      joint_distribution_Times_le_snd[OF rv, of "{a}" "{b}"]
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   276
    have "joint_distribution X Y {x} \<le> distribution Y {b}"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   277
         "joint_distribution X Y {x} \<le> distribution X {a}"
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   278
      by (auto simp del: X.sets_eq_Pow Y.sets_eq_Pow)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   279
    with distr show "joint_distribution X Y {x} = 0" by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   280
  qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   281
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   282
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   283
lemma (in information_space)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   284
  assumes MX: "finite_random_variable MX X"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   285
  assumes MY: "finite_random_variable MY Y"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   286
  shows mutual_information_generic_eq:
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   287
    "mutual_information b MX MY X Y = (\<Sum> (x,y) \<in> space MX \<times> space MY.
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   288
      real (joint_distribution X Y {(x,y)}) *
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   289
      log b (real (joint_distribution X Y {(x,y)}) /
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   290
      (real (distribution X {x}) * real (distribution Y {y}))))"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   291
    (is ?sum)
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   292
  and mutual_information_positive_generic:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   293
     "0 \<le> mutual_information b MX MY X Y" (is ?positive)
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   294
proof -
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   295
  interpret X: finite_prob_space "MX\<lparr>measure := distribution X\<rparr>"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   296
    using MX by (rule distribution_finite_prob_space)
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   297
  interpret Y: finite_prob_space "MY\<lparr>measure := distribution Y\<rparr>"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   298
    using MY by (rule distribution_finite_prob_space)
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   299
  interpret XY: pair_finite_prob_space "MX\<lparr>measure := distribution X\<rparr>" "MY\<lparr>measure := distribution Y\<rparr>" by default
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   300
  interpret P: finite_prob_space "XY.P\<lparr>measure := joint_distribution X Y\<rparr>"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   301
    using assms by (auto intro!: joint_distribution_finite_prob_space)
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   302
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   303
  have P_ms: "finite_measure_space (XY.P\<lparr>measure :=joint_distribution X Y\<rparr>)" by default
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   304
  have P_ps: "finite_prob_space (XY.P\<lparr>measure := joint_distribution X Y\<rparr>)" by default
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   305
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   306
  show ?sum
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   307
    unfolding Let_def mutual_information_def
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   308
    by (subst XY.KL_divergence_eq_finite[OF P_ms finite_variables_absolutely_continuous[OF MX MY]])
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   309
       (auto simp add: space_pair_measure setsum_cartesian_product' real_of_pextreal_mult[symmetric])
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   310
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   311
  show ?positive
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   312
    using XY.KL_divergence_positive_finite[OF P_ps finite_variables_absolutely_continuous[OF MX MY] b_gt_1]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   313
    unfolding mutual_information_def .
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   314
qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   315
41661
baf1964bc468 use pre-image measure, instead of image
hoelzl
parents: 41413
diff changeset
   316
lemma (in information_space) mutual_information_commute:
baf1964bc468 use pre-image measure, instead of image
hoelzl
parents: 41413
diff changeset
   317
  assumes X: "finite_random_variable S X" and Y: "finite_random_variable T Y"
baf1964bc468 use pre-image measure, instead of image
hoelzl
parents: 41413
diff changeset
   318
  shows "mutual_information b S T X Y = mutual_information b T S Y X"
baf1964bc468 use pre-image measure, instead of image
hoelzl
parents: 41413
diff changeset
   319
  unfolding mutual_information_generic_eq[OF X Y] mutual_information_generic_eq[OF Y X]
baf1964bc468 use pre-image measure, instead of image
hoelzl
parents: 41413
diff changeset
   320
  unfolding joint_distribution_commute_singleton[of X Y]
baf1964bc468 use pre-image measure, instead of image
hoelzl
parents: 41413
diff changeset
   321
  by (auto simp add: ac_simps intro!: setsum_reindex_cong[OF swap_inj_on])
baf1964bc468 use pre-image measure, instead of image
hoelzl
parents: 41413
diff changeset
   322
baf1964bc468 use pre-image measure, instead of image
hoelzl
parents: 41413
diff changeset
   323
lemma (in information_space) mutual_information_commute_simple:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   324
  assumes X: "simple_function M X" and Y: "simple_function M Y"
41661
baf1964bc468 use pre-image measure, instead of image
hoelzl
parents: 41413
diff changeset
   325
  shows "\<I>(X;Y) = \<I>(Y;X)"
baf1964bc468 use pre-image measure, instead of image
hoelzl
parents: 41413
diff changeset
   326
  by (intro X Y simple_function_imp_finite_random_variable mutual_information_commute)
baf1964bc468 use pre-image measure, instead of image
hoelzl
parents: 41413
diff changeset
   327
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   328
lemma (in information_space) mutual_information_eq:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   329
  assumes "simple_function M X" "simple_function M Y"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   330
  shows "\<I>(X;Y) = (\<Sum> (x,y) \<in> X ` space M \<times> Y ` space M.
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   331
    real (distribution (\<lambda>x. (X x, Y x)) {(x,y)}) * log b (real (distribution (\<lambda>x. (X x, Y x)) {(x,y)}) /
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   332
                                                   (real (distribution X {x}) * real (distribution Y {y}))))"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   333
  using assms by (simp add: mutual_information_generic_eq)
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   334
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   335
lemma (in information_space) mutual_information_generic_cong:
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   336
  assumes X: "\<And>x. x \<in> space M \<Longrightarrow> X x = X' x"
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   337
  assumes Y: "\<And>x. x \<in> space M \<Longrightarrow> Y x = Y' x"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   338
  shows "mutual_information b MX MY X Y = mutual_information b MX MY X' Y'"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   339
  unfolding mutual_information_def using X Y
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   340
  by (simp cong: distribution_cong)
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   341
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   342
lemma (in information_space) mutual_information_cong:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   343
  assumes X: "\<And>x. x \<in> space M \<Longrightarrow> X x = X' x"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   344
  assumes Y: "\<And>x. x \<in> space M \<Longrightarrow> Y x = Y' x"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   345
  shows "\<I>(X; Y) = \<I>(X'; Y')"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   346
  unfolding mutual_information_def using X Y
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   347
  by (simp cong: distribution_cong image_cong)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   348
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   349
lemma (in information_space) mutual_information_positive:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   350
  assumes "simple_function M X" "simple_function M Y"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   351
  shows "0 \<le> \<I>(X;Y)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   352
  using assms by (simp add: mutual_information_positive_generic)
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   353
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   354
subsection {* Entropy *}
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   355
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   356
abbreviation (in information_space)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   357
  entropy_Pow ("\<H>'(_')") where
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   358
  "\<H>(X) \<equiv> entropy b \<lparr> space = X`space M, sets = Pow (X`space M), measure = distribution X \<rparr> X"
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   359
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   360
lemma (in information_space) entropy_generic_eq:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   361
  assumes MX: "finite_random_variable MX X"
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   362
  shows "entropy b MX X = -(\<Sum> x \<in> space MX. real (distribution X {x}) * log b (real (distribution X {x})))"
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   363
proof -
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   364
  interpret MX: finite_prob_space "MX\<lparr>measure := distribution X\<rparr>"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   365
    using MX by (rule distribution_finite_prob_space)
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   366
  let "?X x" = "real (distribution X {x})"
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   367
  let "?XX x y" = "real (joint_distribution X X {(x, y)})"
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   368
  { fix x y
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   369
    have "(\<lambda>x. (X x, X x)) -` {(x, y)} = (if x = y then X -` {x} else {})" by auto
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   370
    then have "?XX x y * log b (?XX x y / (?X x * ?X y)) =
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   371
        (if x = y then - ?X y * log b (?X y) else 0)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   372
      unfolding distribution_def by (auto simp: log_simps zero_less_mult_iff) }
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   373
  note remove_XX = this
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   374
  show ?thesis
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   375
    unfolding entropy_def mutual_information_generic_eq[OF MX MX]
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   376
    unfolding setsum_cartesian_product[symmetric] setsum_negf[symmetric] remove_XX
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   377
    using MX.finite_space by (auto simp: setsum_cases)
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   378
qed
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   379
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   380
lemma (in information_space) entropy_eq:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   381
  assumes "simple_function M X"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   382
  shows "\<H>(X) = -(\<Sum> x \<in> X ` space M. real (distribution X {x}) * log b (real (distribution X {x})))"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   383
  using assms by (simp add: entropy_generic_eq)
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   384
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   385
lemma (in information_space) entropy_positive:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   386
  "simple_function M X \<Longrightarrow> 0 \<le> \<H>(X)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   387
  unfolding entropy_def by (simp add: mutual_information_positive)
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   388
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   389
lemma (in information_space) entropy_certainty_eq_0:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   390
  assumes "simple_function M X" and "x \<in> X ` space M" and "distribution X {x} = 1"
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   391
  shows "\<H>(X) = 0"
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   392
proof -
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   393
  let ?X = "\<lparr> space = X ` space M, sets = Pow (X ` space M), measure = distribution X\<rparr>"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   394
  note simple_function_imp_finite_random_variable[OF `simple_function M X`]
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   395
  from distribution_finite_prob_space[OF this, of "\<lparr> measure = distribution X \<rparr>"]
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   396
  interpret X: finite_prob_space ?X by simp
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   397
  have "distribution X (X ` space M - {x}) = distribution X (X ` space M) - distribution X {x}"
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   398
    using X.measure_compl[of "{x}"] assms by auto
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   399
  also have "\<dots> = 0" using X.prob_space assms by auto
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   400
  finally have X0: "distribution X (X ` space M - {x}) = 0" by auto
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   401
  { fix y assume asm: "y \<noteq> x" "y \<in> X ` space M"
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   402
    hence "{y} \<subseteq> X ` space M - {x}" by auto
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   403
    from X.measure_mono[OF this] X0 asm
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   404
    have "distribution X {y} = 0" by auto }
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   405
  hence fi: "\<And> y. y \<in> X ` space M \<Longrightarrow> real (distribution X {y}) = (if x = y then 1 else 0)"
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   406
    using assms by auto
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   407
  have y: "\<And>y. (if x = y then 1 else 0) * log b (if x = y then 1 else 0) = 0" by simp
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   408
  show ?thesis unfolding entropy_eq[OF `simple_function M X`] by (auto simp: y fi)
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   409
qed
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   410
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   411
lemma (in information_space) entropy_le_card_not_0:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   412
  assumes "simple_function M X"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   413
  shows "\<H>(X) \<le> log b (real (card (X ` space M \<inter> {x . distribution X {x} \<noteq> 0})))"
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   414
proof -
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   415
  let "?d x" = "distribution X {x}"
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   416
  let "?p x" = "real (?d x)"
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   417
  have "\<H>(X) = (\<Sum>x\<in>X`space M. ?p x * log b (1 / ?p x))"
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   418
    by (auto intro!: setsum_cong simp: entropy_eq[OF `simple_function M X`] setsum_negf[symmetric] log_simps not_less)
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   419
  also have "\<dots> \<le> log b (\<Sum>x\<in>X`space M. ?p x * (1 / ?p x))"
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   420
    apply (rule log_setsum')
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   421
    using not_empty b_gt_1 `simple_function M X` sum_over_space_real_distribution
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   422
    by (auto simp: simple_function_def)
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   423
  also have "\<dots> = log b (\<Sum>x\<in>X`space M. if ?d x \<noteq> 0 then 1 else 0)"
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   424
    using distribution_finite[OF `simple_function M X`[THEN simple_function_imp_random_variable], simplified]
41023
9118eb4eb8dc it is known as the extended reals, not the infinite reals
hoelzl
parents: 40859
diff changeset
   425
    by (intro arg_cong[where f="\<lambda>X. log b X"] setsum_cong) (auto simp: real_of_pextreal_eq_0)
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   426
  finally show ?thesis
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   427
    using `simple_function M X` by (auto simp: setsum_cases real_eq_of_nat simple_function_def)
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   428
qed
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   429
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   430
lemma (in information_space) entropy_uniform_max:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   431
  assumes "simple_function M X"
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   432
  assumes "\<And>x y. \<lbrakk> x \<in> X ` space M ; y \<in> X ` space M \<rbrakk> \<Longrightarrow> distribution X {x} = distribution X {y}"
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   433
  shows "\<H>(X) = log b (real (card (X ` space M)))"
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   434
proof -
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   435
  let ?X = "\<lparr> space = X ` space M, sets = Pow (X ` space M), measure = distribution X\<rparr>"
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   436
  note simple_function_imp_finite_random_variable[OF `simple_function M X`]
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   437
  from distribution_finite_prob_space[OF this, of "\<lparr> measure = distribution X \<rparr>"]
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   438
  interpret X: finite_prob_space ?X by simp
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   439
  have card_gt0: "0 < card (X ` space M)" unfolding card_gt_0_iff
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   440
    using `simple_function M X` not_empty by (auto simp: simple_function_def)
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   441
  { fix x assume "x \<in> X ` space M"
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   442
    hence "real (distribution X {x}) = 1 / real (card (X ` space M))"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   443
    proof (rule X.uniform_prob[simplified])
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   444
      fix x y assume "x \<in> X`space M" "y \<in> X`space M"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   445
      from assms(2)[OF this] show "real (distribution X {x}) = real (distribution X {y})" by simp
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   446
    qed }
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   447
  thus ?thesis
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   448
    using not_empty X.finite_space b_gt_1 card_gt0
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   449
    by (simp add: entropy_eq[OF `simple_function M X`] real_eq_of_nat[symmetric] log_simps)
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   450
qed
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   451
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   452
lemma (in information_space) entropy_le_card:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   453
  assumes "simple_function M X"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   454
  shows "\<H>(X) \<le> log b (real (card (X ` space M)))"
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   455
proof cases
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   456
  assume "X ` space M \<inter> {x. distribution X {x} \<noteq> 0} = {}"
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   457
  then have "\<And>x. x\<in>X`space M \<Longrightarrow> distribution X {x} = 0" by auto
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   458
  moreover
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   459
  have "0 < card (X`space M)"
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   460
    using `simple_function M X` not_empty
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   461
    by (auto simp: card_gt_0_iff simple_function_def)
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   462
  then have "log b 1 \<le> log b (real (card (X`space M)))"
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   463
    using b_gt_1 by (intro log_le) auto
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   464
  ultimately show ?thesis using assms by (simp add: entropy_eq)
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   465
next
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   466
  assume False: "X ` space M \<inter> {x. distribution X {x} \<noteq> 0} \<noteq> {}"
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   467
  have "card (X ` space M \<inter> {x. distribution X {x} \<noteq> 0}) \<le> card (X ` space M)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   468
    (is "?A \<le> ?B") using assms not_empty by (auto intro!: card_mono simp: simple_function_def)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   469
  note entropy_le_card_not_0[OF assms]
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   470
  also have "log b (real ?A) \<le> log b (real ?B)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   471
    using b_gt_1 False not_empty `?A \<le> ?B` assms
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   472
    by (auto intro!: log_le simp: card_gt_0_iff simp: simple_function_def)
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   473
  finally show ?thesis .
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   474
qed
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   475
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   476
lemma (in information_space) entropy_commute:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   477
  assumes "simple_function M X" "simple_function M Y"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   478
  shows "\<H>(\<lambda>x. (X x, Y x)) = \<H>(\<lambda>x. (Y x, X x))"
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   479
proof -
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   480
  have sf: "simple_function M (\<lambda>x. (X x, Y x))" "simple_function M (\<lambda>x. (Y x, X x))"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   481
    using assms by (auto intro: simple_function_Pair)
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   482
  have *: "(\<lambda>x. (Y x, X x))`space M = (\<lambda>(a,b). (b,a))`(\<lambda>x. (X x, Y x))`space M"
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   483
    by auto
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   484
  have inj: "\<And>X. inj_on (\<lambda>(a,b). (b,a)) X"
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   485
    by (auto intro!: inj_onI)
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   486
  show ?thesis
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   487
    unfolding sf[THEN entropy_eq] unfolding * setsum_reindex[OF inj]
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   488
    by (simp add: joint_distribution_commute[of Y X] split_beta)
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   489
qed
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   490
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   491
lemma (in information_space) entropy_eq_cartesian_product:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   492
  assumes "simple_function M X" "simple_function M Y"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   493
  shows "\<H>(\<lambda>x. (X x, Y x)) = -(\<Sum>x\<in>X`space M. \<Sum>y\<in>Y`space M.
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   494
    real (joint_distribution X Y {(x,y)}) *
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   495
    log b (real (joint_distribution X Y {(x,y)})))"
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   496
proof -
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   497
  have sf: "simple_function M (\<lambda>x. (X x, Y x))"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   498
    using assms by (auto intro: simple_function_Pair)
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   499
  { fix x assume "x\<notin>(\<lambda>x. (X x, Y x))`space M"
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   500
    then have "(\<lambda>x. (X x, Y x)) -` {x} \<inter> space M = {}" by auto
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   501
    then have "joint_distribution X Y {x} = 0"
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   502
      unfolding distribution_def by auto }
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   503
  then show ?thesis using sf assms
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   504
    unfolding entropy_eq[OF sf] neg_equal_iff_equal setsum_cartesian_product
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   505
    by (auto intro!: setsum_mono_zero_cong_left simp: simple_function_def)
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   506
qed
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   507
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   508
subsection {* Conditional Mutual Information *}
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   509
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   510
definition (in prob_space)
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   511
  "conditional_mutual_information b MX MY MZ X Y Z \<equiv>
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   512
    mutual_information b MX (MY \<Otimes>\<^isub>M MZ) X (\<lambda>x. (Y x, Z x)) -
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   513
    mutual_information b MX MZ X Z"
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   514
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   515
abbreviation (in information_space)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   516
  conditional_mutual_information_Pow ("\<I>'( _ ; _ | _ ')") where
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   517
  "\<I>(X ; Y | Z) \<equiv> conditional_mutual_information b
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   518
    \<lparr> space = X`space M, sets = Pow (X`space M), measure = distribution X \<rparr>
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   519
    \<lparr> space = Y`space M, sets = Pow (Y`space M), measure = distribution Y \<rparr>
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   520
    \<lparr> space = Z`space M, sets = Pow (Z`space M), measure = distribution Z \<rparr>
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   521
    X Y Z"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   522
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   523
lemma (in information_space) conditional_mutual_information_generic_eq:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   524
  assumes MX: "finite_random_variable MX X"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   525
    and MY: "finite_random_variable MY Y"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   526
    and MZ: "finite_random_variable MZ Z"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   527
  shows "conditional_mutual_information b MX MY MZ X Y Z = (\<Sum>(x, y, z) \<in> space MX \<times> space MY \<times> space MZ.
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   528
             real (distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)}) *
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   529
             log b (real (distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)}) /
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   530
    (real (joint_distribution X Z {(x, z)}) * real (joint_distribution Y Z {(y,z)} / distribution Z {z}))))"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   531
  (is "_ = (\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * log b (?XYZ x y z / (?XZ x z * ?YZdZ y z)))")
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   532
proof -
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   533
  let ?YZ = "\<lambda>y z. real (joint_distribution Y Z {(y, z)})"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   534
  let ?X = "\<lambda>x. real (distribution X {x})"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   535
  let ?Z = "\<lambda>z. real (distribution Z {z})"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   536
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   537
  txt {* This proof is actually quiet easy, however we need to show that the
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   538
    distributions are finite and the joint distributions are zero when one of
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   539
    the variables distribution is also zero. *}
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   540
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   541
  note finite_var = MX MY MZ
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   542
  note random_var = finite_var[THEN finite_random_variableD]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   543
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   544
  note space_simps = space_pair_measure space_sigma algebra.simps
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   545
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   546
  note YZ = finite_random_variable_pairI[OF finite_var(2,3)]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   547
  note XZ = finite_random_variable_pairI[OF finite_var(1,3)]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   548
  note ZX = finite_random_variable_pairI[OF finite_var(3,1)]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   549
  note YZX = finite_random_variable_pairI[OF finite_var(2) ZX]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   550
  note order1 =
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   551
    finite_distribution_order(5,6)[OF finite_var(1) YZ, simplified space_simps]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   552
    finite_distribution_order(5,6)[OF finite_var(1,3), simplified space_simps]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   553
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   554
  note finite = finite_var(1) YZ finite_var(3) XZ YZX
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   555
  note finite[THEN finite_distribution_finite, simplified space_simps, simp]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   556
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   557
  have order2: "\<And>x y z. \<lbrakk>x \<in> space MX; y \<in> space MY; z \<in> space MZ; joint_distribution X Z {(x, z)} = 0\<rbrakk>
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   558
          \<Longrightarrow> joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)} = 0"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   559
    unfolding joint_distribution_commute_singleton[of X]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   560
    unfolding joint_distribution_assoc_singleton[symmetric]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   561
    using finite_distribution_order(6)[OF finite_var(2) ZX]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   562
    by (auto simp: space_simps)
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   563
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   564
  have "(\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * log b (?XYZ x y z / (?XZ x z * ?YZdZ y z))) =
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   565
    (\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * (log b (?XYZ x y z / (?X x * ?YZ y z)) - log b (?XZ x z / (?X x * ?Z z))))"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   566
    (is "(\<Sum>(x, y, z)\<in>?S. ?L x y z) = (\<Sum>(x, y, z)\<in>?S. ?R x y z)")
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   567
  proof (safe intro!: setsum_cong)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   568
    fix x y z assume space: "x \<in> space MX" "y \<in> space MY" "z \<in> space MZ"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   569
    then have *: "?XYZ x y z / (?XZ x z * ?YZdZ y z) =
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   570
      (?XYZ x y z / (?X x * ?YZ y z)) / (?XZ x z / (?X x * ?Z z))"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   571
      using order1(3)
41023
9118eb4eb8dc it is known as the extended reals, not the infinite reals
hoelzl
parents: 40859
diff changeset
   572
      by (auto simp: real_of_pextreal_mult[symmetric] real_of_pextreal_eq_0)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   573
    show "?L x y z = ?R x y z"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   574
    proof cases
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   575
      assume "?XYZ x y z \<noteq> 0"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   576
      with space b_gt_1 order1 order2 show ?thesis unfolding *
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   577
        by (subst log_divide)
41023
9118eb4eb8dc it is known as the extended reals, not the infinite reals
hoelzl
parents: 40859
diff changeset
   578
           (auto simp: zero_less_divide_iff zero_less_real_of_pextreal
9118eb4eb8dc it is known as the extended reals, not the infinite reals
hoelzl
parents: 40859
diff changeset
   579
                       real_of_pextreal_eq_0 zero_less_mult_iff)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   580
    qed simp
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   581
  qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   582
  also have "\<dots> = (\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * log b (?XYZ x y z / (?X x * ?YZ y z))) -
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   583
                  (\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * log b (?XZ x z / (?X x * ?Z z)))"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   584
    by (auto simp add: setsum_subtractf[symmetric] field_simps intro!: setsum_cong)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   585
  also have "(\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * log b (?XZ x z / (?X x * ?Z z))) =
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   586
             (\<Sum>(x, z)\<in>space MX \<times> space MZ. ?XZ x z * log b (?XZ x z / (?X x * ?Z z)))"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   587
    unfolding setsum_cartesian_product[symmetric] setsum_commute[of _ _ "space MY"]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   588
              setsum_left_distrib[symmetric]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   589
    unfolding joint_distribution_commute_singleton[of X]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   590
    unfolding joint_distribution_assoc_singleton[symmetric]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   591
    using setsum_real_joint_distribution_singleton[OF finite_var(2) ZX, unfolded space_simps]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   592
    by (intro setsum_cong refl) simp
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   593
  also have "(\<Sum>(x, y, z)\<in>?S. ?XYZ x y z * log b (?XYZ x y z / (?X x * ?YZ y z))) -
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   594
             (\<Sum>(x, z)\<in>space MX \<times> space MZ. ?XZ x z * log b (?XZ x z / (?X x * ?Z z))) =
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   595
             conditional_mutual_information b MX MY MZ X Y Z"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   596
    unfolding conditional_mutual_information_def
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   597
    unfolding mutual_information_generic_eq[OF finite_var(1,3)]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   598
    unfolding mutual_information_generic_eq[OF finite_var(1) YZ]
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   599
    by (simp add: space_sigma space_pair_measure setsum_cartesian_product')
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   600
  finally show ?thesis by simp
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   601
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   602
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   603
lemma (in information_space) conditional_mutual_information_eq:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   604
  assumes "simple_function M X" "simple_function M Y" "simple_function M Z"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   605
  shows "\<I>(X;Y|Z) = (\<Sum>(x, y, z) \<in> X`space M \<times> Y`space M \<times> Z`space M.
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   606
             real (distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)}) *
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   607
             log b (real (distribution (\<lambda>x. (X x, Y x, Z x)) {(x, y, z)}) /
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   608
    (real (joint_distribution X Z {(x, z)}) * real (joint_distribution Y Z {(y,z)} / distribution Z {z}))))"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   609
  using conditional_mutual_information_generic_eq[OF assms[THEN simple_function_imp_finite_random_variable]]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   610
  by simp
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   611
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   612
lemma (in information_space) conditional_mutual_information_eq_mutual_information:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   613
  assumes X: "simple_function M X" and Y: "simple_function M Y"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   614
  shows "\<I>(X ; Y) = \<I>(X ; Y | (\<lambda>x. ()))"
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   615
proof -
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   616
  have [simp]: "(\<lambda>x. ()) ` space M = {()}" using not_empty by auto
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   617
  have C: "simple_function M (\<lambda>x. ())" by auto
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   618
  show ?thesis
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   619
    unfolding conditional_mutual_information_eq[OF X Y C]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   620
    unfolding mutual_information_eq[OF X Y]
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   621
    by (simp add: setsum_cartesian_product' distribution_remove_const)
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   622
qed
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   623
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   624
lemma (in prob_space) distribution_unit[simp]: "distribution (\<lambda>x. ()) {()} = 1"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   625
  unfolding distribution_def using measure_space_1 by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   626
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   627
lemma (in prob_space) joint_distribution_unit[simp]: "distribution (\<lambda>x. (X x, ())) {(a, ())} = distribution X {a}"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   628
  unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>])
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   629
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   630
lemma (in prob_space) setsum_distribution:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   631
  assumes X: "finite_random_variable MX X" shows "(\<Sum>a\<in>space MX. distribution X {a}) = 1"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   632
  using setsum_joint_distribution[OF assms, of "\<lparr> space = UNIV, sets = Pow UNIV \<rparr>" "\<lambda>x. ()" "{()}"]
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   633
  using sigma_algebra_Pow[of "UNIV::unit set" "()"] by simp
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   634
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   635
lemma (in prob_space) setsum_real_distribution:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   636
  fixes MX :: "('c, 'd) measure_space_scheme"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   637
  assumes X: "finite_random_variable MX X" shows "(\<Sum>a\<in>space MX. real (distribution X {a})) = 1"
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   638
  using setsum_real_joint_distribution[OF assms, of "\<lparr> space = UNIV, sets = Pow UNIV, measure = undefined \<rparr>" "\<lambda>x. ()" "{()}"]
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   639
  using sigma_algebra_Pow[of "UNIV::unit set" "\<lparr> measure = undefined \<rparr>"] by simp
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   640
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   641
lemma (in information_space) conditional_mutual_information_generic_positive:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   642
  assumes "finite_random_variable MX X" and "finite_random_variable MY Y" and "finite_random_variable MZ Z"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   643
  shows "0 \<le> conditional_mutual_information b MX MY MZ X Y Z"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   644
proof (cases "space MX \<times> space MY \<times> space MZ = {}")
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   645
  case True show ?thesis
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   646
    unfolding conditional_mutual_information_generic_eq[OF assms] True
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   647
    by simp
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   648
next
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   649
  case False
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   650
  let "?dXYZ A" = "real (distribution (\<lambda>x. (X x, Y x, Z x)) A)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   651
  let "?dXZ A" = "real (joint_distribution X Z A)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   652
  let "?dYZ A" = "real (joint_distribution Y Z A)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   653
  let "?dX A" = "real (distribution X A)"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   654
  let "?dZ A" = "real (distribution Z A)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   655
  let ?M = "space MX \<times> space MY \<times> space MZ"
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   656
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
   657
  have split_beta: "\<And>f. split f = (\<lambda>x. f (fst x) (snd x))" by (simp add: fun_eq_iff)
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   658
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   659
  note space_simps = space_pair_measure space_sigma algebra.simps
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   660
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   661
  note finite_var = assms
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   662
  note YZ = finite_random_variable_pairI[OF finite_var(2,3)]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   663
  note XZ = finite_random_variable_pairI[OF finite_var(1,3)]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   664
  note ZX = finite_random_variable_pairI[OF finite_var(3,1)]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   665
  note YZ = finite_random_variable_pairI[OF finite_var(2,3)]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   666
  note XYZ = finite_random_variable_pairI[OF finite_var(1) YZ]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   667
  note finite = finite_var(3) YZ XZ XYZ
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   668
  note finite = finite[THEN finite_distribution_finite, simplified space_simps]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   669
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   670
  have order: "\<And>x y z. \<lbrakk>x \<in> space MX; y \<in> space MY; z \<in> space MZ; joint_distribution X Z {(x, z)} = 0\<rbrakk>
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   671
          \<Longrightarrow> joint_distribution X (\<lambda>x. (Y x, Z x)) {(x, y, z)} = 0"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   672
    unfolding joint_distribution_commute_singleton[of X]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   673
    unfolding joint_distribution_assoc_singleton[symmetric]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   674
    using finite_distribution_order(6)[OF finite_var(2) ZX]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   675
    by (auto simp: space_simps)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   676
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   677
  note order = order
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   678
    finite_distribution_order(5,6)[OF finite_var(1) YZ, simplified space_simps]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   679
    finite_distribution_order(5,6)[OF finite_var(2,3), simplified space_simps]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   680
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   681
  have "- conditional_mutual_information b MX MY MZ X Y Z = - (\<Sum>(x, y, z) \<in> ?M. ?dXYZ {(x, y, z)} *
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   682
    log b (?dXYZ {(x, y, z)} / (?dXZ {(x, z)} * ?dYZ {(y,z)} / ?dZ {z})))"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   683
    unfolding conditional_mutual_information_generic_eq[OF assms] neg_equal_iff_equal
41023
9118eb4eb8dc it is known as the extended reals, not the infinite reals
hoelzl
parents: 40859
diff changeset
   684
    by (intro setsum_cong) (auto intro!: arg_cong[where f="log b"] simp: real_of_pextreal_mult[symmetric])
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   685
  also have "\<dots> \<le> log b (\<Sum>(x, y, z) \<in> ?M. ?dXZ {(x, z)} * ?dYZ {(y,z)} / ?dZ {z})"
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   686
    unfolding split_beta
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   687
  proof (rule log_setsum_divide)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   688
    show "?M \<noteq> {}" using False by simp
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   689
    show "1 < b" using b_gt_1 .
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   690
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   691
    show "finite ?M" using assms
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   692
      unfolding finite_sigma_algebra_def finite_sigma_algebra_axioms_def by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   693
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   694
    show "(\<Sum>x\<in>?M. ?dXYZ {(fst x, fst (snd x), snd (snd x))}) = 1"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   695
      unfolding setsum_cartesian_product'
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   696
      unfolding setsum_commute[of _ "space MY"]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   697
      unfolding setsum_commute[of _ "space MZ"]
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   698
      by (simp_all add: space_pair_measure
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   699
        setsum_real_joint_distribution_singleton[OF `finite_random_variable MX X` YZ]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   700
        setsum_real_joint_distribution_singleton[OF `finite_random_variable MY Y` finite_var(3)]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   701
        setsum_real_distribution[OF `finite_random_variable MZ Z`])
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   702
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   703
    fix x assume "x \<in> ?M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   704
    let ?x = "(fst x, fst (snd x), snd (snd x))"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   705
41023
9118eb4eb8dc it is known as the extended reals, not the infinite reals
hoelzl
parents: 40859
diff changeset
   706
    show "0 \<le> ?dXYZ {?x}" using real_pextreal_nonneg .
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   707
    show "0 \<le> ?dXZ {(fst x, snd (snd x))} * ?dYZ {(fst (snd x), snd (snd x))} / ?dZ {snd (snd x)}"
41023
9118eb4eb8dc it is known as the extended reals, not the infinite reals
hoelzl
parents: 40859
diff changeset
   708
     by (simp add: real_pextreal_nonneg mult_nonneg_nonneg divide_nonneg_nonneg)
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   709
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   710
    assume *: "0 < ?dXYZ {?x}"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   711
    with `x \<in> ?M` show "0 < ?dXZ {(fst x, snd (snd x))} * ?dYZ {(fst (snd x), snd (snd x))} / ?dZ {snd (snd x)}"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   712
      using finite order
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   713
      by (cases x)
41023
9118eb4eb8dc it is known as the extended reals, not the infinite reals
hoelzl
parents: 40859
diff changeset
   714
         (auto simp add: zero_less_real_of_pextreal zero_less_mult_iff zero_less_divide_iff)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   715
  qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   716
  also have "(\<Sum>(x, y, z) \<in> ?M. ?dXZ {(x, z)} * ?dYZ {(y,z)} / ?dZ {z}) = (\<Sum>z\<in>space MZ. ?dZ {z})"
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   717
    apply (simp add: setsum_cartesian_product')
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   718
    apply (subst setsum_commute)
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   719
    apply (subst (2) setsum_commute)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   720
    by (auto simp: setsum_divide_distrib[symmetric] setsum_product[symmetric]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   721
                   setsum_real_joint_distribution_singleton[OF finite_var(1,3)]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   722
                   setsum_real_joint_distribution_singleton[OF finite_var(2,3)]
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   723
          intro!: setsum_cong)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   724
  also have "log b (\<Sum>z\<in>space MZ. ?dZ {z}) = 0"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   725
    unfolding setsum_real_distribution[OF finite_var(3)] by simp
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   726
  finally show ?thesis by simp
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   727
qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   728
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   729
lemma (in information_space) conditional_mutual_information_positive:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   730
  assumes "simple_function M X" and "simple_function M Y" and "simple_function M Z"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   731
  shows "0 \<le> \<I>(X;Y|Z)"
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   732
  by (rule conditional_mutual_information_generic_positive[OF assms[THEN simple_function_imp_finite_random_variable]])
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   733
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   734
subsection {* Conditional Entropy *}
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   735
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   736
definition (in prob_space)
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   737
  "conditional_entropy b S T X Y = conditional_mutual_information b S S T X X Y"
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   738
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   739
abbreviation (in information_space)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   740
  conditional_entropy_Pow ("\<H>'(_ | _')") where
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   741
  "\<H>(X | Y) \<equiv> conditional_entropy b
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   742
    \<lparr> space = X`space M, sets = Pow (X`space M), measure = distribution X \<rparr>
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   743
    \<lparr> space = Y`space M, sets = Pow (Y`space M), measure = distribution Y \<rparr> X Y"
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   744
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   745
lemma (in information_space) conditional_entropy_positive:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   746
  "simple_function M X \<Longrightarrow> simple_function M Y \<Longrightarrow> 0 \<le> \<H>(X | Y)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   747
  unfolding conditional_entropy_def by (auto intro!: conditional_mutual_information_positive)
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   748
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   749
lemma (in measure_space) empty_measureI: "A = {} \<Longrightarrow> \<mu> A = 0" by simp
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   750
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   751
lemma (in information_space) conditional_entropy_generic_eq:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   752
  fixes MX :: "('c, 'd) measure_space_scheme" and MY :: "('e, 'f) measure_space_scheme"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   753
  assumes MX: "finite_random_variable MX X"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   754
  assumes MZ: "finite_random_variable MZ Z"
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   755
  shows "conditional_entropy b MX MZ X Z =
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   756
     - (\<Sum>(x, z)\<in>space MX \<times> space MZ.
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   757
         real (joint_distribution X Z {(x, z)}) *
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   758
         log b (real (joint_distribution X Z {(x, z)}) / real (distribution Z {z})))"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   759
proof -
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   760
  interpret MX: finite_sigma_algebra MX using MX by simp
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   761
  interpret MZ: finite_sigma_algebra MZ using MZ by simp
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   762
  let "?XXZ x y z" = "joint_distribution X (\<lambda>x. (X x, Z x)) {(x, y, z)}"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   763
  let "?XZ x z" = "joint_distribution X Z {(x, z)}"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   764
  let "?Z z" = "distribution Z {z}"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   765
  let "?f x y z" = "log b (real (?XXZ x y z) / (real (?XZ x z) * real (?XZ y z / ?Z z)))"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   766
  { fix x z have "?XXZ x x z = ?XZ x z"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   767
      unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>]) }
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   768
  note this[simp]
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   769
  { fix x x' :: 'c and z assume "x' \<noteq> x"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   770
    then have "?XXZ x x' z = 0"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   771
      by (auto simp: distribution_def intro!: arg_cong[where f=\<mu>] empty_measureI) }
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   772
  note this[simp]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   773
  { fix x x' z assume *: "x \<in> space MX" "z \<in> space MZ"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   774
    then have "(\<Sum>x'\<in>space MX. real (?XXZ x x' z) * ?f x x' z)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   775
      = (\<Sum>x'\<in>space MX. if x = x' then real (?XZ x z) * ?f x x z else 0)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   776
      by (auto intro!: setsum_cong)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   777
    also have "\<dots> = real (?XZ x z) * ?f x x z"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   778
      using `x \<in> space MX` by (simp add: setsum_cases[OF MX.finite_space])
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   779
    also have "\<dots> = real (?XZ x z) * log b (real (?Z z) / real (?XZ x z))"
41023
9118eb4eb8dc it is known as the extended reals, not the infinite reals
hoelzl
parents: 40859
diff changeset
   780
      by (auto simp: real_of_pextreal_mult[symmetric])
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   781
    also have "\<dots> = - real (?XZ x z) * log b (real (?XZ x z) / real (?Z z))"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   782
      using assms[THEN finite_distribution_finite]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   783
      using finite_distribution_order(6)[OF MX MZ]
41023
9118eb4eb8dc it is known as the extended reals, not the infinite reals
hoelzl
parents: 40859
diff changeset
   784
      by (auto simp: log_simps field_simps zero_less_mult_iff zero_less_real_of_pextreal real_of_pextreal_eq_0)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   785
    finally have "(\<Sum>x'\<in>space MX. real (?XXZ x x' z) * ?f x x' z) =
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   786
      - real (?XZ x z) * log b (real (?XZ x z) / real (?Z z))" . }
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   787
  note * = this
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   788
  show ?thesis
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   789
    unfolding conditional_entropy_def
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   790
    unfolding conditional_mutual_information_generic_eq[OF MX MX MZ]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   791
    by (auto simp: setsum_cartesian_product' setsum_negf[symmetric]
41023
9118eb4eb8dc it is known as the extended reals, not the infinite reals
hoelzl
parents: 40859
diff changeset
   792
                   setsum_commute[of _ "space MZ"] *   simp del: divide_pextreal_def
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   793
             intro!: setsum_cong)
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   794
qed
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   795
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   796
lemma (in information_space) conditional_entropy_eq:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   797
  assumes "simple_function M X" "simple_function M Z"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   798
  shows "\<H>(X | Z) =
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   799
     - (\<Sum>(x, z)\<in>X ` space M \<times> Z ` space M.
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   800
         real (joint_distribution X Z {(x, z)}) *
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   801
         log b (real (joint_distribution X Z {(x, z)}) / real (distribution Z {z})))"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   802
  using conditional_entropy_generic_eq[OF assms[THEN simple_function_imp_finite_random_variable]]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   803
  by simp
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   804
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   805
lemma (in information_space) conditional_entropy_eq_ce_with_hypothesis:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   806
  assumes X: "simple_function M X" and Y: "simple_function M Y"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   807
  shows "\<H>(X | Y) =
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   808
    -(\<Sum>y\<in>Y`space M. real (distribution Y {y}) *
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   809
      (\<Sum>x\<in>X`space M. real (joint_distribution X Y {(x,y)}) / real (distribution Y {(y)}) *
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   810
              log b (real (joint_distribution X Y {(x,y)}) / real (distribution Y {(y)}))))"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   811
  unfolding conditional_entropy_eq[OF assms]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   812
  using finite_distribution_finite[OF finite_random_variable_pairI[OF assms[THEN simple_function_imp_finite_random_variable]]]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   813
  using finite_distribution_order(5,6)[OF assms[THEN simple_function_imp_finite_random_variable]]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   814
  using finite_distribution_finite[OF Y[THEN simple_function_imp_finite_random_variable]]
41023
9118eb4eb8dc it is known as the extended reals, not the infinite reals
hoelzl
parents: 40859
diff changeset
   815
  by (auto simp: setsum_cartesian_product'  setsum_commute[of _ "Y`space M"] setsum_right_distrib real_of_pextreal_eq_0
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   816
           intro!: setsum_cong)
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   817
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   818
lemma (in information_space) conditional_entropy_eq_cartesian_product:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   819
  assumes "simple_function M X" "simple_function M Y"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   820
  shows "\<H>(X | Y) = -(\<Sum>x\<in>X`space M. \<Sum>y\<in>Y`space M.
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   821
    real (joint_distribution X Y {(x,y)}) *
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   822
    log b (real (joint_distribution X Y {(x,y)}) / real (distribution Y {y})))"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   823
  unfolding conditional_entropy_eq[OF assms]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   824
  by (auto intro!: setsum_cong simp: setsum_cartesian_product')
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   825
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   826
subsection {* Equalities *}
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   827
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   828
lemma (in information_space) mutual_information_eq_entropy_conditional_entropy:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   829
  assumes X: "simple_function M X" and Z: "simple_function M Z"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   830
  shows  "\<I>(X ; Z) = \<H>(X) - \<H>(X | Z)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   831
proof -
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   832
  let "?XZ x z" = "real (joint_distribution X Z {(x, z)})"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   833
  let "?Z z" = "real (distribution Z {z})"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   834
  let "?X x" = "real (distribution X {x})"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   835
  note fX = X[THEN simple_function_imp_finite_random_variable]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   836
  note fZ = Z[THEN simple_function_imp_finite_random_variable]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   837
  note fX[THEN finite_distribution_finite, simp] and fZ[THEN finite_distribution_finite, simp]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   838
  note finite_distribution_order[OF fX fZ, simp]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   839
  { fix x z assume "x \<in> X`space M" "z \<in> Z`space M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   840
    have "?XZ x z * log b (?XZ x z / (?X x * ?Z z)) =
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   841
          ?XZ x z * log b (?XZ x z / ?Z z) - ?XZ x z * log b (?X x)"
41023
9118eb4eb8dc it is known as the extended reals, not the infinite reals
hoelzl
parents: 40859
diff changeset
   842
      by (auto simp: log_simps real_of_pextreal_mult[symmetric] zero_less_mult_iff
9118eb4eb8dc it is known as the extended reals, not the infinite reals
hoelzl
parents: 40859
diff changeset
   843
                     zero_less_real_of_pextreal field_simps real_of_pextreal_eq_0 abs_mult) }
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   844
  note * = this
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   845
  show ?thesis
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   846
    unfolding entropy_eq[OF X] conditional_entropy_eq[OF X Z] mutual_information_eq[OF X Z]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   847
    using setsum_real_joint_distribution_singleton[OF fZ fX, unfolded joint_distribution_commute_singleton[of Z X]]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   848
    by (simp add: * setsum_cartesian_product' setsum_subtractf setsum_left_distrib[symmetric]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   849
                     setsum_real_distribution)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   850
qed
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   851
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   852
lemma (in information_space) conditional_entropy_less_eq_entropy:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   853
  assumes X: "simple_function M X" and Z: "simple_function M Z"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   854
  shows "\<H>(X | Z) \<le> \<H>(X)"
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   855
proof -
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   856
  have "\<I>(X ; Z) = \<H>(X) - \<H>(X | Z)" using mutual_information_eq_entropy_conditional_entropy[OF assms] .
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   857
  with mutual_information_positive[OF X Z] entropy_positive[OF X]
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   858
  show ?thesis by auto
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   859
qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   860
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   861
lemma (in information_space) entropy_chain_rule:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
   862
  assumes X: "simple_function M X" and Y: "simple_function M Y"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   863
  shows  "\<H>(\<lambda>x. (X x, Y x)) = \<H>(X) + \<H>(Y|X)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   864
proof -
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   865
  let "?XY x y" = "real (joint_distribution X Y {(x, y)})"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   866
  let "?Y y" = "real (distribution Y {y})"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   867
  let "?X x" = "real (distribution X {x})"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   868
  note fX = X[THEN simple_function_imp_finite_random_variable]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   869
  note fY = Y[THEN simple_function_imp_finite_random_variable]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   870
  note fX[THEN finite_distribution_finite, simp] and fY[THEN finite_distribution_finite, simp]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   871
  note finite_distribution_order[OF fX fY, simp]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   872
  { fix x y assume "x \<in> X`space M" "y \<in> Y`space M"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   873
    have "?XY x y * log b (?XY x y / ?X x) =
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   874
          ?XY x y * log b (?XY x y) - ?XY x y * log b (?X x)"
41023
9118eb4eb8dc it is known as the extended reals, not the infinite reals
hoelzl
parents: 40859
diff changeset
   875
      by (auto simp: log_simps real_of_pextreal_mult[symmetric] zero_less_mult_iff
9118eb4eb8dc it is known as the extended reals, not the infinite reals
hoelzl
parents: 40859
diff changeset
   876
                     zero_less_real_of_pextreal field_simps real_of_pextreal_eq_0 abs_mult) }
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   877
  note * = this
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   878
  show ?thesis
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   879
    using setsum_real_joint_distribution_singleton[OF fY fX]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   880
    unfolding entropy_eq[OF X] conditional_entropy_eq_cartesian_product[OF Y X] entropy_eq_cartesian_product[OF X Y]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   881
    unfolding joint_distribution_commute_singleton[of Y X] setsum_commute[of _ "X`space M"]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   882
    by (simp add: * setsum_subtractf setsum_left_distrib[symmetric])
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   883
qed
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   884
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   885
section {* Partitioning *}
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   886
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   887
definition "subvimage A f g \<longleftrightarrow> (\<forall>x \<in> A. f -` {f x} \<inter> A \<subseteq> g -` {g x} \<inter> A)"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   888
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   889
lemma subvimageI:
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   890
  assumes "\<And>x y. \<lbrakk> x \<in> A ; y \<in> A ; f x = f y \<rbrakk> \<Longrightarrow> g x = g y"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   891
  shows "subvimage A f g"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   892
  using assms unfolding subvimage_def by blast
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   893
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   894
lemma subvimageE[consumes 1]:
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   895
  assumes "subvimage A f g"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   896
  obtains "\<And>x y. \<lbrakk> x \<in> A ; y \<in> A ; f x = f y \<rbrakk> \<Longrightarrow> g x = g y"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   897
  using assms unfolding subvimage_def by blast
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   898
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   899
lemma subvimageD:
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   900
  "\<lbrakk> subvimage A f g ; x \<in> A ; y \<in> A ; f x = f y \<rbrakk> \<Longrightarrow> g x = g y"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   901
  using assms unfolding subvimage_def by blast
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   902
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   903
lemma subvimage_subset:
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   904
  "\<lbrakk> subvimage B f g ; A \<subseteq> B \<rbrakk> \<Longrightarrow> subvimage A f g"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   905
  unfolding subvimage_def by auto
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   906
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   907
lemma subvimage_idem[intro]: "subvimage A g g"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   908
  by (safe intro!: subvimageI)
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   909
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   910
lemma subvimage_comp_finer[intro]:
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   911
  assumes svi: "subvimage A g h"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   912
  shows "subvimage A g (f \<circ> h)"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   913
proof (rule subvimageI, simp)
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   914
  fix x y assume "x \<in> A" "y \<in> A" "g x = g y"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   915
  from svi[THEN subvimageD, OF this]
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   916
  show "f (h x) = f (h y)" by simp
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   917
qed
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   918
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   919
lemma subvimage_comp_gran:
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   920
  assumes svi: "subvimage A g h"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   921
  assumes inj: "inj_on f (g ` A)"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   922
  shows "subvimage A (f \<circ> g) h"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   923
  by (rule subvimageI) (auto intro!: subvimageD[OF svi] simp: inj_on_iff[OF inj])
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   924
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   925
lemma subvimage_comp:
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   926
  assumes svi: "subvimage (f ` A) g h"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   927
  shows "subvimage A (g \<circ> f) (h \<circ> f)"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   928
  by (rule subvimageI) (auto intro!: svi[THEN subvimageD])
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   929
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   930
lemma subvimage_trans:
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   931
  assumes fg: "subvimage A f g"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   932
  assumes gh: "subvimage A g h"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   933
  shows "subvimage A f h"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   934
  by (rule subvimageI) (auto intro!: fg[THEN subvimageD] gh[THEN subvimageD])
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   935
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   936
lemma subvimage_translator:
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   937
  assumes svi: "subvimage A f g"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   938
  shows "\<exists>h. \<forall>x \<in> A. h (f x)  = g x"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   939
proof (safe intro!: exI[of _ "\<lambda>x. (THE z. z \<in> (g ` (f -` {x} \<inter> A)))"])
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   940
  fix x assume "x \<in> A"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   941
  show "(THE x'. x' \<in> (g ` (f -` {f x} \<inter> A))) = g x"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   942
    by (rule theI2[of _ "g x"])
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   943
      (insert `x \<in> A`, auto intro!: svi[THEN subvimageD])
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   944
qed
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   945
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   946
lemma subvimage_translator_image:
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   947
  assumes svi: "subvimage A f g"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   948
  shows "\<exists>h. h ` f ` A = g ` A"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   949
proof -
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   950
  from subvimage_translator[OF svi]
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   951
  obtain h where "\<And>x. x \<in> A \<Longrightarrow> h (f x) = g x" by auto
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   952
  thus ?thesis
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   953
    by (auto intro!: exI[of _ h]
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   954
      simp: image_compose[symmetric] comp_def cong: image_cong)
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   955
qed
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   956
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   957
lemma subvimage_finite:
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   958
  assumes svi: "subvimage A f g" and fin: "finite (f`A)"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   959
  shows "finite (g`A)"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   960
proof -
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   961
  from subvimage_translator_image[OF svi]
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   962
  obtain h where "g`A = h`f`A" by fastsimp
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   963
  with fin show "finite (g`A)" by simp
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   964
qed
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   965
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   966
lemma subvimage_disj:
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   967
  assumes svi: "subvimage A f g"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   968
  shows "f -` {x} \<inter> A \<subseteq> g -` {y} \<inter> A \<or>
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   969
      f -` {x} \<inter> g -` {y} \<inter> A = {}" (is "?sub \<or> ?dist")
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   970
proof (rule disjCI)
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   971
  assume "\<not> ?dist"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   972
  then obtain z where "z \<in> A" and "x = f z" and "y = g z" by auto
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   973
  thus "?sub" using svi unfolding subvimage_def by auto
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   974
qed
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   975
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   976
lemma setsum_image_split:
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   977
  assumes svi: "subvimage A f g" and fin: "finite (f ` A)"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   978
  shows "(\<Sum>x\<in>f`A. h x) = (\<Sum>y\<in>g`A. \<Sum>x\<in>f`(g -` {y} \<inter> A). h x)"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   979
    (is "?lhs = ?rhs")
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   980
proof -
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   981
  have "f ` A =
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   982
      snd ` (SIGMA x : g ` A. f ` (g -` {x} \<inter> A))"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   983
      (is "_ = snd ` ?SIGMA")
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   984
    unfolding image_split_eq_Sigma[symmetric]
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   985
    by (simp add: image_compose[symmetric] comp_def)
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   986
  moreover
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   987
  have snd_inj: "inj_on snd ?SIGMA"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   988
    unfolding image_split_eq_Sigma[symmetric]
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   989
    by (auto intro!: inj_onI subvimageD[OF svi])
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   990
  ultimately
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   991
  have "(\<Sum>x\<in>f`A. h x) = (\<Sum>(x,y)\<in>?SIGMA. h y)"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   992
    by (auto simp: setsum_reindex intro: setsum_cong)
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   993
  also have "... = ?rhs"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   994
    using subvimage_finite[OF svi fin] fin
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   995
    apply (subst setsum_Sigma[symmetric])
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   996
    by (auto intro!: finite_subset[of _ "f`A"])
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   997
  finally show ?thesis .
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   998
qed
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   999
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1000
lemma (in information_space) entropy_partition:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
  1001
  assumes sf: "simple_function M X" "simple_function M P"
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1002
  assumes svi: "subvimage (space M) X P"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1003
  shows "\<H>(X) = \<H>(P) + \<H>(X|P)"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1004
proof -
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1005
  let "?XP x p" = "real (joint_distribution X P {(x, p)})"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1006
  let "?X x" = "real (distribution X {x})"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1007
  let "?P p" = "real (distribution P {p})"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1008
  note fX = sf(1)[THEN simple_function_imp_finite_random_variable]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1009
  note fP = sf(2)[THEN simple_function_imp_finite_random_variable]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1010
  note fX[THEN finite_distribution_finite, simp] and fP[THEN finite_distribution_finite, simp]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1011
  note finite_distribution_order[OF fX fP, simp]
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
  1012
  have "(\<Sum>x\<in>X ` space M. real (distribution X {x}) * log b (real (distribution X {x}))) =
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1013
    (\<Sum>y\<in>P `space M. \<Sum>x\<in>X ` space M.
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
  1014
    real (joint_distribution X P {(x, y)}) * log b (real (joint_distribution X P {(x, y)})))"
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1015
  proof (subst setsum_image_split[OF svi],
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1016
      safe intro!: setsum_mono_zero_cong_left imageI)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1017
    show "finite (X ` space M)" "finite (X ` space M)" "finite (P ` space M)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1018
      using sf unfolding simple_function_def by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1019
  next
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1020
    fix p x assume in_space: "p \<in> space M" "x \<in> space M"
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
  1021
    assume "real (joint_distribution X P {(X x, P p)}) * log b (real (joint_distribution X P {(X x, P p)})) \<noteq> 0"
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1022
    hence "(\<lambda>x. (X x, P x)) -` {(X x, P p)} \<inter> space M \<noteq> {}" by (auto simp: distribution_def)
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1023
    with svi[unfolded subvimage_def, rule_format, OF `x \<in> space M`]
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1024
    show "x \<in> P -` {P p}" by auto
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1025
  next
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1026
    fix p x assume in_space: "p \<in> space M" "x \<in> space M"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1027
    assume "P x = P p"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1028
    from this[symmetric] svi[unfolded subvimage_def, rule_format, OF `x \<in> space M`]
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1029
    have "X -` {X x} \<inter> space M \<subseteq> P -` {P p} \<inter> space M"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1030
      by auto
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1031
    hence "(\<lambda>x. (X x, P x)) -` {(X x, P p)} \<inter> space M = X -` {X x} \<inter> space M"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1032
      by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
  1033
    thus "real (distribution X {X x}) * log b (real (distribution X {X x})) =
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
  1034
          real (joint_distribution X P {(X x, P p)}) *
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
  1035
          log b (real (joint_distribution X P {(X x, P p)}))"
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1036
      by (auto simp: distribution_def)
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1037
  qed
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1038
  moreover have "\<And>x y. real (joint_distribution X P {(x, y)}) *
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1039
      log b (real (joint_distribution X P {(x, y)}) / real (distribution P {y})) =
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1040
      real (joint_distribution X P {(x, y)}) * log b (real (joint_distribution X P {(x, y)})) -
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1041
      real (joint_distribution X P {(x, y)}) * log b (real (distribution P {y}))"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1042
    by (auto simp add: log_simps zero_less_mult_iff field_simps)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1043
  ultimately show ?thesis
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1044
    unfolding sf[THEN entropy_eq] conditional_entropy_eq[OF sf]
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1045
    using setsum_real_joint_distribution_singleton[OF fX fP]
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
  1046
    by (simp add: setsum_cartesian_product' setsum_subtractf setsum_real_distribution
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1047
      setsum_left_distrib[symmetric] setsum_commute[where B="P`space M"])
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1048
qed
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1049
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1050
corollary (in information_space) entropy_data_processing:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
  1051
  assumes X: "simple_function M X" shows "\<H>(f \<circ> X) \<le> \<H>(X)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1052
proof -
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1053
  note X
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
  1054
  moreover have fX: "simple_function M (f \<circ> X)" using X by auto
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1055
  moreover have "subvimage (space M) X (f \<circ> X)" by auto
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1056
  ultimately have "\<H>(X) = \<H>(f\<circ>X) + \<H>(X|f\<circ>X)" by (rule entropy_partition)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1057
  then show "\<H>(f \<circ> X) \<le> \<H>(X)"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1058
    by (auto intro: conditional_entropy_positive[OF X fX])
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1059
qed
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1060
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1061
corollary (in information_space) entropy_of_inj:
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
  1062
  assumes X: "simple_function M X" and inj: "inj_on f (X`space M)"
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1063
  shows "\<H>(f \<circ> X) = \<H>(X)"
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1064
proof (rule antisym)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1065
  show "\<H>(f \<circ> X) \<le> \<H>(X)" using entropy_data_processing[OF X] .
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1066
next
41689
3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents: 41661
diff changeset
  1067
  have sf: "simple_function M (f \<circ> X)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1068
    using X by auto
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1069
  have "\<H>(X) = \<H>(the_inv_into (X`space M) f \<circ> (f \<circ> X))"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1070
    by (auto intro!: mutual_information_cong simp: entropy_def the_inv_into_f_f[OF inj])
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1071
  also have "... \<le> \<H>(f \<circ> X)"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1072
    using entropy_data_processing[OF sf] .
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1073
  finally show "\<H>(X) \<le> \<H>(f \<circ> X)" .
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1074
qed
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1075
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
  1076
end