author hoelzl Fri Nov 14 13:18:33 2014 +0100 (2014-11-14) changeset 59002 2c8b2fb54b88 parent 59001 44afb337bb92 child 59003 16d92d37a8a1
cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
```     1.1 --- a/src/HOL/Library/Extended_Real.thy	Fri Nov 14 08:18:58 2014 +0100
1.2 +++ b/src/HOL/Library/Extended_Real.thy	Fri Nov 14 13:18:33 2014 +0100
1.3 @@ -863,13 +863,13 @@
1.4
1.5  lemma ereal_left_mult_cong:
1.6    fixes a b c :: ereal
1.7 -  shows "(c \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> c * a = c * b"
1.8 +  shows  "c = d \<Longrightarrow> (d \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> a * c = b * d"
1.9    by (cases "c = 0") simp_all
1.10
1.11  lemma ereal_right_mult_cong:
1.12 -  fixes a b c d :: ereal
1.13 +  fixes a b c :: ereal
1.14    shows "c = d \<Longrightarrow> (d \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> c * a = d * b"
1.15 -  by (cases "d = 0") simp_all
1.16 +  by (cases "c = 0") simp_all
1.17
1.18  lemma ereal_distrib:
1.19    fixes a b c :: ereal
1.20 @@ -891,6 +891,10 @@
1.21    shows "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> r * setsum f A = (\<Sum>n\<in>A. r * f n)"
1.22    by (induct A rule: infinite_finite_induct)  (auto simp: ereal_right_distrib setsum_nonneg)
1.23
1.24 +lemma setsum_ereal_left_distrib:
1.25 +  "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> setsum f A * r = (\<Sum>n\<in>A. f n * r :: ereal)"
1.26 +  using setsum_ereal_right_distrib[of A f r] by (simp add: mult_ac)
1.27 +
1.28  lemma ereal_le_epsilon:
1.29    fixes x y :: ereal
1.30    assumes "\<forall>e. 0 < e \<longrightarrow> x \<le> y + e"
```
```     2.1 --- a/src/HOL/Library/Indicator_Function.thy	Fri Nov 14 08:18:58 2014 +0100
2.2 +++ b/src/HOL/Library/Indicator_Function.thy	Fri Nov 14 13:18:33 2014 +0100
2.3 @@ -57,6 +57,9 @@
2.4  lemma indicator_sum: "indicator (A <+> B) x = (case x of Inl x \<Rightarrow> indicator A x | Inr x \<Rightarrow> indicator B x)"
2.5    unfolding indicator_def by (cases x) auto
2.6
2.7 +lemma indicator_image: "inj f \<Longrightarrow> indicator (f ` X) (f x) = (indicator X x::_::zero_neq_one)"
2.8 +  by (auto simp: indicator_def inj_on_def)
2.9 +
2.10  lemma
2.11    fixes f :: "'a \<Rightarrow> 'b::semiring_1" assumes "finite A"
2.12    shows setsum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator B x) = (\<Sum>x \<in> A \<inter> B. f x)"
```
```     3.1 --- a/src/HOL/Probability/Giry_Monad.thy	Fri Nov 14 08:18:58 2014 +0100
3.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Fri Nov 14 13:18:33 2014 +0100
3.3 @@ -785,7 +785,7 @@
3.4        \<Longrightarrow> emeasure (M \<guillemotright>= f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M"
3.5    by (simp add: bind_nonempty'' emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra)
3.6
3.7 -lemma nn_integral_bind:
3.8 +lemma nn_integral_bind':
3.9    assumes f: "f \<in> borel_measurable B" "\<And>x. 0 \<le> f x"
3.10    assumes N: "N \<in> measurable M (subprob_algebra B)"
3.11    shows "(\<integral>\<^sup>+x. f x \<partial>(M \<guillemotright>= N)) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)"
3.12 @@ -795,6 +795,15 @@
3.13      by (rule nn_integral_distr[OF N nn_integral_measurable_subprob_algebra[OF f]])
3.14  qed (simp add: bind_empty space_empty[of M] nn_integral_count_space)
3.15
3.16 +lemma nn_integral_bind:
3.17 +  assumes [measurable]: "f \<in> borel_measurable B"
3.18 +  assumes N: "N \<in> measurable M (subprob_algebra B)"
3.19 +  shows "(\<integral>\<^sup>+x. f x \<partial>(M \<guillemotright>= N)) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)"
3.20 +  apply (subst (1 3) nn_integral_max_0[symmetric])
3.21 +  apply (rule nn_integral_bind'[OF _ _ N])
3.22 +  apply auto
3.23 +  done
3.24 +
3.25  lemma AE_bind:
3.26    assumes P[measurable]: "Measurable.pred B P"
3.27    assumes N[measurable]: "N \<in> measurable M (subprob_algebra B)"
```
```     4.1 --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Fri Nov 14 08:18:58 2014 +0100
4.2 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Fri Nov 14 13:18:33 2014 +0100
4.3 @@ -552,7 +552,7 @@
4.4      (\<Sum>y\<in>f`space M. y * (\<Sum>z\<in>g`space M.
4.5        if \<exists>x\<in>space M. y = f x \<and> z = g x then emeasure M {x\<in>space M. g x = z} else 0))"
4.6      unfolding simple_integral_def
4.7 -  proof (safe intro!: setsum.cong ereal_left_mult_cong)
4.8 +  proof (safe intro!: setsum.cong ereal_right_mult_cong)
4.9      fix y assume y: "y \<in> space M" "f y \<noteq> 0"
4.10      have [simp]: "g ` space M \<inter> {z. \<exists>x\<in>space M. f y = f x \<and> z = g x} =
4.11          {z. \<exists>x\<in>space M. f y = f x \<and> z = g x}"
4.12 @@ -1894,7 +1894,7 @@
4.13    using simple_function_restrict_space_ereal[THEN iffD1, OF \<Omega>, THEN simple_functionD(1)]
4.14    by (auto simp add: space_restrict_space emeasure_restrict_space[OF \<Omega>(1)] le_infI2 simple_integral_def
4.15             split: split_indicator split_indicator_asm
4.16 -           intro!: setsum.mono_neutral_cong_left ereal_left_mult_cong arg_cong2[where f=emeasure])
4.17 +           intro!: setsum.mono_neutral_cong_left ereal_right_mult_cong[OF refl] arg_cong2[where f=emeasure])
4.18
4.19  lemma one_not_less_zero[simp]: "\<not> 1 < (0::ereal)"
4.20    by (simp add: zero_ereal_def one_ereal_def)
```
```     5.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri Nov 14 08:18:58 2014 +0100
5.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Nov 14 13:18:33 2014 +0100
5.3 @@ -281,6 +281,12 @@
5.4    unfolding `p = q`[symmetric] measure_pmf_inject[symmetric] map_pmf.rep_eq
5.5    by (auto simp add: emeasure_distr AE_measure_pmf_iff intro!: emeasure_eq_AE measure_eqI)
5.6
5.7 +lemma emeasure_map_pmf[simp]: "emeasure (map_pmf f M) X = emeasure M (f -` X)"
5.8 +  unfolding map_pmf.rep_eq by (subst emeasure_distr) auto
5.9 +
5.10 +lemma nn_integral_map_pmf[simp]: "(\<integral>\<^sup>+x. f x \<partial>map_pmf g M) = (\<integral>\<^sup>+x. f (g x) \<partial>M)"
5.11 +  unfolding map_pmf.rep_eq by (intro nn_integral_distr) auto
5.12 +
5.13  lemma pmf_set_map:
5.14    fixes f :: "'a \<Rightarrow> 'b"
5.15    shows "set_pmf \<circ> map_pmf f = op ` f \<circ> set_pmf"
5.16 @@ -433,6 +439,17 @@
5.17  lemma set_pmf_bernoulli: "0 < p \<Longrightarrow> p < 1 \<Longrightarrow> set_pmf (bernoulli_pmf p) = UNIV"
5.18    by (auto simp add: set_pmf_iff UNIV_bool)
5.19
5.20 +lemma nn_integral_bernoulli_pmf[simp]:
5.21 +  assumes [simp]: "0 \<le> p" "p \<le> 1" "\<And>x. 0 \<le> f x"
5.22 +  shows "(\<integral>\<^sup>+x. f x \<partial>bernoulli_pmf p) = f True * p + f False * (1 - p)"
5.23 +  by (subst nn_integral_measure_pmf_support[of UNIV])
5.24 +     (auto simp: UNIV_bool field_simps)
5.25 +
5.26 +lemma integral_bernoulli_pmf[simp]:
5.27 +  assumes [simp]: "0 \<le> p" "p \<le> 1"
5.28 +  shows "(\<integral>x. f x \<partial>bernoulli_pmf p) = f True * p + f False * (1 - p)"
5.29 +  by (subst integral_measure_pmf[of UNIV]) (auto simp: UNIV_bool)
5.30 +
5.31  lift_definition geometric_pmf :: "nat pmf" is "\<lambda>n. 1 / 2^Suc n"
5.32  proof
5.33    note geometric_sums[of "1 / 2"]
5.34 @@ -445,7 +462,7 @@
5.35  lemma pmf_geometric[simp]: "pmf geometric_pmf n = 1 / 2^Suc n"
5.36    by transfer rule
5.37
5.38 -lemma set_pmf_geometric: "set_pmf geometric_pmf = UNIV"
5.39 +lemma set_pmf_geometric[simp]: "set_pmf geometric_pmf = UNIV"
5.40    by (auto simp: set_pmf_iff)
5.41
5.42  context
5.43 @@ -485,6 +502,9 @@
5.44  lemma set_pmf_of_set[simp]: "set_pmf pmf_of_set = S"
5.45    using S_finite S_not_empty by (auto simp: set_pmf_iff)
5.46
5.47 +lemma emeasure_pmf_of_set[simp]: "emeasure pmf_of_set S = 1"
5.48 +  by (rule measure_pmf.emeasure_eq_1_AE) (auto simp: AE_measure_pmf_iff)
5.49 +
5.50  end
5.51
5.52  end
5.53 @@ -558,12 +578,18 @@
5.54  lemma map_return_pmf: "map_pmf f (return_pmf x) = return_pmf (f x)"
5.55    by transfer (simp add: distr_return)
5.56
5.57 -lemma set_pmf_return: "set_pmf (return_pmf x) = {x}"
5.58 +lemma set_return_pmf: "set_pmf (return_pmf x) = {x}"
5.59    by transfer (auto simp add: measure_return split: split_indicator)
5.60
5.61  lemma pmf_return: "pmf (return_pmf x) y = indicator {y} x"
5.62    by transfer (simp add: measure_return)
5.63
5.64 +lemma nn_integral_return_pmf[simp]: "0 \<le> f x \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>return_pmf x) = f x"
5.65 +  unfolding return_pmf.rep_eq by (intro nn_integral_return) auto
5.66 +
5.67 +lemma emeasure_return_pmf[simp]: "emeasure (return_pmf x) X = indicator X x"
5.68 +  unfolding return_pmf.rep_eq by (intro emeasure_return) auto
5.69 +
5.70  end
5.71
5.72  definition "bind_pmf M f = join_pmf (map_pmf f M)"
5.73 @@ -584,6 +610,41 @@
5.74  lemma bind_return_pmf: "bind_pmf (return_pmf x) f = f x"
5.75    unfolding bind_pmf_def map_return_pmf join_return_pmf ..
5.76
5.77 +lemma set_bind_pmf: "set_pmf (bind_pmf M N) = (\<Union>M\<in>set_pmf M. set_pmf (N M))"
5.78 +  apply (simp add: set_eq_iff set_pmf_iff pmf_bind)
5.79 +  apply (subst integral_nonneg_eq_0_iff_AE)
5.80 +  apply (auto simp: pmf_nonneg pmf_le_1 AE_measure_pmf_iff
5.81 +              intro!: measure_pmf.integrable_const_bound[where B=1])
5.82 +  done
5.83 +
5.84 +lemma measurable_pair_restrict_pmf2:
5.85 +  assumes "countable A"
5.86 +  assumes "\<And>y. y \<in> A \<Longrightarrow> (\<lambda>x. f (x, y)) \<in> measurable M L"
5.87 +  shows "f \<in> measurable (M \<Otimes>\<^sub>M restrict_space (measure_pmf N) A) L"
5.88 +  apply (subst measurable_cong_sets)
5.89 +  apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
5.90 +  apply (simp_all add: restrict_count_space)
5.91 +  apply (subst split_eta[symmetric])
5.92 +  unfolding measurable_split_conv
5.93 +  apply (rule measurable_compose_countable'[OF _ measurable_snd `countable A`])
5.94 +  apply (rule measurable_compose[OF measurable_fst])
5.95 +  apply fact
5.96 +  done
5.97 +
5.98 +lemma measurable_pair_restrict_pmf1:
5.99 +  assumes "countable A"
5.100 +  assumes "\<And>x. x \<in> A \<Longrightarrow> (\<lambda>y. f (x, y)) \<in> measurable N L"
5.101 +  shows "f \<in> measurable (restrict_space (measure_pmf M) A \<Otimes>\<^sub>M N) L"
5.102 +  apply (subst measurable_cong_sets)
5.103 +  apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
5.104 +  apply (simp_all add: restrict_count_space)
5.105 +  apply (subst split_eta[symmetric])
5.106 +  unfolding measurable_split_conv
5.107 +  apply (rule measurable_compose_countable'[OF _ measurable_fst `countable A`])
5.108 +  apply (rule measurable_compose[OF measurable_snd])
5.109 +  apply fact
5.110 +  done
5.111 +
5.112  lemma bind_commute_pmf: "bind_pmf A (\<lambda>x. bind_pmf B (C x)) = bind_pmf B (\<lambda>y. bind_pmf A (\<lambda>x. C x y))"
5.113    unfolding pmf_eq_iff pmf_bind
5.114  proof
5.115 @@ -601,36 +662,15 @@
5.116    have "(\<integral> x. \<integral> y. pmf (C x y) i \<partial>B \<partial>A) = (\<integral> x. (\<integral> y. pmf (C x y) i \<partial>restrict_space B B) \<partial>A)"
5.117      by (rule integral_cong) (auto intro!: integral_pmf_restrict)
5.118    also have "\<dots> = (\<integral> x. (\<integral> y. pmf (C x y) i \<partial>restrict_space B B) \<partial>restrict_space A A)"
5.119 -    apply (intro integral_pmf_restrict B.borel_measurable_lebesgue_integral)
5.120 -    apply (auto simp: measurable_split_conv)
5.121 -    apply (subst measurable_cong_sets)
5.122 -    apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
5.123 -    apply (simp add: restrict_count_space)
5.124 -    apply (rule measurable_compose_countable'[OF _ measurable_snd])
5.125 -    apply (rule measurable_compose[OF measurable_fst])
5.126 -    apply (auto intro: countable_set_pmf)
5.127 -    done
5.128 +    by (intro integral_pmf_restrict B.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2
5.129 +              countable_set_pmf borel_measurable_count_space)
5.130    also have "\<dots> = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>restrict_space A A \<partial>restrict_space B B)"
5.131 -    apply (rule AB.Fubini_integral[symmetric])
5.132 -    apply (auto intro!: AB.integrable_const_bound[where B=1] simp: pmf_nonneg pmf_le_1)
5.133 -    apply (auto simp: measurable_split_conv)
5.134 -    apply (subst measurable_cong_sets)
5.135 -    apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
5.136 -    apply (simp add: restrict_count_space)
5.137 -    apply (rule measurable_compose_countable'[OF _ measurable_snd])
5.138 -    apply (rule measurable_compose[OF measurable_fst])
5.139 -    apply (auto intro: countable_set_pmf)
5.140 -    done
5.141 +    by (rule AB.Fubini_integral[symmetric])
5.142 +       (auto intro!: AB.integrable_const_bound[where B=1] measurable_pair_restrict_pmf2
5.143 +             simp: pmf_nonneg pmf_le_1 countable_set_pmf measurable_restrict_space1)
5.144    also have "\<dots> = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>restrict_space A A \<partial>B)"
5.145 -    apply (intro integral_pmf_restrict[symmetric] A.borel_measurable_lebesgue_integral)
5.146 -    apply (auto simp: measurable_split_conv)
5.147 -    apply (subst measurable_cong_sets)
5.148 -    apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
5.149 -    apply (simp add: restrict_count_space)
5.150 -    apply (rule measurable_compose_countable'[OF _ measurable_snd])
5.151 -    apply (rule measurable_compose[OF measurable_fst])
5.152 -    apply (auto intro: countable_set_pmf)
5.153 -    done
5.154 +    by (intro integral_pmf_restrict[symmetric] A.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2
5.155 +              countable_set_pmf borel_measurable_count_space)
5.156    also have "\<dots> = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>A \<partial>B)"
5.157      by (rule integral_cong) (auto intro!: integral_pmf_restrict[symmetric])
5.158    finally show "(\<integral> x. \<integral> y. pmf (C x y) i \<partial>B \<partial>A) = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>A \<partial>B)" .
5.159 @@ -642,6 +682,22 @@
5.160
5.161  interpretation pmf_as_measure .
5.162
5.163 +lemma measure_pmf_bind: "measure_pmf (bind_pmf M f) = (measure_pmf M \<guillemotright>= (\<lambda>x. measure_pmf (f x)))"
5.164 +  by transfer simp
5.165 +
5.166 +lemma nn_integral_bind_pmf[simp]: "(\<integral>\<^sup>+x. f x \<partial>bind_pmf M N) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)"
5.167 +  using measurable_measure_pmf[of N]
5.168 +  unfolding measure_pmf_bind
5.169 +  apply (subst (1 3) nn_integral_max_0[symmetric])
5.170 +  apply (intro nn_integral_bind[where B="count_space UNIV"])
5.171 +  apply auto
5.172 +  done
5.173 +
5.174 +lemma emeasure_bind_pmf[simp]: "emeasure (bind_pmf M N) X = (\<integral>\<^sup>+x. emeasure (N x) X \<partial>M)"
5.175 +  using measurable_measure_pmf[of N]
5.176 +  unfolding measure_pmf_bind
5.177 +  by (subst emeasure_bind[where N="count_space UNIV"]) auto
5.178 +
5.179  lemma bind_return_pmf': "bind_pmf N return_pmf = N"
5.180  proof (transfer, clarify)
5.181    fix N :: "'a measure" assume "sets N = UNIV" then show "N \<guillemotright>= return (count_space UNIV) = N"
5.182 @@ -661,9 +717,6 @@
5.183       (auto intro!: bind_assoc[where N="count_space UNIV" and R="count_space UNIV"]
5.184             simp: measurable_def space_subprob_algebra prob_space_imp_subprob_space)
5.185
5.186 -lemma measure_pmf_bind: "measure_pmf (bind_pmf M f) = (measure_pmf M \<guillemotright>= (\<lambda>x. measure_pmf (f x)))"
5.187 -  by transfer simp
5.188 -
5.189  end
5.190
5.191  definition "pair_pmf A B = bind_pmf A (\<lambda>x. bind_pmf B (\<lambda>y. return_pmf (x, y)))"
5.192 @@ -676,6 +729,9 @@
5.193    apply (auto simp: indicator_eq_0_iff setsum_nonneg_eq_0_iff pmf_nonneg)
5.194    done
5.195
5.196 +lemma set_pair_pmf: "set_pmf (pair_pmf A B) = set_pmf A \<times> set_pmf B"
5.197 +  unfolding pair_pmf_def set_bind_pmf set_return_pmf by auto
5.198 +
5.199  lemma bind_pair_pmf:
5.200    assumes M[measurable]: "M \<in> measurable (count_space UNIV \<Otimes>\<^sub>M count_space UNIV) (subprob_algebra N)"
5.201    shows "measure_pmf (pair_pmf A B) \<guillemotright>= M = (measure_pmf A \<guillemotright>= (\<lambda>x. measure_pmf B \<guillemotright>= (\<lambda>y. M (x, y))))"
5.202 @@ -700,18 +756,18 @@
5.203    then show "emeasure ?L X = emeasure ?R X"
5.204      apply (simp add: emeasure_bind[OF _ M' X])
5.205      unfolding pair_pmf_def measure_pmf_bind[of A]
5.206 -    apply (subst nn_integral_bind[OF _ emeasure_nonneg])
5.207 +    apply (subst nn_integral_bind)
5.208      apply (rule measurable_compose[OF M' measurable_emeasure_subprob_algebra, OF X])
5.209      apply (subst measurable_cong_sets[OF sets_measure_pmf_count_space refl])
5.210      apply (subst subprob_algebra_cong[OF sets_measure_pmf_count_space])
5.211      apply measurable
5.212      unfolding measure_pmf_bind
5.213 -    apply (subst nn_integral_bind[OF _ emeasure_nonneg])
5.214 +    apply (subst nn_integral_bind)
5.215      apply (rule measurable_compose[OF M' measurable_emeasure_subprob_algebra, OF X])
5.216      apply (subst measurable_cong_sets[OF sets_measure_pmf_count_space refl])
5.217      apply (subst subprob_algebra_cong[OF sets_measure_pmf_count_space])
5.218      apply measurable
5.219 -    apply (simp add: nn_integral_measure_pmf_finite set_pmf_return emeasure_nonneg pmf_return one_ereal_def[symmetric])
5.220 +    apply (simp add: nn_integral_measure_pmf_finite set_return_pmf emeasure_nonneg pmf_return one_ereal_def[symmetric])
5.221      apply (subst emeasure_bind[OF _ _ X])
5.222      apply simp
5.223      apply (rule measurable_bind[where N="count_space UNIV"])
5.224 @@ -727,15 +783,6 @@
5.225      done
5.226  qed
5.227
5.228 -lemma set_pmf_bind: "set_pmf (bind_pmf M N) = (\<Union>M\<in>set_pmf M. set_pmf (N M))"
5.229 -  apply (simp add: set_eq_iff set_pmf_iff pmf_bind)
5.230 -  apply (subst integral_nonneg_eq_0_iff_AE)
5.231 -  apply (auto simp: pmf_nonneg pmf_le_1 AE_measure_pmf_iff
5.232 -              intro!: measure_pmf.integrable_const_bound[where B=1])
5.233 -  done
5.234 -
5.235 -lemma set_pmf_pair_pmf: "set_pmf (pair_pmf A B) = set_pmf A \<times> set_pmf B"
5.236 -  unfolding pair_pmf_def set_pmf_bind set_pmf_return by auto
5.237
5.238  (*
5.239
```