--- a/src/HOL/Probability/Complete_Measure.thy Fri Feb 04 17:11:00 2011 +0100
+++ b/src/HOL/Probability/Complete_Measure.thy Fri Feb 04 17:25:12 2011 +0100
@@ -266,7 +266,7 @@
proof (intro bexI)
from AE[unfolded all_AE_countable]
show "AE x. g x = (SUP i. f' i x)" (is "AE x. g x = ?f x")
- proof (rule AE_mp, safe intro!: AE_cong)
+ proof (elim AE_mp, safe intro!: AE_I2)
fix x assume eq: "\<forall>i. f i x = f' i x"
moreover have "g = SUPR UNIV f" using `f \<up> g` unfolding isoton_def by simp
ultimately show "g x = ?f x" by (simp add: SUPR_apply)
--- a/src/HOL/Probability/Lebesgue_Integration.thy Fri Feb 04 17:11:00 2011 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Fri Feb 04 17:25:12 2011 +0100
@@ -694,10 +694,7 @@
assumes "simple_function M f" and "simple_function M g"
and mono: "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x"
shows "integral\<^isup>S M f \<le> integral\<^isup>S M g"
-proof (rule simple_integral_mono_AE[OF assms(1, 2)])
- show "AE x. f x \<le> g x"
- using mono by (rule AE_cong) auto
-qed
+ using assms by (intro simple_integral_mono_AE) auto
lemma (in measure_space) simple_integral_cong_AE:
assumes "simple_function M f" "simple_function M g" and "AE x. f x = g x"
@@ -782,20 +779,14 @@
have "AE x. indicator N x = (0 :: pextreal)"
using `N \<in> null_sets` by (auto simp: indicator_def intro!: AE_I[of _ N])
then have "(\<integral>\<^isup>Sx. u x * indicator N x \<partial>M) = (\<integral>\<^isup>Sx. 0 \<partial>M)"
- using assms by (intro simple_integral_cong_AE) (auto intro!: AE_disjI2)
+ using assms by (intro simple_integral_cong_AE) auto
then show ?thesis by simp
qed
lemma (in measure_space) simple_integral_cong_AE_mult_indicator:
assumes sf: "simple_function M f" and eq: "AE x. x \<in> S" and "S \<in> sets M"
shows "integral\<^isup>S M f = (\<integral>\<^isup>Sx. f x * indicator S x \<partial>M)"
-proof (rule simple_integral_cong_AE)
- show "simple_function M f" by fact
- show "simple_function M (\<lambda>x. f x * indicator S x)"
- using sf `S \<in> sets M` by auto
- from eq show "AE x. f x = f x * indicator S x"
- by (rule AE_mp) simp
-qed
+ using assms by (intro simple_integral_cong_AE) auto
lemma (in measure_space) simple_integral_restricted:
assumes "A \<in> sets M"
@@ -1004,7 +995,7 @@
have *: "{x \<in> space M. \<not> a x \<le> a x * indicator (space M - N) x} =
N \<inter> {x \<in> space M. a x \<noteq> 0}" (is "?N = _")
using `N \<in> sets M`[THEN sets_into_space] by (auto simp: indicator_def)
- then show "?N \<in> sets M"
+ then show "?N \<in> sets M"
using `N \<in> sets M` `simple_function M a`[THEN borel_measurable_simple_function]
by (auto intro!: measure_mono Int)
then have "\<mu> ?N \<le> \<mu> N"
@@ -1032,9 +1023,8 @@
by (auto simp: eq_iff intro!: positive_integral_mono_AE)
lemma (in measure_space) positive_integral_mono:
- assumes mono: "\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x"
- shows "integral\<^isup>P M u \<le> integral\<^isup>P M v"
- using mono by (auto intro!: AE_cong positive_integral_mono_AE)
+ "(\<And>x. x \<in> space M \<Longrightarrow> u x \<le> v x) \<Longrightarrow> integral\<^isup>P M u \<le> integral\<^isup>P M v"
+ by (auto intro: positive_integral_mono_AE)
lemma image_set_cong:
assumes A: "\<And>x. x \<in> A \<Longrightarrow> \<exists>y\<in>B. f x = g y"
@@ -1487,6 +1477,16 @@
qed
qed
+lemma (in measure_space) positive_integral_0_iff_AE:
+ assumes u: "u \<in> borel_measurable M"
+ shows "integral\<^isup>P M u = 0 \<longleftrightarrow> (AE x. u x = 0)"
+proof -
+ have sets: "{x\<in>space M. u x \<noteq> 0} \<in> sets M"
+ using u by auto
+ then show ?thesis
+ using positive_integral_0_iff[OF u] AE_iff_null_set[OF sets] by auto
+qed
+
lemma (in measure_space) positive_integral_restricted:
assumes "A \<in> sets M"
shows "integral\<^isup>P (restricted_space A) f = (\<integral>\<^isup>+ x. f x * indicator A x \<partial>M)"
@@ -1585,10 +1585,8 @@
assumes cong: "AE x. f x = g x"
shows "integral\<^isup>L M f = integral\<^isup>L M g"
proof -
- have "AE x. Real (f x) = Real (g x)"
- using cong by (rule AE_mp) simp
- moreover have "AE x. Real (- f x) = Real (- g x)"
- using cong by (rule AE_mp) simp
+ have "AE x. Real (f x) = Real (g x)" using cong by auto
+ moreover have "AE x. Real (- f x) = Real (- g x)" using cong by auto
ultimately show ?thesis
by (simp cong: positive_integral_cong_AE add: lebesgue_integral_def)
qed
@@ -1756,20 +1754,18 @@
shows "integral\<^isup>L M f \<le> integral\<^isup>L M g"
proof -
have "AE x. Real (f x) \<le> Real (g x)"
- using mono by (rule AE_mp) (auto intro!: AE_cong)
+ using mono by auto
moreover have "AE x. Real (- g x) \<le> Real (- f x)"
- using mono by (rule AE_mp) (auto intro!: AE_cong)
+ using mono by auto
ultimately show ?thesis using fg
by (auto simp: lebesgue_integral_def integrable_def diff_minus
intro!: add_mono real_of_pextreal_mono positive_integral_mono_AE)
qed
lemma (in measure_space) integral_mono:
- assumes fg: "integrable M f" "integrable M g"
- and mono: "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
+ assumes "integrable M f" "integrable M g" "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
shows "integral\<^isup>L M f \<le> integral\<^isup>L M g"
- apply (rule integral_mono_AE[OF fg])
- using mono by (rule AE_cong) auto
+ using assms by (auto intro: integral_mono_AE)
lemma (in measure_space) integral_diff[simp, intro]:
assumes f: "integrable M f" and g: "integrable M g"
@@ -2056,14 +2052,12 @@
lemma (in measure_space) integral_real:
fixes f :: "'a \<Rightarrow> pextreal"
- assumes "AE x. f x \<noteq> \<omega>"
+ assumes [simp]: "AE x. f x \<noteq> \<omega>"
shows "(\<integral>x. real (f x) \<partial>M) = real (integral\<^isup>P M f)" (is ?plus)
and "(\<integral>x. - real (f x) \<partial>M) = - real (integral\<^isup>P M f)" (is ?minus)
proof -
have "(\<integral>\<^isup>+ x. Real (real (f x)) \<partial>M) = integral\<^isup>P M f"
- apply (rule positive_integral_cong_AE)
- apply (rule AE_mp[OF assms(1)])
- by (auto intro!: AE_cong simp: Real_real)
+ by (auto intro!: positive_integral_cong_AE simp: Real_real)
moreover
have "(\<integral>\<^isup>+ x. Real (- real (f x)) \<partial>M) = (\<integral>\<^isup>+ x. 0 \<partial>M)"
by (intro positive_integral_cong) auto
@@ -2073,7 +2067,7 @@
lemma (in measure_space) integral_dominated_convergence:
assumes u: "\<And>i. integrable M (u i)" and bound: "\<And>x j. x\<in>space M \<Longrightarrow> \<bar>u j x\<bar> \<le> w x"
- and w: "integrable M w" "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> w x"
+ and w: "integrable M w"
and u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) ----> u' x"
shows "integrable M u'"
and "(\<lambda>i. (\<integral>x. \<bar>u i x - u' x\<bar> \<partial>M)) ----> 0" (is "?lim_diff")
@@ -2089,13 +2083,18 @@
have u'_borel: "u' \<in> borel_measurable M"
using u' by (blast intro: borel_measurable_LIMSEQ[of u])
+ { fix x assume x: "x \<in> space M"
+ then have "0 \<le> \<bar>u 0 x\<bar>" by auto
+ also have "\<dots> \<le> w x" using bound[OF x] by auto
+ finally have "0 \<le> w x" . }
+ note w_pos = this
+
show "integrable M u'"
proof (rule integrable_bound)
show "integrable M w" by fact
show "u' \<in> borel_measurable M" by fact
next
- fix x assume x: "x \<in> space M"
- thus "0 \<le> w x" by fact
+ fix x assume x: "x \<in> space M" then show "0 \<le> w x" by fact
show "\<bar>u' x\<bar> \<le> w x" using u'_bound[OF x] .
qed
@@ -2113,7 +2112,7 @@
have PI_diff: "\<And>m n. (\<integral>\<^isup>+ x. Real (?diff (m + n) x) \<partial>M) =
(\<integral>\<^isup>+ x. Real (2 * w x) \<partial>M) - (\<integral>\<^isup>+ x. Real \<bar>u (m + n) x - u' x\<bar> \<partial>M)"
- using diff w diff_less_2w
+ using diff w diff_less_2w w_pos
by (subst positive_integral_diff[symmetric])
(auto simp: integrable_def intro!: positive_integral_cong)
@@ -2155,7 +2154,7 @@
unfolding PI_diff pextreal_INF_minus[OF I2w_fin] pextreal_SUP_minus ..
finally show ?thesis using neq_0 I2w_fin by (rule pextreal_le_minus_imp_0)
qed
-
+
have [simp]: "\<And>n m x. Real (- \<bar>u (m + n) x - u' x\<bar>) = 0" by auto
have [simp]: "\<And>n m. (\<integral>\<^isup>+ x. Real \<bar>u (m + n) x - u' x\<bar> \<partial>M) =
@@ -2230,13 +2229,11 @@
show "(\<lambda>i. integral\<^isup>L M (?w' i)) ----> x" unfolding * sums_def .
qed
- have 4: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> ?w x" using 2[of _ 0] by simp
-
from summable[THEN summable_rabs_cancel]
- have 5: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>n. \<Sum>i = 0..<n. f i x) ----> (\<Sum>i. f i x)"
+ have 4: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>n. \<Sum>i = 0..<n. f i x) ----> (\<Sum>i. f i x)"
by (auto intro: summable_sumr_LIMSEQ_suminf)
- note int = integral_dominated_convergence(1,3)[OF 1 2 3 4 5]
+ note int = integral_dominated_convergence(1,3)[OF 1 2 3 4]
from int show "integrable M ?S" by simp
--- a/src/HOL/Probability/Lebesgue_Measure.thy Fri Feb 04 17:11:00 2011 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Fri Feb 04 17:25:12 2011 +0100
@@ -48,6 +48,8 @@
lemma Pi_iff: "f \<in> Pi I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i)"
unfolding Pi_def by auto
+subsection {* Lebesgue measure *}
+
definition lebesgue :: "'a::ordered_euclidean_space measure_space" where
"lebesgue = \<lparr> space = UNIV,
sets = {A. \<forall>n. (indicator A :: 'a \<Rightarrow> real) integrable_on cube n},
@@ -498,6 +500,8 @@
then show ?thesis by auto
qed auto
+subsection {* Lebesgue-Borel measure *}
+
definition "lborel = lebesgue \<lparr> sets := sets borel \<rparr>"
lemma
@@ -544,6 +548,8 @@
by auto
qed
+subsection {* Lebesgue integrable implies Gauge integrable *}
+
lemma simple_function_has_integral:
fixes f::"'a::ordered_euclidean_space \<Rightarrow> pextreal"
assumes f:"simple_function lebesgue f"
@@ -734,13 +740,7 @@
apply(rule borel.borel_measurableI)
using continuous_open_preimage[OF assms] unfolding vimage_def by auto
-lemma (in measure_space) integral_monotone_convergence_pos':
- assumes i: "\<And>i. integrable M (f i)" and mono: "\<And>x. mono (\<lambda>n. f n x)"
- and pos: "\<And>x i. 0 \<le> f i x"
- and lim: "\<And>x. (\<lambda>i. f i x) ----> u x"
- and ilim: "(\<lambda>i. integral\<^isup>L M (f i)) ----> x"
- shows "integrable M u \<and> integral\<^isup>L M u = x"
- using integral_monotone_convergence_pos[OF assms] by auto
+subsection {* Equivalence between product spaces and euclidean spaces *}
definition e2p :: "'a::ordered_euclidean_space \<Rightarrow> (nat \<Rightarrow> real)" where
"e2p x = (\<lambda>i\<in>{..<DIM('a)}. x$$i)"
@@ -756,28 +756,6 @@
"p2e (e2p x) = (x::'a::ordered_euclidean_space)"
by (auto simp: euclidean_eq[where 'a='a] p2e_def e2p_def)
-lemma bij_inv_p2e_e2p:
- shows "bij_inv ({..<DIM('a)} \<rightarrow>\<^isub>E UNIV) (UNIV :: 'a::ordered_euclidean_space set)
- p2e e2p" (is "bij_inv ?P ?U _ _")
-proof (rule bij_invI)
- show "p2e \<in> ?P \<rightarrow> ?U" "e2p \<in> ?U \<rightarrow> ?P" by (auto simp: e2p_def)
-qed auto
-
-declare restrict_extensional[intro]
-
-lemma e2p_extensional[intro]:"e2p (y::'a::ordered_euclidean_space) \<in> extensional {..<DIM('a)}"
- unfolding e2p_def by auto
-
-lemma e2p_image_vimage: fixes A::"'a::ordered_euclidean_space set"
- shows "e2p ` A = p2e -` A \<inter> extensional {..<DIM('a)}"
-proof(rule set_eqI,rule)
- fix x assume "x \<in> e2p ` A" then guess y unfolding image_iff .. note y=this
- show "x \<in> p2e -` A \<inter> extensional {..<DIM('a)}"
- apply safe apply(rule vimageI[OF _ y(1)]) unfolding y p2e_e2p by auto
-next fix x assume "x \<in> p2e -` A \<inter> extensional {..<DIM('a)}"
- thus "x \<in> e2p ` A" unfolding image_iff apply(rule_tac x="p2e x" in bexI) apply(subst e2p_p2e) by auto
-qed
-
interpretation lborel_product: product_sigma_finite "\<lambda>x. lborel::real measure_space"
by default
@@ -850,113 +828,95 @@
then show "p2e -` A \<inter> space ?P \<in> sets ?P" by auto
qed simp
-lemma e2p_Int:"e2p ` A \<inter> e2p ` B = e2p ` (A \<inter> B)" (is "?L = ?R")
- apply(rule image_Int[THEN sym])
- using bij_inv_p2e_e2p[THEN bij_inv_bij_betw(2)]
- unfolding bij_betw_def by auto
+lemma Int_stable_cuboids:
+ fixes x::"'a::ordered_euclidean_space"
+ shows "Int_stable \<lparr>space = UNIV, sets = range (\<lambda>(a, b::'a). {a..b})\<rparr>"
+ by (auto simp: inter_interval Int_stable_def)
-lemma Int_stable_cuboids: fixes x::"'a::ordered_euclidean_space"
- shows "Int_stable \<lparr>space = UNIV, sets = range (\<lambda>(a, b::'a). e2p ` {a..b})\<rparr>"
- unfolding Int_stable_def algebra.select_convs
-proof safe fix a b x y::'a
- have *:"e2p ` {a..b} \<inter> e2p ` {x..y} =
- (\<lambda>(a, b). e2p ` {a..b}) (\<chi>\<chi> i. max (a $$ i) (x $$ i), \<chi>\<chi> i. min (b $$ i) (y $$ i)::'a)"
- unfolding e2p_Int inter_interval by auto
- show "e2p ` {a..b} \<inter> e2p ` {x..y} \<in> range (\<lambda>(a, b). e2p ` {a..b::'a})" unfolding *
- apply(rule range_eqI) ..
-qed
-
-lemma Int_stable_cuboids': fixes x::"'a::ordered_euclidean_space"
- shows "Int_stable \<lparr>space = UNIV, sets = range (\<lambda>(a, b::'a). {a..b})\<rparr>"
- unfolding Int_stable_def algebra.select_convs
- apply safe unfolding inter_interval by auto
-
-lemma lmeasure_measure_eq_borel_prod:
+lemma lborel_eq_lborel_space:
fixes A :: "('a::ordered_euclidean_space) set"
assumes "A \<in> sets borel"
- shows "lebesgue.\<mu> A = lborel_space.\<mu> TYPE('a) (e2p ` A)" (is "_ = ?m A")
-proof (rule measure_unique_Int_stable[where X=A and A=cube])
- show "Int_stable \<lparr> space = UNIV :: 'a set, sets = range (\<lambda>(a,b). {a..b}) \<rparr>"
- (is "Int_stable ?E" ) using Int_stable_cuboids' .
- have [simp]: "sigma ?E = borel" using borel_eq_atLeastAtMost ..
- show "\<And>i. lebesgue.\<mu> (cube i) \<noteq> \<omega>" unfolding cube_def by auto
- show "\<And>X. X \<in> sets ?E \<Longrightarrow> lebesgue.\<mu> X = ?m X"
- proof- case goal1 then obtain a b where X:"X = {a..b}" by auto
- { presume *:"X \<noteq> {} \<Longrightarrow> ?case"
- show ?case apply(cases,rule *,assumption) by auto }
- def XX \<equiv> "\<lambda>i. {a $$ i .. b $$ i}" assume "X \<noteq> {}" note X' = this[unfolded X interval_ne_empty]
- have *:"Pi\<^isub>E {..<DIM('a)} XX = e2p ` X" apply(rule set_eqI)
- proof fix x assume "x \<in> Pi\<^isub>E {..<DIM('a)} XX"
- thus "x \<in> e2p ` X" unfolding image_iff apply(rule_tac x="\<chi>\<chi> i. x i" in bexI)
- unfolding Pi_def extensional_def e2p_def restrict_def X mem_interval XX_def by rule auto
- next fix x assume "x \<in> e2p ` X" then guess y unfolding image_iff .. note y = this
- show "x \<in> Pi\<^isub>E {..<DIM('a)} XX" unfolding y using y(1)
- unfolding Pi_def extensional_def e2p_def restrict_def X mem_interval XX_def by auto
- qed
- have "lebesgue.\<mu> X = (\<Prod>x<DIM('a). Real (b $$ x - a $$ x))" using X' apply- unfolding X
- unfolding lmeasure_atLeastAtMost content_closed_interval apply(subst Real_setprod) by auto
- also have "... = (\<Prod>i<DIM('a). lebesgue.\<mu> (XX i))" apply(rule setprod_cong2)
- unfolding XX_def lmeasure_atLeastAtMost apply(subst content_real) using X' by auto
- also have "... = ?m X" unfolding *[THEN sym]
- apply(rule lborel_space.measure_times[symmetric]) unfolding XX_def by auto
- finally show ?case .
- qed
+ shows "lborel.\<mu> A = lborel_space.\<mu> TYPE('a) (p2e -` A \<inter> (space (lborel_space.P TYPE('a))))"
+ (is "_ = measure ?P (?T A)")
+proof (rule measure_unique_Int_stable_vimage)
+ show "measure_space ?P" by default
+ show "measure_space lborel" by default
+
+ let ?E = "\<lparr> space = UNIV :: 'a set, sets = range (\<lambda>(a,b). {a..b}) \<rparr>"
+ show "Int_stable ?E" using Int_stable_cuboids .
+ show "range cube \<subseteq> sets ?E" unfolding cube_def_raw by auto
+ { fix x have "\<exists>n. x \<in> cube n" using mem_big_cube[of x] by fastsimp }
+ then show "cube \<up> space ?E" by (intro isotoneI cube_subset_Suc) auto
+ { fix i show "lborel.\<mu> (cube i) \<noteq> \<omega>" unfolding cube_def by auto }
+ show "A \<in> sets (sigma ?E)" "sets (sigma ?E) = sets lborel" "space ?E = space lborel"
+ using assms by (simp_all add: borel_eq_atLeastAtMost)
- show "range cube \<subseteq> sets \<lparr>space = UNIV, sets = range (\<lambda>(a, b). {a..b})\<rparr>"
- unfolding cube_def_raw by auto
- have "\<And>x. \<exists>xa. x \<in> cube xa" apply(rule_tac x=x in mem_big_cube) by fastsimp
- thus "cube \<up> space \<lparr>space = UNIV, sets = range (\<lambda>(a, b). {a..b})\<rparr>"
- apply-apply(rule isotoneI) apply(rule cube_subset_Suc) by auto
- show "A \<in> sets (sigma ?E)" using assms by simp
- have "measure_space lborel" by default
- then show "measure_space \<lparr> space = space ?E, sets = sets (sigma ?E), measure = measure lebesgue\<rparr>"
- unfolding lebesgue_def lborel_def by simp
- let ?M = "\<lparr> space = space ?E, sets = sets (sigma ?E), measure = ?m \<rparr>"
- show "measure_space ?M"
- proof (rule lborel_space.measure_space_vimage)
- show "sigma_algebra ?M" by (rule lborel.sigma_algebra_cong) auto
- show "p2e \<in> measurable (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. lborel) ?M"
- using measurable_p2e unfolding measurable_def by auto
- fix A :: "'a set" assume "A \<in> sets ?M"
- show "measure ?M A = lborel_space.\<mu> TYPE('a) (p2e -` A \<inter> space (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. lborel))"
- by (simp add: e2p_image_vimage)
- qed
-qed simp
+ show "p2e \<in> measurable ?P (lborel :: 'a measure_space)"
+ using measurable_p2e unfolding measurable_def by simp
+ { fix X assume "X \<in> sets ?E"
+ then obtain a b where X[simp]: "X = {a .. b}" by auto
+ have *: "?T X = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {a $$ i .. b $$ i})"
+ by (auto simp: Pi_iff eucl_le[where 'a='a] p2e_def)
+ show "lborel.\<mu> X = measure ?P (?T X)"
+ proof cases
+ assume "X \<noteq> {}"
+ then have "a \<le> b"
+ by (simp add: interval_ne_empty eucl_le[where 'a='a])
+ then have "lborel.\<mu> X = (\<Prod>x<DIM('a). lborel.\<mu> {a $$ x .. b $$ x})"
+ by (auto simp: content_closed_interval eucl_le[where 'a='a]
+ intro!: Real_setprod )
+ also have "\<dots> = measure ?P (?T X)"
+ unfolding * by (subst lborel_space.measure_times) auto
+ finally show ?thesis .
+ qed simp }
+qed
-lemma range_e2p:"range (e2p::'a::ordered_euclidean_space \<Rightarrow> _) = extensional {..<DIM('a)}"
- unfolding e2p_def_raw
- apply auto
- by (rule_tac x="\<chi>\<chi> i. x i" in image_eqI) (auto simp: fun_eq_iff extensional_def)
+lemma lebesgue_eq_lborel_space_in_borel:
+ fixes A :: "('a::ordered_euclidean_space) set"
+ assumes A: "A \<in> sets borel"
+ shows "lebesgue.\<mu> A = lborel_space.\<mu> TYPE('a) (p2e -` A \<inter> (space (lborel_space.P TYPE('a))))"
+ using lborel_eq_lborel_space[OF A] by simp
lemma borel_fubini_positiv_integral:
fixes f :: "'a::ordered_euclidean_space \<Rightarrow> pextreal"
assumes f: "f \<in> borel_measurable borel"
shows "integral\<^isup>P lborel f = \<integral>\<^isup>+x. f (p2e x) \<partial>(lborel_space.P TYPE('a))"
-proof (rule lborel.positive_integral_vimage[symmetric, of _ "e2p :: 'a \<Rightarrow> _" "(\<lambda>x. f (p2e x))", unfolded p2e_e2p])
- show "(e2p :: 'a \<Rightarrow> _) \<in> measurable borel (lborel_space.P TYPE('a))" by (rule measurable_e2p)
- show "sigma_algebra (lborel_space.P TYPE('a))" by default
- from measurable_comp[OF measurable_p2e f]
- show "(\<lambda>x. f (p2e x)) \<in> borel_measurable (lborel_space.P TYPE('a))" by (simp add: comp_def)
- let "?L A" = "lebesgue.\<mu> ((e2p::'a \<Rightarrow> (nat \<Rightarrow> real)) -` A \<inter> UNIV)"
- fix A :: "(nat \<Rightarrow> real) set" assume "A \<in> sets (lborel_space.P TYPE('a))"
- then have A: "(e2p::'a \<Rightarrow> (nat \<Rightarrow> real)) -` A \<inter> space borel \<in> sets borel"
- by (rule measurable_sets[OF measurable_e2p])
- have [simp]: "A \<inter> extensional {..<DIM('a)} = A"
- using `A \<in> sets (lborel_space.P TYPE('a))`[THEN lborel_space.sets_into_space] by auto
- show "lborel_space.\<mu> TYPE('a) A = ?L A"
- using lmeasure_measure_eq_borel_prod[OF A] by (simp add: range_e2p)
+proof (rule lborel_space.positive_integral_vimage[OF _ _ _ lborel_eq_lborel_space])
+ show "sigma_algebra lborel" by default
+ show "p2e \<in> measurable (lborel_space.P TYPE('a)) (lborel :: 'a measure_space)"
+ "f \<in> borel_measurable lborel"
+ using measurable_p2e f by (simp_all add: measurable_def)
+qed simp
+
+lemma borel_fubini_integrable:
+ fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
+ shows "integrable lborel f \<longleftrightarrow>
+ integrable (lborel_space.P TYPE('a)) (\<lambda>x. f (p2e x))"
+ (is "_ \<longleftrightarrow> integrable ?B ?f")
+proof
+ assume "integrable lborel f"
+ moreover then have f: "f \<in> borel_measurable borel"
+ by auto
+ moreover with measurable_p2e
+ have "f \<circ> p2e \<in> borel_measurable ?B"
+ by (rule measurable_comp)
+ ultimately show "integrable ?B ?f"
+ by (simp add: comp_def borel_fubini_positiv_integral integrable_def)
+next
+ assume "integrable ?B ?f"
+ moreover then
+ have "?f \<circ> e2p \<in> borel_measurable (borel::'a algebra)"
+ by (auto intro!: measurable_e2p measurable_comp)
+ then have "f \<in> borel_measurable borel"
+ by (simp cong: measurable_cong)
+ ultimately show "integrable lborel f"
+ by (simp add: borel_fubini_positiv_integral integrable_def)
qed
lemma borel_fubini:
fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
assumes f: "f \<in> borel_measurable borel"
shows "integral\<^isup>L lborel f = \<integral>x. f (p2e x) \<partial>(lborel_space.P TYPE('a))"
-proof -
- have 1:"(\<lambda>x. Real (f x)) \<in> borel_measurable borel" using f by auto
- have 2:"(\<lambda>x. Real (- f x)) \<in> borel_measurable borel" using f by auto
- show ?thesis unfolding lebesgue_integral_def
- unfolding borel_fubini_positiv_integral[OF 1] borel_fubini_positiv_integral[OF 2]
- unfolding o_def ..
-qed
+ using f by (simp add: borel_fubini_positiv_integral lebesgue_integral_def)
end
--- a/src/HOL/Probability/Measure.thy Fri Feb 04 17:11:00 2011 +0100
+++ b/src/HOL/Probability/Measure.thy Fri Feb 04 17:25:12 2011 +0100
@@ -624,6 +624,59 @@
ultimately show ?thesis by (simp add: isoton_def)
qed
+lemma (in measure_space) measure_space_vimage:
+ fixes M' :: "('c, 'd) measure_space_scheme"
+ assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
+ and \<nu>: "\<And>A. A \<in> sets M' \<Longrightarrow> measure M' A = \<mu> (T -` A \<inter> space M)"
+ shows "measure_space M'"
+proof -
+ interpret M': sigma_algebra M' by fact
+ show ?thesis
+ proof
+ show "measure M' {} = 0" using \<nu>[of "{}"] by simp
+
+ show "countably_additive M' (measure M')"
+ proof (intro countably_additiveI)
+ fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets M'" "disjoint_family A"
+ then have A: "\<And>i. A i \<in> sets M'" "(\<Union>i. A i) \<in> sets M'" by auto
+ then have *: "range (\<lambda>i. T -` (A i) \<inter> space M) \<subseteq> sets M"
+ using `T \<in> measurable M M'` by (auto simp: measurable_def)
+ moreover have "(\<Union>i. T -` A i \<inter> space M) \<in> sets M"
+ using * by blast
+ moreover have **: "disjoint_family (\<lambda>i. T -` A i \<inter> space M)"
+ using `disjoint_family A` by (auto simp: disjoint_family_on_def)
+ ultimately show "(\<Sum>\<^isub>\<infinity> i. measure M' (A i)) = measure M' (\<Union>i. A i)"
+ using measure_countably_additive[OF _ **] A
+ by (auto simp: comp_def vimage_UN \<nu>)
+ qed
+ qed
+qed
+
+lemma measure_unique_Int_stable_vimage:
+ fixes A :: "nat \<Rightarrow> 'a set"
+ assumes E: "Int_stable E"
+ and A: "range A \<subseteq> sets E" "A \<up> space E" "\<And>i. measure M (A i) \<noteq> \<omega>"
+ and N: "measure_space N" "T \<in> measurable N M"
+ and M: "measure_space M" "sets (sigma E) = sets M" "space E = space M"
+ and eq: "\<And>X. X \<in> sets E \<Longrightarrow> measure M X = measure N (T -` X \<inter> space N)"
+ assumes X: "X \<in> sets (sigma E)"
+ shows "measure M X = measure N (T -` X \<inter> space N)"
+proof (rule measure_unique_Int_stable[OF E A(1,2) _ _ eq _ X])
+ interpret M: measure_space M by fact
+ interpret N: measure_space N by fact
+ let "?T X" = "T -` X \<inter> space N"
+ show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure = measure M\<rparr>"
+ by (rule M.measure_space_cong) (auto simp: M)
+ show "measure_space \<lparr>space = space E, sets = sets (sigma E), measure = \<lambda>X. measure N (?T X)\<rparr>" (is "measure_space ?E")
+ proof (rule N.measure_space_vimage)
+ show "sigma_algebra ?E"
+ by (rule M.sigma_algebra_cong) (auto simp: M)
+ show "T \<in> measurable N ?E"
+ using `T \<in> measurable N M` by (auto simp: M measurable_def)
+ qed simp
+ show "\<And>i. M.\<mu> (A i) \<noteq> \<omega>" by fact
+qed
+
section "@{text \<mu>}-null sets"
abbreviation (in measure_space) "null_sets \<equiv> {N\<in>sets M. \<mu> N = 0}"
@@ -739,12 +792,25 @@
obtains N where "{x \<in> space M. \<not> P x} \<subseteq> N" "\<mu> N = 0" "N \<in> sets M"
using assms unfolding almost_everywhere_def by auto
+lemma (in measure_space) AE_E2:
+ assumes "AE x. P x" "{x\<in>space M. P x} \<in> sets M"
+ shows "\<mu> {x\<in>space M. \<not> P x} = 0" (is "\<mu> ?P = 0")
+proof -
+ obtain A where A: "?P \<subseteq> A" "A \<in> sets M" "\<mu> A = 0"
+ using assms by (auto elim!: AE_E)
+ have "?P = space M - {x\<in>space M. P x}" by auto
+ then have "?P \<in> sets M" using assms by auto
+ with assms `?P \<subseteq> A` `A \<in> sets M` have "\<mu> ?P \<le> \<mu> A"
+ by (auto intro!: measure_mono)
+ then show "\<mu> ?P = 0" using A by simp
+qed
+
lemma (in measure_space) AE_I:
assumes "{x \<in> space M. \<not> P x} \<subseteq> N" "\<mu> N = 0" "N \<in> sets M"
shows "AE x. P x"
using assms unfolding almost_everywhere_def by auto
-lemma (in measure_space) AE_mp:
+lemma (in measure_space) AE_mp[elim!]:
assumes AE_P: "AE x. P x" and AE_imp: "AE x. P x \<longrightarrow> Q x"
shows "AE x. Q x"
proof -
@@ -765,56 +831,28 @@
qed
qed
-lemma (in measure_space) AE_iffI:
- assumes P: "AE x. P x" and Q: "AE x. P x \<longleftrightarrow> Q x" shows "AE x. Q x"
- using AE_mp[OF Q, of "\<lambda>x. P x \<longrightarrow> Q x"] AE_mp[OF P, of Q] by auto
-
-lemma (in measure_space) AE_disjI1:
- assumes P: "AE x. P x" shows "AE x. P x \<or> Q x"
- by (rule AE_mp[OF P]) auto
-
-lemma (in measure_space) AE_disjI2:
- assumes P: "AE x. Q x" shows "AE x. P x \<or> Q x"
- by (rule AE_mp[OF P]) auto
-
-lemma (in measure_space) AE_conjI:
- assumes AE_P: "AE x. P x" and AE_Q: "AE x. Q x"
- shows "AE x. P x \<and> Q x"
- apply (rule AE_mp[OF AE_P])
- apply (rule AE_mp[OF AE_Q])
- by simp
+lemma (in measure_space)
+ shows AE_iffI: "AE x. P x \<Longrightarrow> AE x. P x \<longleftrightarrow> Q x \<Longrightarrow> AE x. Q x"
+ and AE_disjI1: "AE x. P x \<Longrightarrow> AE x. P x \<or> Q x"
+ and AE_disjI2: "AE x. Q x \<Longrightarrow> AE x. P x \<or> Q x"
+ and AE_conjI: "AE x. P x \<Longrightarrow> AE x. Q x \<Longrightarrow> AE x. P x \<and> Q x"
+ and AE_conj_iff[simp]: "(AE x. P x \<and> Q x) \<longleftrightarrow> (AE x. P x) \<and> (AE x. Q x)"
+ by auto
-lemma (in measure_space) AE_conj_iff[simp]:
- shows "(AE x. P x \<and> Q x) \<longleftrightarrow> (AE x. P x) \<and> (AE x. Q x)"
-proof (intro conjI iffI AE_conjI)
- assume *: "AE x. P x \<and> Q x"
- from * show "AE x. P x" by (rule AE_mp) auto
- from * show "AE x. Q x" by (rule AE_mp) auto
-qed auto
-
-lemma (in measure_space) AE_E2:
- assumes "AE x. P x" "{x\<in>space M. P x} \<in> sets M"
- shows "\<mu> {x\<in>space M. \<not> P x} = 0" (is "\<mu> ?P = 0")
-proof -
- obtain A where A: "?P \<subseteq> A" "A \<in> sets M" "\<mu> A = 0"
- using assms by (auto elim!: AE_E)
- have "?P = space M - {x\<in>space M. P x}" by auto
- then have "?P \<in> sets M" using assms by auto
- with assms `?P \<subseteq> A` `A \<in> sets M` have "\<mu> ?P \<le> \<mu> A"
- by (auto intro!: measure_mono)
- then show "\<mu> ?P = 0" using A by simp
-qed
-
-lemma (in measure_space) AE_space[simp, intro]: "AE x. x \<in> space M"
+lemma (in measure_space) AE_space: "AE x. x \<in> space M"
by (rule AE_I[where N="{}"]) auto
-lemma (in measure_space) AE_cong:
- assumes "\<And>x. x \<in> space M \<Longrightarrow> P x" shows "AE x. P x"
-proof -
- have [simp]: "\<And>x. (x \<in> space M \<longrightarrow> P x) \<longleftrightarrow> True" using assms by auto
- show ?thesis
- by (rule AE_mp[OF AE_space]) auto
-qed
+lemma (in measure_space) AE_I2[simp, intro]:
+ "(\<And>x. x \<in> space M \<Longrightarrow> P x) \<Longrightarrow> AE x. P x"
+ using AE_space by auto
+
+lemma (in measure_space) AE_Ball_mp:
+ "\<forall>x\<in>space M. P x \<Longrightarrow> AE x. P x \<longrightarrow> Q x \<Longrightarrow> AE x. Q x"
+ by auto
+
+lemma (in measure_space) AE_cong[cong]:
+ "(\<And>x. x \<in> space M \<Longrightarrow> P x \<longleftrightarrow> Q x) \<Longrightarrow> (AE x. P x) \<longleftrightarrow> (AE x. Q x)"
+ by auto
lemma (in measure_space) all_AE_countable:
"(\<forall>i::'i::countable. AE x. P i x) \<longleftrightarrow> (AE x. \<forall>i. P i x)"
@@ -829,11 +867,7 @@
by (intro null_sets_UN) auto
ultimately show "AE x. \<forall>i. P i x"
unfolding almost_everywhere_def by auto
-next
- assume *: "AE x. \<forall>i. P i x"
- show "\<forall>i. AE x. P i x"
- by (rule allI, rule AE_mp[OF *]) simp
-qed
+qed auto
lemma (in measure_space) restricted_measure_space:
assumes "S \<in> sets M"
@@ -855,34 +889,6 @@
qed
qed
-lemma (in measure_space) measure_space_vimage:
- fixes M' :: "('c, 'd) measure_space_scheme"
- assumes T: "sigma_algebra M'" "T \<in> measurable M M'"
- and \<nu>: "\<And>A. A \<in> sets M' \<Longrightarrow> measure M' A = \<mu> (T -` A \<inter> space M)"
- shows "measure_space M'"
-proof -
- interpret M': sigma_algebra M' by fact
- show ?thesis
- proof
- show "measure M' {} = 0" using \<nu>[of "{}"] by simp
-
- show "countably_additive M' (measure M')"
- proof (intro countably_additiveI)
- fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets M'" "disjoint_family A"
- then have A: "\<And>i. A i \<in> sets M'" "(\<Union>i. A i) \<in> sets M'" by auto
- then have *: "range (\<lambda>i. T -` (A i) \<inter> space M) \<subseteq> sets M"
- using `T \<in> measurable M M'` by (auto simp: measurable_def)
- moreover have "(\<Union>i. T -` A i \<inter> space M) \<in> sets M"
- using * by blast
- moreover have **: "disjoint_family (\<lambda>i. T -` A i \<inter> space M)"
- using `disjoint_family A` by (auto simp: disjoint_family_on_def)
- ultimately show "(\<Sum>\<^isub>\<infinity> i. measure M' (A i)) = measure M' (\<Union>i. A i)"
- using measure_countably_additive[OF _ **] A
- by (auto simp: comp_def vimage_UN \<nu>)
- qed
- qed
-qed
-
lemma (in measure_space) measure_space_subalgebra:
assumes "sigma_algebra N" and [simp]: "sets N \<subseteq> sets M" "space N = space M"
and measure[simp]: "\<And>X. X \<in> sets N \<Longrightarrow> measure N X = measure M X"
--- a/src/HOL/Probability/Product_Measure.thy Fri Feb 04 17:11:00 2011 +0100
+++ b/src/HOL/Probability/Product_Measure.thy Fri Feb 04 17:25:12 2011 +0100
@@ -734,48 +734,37 @@
qed
lemma (in pair_sigma_finite) pair_measure_alt2:
- assumes "A \<in> sets P"
+ assumes A: "A \<in> sets P"
shows "\<mu> A = (\<integral>\<^isup>+y. M1.\<mu> ((\<lambda>x. (x, y)) -` A) \<partial>M2)"
(is "_ = ?\<nu> A")
proof -
+ interpret Q: pair_sigma_finite M2 M1 by default
from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this
have [simp]: "\<And>m. \<lparr> space = space E, sets = sets (sigma E), measure = m \<rparr> = P\<lparr> measure := m \<rparr>"
unfolding pair_measure_def by simp
- show ?thesis
- proof (rule measure_unique_Int_stable[where \<nu>="?\<nu>", OF Int_stable_pair_measure_generator], simp_all)
- show "range F \<subseteq> sets E" "F \<up> space E" "\<And>i. \<mu> (F i) \<noteq> \<omega>" "A \<in> sets (sigma E)"
+
+ have "\<mu> A = Q.\<mu> ((\<lambda>(y, x). (x, y)) -` A \<inter> space Q.P)"
+ proof (rule measure_unique_Int_stable_vimage[OF Int_stable_pair_measure_generator])
+ show "measure_space P" "measure_space Q.P" by default
+ show "(\<lambda>(y, x). (x, y)) \<in> measurable Q.P P" by (rule Q.pair_sigma_algebra_swap_measurable)
+ show "sets (sigma E) = sets P" "space E = space P" "A \<in> sets (sigma E)"
+ using assms unfolding pair_measure_def by auto
+ show "range F \<subseteq> sets E" "F \<up> space E" "\<And>i. \<mu> (F i) \<noteq> \<omega>"
using F `A \<in> sets P` by (auto simp: pair_measure_def)
- show "measure_space P" by default
- interpret Q: pair_sigma_finite M2 M1 by default
- have P: "sigma_algebra (P\<lparr> measure := ?\<nu>\<rparr>)"
- by (intro sigma_algebra_cong) auto
- show "measure_space (P\<lparr> measure := ?\<nu>\<rparr>)"
- apply (rule Q.measure_space_vimage[OF P])
- apply (simp_all)
- apply (rule Q.pair_sigma_algebra_swap_measurable)
- proof -
- fix A assume "A \<in> sets P"
- from sets_swap[OF this]
- show "(\<integral>\<^isup>+ y. M1.\<mu> ((\<lambda>x. (x, y)) -` A) \<partial>M2) = Q.\<mu> ((\<lambda>(x, y). (y, x)) -` A \<inter> space (M2 \<Otimes>\<^isub>M M1))"
- using sets_into_space[OF `A \<in> sets P`]
- by (auto simp add: Q.pair_measure_alt space_pair_measure
- intro!: M2.positive_integral_cong arg_cong[where f="M1.\<mu>"])
- qed
fix X assume "X \<in> sets E"
- then obtain A B where X: "X = A \<times> B" and AB: "A \<in> sets M1" "B \<in> sets M2"
+ then obtain A B where X[simp]: "X = A \<times> B" and AB: "A \<in> sets M1" "B \<in> sets M2"
unfolding pair_measure_def pair_measure_generator_def by auto
- show "\<mu> X = ?\<nu> X"
- proof -
- from AB have "?\<nu> (A \<times> B) = (\<integral>\<^isup>+y. M1.\<mu> A * indicator B y \<partial>M2)"
- by (auto intro!: M2.positive_integral_cong)
- with AB show ?thesis
- unfolding pair_measure_times[OF AB] X
- by (simp add: M2.positive_integral_cmult_indicator ac_simps)
- qed
+ then have "(\<lambda>(y, x). (x, y)) -` X \<inter> space Q.P = B \<times> A"
+ using M1.sets_into_space M2.sets_into_space by (auto simp: space_pair_measure)
+ then show "\<mu> X = Q.\<mu> ((\<lambda>(y, x). (x, y)) -` X \<inter> space Q.P)"
+ using AB by (simp add: pair_measure_times Q.pair_measure_times ac_simps)
qed
+ then show ?thesis
+ using sets_into_space[OF A] Q.pair_measure_alt[OF sets_swap[OF A]]
+ by (auto simp add: Q.pair_measure_alt space_pair_measure
+ intro!: M2.positive_integral_cong arg_cong[where f="M1.\<mu>"])
qed
-
lemma pair_sigma_algebra_sigma:
assumes 1: "S1 \<up> (space E1)" "range S1 \<subseteq> sets E1" and E1: "sets E1 \<subseteq> Pow (space E1)"
assumes 2: "S2 \<up> (space E2)" "range S2 \<subseteq> sets E2" and E2: "sets E2 \<subseteq> Pow (space E2)"
@@ -1061,46 +1050,28 @@
have AE: "M1.almost_everywhere (\<lambda>x. (\<integral>\<^isup>+y. Real (f (x, y)) \<partial>M2) \<noteq> \<omega>)"
"M1.almost_everywhere (\<lambda>x. (\<integral>\<^isup>+y. Real (- f (x, y)) \<partial>M2) \<noteq> \<omega>)"
by (auto intro!: M1.positive_integral_omega_AE)
- then show ?AE
- apply (rule M1.AE_mp[OF _ M1.AE_mp])
- apply (rule M1.AE_cong)
- using assms unfolding integrable_def
- by (auto intro!: measurable_pair_image_snd)
- have "integrable M1 (\<lambda>x. real (\<integral>\<^isup>+y. Real (f (x, y)) \<partial>M2))" (is "integrable M1 ?f")
- proof (intro integrable_def[THEN iffD2] conjI)
- show "?f \<in> borel_measurable M1"
- using borel by (auto intro!: M1.borel_measurable_real positive_integral_fst_measurable)
- have "(\<integral>\<^isup>+x. Real (?f x) \<partial>M1) = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. Real (f (x, y)) \<partial>M2) \<partial>M1)"
- apply (rule M1.positive_integral_cong_AE)
- apply (rule M1.AE_mp[OF AE(1)])
- apply (rule M1.AE_cong)
- by (auto simp: Real_real)
- then show "(\<integral>\<^isup>+x. Real (?f x) \<partial>M1) \<noteq> \<omega>"
- using positive_integral_fst_measurable[OF borel(2)] int by simp
- have "(\<integral>\<^isup>+x. Real (- ?f x) \<partial>M1) = (\<integral>\<^isup>+x. 0 \<partial>M1)"
- by (intro M1.positive_integral_cong) simp
- then show "(\<integral>\<^isup>+x. Real (- ?f x) \<partial>M1) \<noteq> \<omega>" by simp
- qed
- moreover have "integrable M1 (\<lambda>x. real (\<integral>\<^isup>+ y. Real (- f (x, y)) \<partial>M2))"
- (is "integrable M1 ?f")
- proof (intro integrable_def[THEN iffD2] conjI)
- show "?f \<in> borel_measurable M1"
- using borel by (auto intro!: M1.borel_measurable_real positive_integral_fst_measurable)
- have "(\<integral>\<^isup>+x. Real (?f x) \<partial>M1) = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. Real (- f (x, y)) \<partial>M2) \<partial>M1)"
- apply (rule M1.positive_integral_cong_AE)
- apply (rule M1.AE_mp[OF AE(2)])
- apply (rule M1.AE_cong)
- by (auto simp: Real_real)
- then show "(\<integral>\<^isup>+x. Real (?f x) \<partial>M1) \<noteq> \<omega>"
- using positive_integral_fst_measurable[OF borel(1)] int by simp
- have "(\<integral>\<^isup>+x. Real (- ?f x) \<partial>M1) = (\<integral>\<^isup>+x. 0 \<partial>M1)"
- by (intro M1.positive_integral_cong) simp
- then show "(\<integral>\<^isup>+x. Real (- ?f x) \<partial>M1) \<noteq> \<omega>" by simp
- qed
- ultimately show ?INT
+ then show ?AE using assms
+ by (simp add: measurable_pair_image_snd integrable_def)
+ { fix f assume borel: "(\<lambda>x. Real (f x)) \<in> borel_measurable P"
+ and int: "integral\<^isup>P P (\<lambda>x. Real (f x)) \<noteq> \<omega>"
+ and AE: "M1.almost_everywhere (\<lambda>x. (\<integral>\<^isup>+y. Real (f (x, y)) \<partial>M2) \<noteq> \<omega>)"
+ have "integrable M1 (\<lambda>x. real (\<integral>\<^isup>+y. Real (f (x, y)) \<partial>M2))" (is "integrable M1 ?f")
+ proof (intro integrable_def[THEN iffD2] conjI)
+ show "?f \<in> borel_measurable M1"
+ using borel by (auto intro!: M1.borel_measurable_real positive_integral_fst_measurable)
+ have "(\<integral>\<^isup>+x. Real (?f x) \<partial>M1) = (\<integral>\<^isup>+x. (\<integral>\<^isup>+y. Real (f (x, y)) \<partial>M2) \<partial>M1)"
+ using AE by (auto intro!: M1.positive_integral_cong_AE simp: Real_real)
+ then show "(\<integral>\<^isup>+x. Real (?f x) \<partial>M1) \<noteq> \<omega>"
+ using positive_integral_fst_measurable[OF borel] int by simp
+ have "(\<integral>\<^isup>+x. Real (- ?f x) \<partial>M1) = (\<integral>\<^isup>+x. 0 \<partial>M1)"
+ by (intro M1.positive_integral_cong) simp
+ then show "(\<integral>\<^isup>+x. Real (- ?f x) \<partial>M1) \<noteq> \<omega>" by simp
+ qed }
+ from this[OF borel(1) int(1) AE(2)] this[OF borel(2) int(2) AE(1)]
+ show ?INT
unfolding lebesgue_integral_def[of P] lebesgue_integral_def[of M2]
borel[THEN positive_integral_fst_measurable(2), symmetric]
- by (simp add: M1.integral_real[OF AE(1)] M1.integral_real[OF AE(2)])
+ using AE by (simp add: M1.integral_real)
qed
lemma (in pair_sigma_finite) integrable_snd_measurable:
@@ -1577,8 +1548,8 @@
lemma (in product_sigma_finite) measure_fold:
assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
assumes A: "A \<in> sets (Pi\<^isub>M (I \<union> J) M)"
- shows "measure (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) ((\<lambda>(x,y). merge I x J y) -` A \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M)) =
- measure (Pi\<^isub>M (I \<union> J) M) A"
+ shows "measure (Pi\<^isub>M (I \<union> J) M) A =
+ measure (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M) ((\<lambda>(x,y). merge I x J y) -` A \<inter> space (Pi\<^isub>M I M \<Otimes>\<^isub>M Pi\<^isub>M J M))"
proof -
interpret I: finite_product_sigma_finite M I by default fact
interpret J: finite_product_sigma_finite M J by default fact
@@ -1593,10 +1564,12 @@
"\<And>k. \<forall>i\<in>I\<union>J. \<mu> i (F i k) \<noteq> \<omega>"
by auto
let ?F = "\<lambda>k. \<Pi>\<^isub>E i\<in>I \<union> J. F i k"
- show "P.\<mu> (?X A) = IJ.\<mu> A"
- proof (rule measure_unique_Int_stable[where X=A])
- show "A \<in> sets (sigma IJ.G)"
+ show "IJ.\<mu> A = P.\<mu> (?X A)"
+ proof (rule measure_unique_Int_stable_vimage)
+ show "measure_space IJ.P" "measure_space P.P" by default
+ show "sets (sigma IJ.G) = sets IJ.P" "space IJ.G = space IJ.P" "A \<in> sets (sigma IJ.G)"
using A unfolding product_algebra_def by auto
+ next
show "Int_stable IJ.G"
by (simp add: PiE_Int Int_stable_def product_algebra_def
product_algebra_generator_def)
@@ -1605,25 +1578,17 @@
by (simp add: image_subset_iff product_algebra_def
product_algebra_generator_def)
show "?F \<up> space IJ.G " using F(2) by simp
- have "measure_space IJ.P" by fact
- also have "IJ.P = \<lparr> space = space IJ.G, sets = sets (sigma IJ.G), measure = IJ.\<mu> \<rparr>"
- by (simp add: product_algebra_def)
- finally show "measure_space \<dots>" .
- let ?P = "\<lparr> space = space IJ.G, sets = sets (sigma IJ.G),
- measure = \<lambda>A. P.\<mu> (?X A)\<rparr>"
- have *: "?P = (sigma IJ.G \<lparr> measure := \<lambda>A. P.\<mu> (?X A) \<rparr>)"
- by auto
- have "sigma_algebra (sigma IJ.G \<lparr> measure := \<lambda>A. P.\<mu> (?X A) \<rparr>)"
- by (rule IJ.sigma_algebra_cong) (auto simp: product_algebra_def)
- then show "measure_space ?P" unfolding *
- using measurable_merge[OF `I \<inter> J = {}`]
- by (auto intro!: P.measure_space_vimage simp add: product_algebra_def)
+ show "\<And>k. IJ.\<mu> (?F k) \<noteq> \<omega>"
+ using `finite I` F
+ by (subst IJ.measure_times) (auto simp add: setprod_\<omega>)
+ show "?g \<in> measurable P.P IJ.P"
+ using IJ by (rule measurable_merge)
next
fix A assume "A \<in> sets IJ.G"
- then obtain F where A[simp]: "A = Pi\<^isub>E (I \<union> J) F"
+ then obtain F where A: "A = Pi\<^isub>E (I \<union> J) F"
and F: "\<And>i. i \<in> I \<union> J \<Longrightarrow> F i \<in> sets (M i)"
by (auto simp: product_algebra_generator_def)
- then have "?X A = (Pi\<^isub>E I F \<times> Pi\<^isub>E J F)"
+ then have X: "?X A = (Pi\<^isub>E I F \<times> Pi\<^isub>E J F)"
using sets_into_space by (auto simp: space_pair_measure) blast+
then have "P.\<mu> (?X A) = (\<Prod>i\<in>I. \<mu> i (F i)) * (\<Prod>i\<in>J. \<mu> i (F i))"
using `finite J` `finite I` F
@@ -1633,16 +1598,7 @@
also have "\<dots> = IJ.\<mu> A"
using `finite J` `finite I` F unfolding A
by (intro IJ.measure_times[symmetric]) auto
- finally show "P.\<mu> (?X A) = IJ.\<mu> A" .
- next
- fix k
- have k: "\<And>i. i \<in> I \<union> J \<Longrightarrow> F i k \<in> sets (M i)" using F by auto
- then have "?X (?F k) = (\<Pi>\<^isub>E i\<in>I. F i k) \<times> (\<Pi>\<^isub>E i\<in>J. F i k)"
- using sets_into_space by (auto simp: space_pair_measure) blast+
- with k have "P.\<mu> (?X (?F k)) = (\<Prod>i\<in>I. \<mu> i (F i k)) * (\<Prod>i\<in>J. \<mu> i (F i k))"
- by (simp add: P.pair_measure_times I.measure_times J.measure_times)
- then show "P.\<mu> (?X (?F k)) \<noteq> \<omega>"
- using `finite I` F by (simp add: setprod_\<omega>)
+ finally show "IJ.\<mu> A = P.\<mu> (?X A)" by (rule sym)
qed
qed
@@ -1769,7 +1725,7 @@
have 1: "sigma_algebra IJ.P" by default
have 2: "?M \<in> measurable P.P IJ.P" using measurable_merge[OF IJ] .
have 3: "\<And>A. A \<in> sets IJ.P \<Longrightarrow> IJ.\<mu> A = P.\<mu> (?M -` A \<inter> space P.P)"
- by (rule measure_fold[OF IJ fin, symmetric])
+ by (rule measure_fold[OF IJ fin])
have 4: "integrable (Pi\<^isub>M (I \<union> J) M) f" by fact
show "integrable P.P ?f"
by (rule P.integral_vimage[where f=f, OF 1 2 3 4])
--- a/src/HOL/Probability/Radon_Nikodym.thy Fri Feb 04 17:11:00 2011 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy Fri Feb 04 17:25:12 2011 +0100
@@ -817,8 +817,8 @@
(is "(\<forall>A\<in>sets M. ?P f A = ?P g A) \<longleftrightarrow> _")
proof (intro iffI ballI)
fix A assume eq: "AE x. f x = g x"
- show "?P f A = ?P g A"
- by (rule positive_integral_cong_AE[OF AE_mp[OF eq]]) simp
+ then show "?P f A = ?P g A"
+ by (auto intro: positive_integral_cong_AE)
next
assume eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
from this[THEN bspec, OF top] fin
@@ -879,11 +879,10 @@
have "?N \<in> sets M" using borel by auto
have *: "\<And>i x A. \<And>y::pextreal. y * indicator (Q i) x * indicator A x = y * indicator (Q i \<inter> A) x"
unfolding indicator_def by auto
- have 1: "\<forall>i. AE x. ?f (Q i) x = ?f' (Q i) x"
- using borel Q_fin Q
+ have "\<forall>i. AE x. ?f (Q i) x = ?f' (Q i) x" using borel Q_fin Q
by (intro finite_density_unique[THEN iffD1] allI)
(auto intro!: borel_measurable_pextreal_times f Int simp: *)
- have 2: "AE x. ?f Q0 x = ?f' Q0 x"
+ moreover have "AE x. ?f Q0 x = ?f' Q0 x"
proof (rule AE_I')
{ fix f :: "'a \<Rightarrow> pextreal" assume borel: "f \<in> borel_measurable M"
and eq: "\<And>A. A \<in> sets M \<Longrightarrow> ?\<nu> A = (\<integral>\<^isup>+x. f x * indicator A x \<partial>M)"
@@ -911,13 +910,12 @@
show "{x \<in> space M. ?f Q0 x \<noteq> ?f' Q0 x} \<subseteq>
(Q0 \<inter> {x\<in>space M. f x \<noteq> \<omega>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<omega>})" by (auto simp: indicator_def)
qed
- have **: "\<And>x. (?f Q0 x = ?f' Q0 x) \<longrightarrow> (\<forall>i. ?f (Q i) x = ?f' (Q i) x) \<longrightarrow>
+ moreover have "\<And>x. (?f Q0 x = ?f' Q0 x) \<longrightarrow> (\<forall>i. ?f (Q i) x = ?f' (Q i) x) \<longrightarrow>
?f (space M) x = ?f' (space M) x"
by (auto simp: indicator_def Q0)
- have 3: "AE x. ?f (space M) x = ?f' (space M) x"
- by (rule AE_mp[OF 1[unfolded all_AE_countable] AE_mp[OF 2]]) (simp add: **)
- then show "AE x. f x = f' x"
- by (rule AE_mp) (auto intro!: AE_cong simp: indicator_def)
+ ultimately have "AE x. ?f (space M) x = ?f' (space M) x"
+ by (auto simp: all_AE_countable)
+ then show "AE x. f x = f' x" by auto
qed
lemma (in sigma_finite_measure) density_unique:
@@ -978,25 +976,20 @@
and "sets ?N = sets M" and "space ?N = space M" by (auto simp: measurable_def)
from \<nu>.Ex_finite_integrable_function obtain h where
h: "h \<in> borel_measurable M" "integral\<^isup>P ?N h \<noteq> \<omega>"
- and fin: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<omega>" by auto
+ and fin: "\<forall>x\<in>space M. 0 < h x \<and> h x < \<omega>" by auto
have "AE x. f x * h x \<noteq> \<omega>"
proof (rule AE_I')
- have "integral\<^isup>P ?N h = (\<integral>\<^isup>+x. f x * h x \<partial>M)"
- apply (subst \<nu>.positive_integral_cong_measure[symmetric,
- of "M\<lparr> measure := \<lambda> A. \<integral>\<^isup>+x. f x * indicator A x \<partial>M \<rparr>"])
- apply (simp_all add: eq)
- apply (rule positive_integral_translated_density)
- using f h by auto
+ have "integral\<^isup>P ?N h = (\<integral>\<^isup>+x. f x * h x \<partial>M)" using f h
+ by (subst \<nu>.positive_integral_cong_measure[symmetric,
+ of "M\<lparr> measure := \<lambda> A. \<integral>\<^isup>+x. f x * indicator A x \<partial>M \<rparr>"])
+ (auto intro!: positive_integral_translated_density simp: eq)
then have "(\<integral>\<^isup>+x. f x * h x \<partial>M) \<noteq> \<omega>"
using h(2) by simp
then show "(\<lambda>x. f x * h x) -` {\<omega>} \<inter> space M \<in> null_sets"
using f h(1) by (auto intro!: positive_integral_omega borel_measurable_vimage)
qed auto
then show "AE x. f x \<noteq> \<omega>"
- proof (rule AE_mp, intro AE_cong)
- fix x assume "x \<in> space M" from this[THEN fin]
- show "f x * h x \<noteq> \<omega> \<longrightarrow> f x \<noteq> \<omega>" by auto
- qed
+ using fin by (auto elim!: AE_Ball_mp)
next
assume AE: "AE x. f x \<noteq> \<omega>"
from sigma_finite guess Q .. note Q = this
@@ -1043,16 +1036,8 @@
proof (cases i)
case 0
have "AE x. f x * indicator (A i \<inter> Q j) x = 0"
- using AE by (rule AE_mp) (auto intro!: AE_cong simp: A_def `i = 0`)
- then have "(\<integral>\<^isup>+x. f x * indicator (A i \<inter> Q j) x \<partial>M) = 0"
- using A_in_sets f
- apply (subst positive_integral_0_iff)
- apply fast
- apply (subst (asm) AE_iff_null_set)
- apply (intro borel_measurable_pextreal_neq_const)
- apply fast
- by simp
- then show ?thesis by simp
+ using AE by (auto simp: A_def `i = 0`)
+ from positive_integral_cong_AE[OF this] show ?thesis by simp
next
case (Suc n)
then have "(\<integral>\<^isup>+x. f x * indicator (A i \<inter> Q j) x \<partial>M) \<le>
@@ -1157,11 +1142,8 @@
by (simp add: mult_le_0_iff)
then have "RN_deriv M \<nu> x * Real (f x) = Real (real (RN_deriv M \<nu> x) * f x)"
using * by (simp add: Real_real) }
- note * = this
- have "(\<integral>\<^isup>+x. RN_deriv M \<nu> x * Real (f x) \<partial>M) = (\<integral>\<^isup>+x. Real (real (RN_deriv M \<nu> x) * f x) \<partial>M)"
- apply (rule positive_integral_cong_AE)
- apply (rule AE_mp[OF RN_deriv_finite[OF \<nu>]])
- by (auto intro!: AE_cong simp: *) }
+ then have "(\<integral>\<^isup>+x. RN_deriv M \<nu> x * Real (f x) \<partial>M) = (\<integral>\<^isup>+x. Real (real (RN_deriv M \<nu> x) * f x) \<partial>M)"
+ using RN_deriv_finite[OF \<nu>] by (auto intro: positive_integral_cong_AE) }
with this this f f' Nf
show ?integral ?integrable
unfolding lebesgue_integral_def integrable_def
--- a/src/HOL/Probability/Sigma_Algebra.thy Fri Feb 04 17:11:00 2011 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy Fri Feb 04 17:25:12 2011 +0100
@@ -769,48 +769,6 @@
show ?thesis by (simp add: comp_def)
qed
-lemma (in sigma_algebra) vimage_vimage_inv:
- assumes f: "bij_betw f S (space M)"
- assumes [simp]: "\<And>x. x \<in> space M \<Longrightarrow> f (g x) = x" and g: "g \<in> space M \<rightarrow> S"
- shows "sigma_algebra.vimage_algebra (vimage_algebra S f) (space M) g = M"
-proof -
- interpret T: sigma_algebra "vimage_algebra S f"
- using f by (safe intro!: sigma_algebra_vimage bij_betw_imp_funcset)
-
- have inj: "inj_on f S" and [simp]: "f`S = space M"
- using f unfolding bij_betw_def by auto
-
- { fix A assume A: "A \<in> sets M"
- have "g -` f -` A \<inter> g -` S \<inter> space M = (f \<circ> g) -` A \<inter> space M"
- using g by auto
- also have "\<dots> = A"
- using `A \<in> sets M`[THEN sets_into_space] by auto
- finally have "g -` f -` A \<inter> g -` S \<inter> space M = A" . }
- note X = this
- show ?thesis
- unfolding T.vimage_algebra_def unfolding vimage_algebra_def
- by (simp add: image_compose[symmetric] comp_def X cong: image_cong)
-qed
-
-lemma (in sigma_algebra) measurable_vimage_iff:
- fixes f :: "'b \<Rightarrow> 'a" assumes f: "bij_betw f S (space M)"
- shows "g \<in> measurable M M' \<longleftrightarrow> (g \<circ> f) \<in> measurable (vimage_algebra S f) M'"
-proof
- assume "g \<in> measurable M M'"
- from measurable_vimage[OF this f[THEN bij_betw_imp_funcset]]
- show "(g \<circ> f) \<in> measurable (vimage_algebra S f) M'" unfolding comp_def .
-next
- interpret v: sigma_algebra "vimage_algebra S f"
- using f[THEN bij_betw_imp_funcset] by (rule sigma_algebra_vimage)
- note f' = f[THEN bij_betw_the_inv_into]
- assume "g \<circ> f \<in> measurable (vimage_algebra S f) M'"
- from v.measurable_vimage[OF this, unfolded space_vimage_algebra, OF f'[THEN bij_betw_imp_funcset]]
- show "g \<in> measurable M M'"
- using f f'[THEN bij_betw_imp_funcset] f[unfolded bij_betw_def]
- by (subst (asm) vimage_vimage_inv)
- (simp_all add: f_the_inv_into_f cong: measurable_cong)
-qed
-
lemma sigma_sets_vimage:
assumes "f \<in> S' \<rightarrow> S" and "A \<subseteq> Pow S"
shows "sigma_sets S' ((\<lambda>X. f -` X \<inter> S') ` A) = (\<lambda>X. f -` X \<inter> S') ` sigma_sets S A"
@@ -1417,93 +1375,10 @@
by (auto simp: image_space_def)
qed
-subsection "Bijective functions with inverse"
-
-definition "bij_inv A B f g \<longleftrightarrow>
- f \<in> A \<rightarrow> B \<and> g \<in> B \<rightarrow> A \<and> (\<forall>x\<in>A. g (f x) = x) \<and> (\<forall>x\<in>B. f (g x) = x)"
-
-lemma bij_inv_symmetric[sym]: "bij_inv A B f g \<Longrightarrow> bij_inv B A g f"
- unfolding bij_inv_def by auto
-
-lemma bij_invI:
- assumes "f \<in> A \<rightarrow> B" "g \<in> B \<rightarrow> A"
- and "\<And>x. x \<in> A \<Longrightarrow> g (f x) = x"
- and "\<And>x. x \<in> B \<Longrightarrow> f (g x) = x"
- shows "bij_inv A B f g"
- using assms unfolding bij_inv_def by auto
-
-lemma bij_invE:
- assumes "bij_inv A B f g"
- "\<lbrakk> f \<in> A \<rightarrow> B ; g \<in> B \<rightarrow> A ;
- (\<And>x. x \<in> A \<Longrightarrow> g (f x) = x) ;
- (\<And>x. x \<in> B \<Longrightarrow> f (g x) = x) \<rbrakk> \<Longrightarrow> P"
- shows P
- using assms unfolding bij_inv_def by auto
-
-lemma bij_inv_bij_betw:
- assumes "bij_inv A B f g"
- shows "bij_betw f A B" "bij_betw g B A"
- using assms by (auto intro: bij_betwI elim!: bij_invE)
-
-lemma bij_inv_vimage_vimage:
- assumes "bij_inv A B f e"
- shows "f -` (e -` X \<inter> B) \<inter> A = X \<inter> A"
- using assms by (auto elim!: bij_invE)
-
-lemma (in sigma_algebra) measurable_vimage_iff_inv:
- fixes f :: "'b \<Rightarrow> 'a" assumes "bij_inv S (space M) f g"
- shows "h \<in> measurable (vimage_algebra S f) M' \<longleftrightarrow> (\<lambda>x. h (g x)) \<in> measurable M M'"
- unfolding measurable_vimage_iff[OF bij_inv_bij_betw(1), OF assms]
-proof (rule measurable_cong)
- fix w assume "w \<in> space (vimage_algebra S f)"
- then have "w \<in> S" by auto
- then show "h w = ((\<lambda>x. h (g x)) \<circ> f) w"
- using assms by (auto elim: bij_invE)
-qed
-
-lemma vimage_algebra_sigma:
- assumes bi: "bij_inv (space (sigma F)) (space (sigma E)) f e"
- and "sets E \<subseteq> Pow (space E)" and F: "sets F \<subseteq> Pow (space F)"
- and "more E = more F"
- and "f \<in> measurable F E" "e \<in> measurable E F"
- shows "sigma_algebra.vimage_algebra (sigma E) (space (sigma F)) f = sigma F"
-proof -
- interpret sigma_algebra "sigma E"
- using assms by (intro sigma_algebra_sigma) auto
- have eq: "sets F = (\<lambda>X. f -` X \<inter> space F) ` sets E"
- proof safe
- fix X assume "X \<in> sets F"
- then have "e -` X \<inter> space E \<in> sets E"
- using `e \<in> measurable E F` unfolding measurable_def by auto
- then show "X \<in>(\<lambda>Y. f -` Y \<inter> space F) ` sets E"
- apply (rule rev_image_eqI)
- unfolding bij_inv_vimage_vimage[OF bi[simplified]]
- using F `X \<in> sets F` by auto
- next
- fix X assume "X \<in> sets E" then show "f -` X \<inter> space F \<in> sets F"
- using `f \<in> measurable F E` unfolding measurable_def by auto
- qed
- show "vimage_algebra (space (sigma F)) f = sigma F"
- unfolding vimage_algebra_def using assms
- by (auto simp: bij_inv_def eq sigma_sets_vimage[symmetric] sigma_def)
-qed
-
lemma measurable_sigma_sigma:
assumes M: "sets M \<subseteq> Pow (space M)" and N: "sets N \<subseteq> Pow (space N)"
shows "f \<in> measurable M N \<Longrightarrow> f \<in> measurable (sigma M) (sigma N)"
using sigma_algebra.measurable_subset[OF sigma_algebra_sigma[OF M], of N]
using measurable_up_sigma[of M N] N by auto
-lemma bij_inv_the_inv_into:
- assumes "bij_betw f A B" shows "bij_inv A B f (the_inv_into A f)"
-proof (rule bij_invI)
- show "the_inv_into A f \<in> B \<rightarrow> A"
- using bij_betw_the_inv_into[OF assms] by (rule bij_betw_imp_funcset)
- show "f \<in> A \<rightarrow> B" using assms by (rule bij_betw_imp_funcset)
- show "\<And>x. x \<in> A \<Longrightarrow> the_inv_into A f (f x) = x"
- "\<And>x. x \<in> B \<Longrightarrow> f (the_inv_into A f x) = x"
- using the_inv_into_f_f[of f A] f_the_inv_into_f[of f A]
- using assms by (auto simp: bij_betw_def)
-qed
-
end