src/HOL/Probability/Information.thy
author hoelzl
Fri, 02 Nov 2012 14:23:54 +0100
changeset 50003 8c213922ed49
parent 50002 ce0d316b5b44
child 50244 de72bbe42190
permissions -rw-r--r--
use measurability prover
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42067
66c8281349ec standardized headers
hoelzl
parents: 41981
diff changeset
     1
(*  Title:      HOL/Probability/Information.thy
66c8281349ec standardized headers
hoelzl
parents: 41981
diff changeset
     2
    Author:     Johannes Hölzl, TU München
66c8281349ec standardized headers
hoelzl
parents: 41981
diff changeset
     3
    Author:     Armin Heller, TU München
66c8281349ec standardized headers
hoelzl
parents: 41981
diff changeset
     4
*)
66c8281349ec standardized headers
hoelzl
parents: 41981
diff changeset
     5
66c8281349ec standardized headers
hoelzl
parents: 41981
diff changeset
     6
header {*Information theory*}
66c8281349ec standardized headers
hoelzl
parents: 41981
diff changeset
     7
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
     8
theory Information
41413
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 41095
diff changeset
     9
imports
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
    10
  Independent_Family
43556
0d78c8d31d0d move conditional expectation to its own theory file
hoelzl
parents: 43340
diff changeset
    11
  Radon_Nikodym
41413
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 41095
diff changeset
    12
  "~~/src/HOL/Library/Convex"
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    13
begin
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    14
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
    15
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
    16
  by (subst log_le_cancel_iff) auto
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
    17
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
    18
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
    19
  by (subst log_less_cancel_iff) auto
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
    20
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
    21
lemma setsum_cartesian_product':
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
    22
  "(\<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
    23
  unfolding setsum_cartesian_product by simp
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
    24
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
    25
lemma split_pairs:
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    26
  "((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
    27
  "(X = (A, B)) \<longleftrightarrow> (fst X = A \<and> snd X = B)" by auto
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    28
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    29
section "Information theory"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    30
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    31
locale information_space = prob_space +
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    32
  fixes b :: real assumes b_gt_1: "1 < b"
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    33
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    34
context information_space
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    35
begin
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    36
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    37
text {* Introduce some simplification rules for logarithm of base @{term b}. *}
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    38
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    39
lemma log_neg_const:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    40
  assumes "x \<le> 0"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    41
  shows "log b x = log b 0"
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
    42
proof -
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    43
  { fix u :: real
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    44
    have "x \<le> 0" by fact
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    45
    also have "0 < exp u"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    46
      using exp_gt_zero .
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    47
    finally have "exp u \<noteq> x"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    48
      by auto }
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    49
  then show "log b x = log b 0"
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    50
    by (simp add: log_def ln_def)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    51
qed
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    52
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    53
lemma log_mult_eq:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    54
  "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
    55
  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
    56
  by (auto simp: zero_less_mult_iff mult_le_0_iff)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    57
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    58
lemma log_inverse_eq:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    59
  "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
    60
  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
    61
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    62
lemma log_divide_eq:
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    63
  "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
    64
  unfolding divide_inverse log_mult_eq log_inverse_eq abs_inverse
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    65
  by (auto simp: zero_less_mult_iff mult_le_0_iff)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    66
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
    67
lemmas log_simps = log_mult_eq log_inverse_eq log_divide_eq
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    68
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    69
end
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
    70
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
    71
subsection "Kullback$-$Leibler divergence"
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
    72
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
    73
text {* The Kullback$-$Leibler divergence is also known as relative entropy or
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
    74
Kullback$-$Leibler distance. *}
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
    75
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
    76
definition
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    77
  "entropy_density b M N = log b \<circ> real \<circ> RN_deriv M N"
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
    78
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
    79
definition
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    80
  "KL_divergence b M N = integral\<^isup>L N (entropy_density b M N)"
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
    81
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
    82
lemma (in information_space) measurable_entropy_density:
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    83
  assumes ac: "absolutely_continuous M N" "sets N = events"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    84
  shows "entropy_density b M N \<in> borel_measurable M"
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
    85
proof -
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    86
  from borel_measurable_RN_deriv[OF ac] b_gt_1 show ?thesis
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
    87
    unfolding entropy_density_def by auto
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
    88
qed
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
    89
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
    90
lemma borel_measurable_RN_deriv_density[measurable (raw)]:
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
    91
  "f \<in> borel_measurable M \<Longrightarrow> RN_deriv M (density M f) \<in> borel_measurable M"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
    92
  using borel_measurable_RN_deriv_density[of "\<lambda>x. max 0 (f x )" M]
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
    93
  by (simp add: density_max_0[symmetric])
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
    94
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    95
lemma (in sigma_finite_measure) KL_density:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    96
  fixes f :: "'a \<Rightarrow> real"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    97
  assumes "1 < b"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    98
  assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
    99
  shows "KL_divergence b M (density M f) = (\<integral>x. f x * log b (f x) \<partial>M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   100
  unfolding KL_divergence_def
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   101
proof (subst integral_density)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   102
  show "entropy_density b M (density M (\<lambda>x. ereal (f x))) \<in> borel_measurable M"
49776
199d1d5bb17e tuned product measurability
hoelzl
parents: 47694
diff changeset
   103
    using f
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   104
    by (auto simp: comp_def entropy_density_def)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   105
  have "density M (RN_deriv M (density M f)) = density M f"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   106
    using f by (intro density_RN_deriv_density) auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   107
  then have eq: "AE x in M. RN_deriv M (density M f) x = f x"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   108
    using f
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   109
    by (intro density_unique)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   110
       (auto intro!: borel_measurable_log borel_measurable_RN_deriv_density simp: RN_deriv_density_nonneg)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   111
  show "(\<integral>x. f x * entropy_density b M (density M (\<lambda>x. ereal (f x))) x \<partial>M) = (\<integral>x. f x * log b (f x) \<partial>M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   112
    apply (intro integral_cong_AE)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   113
    using eq
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   114
    apply eventually_elim
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   115
    apply (auto simp: entropy_density_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   116
    done
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   117
qed fact+
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   118
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   119
lemma (in sigma_finite_measure) KL_density_density:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   120
  fixes f g :: "'a \<Rightarrow> real"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   121
  assumes "1 < b"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   122
  assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   123
  assumes g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   124
  assumes ac: "AE x in M. f x = 0 \<longrightarrow> g x = 0"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   125
  shows "KL_divergence b (density M f) (density M g) = (\<integral>x. g x * log b (g x / f x) \<partial>M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   126
proof -
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   127
  interpret Mf: sigma_finite_measure "density M f"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   128
    using f by (subst sigma_finite_iff_density_finite) auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   129
  have "KL_divergence b (density M f) (density M g) =
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   130
    KL_divergence b (density M f) (density (density M f) (\<lambda>x. g x / f x))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   131
    using f g ac by (subst density_density_divide) simp_all
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   132
  also have "\<dots> = (\<integral>x. (g x / f x) * log b (g x / f x) \<partial>density M f)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   133
    using f g `1 < b` by (intro Mf.KL_density) (auto simp: AE_density divide_nonneg_nonneg)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   134
  also have "\<dots> = (\<integral>x. g x * log b (g x / f x) \<partial>M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   135
    using ac f g `1 < b` by (subst integral_density) (auto intro!: integral_cong_AE)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   136
  finally show ?thesis .
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   137
qed
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   138
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   139
lemma (in information_space) KL_gt_0:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   140
  fixes D :: "'a \<Rightarrow> real"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   141
  assumes "prob_space (density M D)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   142
  assumes D: "D \<in> borel_measurable M" "AE x in M. 0 \<le> D x"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   143
  assumes int: "integrable M (\<lambda>x. D x * log b (D x))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   144
  assumes A: "density M D \<noteq> M"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   145
  shows "0 < KL_divergence b M (density M D)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   146
proof -
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   147
  interpret N: prob_space "density M D" by fact
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   148
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   149
  obtain A where "A \<in> sets M" "emeasure (density M D) A \<noteq> emeasure M A"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   150
    using measure_eqI[of "density M D" M] `density M D \<noteq> M` by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   151
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   152
  let ?D_set = "{x\<in>space M. D x \<noteq> 0}"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   153
  have [simp, intro]: "?D_set \<in> sets M"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   154
    using D by auto
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   155
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43556
diff changeset
   156
  have D_neg: "(\<integral>\<^isup>+ x. ereal (- D x) \<partial>M) = 0"
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   157
    using D by (subst positive_integral_0_iff_AE) auto
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   158
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   159
  have "(\<integral>\<^isup>+ x. ereal (D x) \<partial>M) = emeasure (density M D) (space M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   160
    using D by (simp add: emeasure_density cong: positive_integral_cong)
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43556
diff changeset
   161
  then have D_pos: "(\<integral>\<^isup>+ x. ereal (D x) \<partial>M) = 1"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   162
    using N.emeasure_space_1 by simp
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   163
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   164
  have "integrable M D" "integral\<^isup>L M D = 1"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   165
    using D D_pos D_neg unfolding integrable_def lebesgue_integral_def by simp_all
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   166
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   167
  have "0 \<le> 1 - measure M ?D_set"
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   168
    using prob_le_1 by (auto simp: field_simps)
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   169
  also have "\<dots> = (\<integral> x. D x - indicator ?D_set x \<partial>M)"
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   170
    using `integrable M D` `integral\<^isup>L M D = 1`
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   171
    by (simp add: emeasure_eq_measure)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   172
  also have "\<dots> < (\<integral> x. D x * (ln b * log b (D x)) \<partial>M)"
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   173
  proof (rule integral_less_AE)
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   174
    show "integrable M (\<lambda>x. D x - indicator ?D_set x)"
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   175
      using `integrable M D`
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   176
      by (intro integral_diff integral_indicator) auto
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   177
  next
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   178
    from integral_cmult(1)[OF int, of "ln b"]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   179
    show "integrable M (\<lambda>x. D x * (ln b * log b (D x)))" 
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   180
      by (simp add: ac_simps)
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   181
  next
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   182
    show "emeasure M {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<noteq> 0"
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   183
    proof
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   184
      assume eq_0: "emeasure M {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} = 0"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   185
      then have disj: "AE x in M. D x = 1 \<or> D x = 0"
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   186
        using D(1) by (auto intro!: AE_I[OF subset_refl] sets_Collect)
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   187
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   188
      have "emeasure M {x\<in>space M. D x = 1} = (\<integral>\<^isup>+ x. indicator {x\<in>space M. D x = 1} x \<partial>M)"
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   189
        using D(1) by auto
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   190
      also have "\<dots> = (\<integral>\<^isup>+ x. ereal (D x) \<partial>M)"
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43556
diff changeset
   191
        using disj by (auto intro!: positive_integral_cong_AE simp: indicator_def one_ereal_def)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   192
      finally have "AE x in M. D x = 1"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   193
        using D D_pos by (intro AE_I_eq_1) auto
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43556
diff changeset
   194
      then have "(\<integral>\<^isup>+x. indicator A x\<partial>M) = (\<integral>\<^isup>+x. ereal (D x) * indicator A x\<partial>M)"
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43556
diff changeset
   195
        by (intro positive_integral_cong_AE) (auto simp: one_ereal_def[symmetric])
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   196
      also have "\<dots> = density M D A"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   197
        using `A \<in> sets M` D by (simp add: emeasure_density)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   198
      finally show False using `A \<in> sets M` `emeasure (density M D) A \<noteq> emeasure M A` by simp
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   199
    qed
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   200
    show "{x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<in> sets M"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   201
      using D(1) by (auto intro: sets_Collect_conj)
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   202
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   203
    show "AE t in M. t \<in> {x\<in>space M. D x \<noteq> 1 \<and> D x \<noteq> 0} \<longrightarrow>
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   204
      D t - indicator ?D_set t \<noteq> D t * (ln b * log b (D t))"
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   205
      using D(2)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   206
    proof (eventually_elim, safe)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   207
      fix t assume Dt: "t \<in> space M" "D t \<noteq> 1" "D t \<noteq> 0" "0 \<le> D t"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   208
        and eq: "D t - indicator ?D_set t = D t * (ln b * log b (D t))"
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   209
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   210
      have "D t - 1 = D t - indicator ?D_set t"
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   211
        using Dt by simp
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   212
      also note eq
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   213
      also have "D t * (ln b * log b (D t)) = - D t * ln (1 / D t)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   214
        using b_gt_1 `D t \<noteq> 0` `0 \<le> D t`
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   215
        by (simp add: log_def ln_div less_le)
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   216
      finally have "ln (1 / D t) = 1 / D t - 1"
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   217
        using `D t \<noteq> 0` by (auto simp: field_simps)
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   218
      from ln_eq_minus_one[OF _ this] `D t \<noteq> 0` `0 \<le> D t` `D t \<noteq> 1`
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   219
      show False by auto
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   220
    qed
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   221
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   222
    show "AE t in M. D t - indicator ?D_set t \<le> D t * (ln b * log b (D t))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   223
      using D(2) AE_space
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   224
    proof eventually_elim
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   225
      fix t assume "t \<in> space M" "0 \<le> D t"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   226
      show "D t - indicator ?D_set t \<le> D t * (ln b * log b (D t))"
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   227
      proof cases
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   228
        assume asm: "D t \<noteq> 0"
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   229
        then have "0 < D t" using `0 \<le> D t` by auto
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   230
        then have "0 < 1 / D t" by auto
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   231
        have "D t - indicator ?D_set t \<le> - D t * (1 / D t - 1)"
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   232
          using asm `t \<in> space M` by (simp add: field_simps)
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   233
        also have "- D t * (1 / D t - 1) \<le> - D t * ln (1 / D t)"
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   234
          using ln_le_minus_one `0 < 1 / D t` by (intro mult_left_mono_neg) auto
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   235
        also have "\<dots> = D t * (ln b * log b (D t))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   236
          using `0 < D t` b_gt_1
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   237
          by (simp_all add: log_def ln_div)
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   238
        finally show ?thesis by simp
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   239
      qed simp
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   240
    qed
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   241
  qed
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   242
  also have "\<dots> = (\<integral> x. ln b * (D x * log b (D x)) \<partial>M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   243
    by (simp add: ac_simps)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   244
  also have "\<dots> = ln b * (\<integral> x. D x * log b (D x) \<partial>M)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   245
    using int by (rule integral_cmult)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   246
  finally show ?thesis
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   247
    using b_gt_1 D by (subst KL_density) (auto simp: zero_less_mult_iff)
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   248
qed
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   249
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   250
lemma (in sigma_finite_measure) KL_same_eq_0: "KL_divergence b M M = 0"
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   251
proof -
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   252
  have "AE x in M. 1 = RN_deriv M M x"
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   253
  proof (rule RN_deriv_unique)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   254
    show "(\<lambda>x. 1) \<in> borel_measurable M" "AE x in M. 0 \<le> (1 :: ereal)" by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   255
    show "density M (\<lambda>x. 1) = M"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   256
      apply (auto intro!: measure_eqI emeasure_density)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   257
      apply (subst emeasure_density)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   258
      apply auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   259
      done
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   260
  qed
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   261
  then have "AE x in M. log b (real (RN_deriv M M x)) = 0"
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   262
    by (elim AE_mp) simp
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   263
  from integral_cong_AE[OF this]
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   264
  have "integral\<^isup>L M (entropy_density b M M) = 0"
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   265
    by (simp add: entropy_density_def comp_def)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   266
  then show "KL_divergence b M M = 0"
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   267
    unfolding KL_divergence_def
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   268
    by auto
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   269
qed
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   270
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   271
lemma (in information_space) KL_eq_0_iff_eq:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   272
  fixes D :: "'a \<Rightarrow> real"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   273
  assumes "prob_space (density M D)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   274
  assumes D: "D \<in> borel_measurable M" "AE x in M. 0 \<le> D x"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   275
  assumes int: "integrable M (\<lambda>x. D x * log b (D x))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   276
  shows "KL_divergence b M (density M D) = 0 \<longleftrightarrow> density M D = M"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   277
  using KL_same_eq_0[of b] KL_gt_0[OF assms]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   278
  by (auto simp: less_le)
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   279
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   280
lemma (in information_space) KL_eq_0_iff_eq_ac:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   281
  fixes D :: "'a \<Rightarrow> real"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   282
  assumes "prob_space N"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   283
  assumes ac: "absolutely_continuous M N" "sets N = sets M"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   284
  assumes int: "integrable N (entropy_density b M N)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   285
  shows "KL_divergence b M N = 0 \<longleftrightarrow> N = M"
41833
563bea92b2c0 add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents: 41689
diff changeset
   286
proof -
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   287
  interpret N: prob_space N by fact
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   288
  have "finite_measure N" by unfold_locales
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   289
  from real_RN_deriv[OF this ac] guess D . note D = this
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   290
  
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   291
  have "N = density M (RN_deriv M N)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   292
    using ac by (rule density_RN_deriv[symmetric])
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   293
  also have "\<dots> = density M D"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   294
    using borel_measurable_RN_deriv[OF ac] D by (auto intro!: density_cong)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   295
  finally have N: "N = density M D" .
41833
563bea92b2c0 add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents: 41689
diff changeset
   296
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   297
  from absolutely_continuous_AE[OF ac(2,1) D(2)] D b_gt_1 ac measurable_entropy_density
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   298
  have "integrable N (\<lambda>x. log b (D x))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   299
    by (intro integrable_cong_AE[THEN iffD2, OF _ _ _ int])
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   300
       (auto simp: N entropy_density_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   301
  with D b_gt_1 have "integrable M (\<lambda>x. D x * log b (D x))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   302
    by (subst integral_density(2)[symmetric]) (auto simp: N[symmetric] comp_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   303
  with `prob_space N` D show ?thesis
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   304
    unfolding N
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   305
    by (intro KL_eq_0_iff_eq) auto
41833
563bea92b2c0 add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents: 41689
diff changeset
   306
qed
563bea92b2c0 add lemma KL_divergence_vimage, mutual_information_generic
hoelzl
parents: 41689
diff changeset
   307
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   308
lemma (in information_space) KL_nonneg:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   309
  assumes "prob_space (density M D)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   310
  assumes D: "D \<in> borel_measurable M" "AE x in M. 0 \<le> D x"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   311
  assumes int: "integrable M (\<lambda>x. D x * log b (D x))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   312
  shows "0 \<le> KL_divergence b M (density M D)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   313
  using KL_gt_0[OF assms] by (cases "density M D = M") (auto simp: KL_same_eq_0)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   314
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   315
lemma (in sigma_finite_measure) KL_density_density_nonneg:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   316
  fixes f g :: "'a \<Rightarrow> real"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   317
  assumes "1 < b"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   318
  assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "prob_space (density M f)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   319
  assumes g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x" "prob_space (density M g)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   320
  assumes ac: "AE x in M. f x = 0 \<longrightarrow> g x = 0"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   321
  assumes int: "integrable M (\<lambda>x. g x * log b (g x / f x))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   322
  shows "0 \<le> KL_divergence b (density M f) (density M g)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   323
proof -
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   324
  interpret Mf: prob_space "density M f" by fact
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   325
  interpret Mf: information_space "density M f" b by default fact
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   326
  have eq: "density (density M f) (\<lambda>x. g x / f x) = density M g" (is "?DD = _")
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   327
    using f g ac by (subst density_density_divide) simp_all
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   328
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   329
  have "0 \<le> KL_divergence b (density M f) (density (density M f) (\<lambda>x. g x / f x))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   330
  proof (rule Mf.KL_nonneg)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   331
    show "prob_space ?DD" unfolding eq by fact
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   332
    from f g show "(\<lambda>x. g x / f x) \<in> borel_measurable (density M f)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   333
      by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   334
    show "AE x in density M f. 0 \<le> g x / f x"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   335
      using f g by (auto simp: AE_density divide_nonneg_nonneg)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   336
    show "integrable (density M f) (\<lambda>x. g x / f x * log b (g x / f x))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   337
      using `1 < b` f g ac
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   338
      by (subst integral_density)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   339
         (auto intro!: integrable_cong_AE[THEN iffD2, OF _ _ _ int] measurable_If)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   340
  qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   341
  also have "\<dots> = KL_divergence b (density M f) (density M g)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   342
    using f g ac by (subst density_density_divide) simp_all
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   343
  finally show ?thesis .
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   344
qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   345
49803
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   346
subsection {* Finite Entropy *}
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   347
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   348
definition (in information_space) 
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   349
  "finite_entropy S X f \<longleftrightarrow> distributed M S X f \<and> integrable S (\<lambda>x. f x * log b (f x))"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   350
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   351
lemma (in information_space) finite_entropy_simple_function:
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   352
  assumes X: "simple_function M X"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   353
  shows "finite_entropy (count_space (X`space M)) X (\<lambda>a. measure M {x \<in> space M. X x = a})"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   354
  unfolding finite_entropy_def
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   355
proof
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   356
  have [simp]: "finite (X ` space M)"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   357
    using X by (auto simp: simple_function_def)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   358
  then show "integrable (count_space (X ` space M))
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   359
     (\<lambda>x. prob {xa \<in> space M. X xa = x} * log b (prob {xa \<in> space M. X xa = x}))"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   360
    by (rule integrable_count_space)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   361
  have d: "distributed M (count_space (X ` space M)) X (\<lambda>x. ereal (if x \<in> X`space M then prob {xa \<in> space M. X xa = x} else 0))"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   362
    by (rule distributed_simple_function_superset[OF X]) (auto intro!: arg_cong[where f=prob])
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   363
  show "distributed M (count_space (X ` space M)) X (\<lambda>x. ereal (prob {xa \<in> space M. X xa = x}))"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   364
    by (rule distributed_cong_density[THEN iffD1, OF _ _ _ d]) auto
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   365
qed
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   366
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   367
lemma distributed_transform_AE:
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   368
  assumes T: "T \<in> measurable P Q" "absolutely_continuous Q (distr P Q T)"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   369
  assumes g: "distributed M Q Y g"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   370
  shows "AE x in P. 0 \<le> g (T x)"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   371
  using g
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   372
  apply (subst AE_distr_iff[symmetric, OF T(1)])
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   373
  apply simp
49803
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   374
  apply (rule absolutely_continuous_AE[OF _ T(2)])
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   375
  apply simp
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   376
  apply (simp add: distributed_AE)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   377
  done
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   378
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   379
lemma ac_fst:
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   380
  assumes "sigma_finite_measure T"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   381
  shows "absolutely_continuous S (distr (S \<Otimes>\<^isub>M T) S fst)"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   382
proof -
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   383
  interpret sigma_finite_measure T by fact
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   384
  { fix A assume "A \<in> sets S" "emeasure S A = 0"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   385
    moreover then have "fst -` A \<inter> space (S \<Otimes>\<^isub>M T) = A \<times> space T"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   386
      by (auto simp: space_pair_measure dest!: sets_into_space)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   387
    ultimately have "emeasure (S \<Otimes>\<^isub>M T) (fst -` A \<inter> space (S \<Otimes>\<^isub>M T)) = 0"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   388
      by (simp add: emeasure_pair_measure_Times) }
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   389
  then show ?thesis
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   390
    unfolding absolutely_continuous_def
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   391
    apply (auto simp: null_sets_distr_iff)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   392
    apply (auto simp: null_sets_def intro!: measurable_sets)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   393
    done
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   394
qed
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   395
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   396
lemma ac_snd:
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   397
  assumes "sigma_finite_measure T"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   398
  shows "absolutely_continuous T (distr (S \<Otimes>\<^isub>M T) T snd)"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   399
proof -
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   400
  interpret sigma_finite_measure T by fact
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   401
  { fix A assume "A \<in> sets T" "emeasure T A = 0"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   402
    moreover then have "snd -` A \<inter> space (S \<Otimes>\<^isub>M T) = space S \<times> A"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   403
      by (auto simp: space_pair_measure dest!: sets_into_space)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   404
    ultimately have "emeasure (S \<Otimes>\<^isub>M T) (snd -` A \<inter> space (S \<Otimes>\<^isub>M T)) = 0"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   405
      by (simp add: emeasure_pair_measure_Times) }
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   406
  then show ?thesis
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   407
    unfolding absolutely_continuous_def
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   408
    apply (auto simp: null_sets_distr_iff)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   409
    apply (auto simp: null_sets_def intro!: measurable_sets)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   410
    done
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   411
qed
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   412
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   413
lemma distributed_integrable:
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   414
  "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow>
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   415
    integrable N (\<lambda>x. f x * g x) \<longleftrightarrow> integrable M (\<lambda>x. g (X x))"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   416
  by (auto simp: distributed_real_AE
49803
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   417
                    distributed_distr_eq_density[symmetric] integral_density[symmetric] integrable_distr_eq)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   418
  
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   419
lemma distributed_transform_integrable:
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   420
  assumes Px: "distributed M N X Px"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   421
  assumes "distributed M P Y Py"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   422
  assumes Y: "Y = (\<lambda>x. T (X x))" and T: "T \<in> measurable N P" and f: "f \<in> borel_measurable P"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   423
  shows "integrable P (\<lambda>x. Py x * f x) \<longleftrightarrow> integrable N (\<lambda>x. Px x * f (T x))"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   424
proof -
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   425
  have "integrable P (\<lambda>x. Py x * f x) \<longleftrightarrow> integrable M (\<lambda>x. f (Y x))"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   426
    by (rule distributed_integrable) fact+
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   427
  also have "\<dots> \<longleftrightarrow> integrable M (\<lambda>x. f (T (X x)))"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   428
    using Y by simp
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   429
  also have "\<dots> \<longleftrightarrow> integrable N (\<lambda>x. Px x * f (T x))"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   430
    using measurable_comp[OF T f] Px by (intro distributed_integrable[symmetric]) (auto simp: comp_def)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   431
  finally show ?thesis .
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   432
qed
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   433
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   434
lemma integrable_cong_AE_imp: "integrable M g \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> (AE x in M. g x = f x) \<Longrightarrow> integrable M f"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   435
  using integrable_cong_AE by blast
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   436
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   437
lemma (in information_space) finite_entropy_integrable:
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   438
  "finite_entropy S X Px \<Longrightarrow> integrable S (\<lambda>x. Px x * log b (Px x))"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   439
  unfolding finite_entropy_def by auto
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   440
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   441
lemma (in information_space) finite_entropy_distributed:
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   442
  "finite_entropy S X Px \<Longrightarrow> distributed M S X Px"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   443
  unfolding finite_entropy_def by auto
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   444
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   445
lemma (in information_space) finite_entropy_integrable_transform:
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   446
  assumes Fx: "finite_entropy S X Px"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   447
  assumes Fy: "distributed M T Y Py"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   448
    and "X = (\<lambda>x. f (Y x))"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   449
    and "f \<in> measurable T S"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   450
  shows "integrable T (\<lambda>x. Py x * log b (Px (f x)))"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   451
  using assms unfolding finite_entropy_def
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   452
  using distributed_transform_integrable[of M T Y Py S X Px f "\<lambda>x. log b (Px x)"]
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   453
  by auto
49803
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   454
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   455
subsection {* Mutual Information *}
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   456
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   457
definition (in prob_space)
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 36649
diff changeset
   458
  "mutual_information b S T X Y =
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   459
    KL_divergence b (distr M S X \<Otimes>\<^isub>M distr M T Y) (distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)))"
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   460
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   461
lemma (in information_space) mutual_information_indep_vars:
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   462
  fixes S T X Y
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   463
  defines "P \<equiv> distr M S X \<Otimes>\<^isub>M distr M T Y"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   464
  defines "Q \<equiv> distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   465
  shows "indep_var S X T Y \<longleftrightarrow>
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   466
    (random_variable S X \<and> random_variable T Y \<and>
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   467
      absolutely_continuous P Q \<and> integrable Q (entropy_density b P Q) \<and>
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   468
      mutual_information b S T X Y = 0)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   469
  unfolding indep_var_distribution_eq
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   470
proof safe
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   471
  assume rv[measurable]: "random_variable S X" "random_variable T Y"
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   472
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   473
  interpret X: prob_space "distr M S X"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   474
    by (rule prob_space_distr) fact
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   475
  interpret Y: prob_space "distr M T Y"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   476
    by (rule prob_space_distr) fact
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   477
  interpret XY: pair_prob_space "distr M S X" "distr M T Y" by default
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   478
  interpret P: information_space P b unfolding P_def by default (rule b_gt_1)
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   479
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   480
  interpret Q: prob_space Q unfolding Q_def
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   481
    by (rule prob_space_distr) simp
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   482
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   483
  { assume "distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   484
    then have [simp]: "Q = P"  unfolding Q_def P_def by simp
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   485
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   486
    show ac: "absolutely_continuous P Q" by (simp add: absolutely_continuous_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   487
    then have ed: "entropy_density b P Q \<in> borel_measurable P"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   488
      by (rule P.measurable_entropy_density) simp
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   489
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   490
    have "AE x in P. 1 = RN_deriv P Q x"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   491
    proof (rule P.RN_deriv_unique)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   492
      show "density P (\<lambda>x. 1) = Q"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   493
        unfolding `Q = P` by (intro measure_eqI) (auto simp: emeasure_density)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   494
    qed auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   495
    then have ae_0: "AE x in P. entropy_density b P Q x = 0"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   496
      by eventually_elim (auto simp: entropy_density_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   497
    then have "integrable P (entropy_density b P Q) \<longleftrightarrow> integrable Q (\<lambda>x. 0)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   498
      using ed unfolding `Q = P` by (intro integrable_cong_AE) auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   499
    then show "integrable Q (entropy_density b P Q)" by simp
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   500
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   501
    show "mutual_information b S T X Y = 0"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   502
      unfolding mutual_information_def KL_divergence_def P_def[symmetric] Q_def[symmetric] `Q = P`
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   503
      using ae_0 by (simp cong: integral_cong_AE) }
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   504
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   505
  { assume ac: "absolutely_continuous P Q"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   506
    assume int: "integrable Q (entropy_density b P Q)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   507
    assume I_eq_0: "mutual_information b S T X Y = 0"
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   508
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   509
    have eq: "Q = P"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   510
    proof (rule P.KL_eq_0_iff_eq_ac[THEN iffD1])
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   511
      show "prob_space Q" by unfold_locales
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   512
      show "absolutely_continuous P Q" by fact
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   513
      show "integrable Q (entropy_density b P Q)" by fact
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   514
      show "sets Q = sets P" by (simp add: P_def Q_def sets_pair_measure)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   515
      show "KL_divergence b P Q = 0"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   516
        using I_eq_0 unfolding mutual_information_def by (simp add: P_def Q_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   517
    qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   518
    then show "distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   519
      unfolding P_def Q_def .. }
43340
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   520
qed
60e181c4eae4 lemma: independence is equal to mutual information = 0
hoelzl
parents: 42148
diff changeset
   521
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   522
abbreviation (in information_space)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   523
  mutual_information_Pow ("\<I>'(_ ; _')") where
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   524
  "\<I>(X ; Y) \<equiv> mutual_information b (count_space (X`space M)) (count_space (Y`space M)) 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
   525
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   526
lemma (in information_space)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   527
  fixes Pxy :: "'b \<times> 'c \<Rightarrow> real" and Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
49803
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   528
  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   529
  assumes Fx: "finite_entropy S X Px" and Fy: "finite_entropy T Y Py"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   530
  assumes Fxy: "finite_entropy (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   531
  defines "f \<equiv> \<lambda>x. Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x)))"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   532
  shows mutual_information_distr': "mutual_information b S T X Y = integral\<^isup>L (S \<Otimes>\<^isub>M T) f" (is "?M = ?R")
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   533
    and mutual_information_nonneg': "0 \<le> mutual_information b S T X Y"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   534
proof -
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   535
  have Px: "distributed M S X Px"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   536
    using Fx by (auto simp: finite_entropy_def)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   537
  have Py: "distributed M T Y Py"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   538
    using Fy by (auto simp: finite_entropy_def)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   539
  have Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   540
    using Fxy by (auto simp: finite_entropy_def)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   541
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   542
  have X: "random_variable S X"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   543
    using Px by auto
49803
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   544
  have Y: "random_variable T Y"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
   545
    using Py by auto
49803
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   546
  interpret S: sigma_finite_measure S by fact
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   547
  interpret T: sigma_finite_measure T by fact
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   548
  interpret ST: pair_sigma_finite S T ..
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   549
  interpret X: prob_space "distr M S X" using X by (rule prob_space_distr)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   550
  interpret Y: prob_space "distr M T Y" using Y by (rule prob_space_distr)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   551
  interpret XY: pair_prob_space "distr M S X" "distr M T Y" ..
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   552
  let ?P = "S \<Otimes>\<^isub>M T"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   553
  let ?D = "distr M ?P (\<lambda>x. (X x, Y x))"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   554
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   555
  { fix A assume "A \<in> sets S"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   556
    with X Y have "emeasure (distr M S X) A = emeasure ?D (A \<times> space T)"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   557
      by (auto simp: emeasure_distr measurable_Pair measurable_space
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   558
               intro!: arg_cong[where f="emeasure M"]) }
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   559
  note marginal_eq1 = this
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   560
  { fix A assume "A \<in> sets T"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   561
    with X Y have "emeasure (distr M T Y) A = emeasure ?D (space S \<times> A)"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   562
      by (auto simp: emeasure_distr measurable_Pair measurable_space
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   563
               intro!: arg_cong[where f="emeasure M"]) }
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   564
  note marginal_eq2 = this
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   565
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   566
  have eq: "(\<lambda>x. ereal (Px (fst x) * Py (snd x))) = (\<lambda>(x, y). ereal (Px x) * ereal (Py y))"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   567
    by auto
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   568
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   569
  have distr_eq: "distr M S X \<Otimes>\<^isub>M distr M T Y = density ?P (\<lambda>x. ereal (Px (fst x) * Py (snd x)))"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   570
    unfolding Px(1)[THEN distributed_distr_eq_density] Py(1)[THEN distributed_distr_eq_density] eq
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   571
  proof (subst pair_measure_density)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   572
    show "(\<lambda>x. ereal (Px x)) \<in> borel_measurable S" "(\<lambda>y. ereal (Py y)) \<in> borel_measurable T"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   573
      "AE x in S. 0 \<le> ereal (Px x)" "AE y in T. 0 \<le> ereal (Py y)"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   574
      using Px Py by (auto simp: distributed_def)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   575
    show "sigma_finite_measure (density T Py)" unfolding Py(1)[THEN distributed_distr_eq_density, symmetric] ..
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   576
  qed (fact | simp)+
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   577
  
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   578
  have M: "?M = KL_divergence b (density ?P (\<lambda>x. ereal (Px (fst x) * Py (snd x)))) (density ?P (\<lambda>x. ereal (Pxy x)))"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   579
    unfolding mutual_information_def distr_eq Pxy(1)[THEN distributed_distr_eq_density] ..
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   580
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   581
  from Px Py have f: "(\<lambda>x. Px (fst x) * Py (snd x)) \<in> borel_measurable ?P"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   582
    by (intro borel_measurable_times) (auto intro: distributed_real_measurable measurable_fst'' measurable_snd'')
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   583
  have PxPy_nonneg: "AE x in ?P. 0 \<le> Px (fst x) * Py (snd x)"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   584
  proof (rule ST.AE_pair_measure)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   585
    show "{x \<in> space ?P. 0 \<le> Px (fst x) * Py (snd x)} \<in> sets ?P"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   586
      using f by auto
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   587
    show "AE x in S. AE y in T. 0 \<le> Px (fst (x, y)) * Py (snd (x, y))"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   588
      using Px Py by (auto simp: zero_le_mult_iff dest!: distributed_real_AE)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   589
  qed
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   590
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   591
  have "(AE x in ?P. Px (fst x) = 0 \<longrightarrow> Pxy x = 0)"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   592
    by (rule subdensity_real[OF measurable_fst Pxy Px]) auto
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   593
  moreover
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   594
  have "(AE x in ?P. Py (snd x) = 0 \<longrightarrow> Pxy x = 0)"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   595
    by (rule subdensity_real[OF measurable_snd Pxy Py]) auto
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   596
  ultimately have ac: "AE x in ?P. Px (fst x) * Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   597
    by eventually_elim auto
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   598
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   599
  show "?M = ?R"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   600
    unfolding M f_def
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   601
    using b_gt_1 f PxPy_nonneg Pxy[THEN distributed_real_measurable] Pxy[THEN distributed_real_AE] ac
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   602
    by (rule ST.KL_density_density)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   603
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   604
  have X: "X = fst \<circ> (\<lambda>x. (X x, Y x))" and Y: "Y = snd \<circ> (\<lambda>x. (X x, Y x))"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   605
    by auto
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   606
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   607
  have "integrable (S \<Otimes>\<^isub>M T) (\<lambda>x. Pxy x * log b (Pxy x) - Pxy x * log b (Px (fst x)) - Pxy x * log b (Py (snd x)))"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   608
    using finite_entropy_integrable[OF Fxy]
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   609
    using finite_entropy_integrable_transform[OF Fx Pxy, of fst]
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   610
    using finite_entropy_integrable_transform[OF Fy Pxy, of snd]
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   611
    by simp
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   612
  moreover have "f \<in> borel_measurable (S \<Otimes>\<^isub>M T)"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   613
    unfolding f_def using Px Py Pxy
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   614
    by (auto intro: distributed_real_measurable measurable_fst'' measurable_snd''
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   615
      intro!: borel_measurable_times borel_measurable_log borel_measurable_divide)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   616
  ultimately have int: "integrable (S \<Otimes>\<^isub>M T) f"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   617
    apply (rule integrable_cong_AE_imp)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   618
    using
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   619
      distributed_transform_AE[OF measurable_fst ac_fst, of T, OF T Px]
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   620
      distributed_transform_AE[OF measurable_snd ac_snd, of _ _ _ _ S, OF T Py]
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   621
      subdensity_real[OF measurable_fst Pxy Px X]
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   622
      subdensity_real[OF measurable_snd Pxy Py Y]
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   623
      distributed_real_AE[OF Pxy]
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   624
    by eventually_elim
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   625
       (auto simp: f_def log_divide_eq log_mult_eq field_simps zero_less_mult_iff mult_nonneg_nonneg)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   626
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   627
  show "0 \<le> ?M" unfolding M
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   628
  proof (rule ST.KL_density_density_nonneg
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   629
    [OF b_gt_1 f PxPy_nonneg _ Pxy[THEN distributed_real_measurable] Pxy[THEN distributed_real_AE] _ ac int[unfolded f_def]])
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   630
    show "prob_space (density (S \<Otimes>\<^isub>M T) (\<lambda>x. ereal (Pxy x))) "
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   631
      unfolding distributed_distr_eq_density[OF Pxy, symmetric]
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   632
      using distributed_measurable[OF Pxy] by (rule prob_space_distr)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   633
    show "prob_space (density (S \<Otimes>\<^isub>M T) (\<lambda>x. ereal (Px (fst x) * Py (snd x))))"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   634
      unfolding distr_eq[symmetric] by unfold_locales
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   635
  qed
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   636
qed
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   637
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   638
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   639
lemma (in information_space)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
   640
  fixes Pxy :: "'b \<times> 'c \<Rightarrow> real" and Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   641
  assumes "sigma_finite_measure S" "sigma_finite_measure T"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   642
  assumes Px: "distributed M S X Px" and Py: "distributed M T Y Py"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   643
  assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   644
  defines "f \<equiv> \<lambda>x. Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x)))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   645
  shows mutual_information_distr: "mutual_information b S T X Y = integral\<^isup>L (S \<Otimes>\<^isub>M T) f" (is "?M = ?R")
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   646
    and mutual_information_nonneg: "integrable (S \<Otimes>\<^isub>M T) f \<Longrightarrow> 0 \<le> mutual_information b S T X Y"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   647
proof -
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   648
  have X: "random_variable S X"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   649
    using Px by (auto simp: distributed_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   650
  have Y: "random_variable T Y"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   651
    using Py by (auto simp: distributed_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   652
  interpret S: sigma_finite_measure S by fact
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   653
  interpret T: sigma_finite_measure T by fact
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   654
  interpret ST: pair_sigma_finite S T ..
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   655
  interpret X: prob_space "distr M S X" using X by (rule prob_space_distr)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   656
  interpret Y: prob_space "distr M T Y" using Y by (rule prob_space_distr)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   657
  interpret XY: pair_prob_space "distr M S X" "distr M T Y" ..
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   658
  let ?P = "S \<Otimes>\<^isub>M T"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   659
  let ?D = "distr M ?P (\<lambda>x. (X x, Y x))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   660
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   661
  { fix A assume "A \<in> sets S"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   662
    with X Y have "emeasure (distr M S X) A = emeasure ?D (A \<times> space T)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   663
      by (auto simp: emeasure_distr measurable_Pair measurable_space
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   664
               intro!: arg_cong[where f="emeasure M"]) }
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   665
  note marginal_eq1 = this
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   666
  { fix A assume "A \<in> sets T"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   667
    with X Y have "emeasure (distr M T Y) A = emeasure ?D (space S \<times> A)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   668
      by (auto simp: emeasure_distr measurable_Pair measurable_space
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   669
               intro!: arg_cong[where f="emeasure M"]) }
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   670
  note marginal_eq2 = this
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   671
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   672
  have eq: "(\<lambda>x. ereal (Px (fst x) * Py (snd x))) = (\<lambda>(x, y). ereal (Px x) * ereal (Py y))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   673
    by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   674
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   675
  have distr_eq: "distr M S X \<Otimes>\<^isub>M distr M T Y = density ?P (\<lambda>x. ereal (Px (fst x) * Py (snd x)))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   676
    unfolding Px(1)[THEN distributed_distr_eq_density] Py(1)[THEN distributed_distr_eq_density] eq
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   677
  proof (subst pair_measure_density)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   678
    show "(\<lambda>x. ereal (Px x)) \<in> borel_measurable S" "(\<lambda>y. ereal (Py y)) \<in> borel_measurable T"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   679
      "AE x in S. 0 \<le> ereal (Px x)" "AE y in T. 0 \<le> ereal (Py y)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   680
      using Px Py by (auto simp: distributed_def)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   681
    show "sigma_finite_measure (density T Py)" unfolding Py(1)[THEN distributed_distr_eq_density, symmetric] ..
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   682
  qed (fact | simp)+
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   683
  
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   684
  have M: "?M = KL_divergence b (density ?P (\<lambda>x. ereal (Px (fst x) * Py (snd x)))) (density ?P (\<lambda>x. ereal (Pxy x)))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   685
    unfolding mutual_information_def distr_eq Pxy(1)[THEN distributed_distr_eq_density] ..
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   686
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   687
  from Px Py have f: "(\<lambda>x. Px (fst x) * Py (snd x)) \<in> borel_measurable ?P"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   688
    by (intro borel_measurable_times) (auto intro: distributed_real_measurable measurable_fst'' measurable_snd'')
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   689
  have PxPy_nonneg: "AE x in ?P. 0 \<le> Px (fst x) * Py (snd x)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   690
  proof (rule ST.AE_pair_measure)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   691
    show "{x \<in> space ?P. 0 \<le> Px (fst x) * Py (snd x)} \<in> sets ?P"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   692
      using f by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   693
    show "AE x in S. AE y in T. 0 \<le> Px (fst (x, y)) * Py (snd (x, y))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   694
      using Px Py by (auto simp: zero_le_mult_iff dest!: distributed_real_AE)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   695
  qed
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   696
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   697
  have "(AE x in ?P. Px (fst x) = 0 \<longrightarrow> Pxy x = 0)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   698
    by (rule subdensity_real[OF measurable_fst Pxy Px]) auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   699
  moreover
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   700
  have "(AE x in ?P. Py (snd x) = 0 \<longrightarrow> Pxy x = 0)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   701
    by (rule subdensity_real[OF measurable_snd Pxy Py]) auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   702
  ultimately have ac: "AE x in ?P. Px (fst x) * Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   703
    by eventually_elim auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   704
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   705
  show "?M = ?R"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   706
    unfolding M f_def
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   707
    using b_gt_1 f PxPy_nonneg Pxy[THEN distributed_real_measurable] Pxy[THEN distributed_real_AE] ac
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   708
    by (rule ST.KL_density_density)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   709
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   710
  assume int: "integrable (S \<Otimes>\<^isub>M T) f"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   711
  show "0 \<le> ?M" unfolding M
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   712
  proof (rule ST.KL_density_density_nonneg
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   713
    [OF b_gt_1 f PxPy_nonneg _ Pxy[THEN distributed_real_measurable] Pxy[THEN distributed_real_AE] _ ac int[unfolded f_def]])
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   714
    show "prob_space (density (S \<Otimes>\<^isub>M T) (\<lambda>x. ereal (Pxy x))) "
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   715
      unfolding distributed_distr_eq_density[OF Pxy, symmetric]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   716
      using distributed_measurable[OF Pxy] by (rule prob_space_distr)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   717
    show "prob_space (density (S \<Otimes>\<^isub>M T) (\<lambda>x. ereal (Px (fst x) * Py (snd x))))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   718
      unfolding distr_eq[symmetric] by unfold_locales
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   719
  qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   720
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   721
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   722
lemma (in information_space)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   723
  fixes Pxy :: "'b \<times> 'c \<Rightarrow> real" and Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   724
  assumes "sigma_finite_measure S" "sigma_finite_measure T"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   725
  assumes Px: "distributed M S X Px" and Py: "distributed M T Y Py"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   726
  assumes Pxy: "distributed M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x)) Pxy"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   727
  assumes ae: "AE x in S. AE y in T. Pxy (x, y) = Px x * Py y"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   728
  shows mutual_information_eq_0: "mutual_information b S T X Y = 0"
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   729
proof -
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   730
  interpret S: sigma_finite_measure S by fact
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   731
  interpret T: sigma_finite_measure T by fact
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   732
  interpret ST: pair_sigma_finite S T ..
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   733
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   734
  have "AE x in S \<Otimes>\<^isub>M T. Px (fst x) = 0 \<longrightarrow> Pxy x = 0"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   735
    by (rule subdensity_real[OF measurable_fst Pxy Px]) auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   736
  moreover
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   737
  have "AE x in S \<Otimes>\<^isub>M T. Py (snd x) = 0 \<longrightarrow> Pxy x = 0"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   738
    by (rule subdensity_real[OF measurable_snd Pxy Py]) auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   739
  moreover 
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   740
  have "AE x in S \<Otimes>\<^isub>M T. Pxy x = Px (fst x) * Py (snd x)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   741
    using distributed_real_measurable[OF Px] distributed_real_measurable[OF Py] distributed_real_measurable[OF Pxy]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   742
    by (intro ST.AE_pair_measure) (auto simp: ae intro!: measurable_snd'' measurable_fst'')
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   743
  ultimately have "AE x in S \<Otimes>\<^isub>M T. Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x))) = 0"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   744
    by eventually_elim simp
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   745
  then have "(\<integral>x. Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x))) \<partial>(S \<Otimes>\<^isub>M T)) = (\<integral>x. 0 \<partial>(S \<Otimes>\<^isub>M T))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   746
    by (rule integral_cong_AE)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   747
  then show ?thesis
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   748
    by (subst mutual_information_distr[OF assms(1-5)]) simp
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   749
qed
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   750
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   751
lemma (in information_space) mutual_information_simple_distributed:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   752
  assumes X: "simple_distributed M X Px" and Y: "simple_distributed M Y Py"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   753
  assumes XY: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   754
  shows "\<I>(X ; Y) = (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x))`space M. Pxy (x, y) * log b (Pxy (x, y) / (Px x * Py y)))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   755
proof (subst mutual_information_distr[OF _ _ simple_distributed[OF X] simple_distributed[OF Y] simple_distributed_joint[OF XY]])
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   756
  note fin = simple_distributed_joint_finite[OF XY, simp]
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   757
  show "sigma_finite_measure (count_space (X ` space M))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   758
    by (simp add: sigma_finite_measure_count_space_finite)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   759
  show "sigma_finite_measure (count_space (Y ` space M))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   760
    by (simp add: sigma_finite_measure_count_space_finite)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   761
  let ?Pxy = "\<lambda>x. (if x \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy x else 0)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   762
  let ?f = "\<lambda>x. ?Pxy x * log b (?Pxy x / (Px (fst x) * Py (snd x)))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   763
  have "\<And>x. ?f x = (if x \<in> (\<lambda>x. (X x, Y x)) ` space M then Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x))) else 0)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   764
    by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   765
  with fin show "(\<integral> x. ?f x \<partial>(count_space (X ` space M) \<Otimes>\<^isub>M count_space (Y ` space M))) =
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   766
    (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / (Px x * Py y)))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   767
    by (auto simp add: pair_measure_count_space lebesgue_integral_count_space_finite setsum_cases split_beta'
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   768
             intro!: setsum_cong)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   769
qed
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   770
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   771
lemma (in information_space)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   772
  fixes Pxy :: "'b \<times> 'c \<Rightarrow> real" and Px :: "'b \<Rightarrow> real" and Py :: "'c \<Rightarrow> real"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   773
  assumes Px: "simple_distributed M X Px" and Py: "simple_distributed M Y Py"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   774
  assumes Pxy: "simple_distributed M (\<lambda>x. (X x, Y x)) Pxy"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   775
  assumes ae: "\<forall>x\<in>space M. Pxy (X x, Y x) = Px (X x) * Py (Y x)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   776
  shows mutual_information_eq_0_simple: "\<I>(X ; Y) = 0"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   777
proof (subst mutual_information_simple_distributed[OF Px Py Pxy])
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   778
  have "(\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. Pxy (x, y) * log b (Pxy (x, y) / (Px x * Py y))) =
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   779
    (\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M. 0)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   780
    by (intro setsum_cong) (auto simp: ae)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   781
  then show "(\<Sum>(x, y)\<in>(\<lambda>x. (X x, Y x)) ` space M.
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   782
    Pxy (x, y) * log b (Pxy (x, y) / (Px x * Py y))) = 0" by simp
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   783
qed
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   784
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   785
subsection {* Entropy *}
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   786
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   787
definition (in prob_space) entropy :: "real \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> real" where
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   788
  "entropy b S X = - KL_divergence b S (distr M S X)"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   789
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   790
abbreviation (in information_space)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   791
  entropy_Pow ("\<H>'(_')") where
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   792
  "\<H>(X) \<equiv> entropy b (count_space (X`space M)) X"
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41833
diff changeset
   793
49791
e0854abfb3fc alternative definition of conditional entropy
hoelzl
parents: 49790
diff changeset
   794
lemma (in prob_space) distributed_RN_deriv:
e0854abfb3fc alternative definition of conditional entropy
hoelzl
parents: 49790
diff changeset
   795
  assumes X: "distributed M S X Px"
e0854abfb3fc alternative definition of conditional entropy
hoelzl
parents: 49790
diff changeset
   796
  shows "AE x in S. RN_deriv S (density S Px) x = Px x"
e0854abfb3fc alternative definition of conditional entropy
hoelzl
parents: 49790
diff changeset
   797
proof -
e0854abfb3fc alternative definition of conditional entropy
hoelzl
parents: 49790
diff changeset
   798
  note D = distributed_measurable[OF X] distributed_borel_measurable[OF X] distributed_AE[OF X]
e0854abfb3fc alternative definition of conditional entropy
hoelzl
parents: 49790
diff changeset
   799
  interpret X: prob_space "distr M S X"
e0854abfb3fc alternative definition of conditional entropy
hoelzl
parents: 49790
diff changeset
   800
    using D(1) by (rule prob_space_distr)
e0854abfb3fc alternative definition of conditional entropy
hoelzl
parents: 49790
diff changeset
   801
e0854abfb3fc alternative definition of conditional entropy
hoelzl
parents: 49790
diff changeset
   802
  have sf: "sigma_finite_measure (distr M S X)" by default
e0854abfb3fc alternative definition of conditional entropy
hoelzl
parents: 49790
diff changeset
   803
  show ?thesis
e0854abfb3fc alternative definition of conditional entropy
hoelzl
parents: 49790
diff changeset
   804
    using D
e0854abfb3fc alternative definition of conditional entropy
hoelzl
parents: 49790
diff changeset
   805
    apply (subst eq_commute)
e0854abfb3fc alternative definition of conditional entropy
hoelzl
parents: 49790
diff changeset
   806
    apply (intro RN_deriv_unique_sigma_finite)
e0854abfb3fc alternative definition of conditional entropy
hoelzl
parents: 49790
diff changeset
   807
    apply (auto intro: divide_nonneg_nonneg measure_nonneg
e0854abfb3fc alternative definition of conditional entropy
hoelzl
parents: 49790
diff changeset
   808
             simp: distributed_distr_eq_density[symmetric, OF X] sf)
e0854abfb3fc alternative definition of conditional entropy
hoelzl
parents: 49790
diff changeset
   809
    done
e0854abfb3fc alternative definition of conditional entropy
hoelzl
parents: 49790
diff changeset
   810
qed
e0854abfb3fc alternative definition of conditional entropy
hoelzl
parents: 49790
diff changeset
   811
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49787
diff changeset
   812
lemma (in information_space)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   813
  fixes X :: "'a \<Rightarrow> 'b"
49785
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   814
  assumes X: "distributed M MX X f"
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49787
diff changeset
   815
  shows entropy_distr: "entropy b MX X = - (\<integral>x. f x * log b (f x) \<partial>MX)" (is ?eq)
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49787
diff changeset
   816
proof -
49785
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   817
  note D = distributed_measurable[OF X] distributed_borel_measurable[OF X] distributed_AE[OF X]
49791
e0854abfb3fc alternative definition of conditional entropy
hoelzl
parents: 49790
diff changeset
   818
  note ae = distributed_RN_deriv[OF X]
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49787
diff changeset
   819
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49787
diff changeset
   820
  have ae_eq: "AE x in distr M MX X. log b (real (RN_deriv MX (distr M MX X) x)) =
49785
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   821
    log b (f x)"
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   822
    unfolding distributed_distr_eq_density[OF X]
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   823
    apply (subst AE_density)
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   824
    using D apply simp
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   825
    using ae apply eventually_elim
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   826
    apply auto
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   827
    done
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49787
diff changeset
   828
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49787
diff changeset
   829
  have int_eq: "- (\<integral> x. log b (f x) \<partial>distr M MX X) = - (\<integral> x. f x * log b (f x) \<partial>MX)"
49785
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   830
    unfolding distributed_distr_eq_density[OF X]
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   831
    using D
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   832
    by (subst integral_density)
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   833
       (auto simp: borel_measurable_ereal_iff)
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49787
diff changeset
   834
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49787
diff changeset
   835
  show ?eq
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49787
diff changeset
   836
    unfolding entropy_def KL_divergence_def entropy_density_def comp_def
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49787
diff changeset
   837
    apply (subst integral_cong_AE)
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49787
diff changeset
   838
    apply (rule ae_eq)
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49787
diff changeset
   839
    apply (rule int_eq)
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49787
diff changeset
   840
    done
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49787
diff changeset
   841
qed
49785
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   842
49786
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   843
lemma (in prob_space) distributed_imp_emeasure_nonzero:
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   844
  assumes X: "distributed M MX X Px"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   845
  shows "emeasure MX {x \<in> space MX. Px x \<noteq> 0} \<noteq> 0"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   846
proof
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   847
  note Px = distributed_borel_measurable[OF X] distributed_AE[OF X]
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   848
  interpret X: prob_space "distr M MX X"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   849
    using distributed_measurable[OF X] by (rule prob_space_distr)
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   850
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   851
  assume "emeasure MX {x \<in> space MX. Px x \<noteq> 0} = 0"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   852
  with Px have "AE x in MX. Px x = 0"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   853
    by (intro AE_I[OF subset_refl]) (auto simp: borel_measurable_ereal_iff)
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   854
  moreover
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   855
  from X.emeasure_space_1 have "(\<integral>\<^isup>+x. Px x \<partial>MX) = 1"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   856
    unfolding distributed_distr_eq_density[OF X] using Px
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   857
    by (subst (asm) emeasure_density)
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   858
       (auto simp: borel_measurable_ereal_iff intro!: integral_cong cong: positive_integral_cong)
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   859
  ultimately show False
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   860
    by (simp add: positive_integral_cong_AE)
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   861
qed
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   862
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   863
lemma (in information_space) entropy_le:
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   864
  fixes Px :: "'b \<Rightarrow> real" and MX :: "'b measure"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   865
  assumes X: "distributed M MX X Px"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   866
  and fin: "emeasure MX {x \<in> space MX. Px x \<noteq> 0} \<noteq> \<infinity>"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   867
  and int: "integrable MX (\<lambda>x. - Px x * log b (Px x))"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   868
  shows "entropy b MX X \<le> log b (measure MX {x \<in> space MX. Px x \<noteq> 0})"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   869
proof -
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   870
  note Px = distributed_borel_measurable[OF X] distributed_AE[OF X]
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   871
  interpret X: prob_space "distr M MX X"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   872
    using distributed_measurable[OF X] by (rule prob_space_distr)
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   873
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   874
  have " - log b (measure MX {x \<in> space MX. Px x \<noteq> 0}) = 
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   875
    - log b (\<integral> x. indicator {x \<in> space MX. Px x \<noteq> 0} x \<partial>MX)"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   876
    using Px fin
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   877
    by (subst integral_indicator) (auto simp: measure_def borel_measurable_ereal_iff)
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   878
  also have "- log b (\<integral> x. indicator {x \<in> space MX. Px x \<noteq> 0} x \<partial>MX) = - log b (\<integral> x. 1 / Px x \<partial>distr M MX X)"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   879
    unfolding distributed_distr_eq_density[OF X] using Px
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   880
    apply (intro arg_cong[where f="log b"] arg_cong[where f=uminus])
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   881
    by (subst integral_density) (auto simp: borel_measurable_ereal_iff intro!: integral_cong)
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   882
  also have "\<dots> \<le> (\<integral> x. - log b (1 / Px x) \<partial>distr M MX X)"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   883
  proof (rule X.jensens_inequality[of "\<lambda>x. 1 / Px x" "{0<..}" 0 1 "\<lambda>x. - log b x"])
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   884
    show "AE x in distr M MX X. 1 / Px x \<in> {0<..}"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   885
      unfolding distributed_distr_eq_density[OF X]
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   886
      using Px by (auto simp: AE_density)
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   887
    have [simp]: "\<And>x. x \<in> space MX \<Longrightarrow> ereal (if Px x = 0 then 0 else 1) = indicator {x \<in> space MX. Px x \<noteq> 0} x"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   888
      by (auto simp: one_ereal_def)
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   889
    have "(\<integral>\<^isup>+ x. max 0 (ereal (- (if Px x = 0 then 0 else 1))) \<partial>MX) = (\<integral>\<^isup>+ x. 0 \<partial>MX)"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   890
      by (intro positive_integral_cong) (auto split: split_max)
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   891
    then show "integrable (distr M MX X) (\<lambda>x. 1 / Px x)"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   892
      unfolding distributed_distr_eq_density[OF X] using Px
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   893
      by (auto simp: positive_integral_density integrable_def borel_measurable_ereal_iff fin positive_integral_max_0
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   894
              cong: positive_integral_cong)
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   895
    have "integrable MX (\<lambda>x. Px x * log b (1 / Px x)) =
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   896
      integrable MX (\<lambda>x. - Px x * log b (Px x))"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   897
      using Px
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   898
      by (intro integrable_cong_AE)
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   899
         (auto simp: borel_measurable_ereal_iff log_divide_eq
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   900
                  intro!: measurable_If)
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   901
    then show "integrable (distr M MX X) (\<lambda>x. - log b (1 / Px x))"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   902
      unfolding distributed_distr_eq_density[OF X]
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   903
      using Px int
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   904
      by (subst integral_density) (auto simp: borel_measurable_ereal_iff)
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   905
  qed (auto simp: minus_log_convex[OF b_gt_1])
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   906
  also have "\<dots> = (\<integral> x. log b (Px x) \<partial>distr M MX X)"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   907
    unfolding distributed_distr_eq_density[OF X] using Px
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   908
    by (intro integral_cong_AE) (auto simp: AE_density log_divide_eq)
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   909
  also have "\<dots> = - entropy b MX X"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   910
    unfolding distributed_distr_eq_density[OF X] using Px
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   911
    by (subst entropy_distr[OF X]) (auto simp: borel_measurable_ereal_iff integral_density)
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   912
  finally show ?thesis
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   913
    by simp
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   914
qed
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   915
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   916
lemma (in information_space) entropy_le_space:
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   917
  fixes Px :: "'b \<Rightarrow> real" and MX :: "'b measure"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   918
  assumes X: "distributed M MX X Px"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   919
  and fin: "finite_measure MX"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   920
  and int: "integrable MX (\<lambda>x. - Px x * log b (Px x))"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   921
  shows "entropy b MX X \<le> log b (measure MX (space MX))"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   922
proof -
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   923
  note Px = distributed_borel_measurable[OF X] distributed_AE[OF X]
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   924
  interpret finite_measure MX by fact
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   925
  have "entropy b MX X \<le> log b (measure MX {x \<in> space MX. Px x \<noteq> 0})"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   926
    using int X by (intro entropy_le) auto
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   927
  also have "\<dots> \<le> log b (measure MX (space MX))"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   928
    using Px distributed_imp_emeasure_nonzero[OF X]
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   929
    by (intro log_le)
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   930
       (auto intro!: borel_measurable_ereal_iff finite_measure_mono b_gt_1
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   931
                     less_le[THEN iffD2] measure_nonneg simp: emeasure_eq_measure)
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   932
  finally show ?thesis .
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   933
qed
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   934
49785
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   935
lemma (in prob_space) uniform_distributed_params:
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   936
  assumes X: "distributed M MX X (\<lambda>x. indicator A x / measure MX A)"
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   937
  shows "A \<in> sets MX" "measure MX A \<noteq> 0"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   938
proof -
49785
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   939
  interpret X: prob_space "distr M MX X"
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   940
    using distributed_measurable[OF X] by (rule prob_space_distr)
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   941
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   942
  show "measure MX A \<noteq> 0"
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   943
  proof
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   944
    assume "measure MX A = 0"
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   945
    with X.emeasure_space_1 X.prob_space distributed_distr_eq_density[OF X]
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   946
    show False
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   947
      by (simp add: emeasure_density zero_ereal_def[symmetric])
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   948
  qed
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   949
  with measure_notin_sets[of A MX] show "A \<in> sets MX"
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   950
    by blast
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   951
qed
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
   952
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   953
lemma (in information_space) entropy_uniform:
49785
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   954
  assumes X: "distributed M MX X (\<lambda>x. indicator A x / measure MX A)" (is "distributed _ _ _ ?f")
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   955
  shows "entropy b MX X = log b (measure MX A)"
49785
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   956
proof (subst entropy_distr[OF X])
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   957
  have [simp]: "emeasure MX A \<noteq> \<infinity>"
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   958
    using uniform_distributed_params[OF X] by (auto simp add: measure_def)
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   959
  have eq: "(\<integral> x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \<partial>MX) =
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   960
    (\<integral> x. (- log b (measure MX A) / measure MX A) * indicator A x \<partial>MX)"
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   961
    using measure_nonneg[of MX A] uniform_distributed_params[OF X]
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   962
    by (auto intro!: integral_cong split: split_indicator simp: log_divide_eq)
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   963
  show "- (\<integral> x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \<partial>MX) =
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   964
    log b (measure MX A)"
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   965
    unfolding eq using uniform_distributed_params[OF X]
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   966
    by (subst lebesgue_integral_cmult) (auto simp: measure_def)
0a8adca22974 simplified entropy_uniform
hoelzl
parents: 49776
diff changeset
   967
qed
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
   968
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   969
lemma (in information_space) entropy_simple_distributed:
49786
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   970
  "simple_distributed M X f \<Longrightarrow> \<H>(X) = - (\<Sum>x\<in>X`space M. f x * log b (f x))"
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   971
  by (subst entropy_distr[OF simple_distributed])
f33d5f009627 continuous version of entropy_le
hoelzl
parents: 49785
diff changeset
   972
     (auto simp add: lebesgue_integral_count_space_finite)
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   973
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   974
lemma (in information_space) entropy_le_card_not_0:
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   975
  assumes X: "simple_distributed M X f"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
   976
  shows "\<H>(X) \<le> log b (card (X ` space M \<inter> {x. f x \<noteq> 0}))"
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   977
proof -
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
   978
  let ?X = "count_space (X`space M)"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
   979
  have "\<H>(X) \<le> log b (measure ?X {x \<in> space ?X. f x \<noteq> 0})"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
   980
    by (rule entropy_le[OF simple_distributed[OF X]])
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
   981
       (simp_all add: simple_distributed_finite[OF X] subset_eq integrable_count_space emeasure_count_space)
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
   982
  also have "measure ?X {x \<in> space ?X. f x \<noteq> 0} = card (X ` space M \<inter> {x. f x \<noteq> 0})"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
   983
    by (simp_all add: simple_distributed_finite[OF X] subset_eq emeasure_count_space measure_def Int_def)
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
   984
  finally show ?thesis .
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   985
qed
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   986
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   987
lemma (in information_space) entropy_le_card:
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
   988
  assumes X: "simple_distributed M X f"
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
   989
  shows "\<H>(X) \<le> log b (real (card (X ` space M)))"
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
   990
proof -
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
   991
  let ?X = "count_space (X`space M)"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
   992
  have "\<H>(X) \<le> log b (measure ?X (space ?X))"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
   993
    by (rule entropy_le_space[OF simple_distributed[OF X]])
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
   994
       (simp_all add: simple_distributed_finite[OF X] subset_eq integrable_count_space emeasure_count_space finite_measure_count_space)
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
   995
  also have "measure ?X (space ?X) = card (X ` space M)"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
   996
    by (simp_all add: simple_distributed_finite[OF X] subset_eq emeasure_count_space measure_def)
39097
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   997
  finally show ?thesis .
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   998
qed
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
   999
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
  1000
subsection {* Conditional Mutual Information *}
943c7b348524 Moved lemmas to appropriate locations
hoelzl
parents: 39092
diff changeset
  1001
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
  1002
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
  1003
  "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
  1004
    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
  1005
    mutual_information b MX MZ X Z"
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
  1006
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1007
abbreviation (in information_space)
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1008
  conditional_mutual_information_Pow ("\<I>'( _ ; _ | _ ')") where
36624
25153c08655e Cleanup information theory
hoelzl
parents: 36623
diff changeset
  1009
  "\<I>(X ; Y | Z) \<equiv> conditional_mutual_information b
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1010
    (count_space (X ` space M)) (count_space (Y ` space M)) (count_space (Z ` space M)) X Y Z"
36080
0d9affa4e73c Added Information theory and Example: dining cryptographers
hoelzl
parents:
diff changeset
  1011
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1012
lemma (in information_space)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1013
  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" and P: "sigma_finite_measure P"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1014
  assumes Px[measurable]: "distributed M S X Px"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1015
  assumes Pz[measurable]: "distributed M P Z Pz"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1016
  assumes Pyz[measurable]: "distributed M (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x)) Pyz"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1017
  assumes Pxz[measurable]: "distributed M (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) Pxz"
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1018
  assumes Pxyz[measurable]: "distributed M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Y x, Z x)) Pxyz"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1019
  assumes I1: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Px x * Pyz (y, z))))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1020
  assumes I2: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxz (x, z) / (Px x * Pz z)))"
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1021
  shows conditional_mutual_information_generic_eq: "conditional_mutual_information b S T P X Y Z
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1022
    = (\<integral>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))" (is "?eq")
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1023
    and conditional_mutual_information_generic_nonneg: "0 \<le> conditional_mutual_information b S T P X Y Z" (is "?nonneg")
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1024
proof -
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1025
  interpret S: sigma_finite_measure S by fact
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1026
  interpret T: sigma_finite_measure T by fact
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1027
  interpret P: sigma_finite_measure P by fact
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1028
  interpret TP: pair_sigma_finite T P ..
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1029
  interpret SP: pair_sigma_finite S P ..
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1030
  interpret ST: pair_sigma_finite S T ..
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1031
  interpret SPT: pair_sigma_finite "S \<Otimes>\<^isub>M P" T ..
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1032
  interpret STP: pair_sigma_finite S "T \<Otimes>\<^isub>M P" ..
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1033
  interpret TPS: pair_sigma_finite "T \<Otimes>\<^isub>M P" S ..
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1034
  have TP: "sigma_finite_measure (T \<Otimes>\<^isub>M P)" ..
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1035
  have SP: "sigma_finite_measure (S \<Otimes>\<^isub>M P)" ..
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1036
  have YZ: "random_variable (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1037
    using Pyz by (simp add: distributed_measurable)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1038
  
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1039
  from Pxz Pxyz have distr_eq: "distr M (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) =
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1040
    distr (distr M (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Y x, Z x))) (S \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). (x, z))"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1041
    by (simp add: comp_def distr_distr)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1042
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1043
  have "mutual_information b S P X Z =
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1044
    (\<integral>x. Pxz x * log b (Pxz x / (Px (fst x) * Pz (snd x))) \<partial>(S \<Otimes>\<^isub>M P))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1045
    by (rule mutual_information_distr[OF S P Px Pz Pxz])
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1046
  also have "\<dots> = (\<integral>(x,y,z). Pxyz (x,y,z) * log b (Pxz (x,z) / (Px x * Pz z)) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1047
    using b_gt_1 Pxz Px Pz
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1048
    by (subst distributed_transform_integral[OF Pxyz Pxz, where T="\<lambda>(x, y, z). (x, z)"]) (auto simp: split_beta')
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1049
  finally have mi_eq:
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1050
    "mutual_information b S P X Z = (\<integral>(x,y,z). Pxyz (x,y,z) * log b (Pxz (x,z) / (Px x * Pz z)) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))" .
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1051
  
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1052
  have ae1: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Px (fst x) = 0 \<longrightarrow> Pxyz x = 0"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1053
    by (intro subdensity_real[of fst, OF _ Pxyz Px]) auto
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1054
  moreover have ae2: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pz (snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1055
    by (intro subdensity_real[of "\<lambda>x. snd (snd x)", OF _ Pxyz Pz]) auto
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1056
  moreover have ae3: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pxz (fst x, snd (snd x)) = 0 \<longrightarrow> Pxyz x = 0"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1057
    by (intro subdensity_real[of "\<lambda>x. (fst x, snd (snd x))", OF _ Pxyz Pxz]) auto
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1058
  moreover have ae4: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pyz (snd x) = 0 \<longrightarrow> Pxyz x = 0"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1059
    by (intro subdensity_real[of snd, OF _ Pxyz Pyz]) auto
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1060
  moreover have ae5: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Px (fst x)"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1061
    using Px by (intro STP.AE_pair_measure) (auto simp: comp_def dest: distributed_real_AE)
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1062
  moreover have ae6: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pyz (snd x)"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1063
    using Pyz by (intro STP.AE_pair_measure) (auto simp: comp_def dest: distributed_real_AE)
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1064
  moreover have ae7: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pz (snd (snd x))"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1065
    using Pz Pz[THEN distributed_real_measurable]
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1066
    by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure AE_I2[of S] dest: distributed_real_AE)
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1067
  moreover have ae8: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. 0 \<le> Pxz (fst x, snd (snd x))"
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1068
    using Pxz[THEN distributed_real_AE, THEN SP.AE_pair]
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1069
    by (auto intro!: TP.AE_pair_measure STP.AE_pair_measure)
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1070
  moreover note Pxyz[THEN distributed_real_AE]
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1071
  ultimately have ae: "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P.
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1072
    Pxyz x * log b (Pxyz x / (Px (fst x) * Pyz (snd x))) -
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1073
    Pxyz x * log b (Pxz (fst x, snd (snd x)) / (Px (fst x) * Pz (snd (snd x)))) =
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1074
    Pxyz x * log b (Pxyz x * Pz (snd (snd x)) / (Pxz (fst x, snd (snd x)) * Pyz (snd x))) "
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1075
  proof eventually_elim
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1076
    case (goal1 x)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1077
    show ?case
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1078
    proof cases
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1079
      assume "Pxyz x \<noteq> 0"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1080
      with goal1 have "0 < Px (fst x)" "0 < Pz (snd (snd x))" "0 < Pxz (fst x, snd (snd x))" "0 < Pyz (snd x)" "0 < Pxyz x"
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1081
        by auto
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1082
      then show ?thesis
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1083
        using b_gt_1 by (simp add: log_simps mult_pos_pos less_imp_le field_simps)
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1084
    qed simp
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1085
  qed
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1086
  with I1 I2 show ?eq
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1087
    unfolding conditional_mutual_information_def
47694
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1088
    apply (subst mi_eq)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1089
    apply (subst mutual_information_distr[OF S TP Px Pyz Pxyz])
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1090
    apply (subst integral_diff(2)[symmetric])
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1091
    apply (auto intro!: integral_cong_AE simp: split_beta' simp del: integral_diff)
05663f75964c reworked Probability theory
hoelzl
parents: 46905
diff changeset
  1092
    done
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1093
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1094
  let ?P = "density (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) Pxyz"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1095
  interpret P: prob_space ?P
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1096
    unfolding distributed_distr_eq_density[OF Pxyz, symmetric]
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1097
    by (rule prob_space_distr) simp
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1098
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1099
  let ?Q = "density (T \<Otimes>\<^isub>M P) Pyz"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1100
  interpret Q: prob_space ?Q
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1101
    unfolding distributed_distr_eq_density[OF Pyz, symmetric]
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1102
    by (rule prob_space_distr) simp
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1103
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1104
  let ?f = "\<lambda>(x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) / Pxyz (x, y, z)"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1105
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1106
  from subdensity_real[of snd, OF _ Pyz Pz]
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1107
  have aeX1: "AE x in T \<Otimes>\<^isub>M P. Pz (snd x) = 0 \<longrightarrow> Pyz x = 0" by (auto simp: comp_def)
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1108
  have aeX2: "AE x in T \<Otimes>\<^isub>M P. 0 \<le> Pz (snd x)"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1109
    using Pz by (intro TP.AE_pair_measure) (auto simp: comp_def dest: distributed_real_AE)
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1110
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1111
  have aeX3: "AE y in T \<Otimes>\<^isub>M P. (\<integral>\<^isup>+ x. ereal (Pxz (x, snd y)) \<partial>S) = ereal (Pz (snd y))"
49788
3c10763f5cb4 show and use distributed_swap and distributed_jointI
hoelzl
parents: 49787
diff changeset
  1112
    using Pz distributed_marginal_eq_joint2[OF P S Pz Pxz]
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1113
    by (intro TP.AE_pair_measure) (auto dest: distributed_real_AE)
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1114
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1115
  have "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<le> (\<integral>\<^isup>+ (x, y, z). Pxz (x, z) * (Pyz (y, z) / Pz z) \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P))"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1116
    apply (subst positive_integral_density)
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1117
    apply simp
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1118
    apply (rule distributed_AE[OF Pxyz])
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1119
    apply auto []
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1120
    apply (rule positive_integral_mono_AE)
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1121
    using ae5 ae6 ae7 ae8
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1122
    apply eventually_elim
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1123
    apply (auto intro!: divide_nonneg_nonneg mult_nonneg_nonneg)
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1124
    done
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1125
  also have "\<dots> = (\<integral>\<^isup>+(y, z). \<integral>\<^isup>+ x. ereal (Pxz (x, z)) * ereal (Pyz (y, z) / Pz z) \<partial>S \<partial>T \<Otimes>\<^isub>M P)"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1126
    by (subst STP.positive_integral_snd_measurable[symmetric]) (auto simp add: split_beta')
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1127
  also have "\<dots> = (\<integral>\<^isup>+x. ereal (Pyz x) * 1 \<partial>T \<Otimes>\<^isub>M P)"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1128
    apply (rule positive_integral_cong_AE)
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1129
    using aeX1 aeX2 aeX3 distributed_AE[OF Pyz] AE_space
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1130
    apply eventually_elim
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1131
  proof (case_tac x, simp del: times_ereal.simps add: space_pair_measure)
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1132
    fix a b assume "Pz b = 0 \<longrightarrow> Pyz (a, b) = 0" "0 \<le> Pz b" "a \<in> space T \<and> b \<in> space P"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1133
      "(\<integral>\<^isup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)" 
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1134
    then show "(\<integral>\<^isup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1135
      by (subst positive_integral_multc)
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1136
         (auto intro!: divide_nonneg_nonneg split: prod.split)
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1137
  qed
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1138
  also have "\<dots> = 1"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1139
    using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1140
    by (subst positive_integral_density[symmetric]) auto
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1141
  finally have le1: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<le> 1" .
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1142
  also have "\<dots> < \<infinity>" by simp
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1143
  finally have fin: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<noteq> \<infinity>" by simp
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1144
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1145
  have pos: "(\<integral>\<^isup>+ x. ?f x \<partial>?P) \<noteq> 0"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1146
    apply (subst positive_integral_density)
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1147
    apply simp
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1148
    apply (rule distributed_AE[OF Pxyz])
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1149
    apply auto []
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1150
    apply (simp add: split_beta')
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1151
  proof
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1152
    let ?g = "\<lambda>x. ereal (if Pxyz x = 0 then 0 else Pxz (fst x, snd (snd x)) * Pyz (snd x) / Pz (snd (snd x)))"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1153
    assume "(\<integral>\<^isup>+ x. ?g x \<partial>(S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P)) = 0"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1154
    then have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. ?g x \<le> 0"
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1155
      by (intro positive_integral_0_iff_AE[THEN iffD1]) auto
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1156
    then have "AE x in S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P. Pxyz x = 0"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1157
      using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1158
      by eventually_elim (auto split: split_if_asm simp: mult_le_0_iff divide_le_0_iff)
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1159
    then have "(\<integral>\<^isup>+ x. ereal (Pxyz x) \<partial>S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) = 0"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1160
      by (subst positive_integral_cong_AE[of _ "\<lambda>x. 0"]) auto
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1161
    with P.emeasure_space_1 show False
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1162
      by (subst (asm) emeasure_density) (auto cong: positive_integral_cong)
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1163
  qed
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1164
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1165
  have neg: "(\<integral>\<^isup>+ x. - ?f x \<partial>?P) = 0"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1166
    apply (rule positive_integral_0_iff_AE[THEN iffD2])
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1167
    apply simp
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1168
    apply (subst AE_density)
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1169
    apply simp
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1170
    using ae5 ae6 ae7 ae8
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1171
    apply eventually_elim
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1172
    apply (auto intro!: mult_nonneg_nonneg divide_nonneg_nonneg)
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1173
    done
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1174
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1175
  have I3: "integrable (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1176
    apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ integral_diff(1)[OF I1 I2]])
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1177
    using ae
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1178
    apply (auto simp: split_beta')
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1179
    done
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1180
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1181
  have "- log b 1 \<le> - log b (integral\<^isup>L ?P ?f)"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1182
  proof (intro le_imp_neg_le log_le[OF b_gt_1])
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1183
    show "0 < integral\<^isup>L ?P ?f"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1184
      using neg pos fin positive_integral_positive[of ?P ?f]
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1185
      by (cases "(\<integral>\<^isup>+ x. ?f x \<partial>?P)") (auto simp add: lebesgue_integral_def less_le split_beta')
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1186
    show "integral\<^isup>L ?P ?f \<le> 1"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1187
      using neg le1 fin positive_integral_positive[of ?P ?f]
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1188
      by (cases "(\<integral>\<^isup>+ x. ?f x \<partial>?P)") (auto simp add: lebesgue_integral_def split_beta' one_ereal_def)
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1189
  qed
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1190
  also have "- log b (integral\<^isup>L ?P ?f) \<le> (\<integral> x. - log b (?f x) \<partial>?P)"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1191
  proof (rule P.jensens_inequality[where a=0 and b=1 and I="{0<..}"])
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1192
    show "AE x in ?P. ?f x \<in> {0<..}"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1193
      unfolding AE_density[OF distributed_borel_measurable[OF Pxyz]]
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1194
      using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1195
      by eventually_elim (auto simp: divide_pos_pos mult_pos_pos)
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1196
    show "integrable ?P ?f"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1197
      unfolding integrable_def 
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1198
      using fin neg by (auto simp: split_beta')
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1199
    show "integrable ?P (\<lambda>x. - log b (?f x))"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1200
      apply (subst integral_density)
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1201
      apply simp
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1202
      apply (auto intro!: distributed_real_AE[OF Pxyz]) []
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1203
      apply simp
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1204
      apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ I3])
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1205
      apply simp
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1206
      apply simp
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1207
      using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1208
      apply eventually_elim
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1209
      apply (auto simp: log_divide_eq log_mult_eq zero_le_mult_iff zero_less_mult_iff zero_less_divide_iff field_simps)
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1210
      done
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1211
  qed (auto simp: b_gt_1 minus_log_convex)
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1212
  also have "\<dots> = conditional_mutual_information b S T P X Y Z"
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1213
    unfolding `?eq`
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1214
    apply (subst integral_density)
50003
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1215
    apply simp
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1216
    apply (auto intro!: distributed_real_AE[OF Pxyz]) []
8c213922ed49 use measurability prover
hoelzl
parents: 50002
diff changeset
  1217
    apply simp
49787
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1218
    apply (intro integral_cong_AE)
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1219
    using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1220
    apply eventually_elim
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1221
    apply (auto simp: log_divide_eq zero_less_mult_iff zero_less_divide_iff field_simps)
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1222
    done
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1223
  finally show ?nonneg
d8de705b48d4 rule to show that conditional mutual information is non-negative in the continuous case
hoelzl
parents: 49786
diff changeset
  1224
    by simp
40859
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1225
qed
de0b30e6c2d2 Support product spaces on sigma finite measures.
hoelzl
parents: 39302
diff changeset
  1226
49803
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
  1227
lemma (in information_space)
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
  1228
  fixes Px :: "_ \<Rightarrow> real"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
  1229
  assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" and P: "sigma_finite_measure P"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
  1230
  assumes Fx: "finite_entropy S X Px"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
  1231
  assumes Fz: "finite_entropy P Z Pz"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
  1232
  assumes Fyz: "finite_entropy (T \<Otimes>\<^isub>M P) (\<lambda>x. (Y x, Z x)) Pyz"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
  1233
  assumes Fxz: "finite_entropy (S \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Z x)) Pxz"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
  1234
  assumes Fxyz: "finite_entropy (S \<Otimes>\<^isub>M T \<Otimes>\<^isub>M P) (\<lambda>x. (X x, Y x, Z x)) Pxyz"
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff changeset
  1235
  shows conditional_mutual_information_generic_eq': "conditional_mutual_information b S T P X Y Z
2f076e377703 add finite entropy
hoelzl
parents: 49802
diff