--- a/src/HOL/Probability/Information.thy Wed Oct 10 12:12:23 2012 +0200
+++ b/src/HOL/Probability/Information.thy Wed Oct 10 12:12:24 2012 +0200
@@ -666,41 +666,75 @@
lemma (in information_space) entropy_distr:
fixes X :: "'a \<Rightarrow> 'b"
- assumes "sigma_finite_measure MX" and X: "distributed M MX X f"
+ assumes X: "distributed M MX X f"
shows "entropy b MX X = - (\<integral>x. f x * log b (f x) \<partial>MX)"
+ unfolding entropy_def KL_divergence_def entropy_density_def comp_def
+proof (subst integral_cong_AE)
+ note D = distributed_measurable[OF X] distributed_borel_measurable[OF X] distributed_AE[OF X]
+ interpret X: prob_space "distr M MX X"
+ using D(1) by (rule prob_space_distr)
+
+ have sf: "sigma_finite_measure (distr M MX X)" by default
+ have ae: "AE x in MX. f x = RN_deriv MX (density MX f) x"
+ using D
+ by (intro RN_deriv_unique_sigma_finite)
+ (auto intro: divide_nonneg_nonneg measure_nonneg
+ simp: distributed_distr_eq_density[symmetric, OF X] sf)
+ show "AE x in distr M MX X. log b (real (RN_deriv MX (distr M MX X) x)) =
+ log b (f x)"
+ unfolding distributed_distr_eq_density[OF X]
+ apply (subst AE_density)
+ using D apply simp
+ using ae apply eventually_elim
+ apply (subst (asm) eq_commute)
+ apply auto
+ done
+ show "- (\<integral> x. log b (f x) \<partial>distr M MX X) = - (\<integral> x. f x * log b (f x) \<partial>MX)"
+ unfolding distributed_distr_eq_density[OF X]
+ using D
+ by (subst integral_density)
+ (auto simp: borel_measurable_ereal_iff)
+qed
+
+lemma (in prob_space) uniform_distributed_params:
+ assumes X: "distributed M MX X (\<lambda>x. indicator A x / measure MX A)"
+ shows "A \<in> sets MX" "measure MX A \<noteq> 0"
proof -
- interpret MX: sigma_finite_measure MX by fact
- from X show ?thesis
- unfolding entropy_def X[THEN distributed_distr_eq_density]
- by (subst MX.KL_density[OF b_gt_1]) (simp_all add: distributed_real_AE distributed_real_measurable)
+ interpret X: prob_space "distr M MX X"
+ using distributed_measurable[OF X] by (rule prob_space_distr)
+
+ show "measure MX A \<noteq> 0"
+ proof
+ assume "measure MX A = 0"
+ with X.emeasure_space_1 X.prob_space distributed_distr_eq_density[OF X]
+ show False
+ by (simp add: emeasure_density zero_ereal_def[symmetric])
+ qed
+ with measure_notin_sets[of A MX] show "A \<in> sets MX"
+ by blast
qed
lemma (in information_space) entropy_uniform:
- assumes "sigma_finite_measure MX"
- assumes A: "A \<in> sets MX" "emeasure MX A \<noteq> 0" "emeasure MX A \<noteq> \<infinity>"
- assumes X: "distributed M MX X (\<lambda>x. 1 / measure MX A * indicator A x)"
+ assumes X: "distributed M MX X (\<lambda>x. indicator A x / measure MX A)" (is "distributed _ _ _ ?f")
shows "entropy b MX X = log b (measure MX A)"
-proof (subst entropy_distr[OF _ X])
- let ?f = "\<lambda>x. 1 / measure MX A * indicator A x"
- have "- (\<integral>x. ?f x * log b (?f x) \<partial>MX) =
- - (\<integral>x. (log b (1 / measure MX A) / measure MX A) * indicator A x \<partial>MX)"
- by (auto intro!: integral_cong simp: indicator_def)
- also have "\<dots> = - log b (inverse (measure MX A))"
- using A by (subst integral_cmult(2))
- (simp_all add: measure_def real_of_ereal_eq_0 integral_cmult inverse_eq_divide)
- also have "\<dots> = log b (measure MX A)"
- using b_gt_1 A by (subst log_inverse) (auto simp add: measure_def less_le real_of_ereal_eq_0
- emeasure_nonneg real_of_ereal_pos)
- finally show "- (\<integral>x. ?f x * log b (?f x) \<partial>MX) = log b (measure MX A)" by simp
-qed fact+
+proof (subst entropy_distr[OF X])
+ have [simp]: "emeasure MX A \<noteq> \<infinity>"
+ using uniform_distributed_params[OF X] by (auto simp add: measure_def)
+ have eq: "(\<integral> x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \<partial>MX) =
+ (\<integral> x. (- log b (measure MX A) / measure MX A) * indicator A x \<partial>MX)"
+ using measure_nonneg[of MX A] uniform_distributed_params[OF X]
+ by (auto intro!: integral_cong split: split_indicator simp: log_divide_eq)
+ show "- (\<integral> x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \<partial>MX) =
+ log b (measure MX A)"
+ unfolding eq using uniform_distributed_params[OF X]
+ by (subst lebesgue_integral_cmult) (auto simp: measure_def)
+qed
lemma (in information_space) entropy_simple_distributed:
fixes X :: "'a \<Rightarrow> 'b"
assumes X: "simple_distributed M X f"
shows "\<H>(X) = - (\<Sum>x\<in>X`space M. f x * log b (f x))"
-proof (subst entropy_distr[OF _ simple_distributed[OF X]])
- show "sigma_finite_measure (count_space (X ` space M))"
- using X by (simp add: sigma_finite_measure_count_space_finite simple_distributed_def)
+proof (subst entropy_distr[OF simple_distributed[OF X]])
show "- (\<integral>x. f x * log b (f x) \<partial>(count_space (X`space M))) = - (\<Sum>x\<in>X ` space M. f x * log b (f x))"
using X by (auto simp add: lebesgue_integral_count_space_finite)
qed
--- a/src/HOL/Probability/Radon_Nikodym.thy Wed Oct 10 12:12:23 2012 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy Wed Oct 10 12:12:24 2012 +0200
@@ -776,15 +776,16 @@
assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
assumes pos: "AE x in M. 0 \<le> f x" "AE x in M. 0 \<le> g x"
and fin: "integral\<^isup>P M f \<noteq> \<infinity>"
- shows "(\<forall>A\<in>sets M. (\<integral>\<^isup>+x. f x * indicator A x \<partial>M) = (\<integral>\<^isup>+x. g x * indicator A x \<partial>M))
- \<longleftrightarrow> (AE x in M. f x = g x)"
- (is "(\<forall>A\<in>sets M. ?P f A = ?P g A) \<longleftrightarrow> _")
+ shows "density M f = density M g \<longleftrightarrow> (AE x in M. f x = g x)"
proof (intro iffI ballI)
fix A assume eq: "AE x in M. f x = g x"
- then show "?P f A = ?P g A"
- by (auto intro: positive_integral_cong_AE)
+ with borel show "density M f = density M g"
+ by (auto intro: density_cong)
next
- assume eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
+ let ?P = "\<lambda>f A. \<integral>\<^isup>+ x. f x * indicator A x \<partial>M"
+ assume "density M f = density M g"
+ with borel have eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
+ by (simp add: emeasure_density[symmetric])
from this[THEN bspec, OF top] fin
have g_fin: "integral\<^isup>P M g \<noteq> \<infinity>" by (simp cong: positive_integral_cong)
{ fix f g assume borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
@@ -844,7 +845,7 @@
unfolding indicator_def by auto
have "\<forall>i. AE x in M. ?f (Q i) x = ?f' (Q i) x" using borel Q_fin Q pos
by (intro finite_density_unique[THEN iffD1] allI)
- (auto intro!: borel_measurable_ereal_times f Int simp: *)
+ (auto intro!: borel_measurable_ereal_times f measure_eqI Int simp: emeasure_density * subset_eq)
moreover have "AE x in M. ?f Q0 x = ?f' Q0 x"
proof (rule AE_I')
{ fix f :: "'a \<Rightarrow> ereal" assume borel: "f \<in> borel_measurable M"
@@ -933,6 +934,41 @@
shows "density M f = density M f' \<longleftrightarrow> (AE x in M. f x = f' x)"
using density_unique[OF assms] density_cong[OF f f'] by auto
+lemma sigma_finite_density_unique:
+ assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
+ assumes pos: "AE x in M. 0 \<le> f x" "AE x in M. 0 \<le> g x"
+ and fin: "sigma_finite_measure (density M f)"
+ shows "density M f = density M g \<longleftrightarrow> (AE x in M. f x = g x)"
+proof
+ assume "AE x in M. f x = g x" with borel show "density M f = density M g"
+ by (auto intro: density_cong)
+next
+ assume eq: "density M f = density M g"
+ interpret f!: sigma_finite_measure "density M f" by fact
+ from f.sigma_finite_incseq guess A . note cover = this
+
+ have "AE x in M. \<forall>i. x \<in> A i \<longrightarrow> f x = g x"
+ unfolding AE_all_countable
+ proof
+ fix i
+ have "density (density M f) (indicator (A i)) = density (density M g) (indicator (A i))"
+ unfolding eq ..
+ moreover have "(\<integral>\<^isup>+x. f x * indicator (A i) x \<partial>M) \<noteq> \<infinity>"
+ using cover(1) cover(3)[of i] borel by (auto simp: emeasure_density subset_eq)
+ ultimately have "AE x in M. f x * indicator (A i) x = g x * indicator (A i) x"
+ using borel pos cover(1) pos
+ by (intro finite_density_unique[THEN iffD1])
+ (auto simp: density_density_eq subset_eq)
+ then show "AE x in M. x \<in> A i \<longrightarrow> f x = g x"
+ by auto
+ qed
+ with AE_space show "AE x in M. f x = g x"
+ apply eventually_elim
+ using cover(2)[symmetric]
+ apply auto
+ done
+qed
+
lemma (in sigma_finite_measure) sigma_finite_iff_density_finite':
assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
shows "sigma_finite_measure (density M f) \<longleftrightarrow> (AE x in M. f x \<noteq> \<infinity>)"
@@ -1076,15 +1112,17 @@
assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
and eq: "density M f = N"
shows "AE x in M. f x = RN_deriv M N x"
-proof (rule density_unique)
- have ac: "absolutely_continuous M N"
- using f(1) unfolding eq[symmetric] by (rule absolutely_continuousI_density)
- have eq2: "sets N = sets M"
- unfolding eq[symmetric] by simp
- show "RN_deriv M N \<in> borel_measurable M" "AE x in M. 0 \<le> RN_deriv M N x"
- "density M f = density M (RN_deriv M N)"
- using RN_deriv[OF ac eq2] eq by auto
-qed fact+
+ unfolding eq[symmetric]
+ by (intro density_unique_iff[THEN iffD1] f borel_measurable_RN_deriv_density
+ RN_deriv_density_nonneg[THEN AE_I2] density_RN_deriv_density[symmetric])
+
+lemma RN_deriv_unique_sigma_finite:
+ assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
+ and eq: "density M f = N" and fin: "sigma_finite_measure N"
+ shows "AE x in M. f x = RN_deriv M N x"
+ using fin unfolding eq[symmetric]
+ by (intro sigma_finite_density_unique[THEN iffD1] f borel_measurable_RN_deriv_density
+ RN_deriv_density_nonneg[THEN AE_I2] density_RN_deriv_density[symmetric])
lemma (in sigma_finite_measure) RN_deriv_distr:
fixes T :: "'a \<Rightarrow> 'b"