summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Probability/Information.thy

changeset 45777 | c36637603821 |

parent 45712 | 852597248663 |

child 46731 | 5302e932d1e5 |

1.1 --- a/src/HOL/Probability/Information.thy Mon Dec 05 15:10:15 2011 +0100 1.2 +++ b/src/HOL/Probability/Information.thy Wed Dec 07 15:10:29 2011 +0100 1.3 @@ -198,7 +198,7 @@ 1.4 proof - 1.5 interpret \<nu>: prob_space "M\<lparr>measure := \<nu>\<rparr>" by fact 1.6 have ms: "measure_space (M\<lparr>measure := \<nu>\<rparr>)" by default 1.7 - have fms: "finite_measure (M\<lparr>measure := \<nu>\<rparr>)" by default 1.8 + have fms: "finite_measure (M\<lparr>measure := \<nu>\<rparr>)" by unfold_locales 1.9 note RN = RN_deriv[OF ms ac] 1.10 1.11 from real_RN_deriv[OF fms ac] guess D . note D = this 1.12 @@ -460,7 +460,7 @@ 1.13 proof - 1.14 interpret information_space M by default fact 1.15 interpret v: finite_prob_space "M\<lparr>measure := \<nu>\<rparr>" by fact 1.16 - have ps: "prob_space (M\<lparr>measure := \<nu>\<rparr>)" by default 1.17 + have ps: "prob_space (M\<lparr>measure := \<nu>\<rparr>)" by unfold_locales 1.18 from KL_ge_0[OF this ac v.integral_finite_singleton(1)] show ?thesis . 1.19 qed 1.20 1.21 @@ -558,7 +558,7 @@ 1.22 1.23 have eq: "\<forall>A\<in>sets XY.P. (ereal \<circ> joint_distribution X Y) A = XY.\<mu> A" 1.24 proof (rule XY.KL_eq_0_imp) 1.25 - show "prob_space ?J" by default 1.26 + show "prob_space ?J" by unfold_locales 1.27 show "XY.absolutely_continuous (ereal\<circ>joint_distribution X Y)" 1.28 using ac by (simp add: P_def) 1.29 show "integrable ?J (entropy_density b XY.P (ereal\<circ>joint_distribution X Y))" 1.30 @@ -624,7 +624,7 @@ 1.31 have "prob_space (P.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)" 1.32 using X Y by (auto intro!: distribution_prob_space random_variable_pairI) 1.33 then show "measure_space (P.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)" 1.34 - unfolding prob_space_def by simp 1.35 + unfolding prob_space_def finite_measure_def sigma_finite_measure_def by simp 1.36 qed auto 1.37 qed 1.38 1.39 @@ -654,7 +654,7 @@ 1.40 note rv = assms[THEN finite_random_variableD] 1.41 show "XY.absolutely_continuous (ereal\<circ>joint_distribution X Y)" 1.42 proof (rule XY.absolutely_continuousI) 1.43 - show "finite_measure_space (XY.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)" by default 1.44 + show "finite_measure_space (XY.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)" by unfold_locales 1.45 fix x assume "x \<in> space XY.P" and "XY.\<mu> {x} = 0" 1.46 then obtain a b where "x = (a, b)" 1.47 and "distribution X {a} = 0 \<or> distribution Y {b} = 0" 1.48 @@ -684,8 +684,8 @@ 1.49 interpret P: finite_prob_space "XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>" 1.50 using assms by (auto intro!: joint_distribution_finite_prob_space) 1.51 1.52 - have P_ms: "finite_measure_space (XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>)" by default 1.53 - have P_ps: "finite_prob_space (XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>)" by default 1.54 + have P_ms: "finite_measure_space (XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>)" by unfold_locales 1.55 + have P_ps: "finite_prob_space (XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>)" by unfold_locales 1.56 1.57 show ?sum 1.58 unfolding Let_def mutual_information_def