--- a/src/HOL/Probability/Borel_Space.thy Fri Nov 16 16:59:56 2012 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Fri Nov 16 18:49:46 2012 +0100
@@ -84,8 +84,13 @@
unfolding indicator_def [abs_def] using A
by (auto intro!: measurable_If_set)
-lemma borel_measurable_indicator'[measurable]:
- "{x\<in>space M. x \<in> A} \<in> sets M \<Longrightarrow> indicator A \<in> borel_measurable M"
+lemma borel_measurable_count_space[measurable (raw)]:
+ "f \<in> borel_measurable (count_space S)"
+ unfolding measurable_def by auto
+
+lemma borel_measurable_indicator'[measurable (raw)]:
+ assumes [measurable]: "{x\<in>space M. f x \<in> A x} \<in> sets M"
+ shows "(\<lambda>x. indicator (A x) (f x)) \<in> borel_measurable M"
unfolding indicator_def[abs_def]
by (auto intro!: measurable_If)
--- a/src/HOL/Probability/Fin_Map.thy Fri Nov 16 16:59:56 2012 +0100
+++ b/src/HOL/Probability/Fin_Map.thy Fri Nov 16 18:49:46 2012 +0100
@@ -1278,7 +1278,7 @@
subsection {* Isomorphism between Functions and Finite Maps *}
lemma
- measurable_compose:
+ measurable_finmap_compose:
fixes f::"'a \<Rightarrow> 'b"
assumes inj: "\<And>j. j \<in> J \<Longrightarrow> f' (f j) = j"
assumes "finite J"
@@ -1326,7 +1326,7 @@
shows "(\<lambda>m. compose (f ` J) m f') \<in> measurable (PiM J (\<lambda>_. M)) (PiM (f ` J) (\<lambda>_. M))"
proof -
have "(\<lambda>m. compose (f ` J) m f') \<in> measurable (Pi\<^isub>M (f' ` f ` J) (\<lambda>_. M)) (Pi\<^isub>M (f ` J) (\<lambda>_. M))"
- using assms by (auto intro: measurable_compose)
+ using assms by (auto intro: measurable_finmap_compose)
moreover
from inj have "f' ` f ` J = J" by (metis (hide_lams, mono_tags) image_iff set_eqI)
ultimately show ?thesis by simp
@@ -1426,7 +1426,7 @@
proof (rule measurable_comp, rule measurable_proj_PiM)
show "(\<lambda>g. compose J g f) \<in>
measurable (Pi\<^isub>M (f ` J) (\<lambda>x. M)) (Pi\<^isub>M J (\<lambda>_. M))"
- by (rule measurable_compose, rule inv) auto
+ by (rule measurable_finmap_compose, rule inv) auto
qed (auto simp add: space_PiM extensional_def assms)
lemma fm_image_measurable:
--- a/src/HOL/Probability/Finite_Product_Measure.thy Fri Nov 16 16:59:56 2012 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Fri Nov 16 18:49:46 2012 +0100
@@ -540,6 +540,18 @@
finally show "f -` A \<inter> space N \<in> sets N" .
qed (auto simp: space)
+lemma measurable_PiM_single':
+ assumes f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> measurable N (M i)"
+ and "(\<lambda>\<omega> i. f i \<omega>) \<in> space N \<rightarrow> (\<Pi>\<^isub>E i\<in>I. space (M i))"
+ shows "(\<lambda>\<omega> i. f i \<omega>) \<in> measurable N (Pi\<^isub>M I M)"
+proof (rule measurable_PiM_single)
+ fix A i assume A: "i \<in> I" "A \<in> sets (M i)"
+ then have "{\<omega> \<in> space N. f i \<omega> \<in> A} = f i -` A \<inter> space N"
+ by auto
+ then show "{\<omega> \<in> space N. f i \<omega> \<in> A} \<in> sets N"
+ using A f by (auto intro!: measurable_sets)
+qed fact
+
lemma sets_PiM_I_finite[measurable]:
assumes "finite I" and sets: "(\<And>i. i \<in> I \<Longrightarrow> E i \<in> sets (M i))"
shows "(PIE j:I. E j) \<in> sets (PIM i:I. M i)"
@@ -562,12 +574,22 @@
shows "(\<lambda>x. (f x) i) \<in> measurable N (M i)"
using measurable_compose[OF f measurable_component_singleton, OF i] .
+lemma measurable_PiM_component_rev[measurable (raw)]:
+ "i \<in> I \<Longrightarrow> f \<in> measurable (M i) N \<Longrightarrow> (\<lambda>x. f (x i)) \<in> measurable (PiM I M) N"
+ by simp
+
lemma measurable_nat_case[measurable (raw)]:
assumes [measurable (raw)]: "i = 0 \<Longrightarrow> f \<in> measurable M N"
"\<And>j. i = Suc j \<Longrightarrow> (\<lambda>x. g x j) \<in> measurable M N"
shows "(\<lambda>x. nat_case (f x) (g x) i) \<in> measurable M N"
by (cases i) simp_all
+lemma measurable_nat_case'[measurable (raw)]:
+ assumes fg[measurable]: "f \<in> measurable N M" "g \<in> measurable N (\<Pi>\<^isub>M i\<in>UNIV. M)"
+ shows "(\<lambda>x. nat_case (f x) (g x)) \<in> measurable N (\<Pi>\<^isub>M i\<in>UNIV. M)"
+ using fg[THEN measurable_space]
+ by (auto intro!: measurable_PiM_single' simp add: space_PiM Pi_iff split: nat.split)
+
lemma measurable_add_dim[measurable]:
"(\<lambda>(f, y). f(i := y)) \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) (Pi\<^isub>M (insert i I) M)"
(is "?f \<in> measurable ?P ?I")
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Fri Nov 16 16:59:56 2012 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Fri Nov 16 18:49:46 2012 +0100
@@ -449,23 +449,6 @@
subsection {* Sequence space *}
-lemma measurable_nat_case: "(\<lambda>(x, \<omega>). nat_case x \<omega>) \<in> measurable (M \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)) (\<Pi>\<^isub>M i\<in>UNIV. M)"
-proof (rule measurable_PiM_single)
- show "(\<lambda>(x, \<omega>). nat_case x \<omega>) \<in> space (M \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)) \<rightarrow> (UNIV \<rightarrow>\<^isub>E space M)"
- by (auto simp: space_pair_measure space_PiM Pi_iff split: nat.split)
- fix i :: nat and A assume A: "A \<in> sets M"
- then have *: "{\<omega> \<in> space (M \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)). prod_case nat_case \<omega> i \<in> A} =
- (case i of 0 \<Rightarrow> A \<times> space (\<Pi>\<^isub>M i\<in>UNIV. M) | Suc n \<Rightarrow> space M \<times> {\<omega>\<in>space (\<Pi>\<^isub>M i\<in>UNIV. M). \<omega> n \<in> A})"
- by (auto simp: space_PiM space_pair_measure split: nat.split dest: sets_into_space)
- show "{\<omega> \<in> space (M \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)). prod_case nat_case \<omega> i \<in> A} \<in> sets (M \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M))"
- unfolding * by (auto simp: A split: nat.split intro!: sets_Collect_single)
-qed
-
-lemma measurable_nat_case':
- assumes f: "f \<in> measurable N M" and g: "g \<in> measurable N (\<Pi>\<^isub>M i\<in>UNIV. M)"
- shows "(\<lambda>x. nat_case (f x) (g x)) \<in> measurable N (\<Pi>\<^isub>M i\<in>UNIV. M)"
- using measurable_compose[OF measurable_Pair[OF f g] measurable_nat_case] by simp
-
definition comb_seq :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a)" where
"comb_seq i \<omega> \<omega>' j = (if j < i then \<omega> j else \<omega>' (j - i))"
@@ -475,7 +458,8 @@
lemma split_comb_seq_asm: "P (comb_seq i \<omega> \<omega>' j) \<longleftrightarrow> \<not> ((j < i \<and> \<not> P (\<omega> j)) \<or> (\<exists>k. j = i + k \<and> \<not> P (\<omega>' k)))"
by (auto simp: comb_seq_def)
-lemma measurable_comb_seq: "(\<lambda>(\<omega>, \<omega>'). comb_seq i \<omega> \<omega>') \<in> measurable ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)) (\<Pi>\<^isub>M i\<in>UNIV. M)"
+lemma measurable_comb_seq:
+ "(\<lambda>(\<omega>, \<omega>'). comb_seq i \<omega> \<omega>') \<in> measurable ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)) (\<Pi>\<^isub>M i\<in>UNIV. M)"
proof (rule measurable_PiM_single)
show "(\<lambda>(\<omega>, \<omega>'). comb_seq i \<omega> \<omega>') \<in> space ((\<Pi>\<^isub>M i\<in>UNIV. M) \<Otimes>\<^isub>M (\<Pi>\<^isub>M i\<in>UNIV. M)) \<rightarrow> (UNIV \<rightarrow>\<^isub>E space M)"
by (auto simp: space_pair_measure space_PiM Pi_iff split: split_comb_seq)
@@ -488,11 +472,33 @@
unfolding * by (auto simp: A intro!: sets_Collect_single)
qed
-lemma measurable_comb_seq':
+lemma measurable_comb_seq'[measurable (raw)]:
assumes f: "f \<in> measurable N (\<Pi>\<^isub>M i\<in>UNIV. M)" and g: "g \<in> measurable N (\<Pi>\<^isub>M i\<in>UNIV. M)"
shows "(\<lambda>x. comb_seq i (f x) (g x)) \<in> measurable N (\<Pi>\<^isub>M i\<in>UNIV. M)"
using measurable_compose[OF measurable_Pair[OF f g] measurable_comb_seq] by simp
+lemma comb_seq_0: "comb_seq 0 \<omega> \<omega>' = \<omega>'"
+ by (auto simp add: comb_seq_def)
+
+lemma comb_seq_Suc: "comb_seq (Suc n) \<omega> \<omega>' = comb_seq n \<omega> (nat_case (\<omega> n) \<omega>')"
+ by (auto simp add: comb_seq_def not_less less_Suc_eq le_imp_diff_is_add intro!: ext split: nat.split)
+
+lemma comb_seq_Suc_0[simp]: "comb_seq (Suc 0) \<omega> = nat_case (\<omega> 0)"
+ by (intro ext) (simp add: comb_seq_Suc comb_seq_0)
+
+lemma comb_seq_less: "i < n \<Longrightarrow> comb_seq n \<omega> \<omega>' i = \<omega> i"
+ by (auto split: split_comb_seq)
+
+lemma comb_seq_add: "comb_seq n \<omega> \<omega>' (i + n) = \<omega>' i"
+ by (auto split: nat.split split_comb_seq)
+
+lemma nat_case_comb_seq: "nat_case s' (comb_seq n \<omega> \<omega>') (i + n) = nat_case (nat_case s' \<omega> n) \<omega>' i"
+ by (auto split: nat.split split_comb_seq)
+
+lemma nat_case_comb_seq':
+ "nat_case s (comb_seq i \<omega> \<omega>') = comb_seq (Suc i) (nat_case s \<omega>) \<omega>'"
+ by (auto split: split_comb_seq nat.split)
+
locale sequence_space = product_prob_space "\<lambda>i. M" "UNIV :: nat set" for M
begin
@@ -578,7 +584,7 @@
by (auto simp: space_pair_measure space_PiM Pi_iff prod_emb_def all_conj_distrib
split: nat.split nat.split_asm)
then have "emeasure ?D ?X = emeasure (M \<Otimes>\<^isub>M S) (?E \<times> ?F)"
- by (subst emeasure_distr[OF measurable_nat_case])
+ by (subst emeasure_distr)
(auto intro!: sets_PiM_I simp: split_beta' J)
also have "\<dots> = emeasure M ?E * emeasure S ?F"
using J by (intro P.emeasure_pair_measure_Times) (auto intro!: sets_PiM_I finite_vimageI)
--- a/src/HOL/Probability/Lebesgue_Integration.thy Fri Nov 16 16:59:56 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Fri Nov 16 18:49:46 2012 +0100
@@ -1181,6 +1181,17 @@
by (subst positive_integral_eq_simple_integral)
(auto simp: simple_function_indicator simple_integral_indicator)
+lemma positive_integral_indicator':
+ assumes [measurable]: "A \<inter> space M \<in> sets M"
+ shows "(\<integral>\<^isup>+ x. indicator A x \<partial>M) = emeasure M (A \<inter> space M)"
+proof -
+ have "(\<integral>\<^isup>+ x. indicator A x \<partial>M) = (\<integral>\<^isup>+ x. indicator (A \<inter> space M) x \<partial>M)"
+ by (intro positive_integral_cong) (simp split: split_indicator)
+ also have "\<dots> = emeasure M (A \<inter> space M)"
+ by simp
+ finally show ?thesis .
+qed
+
lemma positive_integral_add:
assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
and g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
@@ -1430,6 +1441,32 @@
done
qed
+lemma positive_integral_nat_function:
+ fixes f :: "'a \<Rightarrow> nat"
+ assumes "f \<in> measurable M (count_space UNIV)"
+ shows "(\<integral>\<^isup>+x. ereal (of_nat (f x)) \<partial>M) = (\<Sum>t. emeasure M {x\<in>space M. t < f x})"
+proof -
+ def F \<equiv> "\<lambda>i. {x\<in>space M. i < f x}"
+ with assms have [measurable]: "\<And>i. F i \<in> sets M"
+ by auto
+
+ { fix x assume "x \<in> space M"
+ have "(\<lambda>i. if i < f x then 1 else 0) sums (of_nat (f x)::real)"
+ using sums_If_finite[of "\<lambda>i. i < f x" "\<lambda>_. 1::real"] by simp
+ then have "(\<lambda>i. ereal(if i < f x then 1 else 0)) sums (ereal(of_nat(f x)))"
+ unfolding sums_ereal .
+ moreover have "\<And>i. ereal (if i < f x then 1 else 0) = indicator (F i) x"
+ using `x \<in> space M` by (simp add: one_ereal_def F_def)
+ ultimately have "ereal(of_nat(f x)) = (\<Sum>i. indicator (F i) x)"
+ by (simp add: sums_iff) }
+ then have "(\<integral>\<^isup>+x. ereal (of_nat (f x)) \<partial>M) = (\<integral>\<^isup>+x. (\<Sum>i. indicator (F i) x) \<partial>M)"
+ by (simp cong: positive_integral_cong)
+ also have "\<dots> = (\<Sum>i. emeasure M (F i))"
+ by (simp add: positive_integral_suminf)
+ finally show ?thesis
+ by (simp add: F_def)
+qed
+
section "Lebesgue Integral"
definition integrable :: "'a measure \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool" where
@@ -1639,25 +1676,9 @@
unfolding integrable_def lebesgue_integral_def
by auto
-lemma integral_cmult[simp, intro]:
- assumes "integrable M f"
- shows "integrable M (\<lambda>t. a * f t)" (is ?P)
- and "(\<integral> t. a * f t \<partial>M) = a * integral\<^isup>L M f" (is ?I)
-proof -
- have "integrable M (\<lambda>t. a * f t) \<and> (\<integral> t. a * f t \<partial>M) = a * integral\<^isup>L M f"
- proof (cases rule: le_cases)
- assume "0 \<le> a" show ?thesis
- using integral_linear[OF assms integral_zero(1) `0 \<le> a`]
- by simp
- next
- assume "a \<le> 0" hence "0 \<le> - a" by auto
- have *: "\<And>t. - a * t + 0 = (-a) * t" by simp
- show ?thesis using integral_linear[OF assms integral_zero(1) `0 \<le> - a`]
- integral_minus(1)[of M "\<lambda>t. - a * f t"]
- unfolding * integral_zero by simp
- qed
- thus ?P ?I by auto
-qed
+lemma lebesgue_integral_uminus:
+ "(\<integral>x. - f x \<partial>M) = - integral\<^isup>L M f"
+ unfolding lebesgue_integral_def by simp
lemma lebesgue_integral_cmult_nonneg:
assumes f: "f \<in> borel_measurable M" and "0 \<le> c"
@@ -1682,10 +1703,6 @@
by (simp add: lebesgue_integral_def field_simps)
qed
-lemma lebesgue_integral_uminus:
- "(\<integral>x. - f x \<partial>M) = - integral\<^isup>L M f"
- unfolding lebesgue_integral_def by simp
-
lemma lebesgue_integral_cmult:
assumes f: "f \<in> borel_measurable M"
shows "(\<integral>x. c * f x \<partial>M) = c * integral\<^isup>L M f"
@@ -1698,10 +1715,33 @@
by (simp add: lebesgue_integral_def)
qed
+lemma lebesgue_integral_multc:
+ "f \<in> borel_measurable M \<Longrightarrow> (\<integral>x. f x * c \<partial>M) = integral\<^isup>L M f * c"
+ using lebesgue_integral_cmult[of f M c] by (simp add: ac_simps)
+
lemma integral_multc:
+ "integrable M f \<Longrightarrow> (\<integral> x. f x * c \<partial>M) = integral\<^isup>L M f * c"
+ by (simp add: lebesgue_integral_multc)
+
+lemma integral_cmult[simp, intro]:
assumes "integrable M f"
- shows "(\<integral> x. f x * c \<partial>M) = integral\<^isup>L M f * c"
- unfolding mult_commute[of _ c] integral_cmult[OF assms] ..
+ shows "integrable M (\<lambda>t. a * f t)" (is ?P)
+ and "(\<integral> t. a * f t \<partial>M) = a * integral\<^isup>L M f" (is ?I)
+proof -
+ have "integrable M (\<lambda>t. a * f t) \<and> (\<integral> t. a * f t \<partial>M) = a * integral\<^isup>L M f"
+ proof (cases rule: le_cases)
+ assume "0 \<le> a" show ?thesis
+ using integral_linear[OF assms integral_zero(1) `0 \<le> a`]
+ by simp
+ next
+ assume "a \<le> 0" hence "0 \<le> - a" by auto
+ have *: "\<And>t. - a * t + 0 = (-a) * t" by simp
+ show ?thesis using integral_linear[OF assms integral_zero(1) `0 \<le> - a`]
+ integral_minus(1)[of M "\<lambda>t. - a * f t"]
+ unfolding * integral_zero by simp
+ qed
+ thus ?P ?I by auto
+qed
lemma integral_diff[simp, intro]:
assumes f: "integrable M f" and g: "integrable M g"
@@ -1713,7 +1753,7 @@
lemma integral_indicator[simp, intro]:
assumes "A \<in> sets M" and "(emeasure M) A \<noteq> \<infinity>"
- shows "integral\<^isup>L M (indicator A) = real ((emeasure M) A)" (is ?int)
+ shows "integral\<^isup>L M (indicator A) = real (emeasure M A)" (is ?int)
and "integrable M (indicator A)" (is ?able)
proof -
from `A \<in> sets M` have *:
@@ -1850,6 +1890,16 @@
finally show ?thesis .
qed
+lemma integrable_nonneg:
+ assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "(\<integral>\<^isup>+ x. f x \<partial>M) \<noteq> \<infinity>"
+ shows "integrable M f"
+ unfolding integrable_def
+proof (intro conjI f)
+ have "(\<integral>\<^isup>+ x. ereal (- f x) \<partial>M) = 0"
+ using f by (subst positive_integral_0_iff_AE) auto
+ then show "(\<integral>\<^isup>+ x. ereal (- f x) \<partial>M) \<noteq> \<infinity>" by simp
+qed
+
lemma integral_positive:
assumes "integrable M f" "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x"
shows "0 \<le> integral\<^isup>L M f"
@@ -1986,7 +2036,7 @@
lemma (in finite_measure) lebesgue_integral_const[simp]:
shows "integrable M (\<lambda>x. a)"
- and "(\<integral>x. a \<partial>M) = a * (measure M) (space M)"
+ and "(\<integral>x. a \<partial>M) = a * measure M (space M)"
proof -
{ fix a :: real assume "0 \<le> a"
then have "(\<integral>\<^isup>+ x. ereal a \<partial>M) = ereal a * (emeasure M) (space M)"
@@ -2008,6 +2058,10 @@
by (simp add: lebesgue_integral_def positive_integral_const_If emeasure_eq_measure)
qed
+lemma (in finite_measure) integrable_const_bound:
+ assumes "AE x in M. \<bar>f x\<bar> \<le> B" and "f \<in> borel_measurable M" shows "integrable M f"
+ by (auto intro: integrable_bound[where f="\<lambda>x. B"] lebesgue_integral_const assms)
+
lemma indicator_less[simp]:
"indicator A x \<le> (indicator B x::ereal) \<longleftrightarrow> (x \<in> A \<longrightarrow> x \<in> B)"
by (simp add: indicator_def not_le)
--- a/src/HOL/Probability/Probability_Measure.thy Fri Nov 16 16:59:56 2012 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy Fri Nov 16 18:49:46 2012 +0100
@@ -219,6 +219,17 @@
with AE_in_set_eq_1 assms show ?thesis by simp
qed
+lemma (in prob_space) AE_const[simp]: "(AE x in M. P) \<longleftrightarrow> P"
+ by (cases P) (auto simp: AE_False)
+
+lemma (in prob_space) AE_contr:
+ assumes ae: "AE \<omega> in M. P \<omega>" "AE \<omega> in M. \<not> P \<omega>"
+ shows False
+proof -
+ from ae have "AE \<omega> in M. False" by eventually_elim auto
+ then show False by auto
+qed
+
lemma (in finite_measure) prob_space_increasing: "increasing M (measure M)"
by (auto intro!: finite_measure_mono simp: increasing_def)
@@ -438,6 +449,23 @@
then show ?thesis by simp
qed (simp add: measure_notin_sets)
+lemma (in prob_space) prob_Collect_eq_0:
+ "{x \<in> space M. P x} \<in> sets M \<Longrightarrow> \<P>(x in M. P x) = 0 \<longleftrightarrow> (AE x in M. \<not> P x)"
+ using AE_iff_measurable[OF _ refl, of M "\<lambda>x. \<not> P x"] by (simp add: emeasure_eq_measure)
+
+lemma (in prob_space) prob_Collect_eq_1:
+ "{x \<in> space M. P x} \<in> sets M \<Longrightarrow> \<P>(x in M. P x) = 1 \<longleftrightarrow> (AE x in M. P x)"
+ using AE_in_set_eq_1[of "{x\<in>space M. P x}"] by simp
+
+lemma (in prob_space) prob_eq_0:
+ "A \<in> sets M \<Longrightarrow> prob A = 0 \<longleftrightarrow> (AE x in M. x \<notin> A)"
+ using AE_iff_measurable[OF _ refl, of M "\<lambda>x. x \<notin> A"]
+ by (auto simp add: emeasure_eq_measure Int_def[symmetric])
+
+lemma (in prob_space) prob_eq_1:
+ "A \<in> sets M \<Longrightarrow> prob A = 1 \<longleftrightarrow> (AE x in M. x \<in> A)"
+ using AE_in_set_eq_1[of A] by simp
+
lemma (in prob_space) prob_sums:
assumes P: "\<And>n. {x\<in>space M. P n x} \<in> events"
assumes Q: "{x\<in>space M. Q x} \<in> events"
--- a/src/HOL/Probability/Projective_Family.thy Fri Nov 16 16:59:56 2012 +0100
+++ b/src/HOL/Probability/Projective_Family.thy Fri Nov 16 18:49:46 2012 +0100
@@ -81,7 +81,7 @@
fixes I::"'i set" and P::"'i set \<Rightarrow> ('i \<Rightarrow> 'a) measure" and M::"('i \<Rightarrow> 'a measure)"
assumes projective: "\<And>J H X. J \<noteq> {} \<Longrightarrow> J \<subseteq> H \<Longrightarrow> H \<subseteq> I \<Longrightarrow> finite H \<Longrightarrow> X \<in> sets (PiM J M) \<Longrightarrow>
(P H) (prod_emb H M J X) = (P J) X"
- assumes prob_space: "\<And>J. finite J \<Longrightarrow> prob_space (P J)"
+ assumes proj_prob_space: "\<And>J. finite J \<Longrightarrow> prob_space (P J)"
assumes proj_space: "\<And>J. finite J \<Longrightarrow> space (P J) = space (PiM J M)"
assumes proj_sets: "\<And>J. finite J \<Longrightarrow> sets (P J) = sets (PiM J M)"
begin
@@ -133,7 +133,7 @@
let ?\<Omega> = "(\<Pi>\<^isub>E k\<in>J. space (M k))"
show "Int_stable ?J"
by (rule Int_stable_PiE)
- interpret prob_space "P J" using prob_space `finite J` by simp
+ interpret prob_space "P J" using proj_prob_space `finite J` by simp
show "emeasure ?P (?F _) \<noteq> \<infinity>" using assms `finite J` by (auto simp: emeasure_limP)
show "?J \<subseteq> Pow ?\<Omega>" by (auto simp: Pi_iff dest: sets_into_space)
show "sets (limP J M P) = sigma_sets ?\<Omega> ?J" "sets (P J) = sigma_sets ?\<Omega> ?J"
@@ -165,7 +165,7 @@
have "\<forall>i\<in>L. \<exists>x. x \<in> space (M i)"
proof
fix i assume "i \<in> L"
- interpret prob_space "P {i}" using prob_space by simp
+ interpret prob_space "P {i}" using proj_prob_space by simp
from not_empty show "\<exists>x. x \<in> space (M i)" by (auto simp add: proj_space space_PiM)
qed
from bchoice[OF this]
--- a/src/HOL/Probability/Projective_Limit.thy Fri Nov 16 16:59:56 2012 +0100
+++ b/src/HOL/Probability/Projective_Limit.thy Fri Nov 16 18:49:46 2012 +0100
@@ -207,7 +207,7 @@
OF `I \<noteq> {}`, OF `I \<noteq> {}`])
fix A assume "A \<in> ?G"
with generatorE guess J X . note JX = this
- interpret prob_space "P J" using prob_space[OF `finite J`] .
+ interpret prob_space "P J" using proj_prob_space[OF `finite J`] .
show "\<mu>G A \<noteq> \<infinity>" using JX by (simp add: limP_finite)
next
fix Z assume Z: "range Z \<subseteq> ?G" "decseq Z" "(\<Inter>i. Z i) = {}"
@@ -241,7 +241,7 @@
note [simp] = `\<And>n. finite (J n)`
from J Z_emb have Z_eq: "\<And>n. Z n = emb I (J n) (B n)" "\<And>n. Z n \<in> ?G"
unfolding J_def B_def by (subst prod_emb_trans) (insert Z, auto)
- interpret prob_space "P (J i)" for i using prob_space by simp
+ interpret prob_space "P (J i)" for i using proj_prob_space by simp
have "?a \<le> \<mu>G (Z 0)" by (auto intro: INF_lower)
also have "\<dots> < \<infinity>" using J by (auto simp: Z_eq \<mu>G_eq limP_finite proj_sets)
finally have "?a \<noteq> \<infinity>" by simp
@@ -636,13 +636,13 @@
show "emeasure (lim\<^isub>B I P) (space (lim\<^isub>B I P)) = 1"
proof cases
assume "I = {}"
- interpret prob_space "P {}" using prob_space by simp
+ interpret prob_space "P {}" using proj_prob_space by simp
show ?thesis
by (simp add: space_PiM_empty limP_finite emeasure_space_1 `I = {}`)
next
assume "I \<noteq> {}"
then obtain i where "i \<in> I" by auto
- interpret prob_space "P {i}" using prob_space by simp
+ interpret prob_space "P {i}" using proj_prob_space by simp
have R: "(space (lim\<^isub>B I P)) = (emb I {i} (Pi\<^isub>E {i} (\<lambda>_. space borel)))"
by (auto simp: prod_emb_def space_PiM)
moreover have "extensional {i} = space (P {i})" by (simp add: proj_space space_PiM)
@@ -660,7 +660,7 @@
assumes X: "J \<subseteq> I" "finite J" "\<forall>i\<in>J. B i \<in> sets borel"
shows "emeasure (lim\<^isub>B I P) (emb I J (Pi\<^isub>E J B)) = emeasure (P J) (Pi\<^isub>E J B)"
proof cases
- interpret prob_space "P {}" using prob_space by simp
+ interpret prob_space "P {}" using proj_prob_space by simp
assume "J = {}"
moreover have "emb I {} {\<lambda>x. undefined} = space (lim\<^isub>B I P)"
by (auto simp: space_PiM prod_emb_def)
@@ -677,7 +677,7 @@
assumes "J \<subseteq> I" "finite J" "\<forall>i\<in>J. B i \<in> sets borel"
shows "measure (lim\<^isub>B I P) (emb I J (Pi\<^isub>E J B)) = measure (P J) (Pi\<^isub>E J B)"
proof -
- interpret prob_space "P J" using prob_space assms by simp
+ interpret prob_space "P J" using proj_prob_space assms by simp
show ?thesis
using emeasure_limB_emb[OF assms]
unfolding emeasure_eq_measure limP_finite[OF `finite J` `J \<subseteq> I`] P.emeasure_eq_measure
--- a/src/HOL/Probability/Sigma_Algebra.thy Fri Nov 16 16:59:56 2012 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy Fri Nov 16 18:49:46 2012 +0100
@@ -1616,7 +1616,7 @@
fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt)))
fun inst t (ts, Ts) = Drule.instantiate' (cert ctyp_of Ts) (cert cterm_of ts) t
val cps = cnt_prefixes ctxt f |> map (inst @{thm measurable_compose_countable})
- in if null cps then no_tac else debug_tac ctxt (K ("split countable fun")) (resolve_tac cps i) end
+ in if null cps then no_tac else debug_tac ctxt (K "split countable fun") (resolve_tac cps i) end
handle TERM _ => no_tac) 1)
fun measurable_tac' ctxt ss facts = let
@@ -1764,7 +1764,7 @@
"pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x = P x)"
"pred M (\<lambda>x. f x \<in> UNIV)"
"pred M (\<lambda>x. f x \<in> {})"
- "pred M (\<lambda>x. P' (f x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> {x. P' x})"
+ "pred M (\<lambda>x. P' (f x) x) \<Longrightarrow> pred M (\<lambda>x. f x \<in> {y. P' y x})"
"pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> - (B x))"
"pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) - (B x))"
"pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<inter> (B x))"
@@ -1815,10 +1815,23 @@
qed
lemma [measurable (raw generic)]:
- assumes f: "f \<in> measurable M N" and c: "{c} \<in> sets N"
+ assumes f: "f \<in> measurable M N" and c: "c \<in> space N \<Longrightarrow> {c} \<in> sets N"
shows pred_eq_const1: "pred M (\<lambda>x. f x = c)"
and pred_eq_const2: "pred M (\<lambda>x. c = f x)"
- using measurable_sets[OF f c] by (auto simp: Int_def conj_commute eq_commute pred_def)
+proof -
+ show "pred M (\<lambda>x. f x = c)"
+ proof cases
+ assume "c \<in> space N"
+ with measurable_sets[OF f c] show ?thesis
+ by (auto simp: Int_def conj_commute pred_def)
+ next
+ assume "c \<notin> space N"
+ with f[THEN measurable_space] have "{x \<in> space M. f x = c} = {}" by auto
+ then show ?thesis by (auto simp: pred_def cong: conj_cong)
+ qed
+ then show "pred M (\<lambda>x. c = f x)"
+ by (simp add: eq_commute)
+qed
lemma pred_le_const[measurable (raw generic)]:
assumes f: "f \<in> measurable M N" and c: "{.. c} \<in> sets N" shows "pred M (\<lambda>x. f x \<le> c)"
@@ -1872,6 +1885,21 @@
"\<forall>i\<in>I. A i \<in> sets (N i) \<Longrightarrow> i\<in>I \<Longrightarrow> f \<in> measurable M (N i) \<Longrightarrow> pred M (\<lambda>x. f x \<in> A i)"
using pred_sets2[OF sets_Ball, of _ _ _ f] by auto
+lemma measurable_finite[measurable (raw)]:
+ fixes S :: "'a \<Rightarrow> nat set"
+ assumes [measurable]: "\<And>i. {x\<in>space M. i \<in> S x} \<in> sets M"
+ shows "pred M (\<lambda>x. finite (S x))"
+ unfolding finite_nat_set_iff_bounded by (simp add: Ball_def)
+
+lemma measurable_Least[measurable]:
+ assumes [measurable]: "(\<And>i::nat. (\<lambda>x. P i x) \<in> measurable M (count_space UNIV))"q
+ shows "(\<lambda>x. LEAST i. P i x) \<in> measurable M (count_space UNIV)"
+ unfolding measurable_def by (safe intro!: sets_Least) simp_all
+
+lemma measurable_count_space_insert[measurable (raw)]:
+ "s \<in> S \<Longrightarrow> A \<in> sets (count_space S) \<Longrightarrow> insert s A \<in> sets (count_space S)"
+ by simp
+
hide_const (open) pred
subsection {* Extend measure *}