--- a/src/HOL/Probability/Borel_Space.thy Thu Dec 09 17:25:43 2010 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Thu Dec 09 17:26:08 2010 +0100
@@ -1347,6 +1347,16 @@
by (auto intro!: measurable_If)
qed
+lemma (in sigma_algebra) borel_measurable_pextreal_setsum[simp, intro]:
+ fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> pextreal"
+ assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
+ shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
+proof cases
+ assume "finite S"
+ thus ?thesis using assms
+ by induct auto
+qed (simp add: borel_measurable_const)
+
lemma (in sigma_algebra) borel_measurable_pextreal_times[intro, simp]:
fixes f :: "'a \<Rightarrow> pextreal" assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
@@ -1359,15 +1369,14 @@
by (auto intro!: measurable_If)
qed
-lemma (in sigma_algebra) borel_measurable_pextreal_setsum[simp, intro]:
+lemma (in sigma_algebra) borel_measurable_pextreal_setprod[simp, intro]:
fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> pextreal"
assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
- shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
+ shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
proof cases
assume "finite S"
- thus ?thesis using assms
- by induct auto
-qed (simp add: borel_measurable_const)
+ thus ?thesis using assms by induct auto
+qed simp
lemma (in sigma_algebra) borel_measurable_pextreal_min[simp, intro]:
fixes f g :: "'a \<Rightarrow> pextreal"
@@ -1386,7 +1395,7 @@
lemma (in sigma_algebra) borel_measurable_SUP[simp, intro]:
fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> pextreal"
assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
- shows "(SUP i : A. f i) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M")
+ shows "(\<lambda>x. SUP i : A. f i x) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M")
unfolding borel_measurable_pextreal_iff_greater
proof safe
fix a
@@ -1399,7 +1408,7 @@
lemma (in sigma_algebra) borel_measurable_INF[simp, intro]:
fixes f :: "'d :: countable \<Rightarrow> 'a \<Rightarrow> pextreal"
assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
- shows "(INF i : A. f i) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M")
+ shows "(\<lambda>x. INF i : A. f i x) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M")
unfolding borel_measurable_pextreal_iff_less
proof safe
fix a
@@ -1423,20 +1432,10 @@
using assms by auto
qed
-lemma INFI_fun_expand:
- "(INF y:A. f y) = (\<lambda>x. (INF y:A. f y x))"
- by (simp add: fun_eq_iff INFI_apply)
-
-lemma SUPR_fun_expand:
- "(SUP y:A. f y) = (\<lambda>x. (SUP y:A. f y x))"
- by (simp add: fun_eq_iff SUPR_apply)
-
lemma (in sigma_algebra) borel_measurable_psuminf[simp, intro]:
assumes "\<And>i. f i \<in> borel_measurable M"
shows "(\<lambda>x. (\<Sum>\<^isub>\<infinity> i. f i x)) \<in> borel_measurable M"
- using assms unfolding psuminf_def
- by (auto intro!: borel_measurable_SUP [unfolded SUPR_fun_expand])
-
+ using assms unfolding psuminf_def by auto
section "LIMSEQ is borel measurable"
@@ -1459,13 +1458,12 @@
note eq = this
have *: "\<And>x. real (Real (u' x)) - real (Real (- u' x)) = u' x"
by auto
- have "(SUP n. INF m. (\<lambda>x. Real (u (n + m) x))) \<in> borel_measurable M"
- "(SUP n. INF m. (\<lambda>x. Real (- u (n + m) x))) \<in> borel_measurable M"
- using u by (auto intro: borel_measurable_SUP borel_measurable_INF borel_measurable_Real)
+ have "(\<lambda>x. SUP n. INF m. Real (u (n + m) x)) \<in> borel_measurable M"
+ "(\<lambda>x. SUP n. INF m. Real (- u (n + m) x)) \<in> borel_measurable M"
+ using u by auto
with eq[THEN measurable_cong, of M "\<lambda>x. x" borel]
have "(\<lambda>x. Real (u' x)) \<in> borel_measurable M"
- "(\<lambda>x. Real (- u' x)) \<in> borel_measurable M"
- unfolding SUPR_fun_expand INFI_fun_expand by auto
+ "(\<lambda>x. Real (- u' x)) \<in> borel_measurable M" by auto
note this[THEN borel_measurable_real]
from borel_measurable_diff[OF this]
show ?thesis unfolding * .
--- a/src/HOL/Probability/Complete_Measure.thy Thu Dec 09 17:25:43 2010 +0100
+++ b/src/HOL/Probability/Complete_Measure.thy Thu Dec 09 17:26:08 2010 +0100
@@ -257,17 +257,14 @@
show ?thesis
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")
+ 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)
fix x assume eq: "\<forall>i. f i x = f' i x"
- have "g x = (SUP i. f i x)"
- using `f \<up> g` unfolding isoton_def SUPR_fun_expand by auto
- then show "g x = ?f x"
- using eq unfolding SUPR_fun_expand by auto
+ 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)
qed
show "?f \<in> borel_measurable M"
- using sf by (auto intro!: borel_measurable_SUP
- intro: borel_measurable_simple_function)
+ using sf by (auto intro: borel_measurable_simple_function)
qed
qed
--- a/src/HOL/Probability/Information.thy Thu Dec 09 17:25:43 2010 +0100
+++ b/src/HOL/Probability/Information.thy Thu Dec 09 17:26:08 2010 +0100
@@ -188,7 +188,7 @@
using f by (rule \<nu>.measure_space_isomorphic)
let ?RN = "sigma_finite_measure.RN_deriv ?M ?\<mu> ?\<nu>"
- from RN_deriv_vimage[OF f \<nu>]
+ from RN_deriv_vimage[OF f[THEN bij_inv_the_inv_into] \<nu>]
have *: "\<nu>.almost_everywhere (\<lambda>x. ?RN (the_inv_into S f x) = RN_deriv \<nu> x)"
by (rule absolutely_continuous_AE[OF \<nu>])
--- a/src/HOL/Probability/Lebesgue_Integration.thy Thu Dec 09 17:25:43 2010 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Thu Dec 09 17:26:08 2010 +0100
@@ -1069,16 +1069,16 @@
lemma (in measure_space) positive_integral_vimage_inv:
fixes g :: "'d \<Rightarrow> pextreal" and f :: "'d \<Rightarrow> 'a"
- assumes f: "bij_betw f S (space M)"
+ assumes f: "bij_inv S (space M) f h"
shows "measure_space.positive_integral (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) g =
- positive_integral (\<lambda>x. g (the_inv_into S f x))"
+ positive_integral (\<lambda>x. g (h x))"
proof -
interpret v: measure_space "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
- using f by (rule measure_space_isomorphic)
+ using f by (rule measure_space_isomorphic[OF bij_inv_bij_betw(1)])
show ?thesis
- unfolding positive_integral_vimage[OF f, of "\<lambda>x. g (the_inv_into S f x)"]
- using f[unfolded bij_betw_def]
- by (auto intro!: v.positive_integral_cong simp: the_inv_into_f_f)
+ unfolding positive_integral_vimage[OF f[THEN bij_inv_bij_betw(1)], of "\<lambda>x. g (h x)"]
+ using f[unfolded bij_inv_def]
+ by (auto intro!: v.positive_integral_cong)
qed
lemma (in measure_space) positive_integral_SUP_approx:
@@ -1176,8 +1176,6 @@
apply (rule positive_integral_mono)
using `f \<up> u` unfolding isoton_def le_fun_def by auto
next
- have "u \<in> borel_measurable M"
- using borel_measurable_SUP[of UNIV f] assms by (auto simp: isoton_def)
have u: "u = (SUP i. f i)" using `f \<up> u` unfolding isoton_def by auto
show "(SUP i. positive_integral (f i)) = positive_integral u"
@@ -1198,8 +1196,6 @@
shows "(SUP i. positive_integral (f i)) = positive_integral (\<lambda>x. SUP i. f i x)"
(is "_ = positive_integral ?u")
proof -
- have "?u \<in> borel_measurable M"
- using borel_measurable_SUP[of _ f] assms by (simp add: SUPR_fun_expand)
show ?thesis
proof (rule antisym)
show "(SUP j. positive_integral (f j)) \<le> positive_integral ?u"
@@ -1209,9 +1205,9 @@
have "\<And>i. rf i \<in> borel_measurable M" unfolding rf_def
using assms by (simp cong: measurable_cong)
moreover have iso: "rf \<up> ru" using assms unfolding rf_def ru_def
- unfolding isoton_def SUPR_fun_expand le_fun_def fun_eq_iff
+ unfolding isoton_def le_fun_def fun_eq_iff SUPR_apply
using SUP_const[OF UNIV_not_empty]
- by (auto simp: restrict_def le_fun_def SUPR_fun_expand fun_eq_iff)
+ by (auto simp: restrict_def le_fun_def fun_eq_iff)
ultimately have "positive_integral ru \<le> (SUP i. positive_integral (rf i))"
unfolding positive_integral_alt[of ru]
by (auto simp: le_fun_def intro!: SUP_leI positive_integral_SUP_approx)
@@ -1283,6 +1279,11 @@
shows "positive_integral (\<lambda>x. c * f x) = c * positive_integral f"
using positive_integral_linear[OF assms, of "\<lambda>x. 0" c] by auto
+lemma (in measure_space) positive_integral_multc:
+ assumes "f \<in> borel_measurable M"
+ shows "positive_integral (\<lambda>x. f x * c) = positive_integral f * c"
+ unfolding mult_commute[of _ c] positive_integral_cmult[OF assms] by simp
+
lemma (in measure_space) positive_integral_indicator[simp]:
"A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. indicator A x) = \<mu> A"
by (subst positive_integral_eq_simple_integral) (auto simp: simple_function_indicator simple_integral_indicator)
@@ -1349,24 +1350,16 @@
lemma (in measure_space) positive_integral_lim_INF:
fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> pextreal"
assumes "\<And>i. u i \<in> borel_measurable M"
- shows "positive_integral (SUP n. INF m. u (m + n)) \<le>
+ shows "positive_integral (\<lambda>x. SUP n. INF m. u (m + n) x) \<le>
(SUP n. INF m. positive_integral (u (m + n)))"
proof -
- have "(SUP n. INF m. u (m + n)) \<in> borel_measurable M"
- by (auto intro!: borel_measurable_SUP borel_measurable_INF assms)
-
- have "(\<lambda>n. INF m. u (m + n)) \<up> (SUP n. INF m. u (m + n))"
- proof (unfold isoton_def, safe intro!: INF_mono bexI)
- fix i m show "u (Suc m + i) \<le> u (m + Suc i)" by simp
- qed simp
- from positive_integral_isoton[OF this] assms
- have "positive_integral (SUP n. INF m. u (m + n)) =
- (SUP n. positive_integral (INF m. u (m + n)))"
- unfolding isoton_def by (simp add: borel_measurable_INF)
+ have "positive_integral (\<lambda>x. SUP n. INF m. u (m + n) x)
+ = (SUP n. positive_integral (\<lambda>x. INF m. u (m + n) x))"
+ using assms
+ by (intro positive_integral_monotone_convergence_SUP[symmetric] INF_mono)
+ (auto simp del: add_Suc simp add: add_Suc[symmetric])
also have "\<dots> \<le> (SUP n. INF m. positive_integral (u (m + n)))"
- apply (rule SUP_mono)
- apply (rule_tac x=n in bexI)
- by (auto intro!: positive_integral_mono INFI_bound INF_leI exI simp: INFI_fun_expand)
+ by (auto intro!: SUP_mono bexI le_INFI positive_integral_mono INF_leI)
finally show ?thesis .
qed
@@ -1763,6 +1756,11 @@
thus ?P ?I by auto
qed
+lemma (in measure_space) integral_multc:
+ assumes "integrable f"
+ shows "integral (\<lambda>x. f x * c) = integral f * c"
+ unfolding mult_commute[of _ c] integral_cmult[OF assms] ..
+
lemma (in measure_space) integral_mono_AE:
assumes fg: "integrable f" "integrable g"
and mono: "AE t. f t \<le> g t"
@@ -1950,10 +1948,10 @@
have borel_f: "\<And>i. (\<lambda>x. Real (f i x)) \<in> borel_measurable M"
using i unfolding integrable_def by auto
- hence "(SUP i. (\<lambda>x. Real (f i x))) \<in> borel_measurable M"
+ hence "(\<lambda>x. SUP i. Real (f i x)) \<in> borel_measurable M"
by auto
hence borel_u: "u \<in> borel_measurable M"
- using pos_u by (auto simp: borel_measurable_Real_eq SUPR_fun_expand SUP_F)
+ using pos_u by (auto simp: borel_measurable_Real_eq SUP_F)
have integral_eq: "\<And>n. positive_integral (\<lambda>x. Real (f n x)) = Real (integral (f n))"
using i unfolding integral_def integrable_def by (auto simp: Real_real)
@@ -2134,8 +2132,8 @@
thus ?thesis by simp
next
assume neq_0: "positive_integral (\<lambda>x. Real (2 * w x)) \<noteq> 0"
- have "positive_integral (\<lambda>x. Real (2 * w x)) = positive_integral (SUP n. INF m. (\<lambda>x. Real (?diff (m + n) x)))"
- proof (rule positive_integral_cong, unfold SUPR_fun_expand INFI_fun_expand, subst add_commute)
+ have "positive_integral (\<lambda>x. Real (2 * w x)) = positive_integral (\<lambda>x. SUP n. INF m. Real (?diff (m + n) x))"
+ proof (rule positive_integral_cong, subst add_commute)
fix x assume x: "x \<in> space M"
show "Real (2 * w x) = (SUP n. INF m. Real (?diff (n + m) x))"
proof (rule LIMSEQ_imp_lim_INF[symmetric])
--- a/src/HOL/Probability/Lebesgue_Measure.thy Thu Dec 09 17:25:43 2010 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Thu Dec 09 17:26:08 2010 +0100
@@ -552,10 +552,10 @@
proof -
from positive_integral_isoton[unfolded isoton_fun_expand isoton_iff_Lim_mono, of f u]
show ?ilim using mono lim i by auto
- have "(SUP i. f i) = u" using mono lim SUP_Lim_pextreal
- unfolding fun_eq_iff SUPR_fun_expand mono_def by auto
- moreover have "(SUP i. f i) \<in> borel_measurable M"
- using i by (rule borel_measurable_SUP)
+ have "\<And>x. (SUP i. f i x) = u x" using mono lim SUP_Lim_pextreal
+ unfolding fun_eq_iff mono_def by auto
+ moreover have "(\<lambda>x. SUP i. f i x) \<in> borel_measurable M"
+ using i by auto
ultimately show "u \<in> borel_measurable M" by simp
qed
@@ -647,44 +647,20 @@
definition p2e :: "(nat \<Rightarrow> real) \<Rightarrow> 'a::ordered_euclidean_space" where
"p2e x = (\<chi>\<chi> i. x i)"
-lemma bij_euclidean_component:
- "bij_betw (e2p::'a::ordered_euclidean_space \<Rightarrow> _) (UNIV :: 'a set)
- ({..<DIM('a)} \<rightarrow>\<^isub>E (UNIV :: real set))"
- unfolding bij_betw_def e2p_def_raw
-proof let ?e = "\<lambda>x.\<lambda>i\<in>{..<DIM('a::ordered_euclidean_space)}. (x::'a)$$i"
- show "inj ?e" unfolding inj_on_def restrict_def apply(subst euclidean_eq) apply safe
- apply(drule_tac x=i in fun_cong) by auto
- { fix x::"nat \<Rightarrow> real" assume x:"\<forall>i. i \<notin> {..<DIM('a)} \<longrightarrow> x i = undefined"
- hence "x = ?e (\<chi>\<chi> i. x i)" apply-apply(rule,case_tac "xa<DIM('a)") by auto
- hence "x \<in> range ?e" by fastsimp
- } thus "range ?e = ({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)}"
- unfolding extensional_def using DIM_positive by auto
-qed
+lemma e2p_p2e[simp]:
+ "x \<in> extensional {..<DIM('a)} \<Longrightarrow> e2p (p2e x::'a::ordered_euclidean_space) = x"
+ by (auto simp: fun_eq_iff extensional_def p2e_def e2p_def)
-lemma bij_p2e:
- "bij_betw (p2e::_ \<Rightarrow> 'a::ordered_euclidean_space) ({..<DIM('a)} \<rightarrow>\<^isub>E (UNIV :: real set))
- (UNIV :: 'a set)" (is "bij_betw ?p ?U _")
- unfolding bij_betw_def
-proof show "inj_on ?p ?U" unfolding inj_on_def p2e_def
- apply(subst euclidean_eq) apply(safe,rule) unfolding extensional_def
- apply(case_tac "xa<DIM('a)") by auto
- { fix x::'a have "x \<in> ?p ` extensional {..<DIM('a)}"
- unfolding image_iff apply(rule_tac x="\<lambda>i. if i<DIM('a) then x$$i else undefined" in bexI)
- apply(subst euclidean_eq,safe) unfolding p2e_def extensional_def by auto
- } thus "?p ` ?U = UNIV" by auto
-qed
+lemma p2e_e2p[simp]:
+ "p2e (e2p x) = (x::'a::ordered_euclidean_space)"
+ by (auto simp: euclidean_eq[where 'a='a] p2e_def e2p_def)
-lemma e2p_p2e[simp]: fixes z::"'a::ordered_euclidean_space"
- assumes "x \<in> extensional {..<DIM('a)}"
- shows "e2p (p2e x::'a) = x"
-proof fix i::nat
- show "e2p (p2e x::'a) i = x i" unfolding e2p_def p2e_def restrict_def
- using assms unfolding extensional_def by auto
-qed
-
-lemma p2e_e2p[simp]: fixes x::"'a::ordered_euclidean_space"
- shows "p2e (e2p x) = x"
- apply(subst euclidean_eq) unfolding e2p_def p2e_def restrict_def by auto
+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
interpretation borel_product: product_sigma_finite "\<lambda>x. borel::real algebra" "\<lambda>x. lmeasure"
by default
@@ -692,71 +668,80 @@
lemma cube_subset_Suc[intro]: "cube n \<subseteq> cube (Suc n)"
unfolding cube_def_raw subset_eq apply safe unfolding mem_interval by auto
-lemma borel_vimage_algebra_eq:
- "sigma_algebra.vimage_algebra
- (borel :: ('a::ordered_euclidean_space) algebra) ({..<DIM('a)} \<rightarrow>\<^isub>E UNIV) p2e =
- sigma (product_algebra (\<lambda>x. \<lparr> space = UNIV::real set, sets = range (\<lambda>a. {..<a}) \<rparr>) {..<DIM('a)} )"
-proof- note bor = borel_eq_lessThan
- def F \<equiv> "product_algebra (\<lambda>x. \<lparr> space = UNIV::real set, sets = range (\<lambda>a. {..<a}) \<rparr>) {..<DIM('a)}"
- def E \<equiv> "\<lparr>space = (UNIV::'a set), sets = range lessThan\<rparr>"
- have *:"(({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)}) = space F" unfolding F_def by auto
- show ?thesis unfolding F_def[symmetric] * bor
- proof(rule vimage_algebra_sigma,unfold E_def[symmetric])
- show "sets E \<subseteq> Pow (space E)" "p2e \<in> space F \<rightarrow> space E" unfolding E_def by auto
- next fix A assume "A \<in> sets F"
- hence A:"A \<in> (Pi\<^isub>E {..<DIM('a)}) ` ({..<DIM('a)} \<rightarrow> range lessThan)"
- unfolding F_def product_algebra_def algebra.simps .
- then guess B unfolding image_iff .. note B=this
- hence "\<forall>x<DIM('a). B x \<in> range lessThan" by auto
- hence "\<forall>x. \<exists>xa. x<DIM('a) \<longrightarrow> B x = {..<xa}" unfolding image_iff by auto
- from choice[OF this] guess b .. note b=this
- hence b':"\<forall>i<DIM('a). Sup (B i) = b i" using Sup_lessThan by auto
+lemma Pi_iff: "f \<in> Pi I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i)"
+ unfolding Pi_def by auto
- show "A \<in> (\<lambda>X. p2e -` X \<inter> space F) ` sets E" unfolding image_iff B
- proof(rule_tac x="{..< \<chi>\<chi> i. Sup (B i)}" in bexI)
- show "Pi\<^isub>E {..<DIM('a)} B = p2e -` {..<(\<chi>\<chi> i. Sup (B i))::'a} \<inter> space F"
- unfolding F_def E_def product_algebra_def algebra.simps
- proof(rule,unfold subset_eq,rule_tac[!] ballI)
- fix x assume "x \<in> Pi\<^isub>E {..<DIM('a)} B"
- hence *:"\<forall>i<DIM('a). x i < b i" "\<forall>i\<ge>DIM('a). x i = undefined"
- unfolding Pi_def extensional_def using b by auto
- have "(p2e x::'a) < (\<chi>\<chi> i. Sup (B i))" unfolding less_prod_def eucl_less[of "p2e x"]
- apply safe unfolding euclidean_lambda_beta b'[rule_format] p2e_def using * by auto
- moreover have "x \<in> extensional {..<DIM('a)}"
- using *(2) unfolding extensional_def by auto
- ultimately show "x \<in> p2e -` {..<(\<chi>\<chi> i. Sup (B i)) ::'a} \<inter>
- (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})" by auto
- next fix x assume as:"x \<in> p2e -` {..<(\<chi>\<chi> i. Sup (B i))::'a} \<inter>
- (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})"
- hence "p2e x < ((\<chi>\<chi> i. Sup (B i))::'a)" by auto
- hence "\<forall>i<DIM('a). x i \<in> B i" apply-apply(subst(asm) eucl_less)
- unfolding p2e_def using b b' by auto
- thus "x \<in> Pi\<^isub>E {..<DIM('a)} B" using as unfolding Pi_def extensional_def by auto
- qed
- show "{..<(\<chi>\<chi> i. Sup (B i))::'a} \<in> sets E" unfolding E_def algebra.simps by auto
- qed
- next fix A assume "A \<in> sets E"
- then guess a unfolding E_def algebra.simps image_iff .. note a = this(2)
- def B \<equiv> "\<lambda>i. {..<a $$ i}"
- show "p2e -` A \<inter> space F \<in> sets F" unfolding F_def
- unfolding product_algebra_def algebra.simps image_iff
- apply(rule_tac x=B in bexI) apply rule unfolding subset_eq apply(rule_tac[1-2] ballI)
- proof- show "B \<in> {..<DIM('a)} \<rightarrow> range lessThan" unfolding B_def by auto
- fix x assume as:"x \<in> p2e -` A \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})"
- hence "p2e x \<in> A" by auto
- hence "\<forall>i<DIM('a). x i \<in> B i" unfolding B_def a lessThan_iff
- apply-apply(subst (asm) eucl_less) unfolding p2e_def by auto
- thus "x \<in> Pi\<^isub>E {..<DIM('a)} B" using as unfolding Pi_def extensional_def by auto
- next fix x assume x:"x \<in> Pi\<^isub>E {..<DIM('a)} B"
- moreover have "p2e x \<in> A" unfolding a lessThan_iff p2e_def apply(subst eucl_less)
- using x unfolding Pi_def extensional_def B_def by auto
- ultimately show "x \<in> p2e -` A \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})" by auto
- qed
- qed
+lemma measurable_e2p_on_generator:
+ "e2p \<in> measurable \<lparr> space = UNIV::'a set, sets = range lessThan \<rparr>
+ (product_algebra
+ (\<lambda>x. \<lparr> space = UNIV::real set, sets = range lessThan \<rparr>)
+ {..<DIM('a::ordered_euclidean_space)})"
+ (is "e2p \<in> measurable ?E ?P")
+proof (unfold measurable_def, intro CollectI conjI ballI)
+ show "e2p \<in> space ?E \<rightarrow> space ?P" by (auto simp: e2p_def)
+ fix A assume "A \<in> sets ?P"
+ then obtain E where A: "A = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. E i)"
+ and "E \<in> {..<DIM('a)} \<rightarrow> (range lessThan)"
+ by (auto elim!: product_algebraE)
+ then have "\<forall>i\<in>{..<DIM('a)}. \<exists>xs. E i = {..< xs}" by auto
+ from this[THEN bchoice] guess xs ..
+ then have A_eq: "A = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..< xs i})"
+ using A by auto
+ have "e2p -` A = {..< (\<chi>\<chi> i. xs i) :: 'a}"
+ using DIM_positive by (auto simp add: Pi_iff set_eq_iff e2p_def A_eq
+ euclidean_eq[where 'a='a] eucl_less[where 'a='a])
+ then show "e2p -` A \<inter> space ?E \<in> sets ?E" by simp
qed
+lemma measurable_p2e_on_generator:
+ "p2e \<in> measurable
+ (product_algebra
+ (\<lambda>x. \<lparr> space = UNIV::real set, sets = range lessThan \<rparr>)
+ {..<DIM('a::ordered_euclidean_space)})
+ \<lparr> space = UNIV::'a set, sets = range lessThan \<rparr>"
+ (is "p2e \<in> measurable ?P ?E")
+proof (unfold measurable_def, intro CollectI conjI ballI)
+ show "p2e \<in> space ?P \<rightarrow> space ?E" by simp
+ fix A assume "A \<in> sets ?E"
+ then obtain x where "A = {..<x}" by auto
+ then have "p2e -` A \<inter> space ?P = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..< x $$ i})"
+ using DIM_positive
+ by (auto simp: Pi_iff set_eq_iff p2e_def
+ euclidean_eq[where 'a='a] eucl_less[where 'a='a])
+ then show "p2e -` A \<inter> space ?P \<in> sets ?P" by auto
+qed
+
+lemma borel_vimage_algebra_eq:
+ defines "F \<equiv> product_algebra (\<lambda>x. \<lparr> space = (UNIV::real set), sets = range lessThan \<rparr>) {..<DIM('a::ordered_euclidean_space)}"
+ shows "sigma_algebra.vimage_algebra (borel::'a::ordered_euclidean_space algebra) (space (sigma F)) p2e = sigma F"
+ unfolding borel_eq_lessThan
+proof (intro vimage_algebra_sigma)
+ let ?E = "\<lparr>space = (UNIV::'a set), sets = range lessThan\<rparr>"
+ show "bij_inv (space (sigma F)) (space (sigma ?E)) p2e e2p"
+ using bij_inv_p2e_e2p unfolding F_def by simp
+ show "sets F \<subseteq> Pow (space F)" "sets ?E \<subseteq> Pow (space ?E)" unfolding F_def
+ by (intro product_algebra_sets_into_space) auto
+ show "p2e \<in> measurable F ?E"
+ "e2p \<in> measurable ?E F"
+ unfolding F_def using measurable_p2e_on_generator measurable_e2p_on_generator by auto
+qed
+
+lemma product_borel_eq_vimage:
+ "sigma (product_algebra (\<lambda>x. borel) {..<DIM('a::ordered_euclidean_space)}) =
+ sigma_algebra.vimage_algebra borel (extensional {..<DIM('a)})
+ (p2e:: _ \<Rightarrow> 'a::ordered_euclidean_space)"
+ unfolding borel_vimage_algebra_eq[simplified]
+ unfolding borel_eq_lessThan
+ apply(subst sigma_product_algebra_sigma_eq[where S="\<lambda>i. \<lambda>n. lessThan (real n)"])
+ unfolding lessThan_iff
+proof- fix i assume i:"i<DIM('a)"
+ show "(\<lambda>n. {..<real n}) \<up> space \<lparr>space = UNIV, sets = range lessThan\<rparr>"
+ by(auto intro!:real_arch_lt isotoneI)
+qed auto
+
lemma e2p_Int:"e2p ` A \<inter> e2p ` B = e2p ` (A \<inter> B)" (is "?L = ?R")
- apply(rule image_Int[THEN sym]) using bij_euclidean_component
+ 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"
@@ -775,18 +760,6 @@
unfolding Int_stable_def algebra.select_convs
apply safe unfolding inter_interval by auto
-lemma product_borel_eq_vimage:
- "sigma (product_algebra (\<lambda>x. borel) {..<DIM('a::ordered_euclidean_space)}) =
- sigma_algebra.vimage_algebra borel (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})
- (p2e:: _ \<Rightarrow> 'a::ordered_euclidean_space)"
- unfolding borel_vimage_algebra_eq unfolding borel_eq_lessThan
- apply(subst sigma_product_algebra_sigma_eq[where S="\<lambda>i. \<lambda>n. lessThan (real n)"])
- unfolding lessThan_iff
-proof- fix i assume i:"i<DIM('a)"
- show "(\<lambda>n. {..<real n}) \<up> space \<lparr>space = UNIV, sets = range lessThan\<rparr>"
- by(auto intro!:real_arch_lt isotoneI)
-qed auto
-
lemma inj_on_disjoint_family_on: assumes "disjoint_family_on A S" "inj f"
shows "disjoint_family_on (\<lambda>x. f ` A x) S"
unfolding disjoint_family_on_def
@@ -808,12 +781,12 @@
unfolding e2p_def by auto
lemma e2p_image_vimage: fixes A::"'a::ordered_euclidean_space set"
- shows "e2p ` A = p2e -` A \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})"
+ 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> (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})"
+ 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> (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})"
+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
@@ -879,17 +852,15 @@
qed
show "disjoint_family (\<lambda>n. e2p ` A n)" apply(rule inj_on_disjoint_family_on)
- using bij_euclidean_component using A(2) unfolding bij_betw_def by auto
+ using bij_inv_p2e_e2p[THEN bij_inv_bij_betw(2)] using A(2) unfolding bij_betw_def by auto
show "(\<Union>n. e2p ` A n) \<in> sets (sigma (product_algebra (\<lambda>x. borel) {..<DIM('a)}))"
unfolding product_borel_eq_vimage borel.in_vimage_algebra
proof(rule bexI[OF _ A(3)],rule set_eqI,rule)
fix x assume x:"x \<in> (\<Union>n. e2p ` A n)" hence "p2e x \<in> (\<Union>i. A i)" by auto
moreover have "x \<in> extensional {..<DIM('a)}"
using x unfolding extensional_def e2p_def_raw by auto
- ultimately show "x \<in> p2e -` (\<Union>i. A i) \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter>
- extensional {..<DIM('a)})" by auto
- next fix x assume x:"x \<in> p2e -` (\<Union>i. A i) \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter>
- extensional {..<DIM('a)})"
+ ultimately show "x \<in> p2e -` (\<Union>i. A i) \<inter> extensional {..<DIM('a)}" by auto
+ next fix x assume x:"x \<in> p2e -` (\<Union>i. A i) \<inter> extensional {..<DIM('a)}"
hence "p2e x \<in> (\<Union>i. A i)" by auto
hence "\<exists>n. x \<in> e2p ` A n" apply safe apply(rule_tac x=i in exI)
unfolding image_iff apply(rule_tac x="p2e x" in bexI)
@@ -925,23 +896,20 @@
assumes f: "f \<in> borel_measurable borel"
shows "borel.positive_integral f =
borel_product.product_positive_integral {..<DIM('a)} (f \<circ> p2e)"
-proof- def U \<equiv> "(({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)}):: (nat \<Rightarrow> real) set"
+proof- def U \<equiv> "extensional {..<DIM('a)} :: (nat \<Rightarrow> real) set"
interpret fprod: finite_product_sigma_finite "\<lambda>x. borel" "\<lambda>x. lmeasure" "{..<DIM('a)}" by default auto
- have "\<And>x. \<exists>i::nat. x < real i" by (metis real_arch_lt)
- hence "(\<lambda>n::nat. {..<real n}) \<up> UNIV" apply-apply(rule isotoneI) by auto
- hence *:"sigma_algebra.vimage_algebra borel U (p2e:: _ \<Rightarrow> 'a)
+ have *:"sigma_algebra.vimage_algebra borel U (p2e:: _ \<Rightarrow> 'a)
= sigma (product_algebra (\<lambda>x. borel) {..<DIM('a)})"
- unfolding U_def apply-apply(subst borel_vimage_algebra_eq)
- apply(subst sigma_product_algebra_sigma_eq[where S="\<lambda>x. \<lambda>n. {..<(\<chi>\<chi> i. real n)}", THEN sym])
- unfolding borel_eq_lessThan[THEN sym] by auto
- show ?thesis unfolding borel.positive_integral_vimage[unfolded space_borel,OF bij_p2e]
+ unfolding U_def product_borel_eq_vimage[symmetric] ..
+ show ?thesis
+ unfolding borel.positive_integral_vimage[unfolded space_borel, OF bij_inv_p2e_e2p[THEN bij_inv_bij_betw(1)]]
apply(subst fprod.positive_integral_cong_measure[THEN sym, of "\<lambda>A. lmeasure (p2e ` A)"])
unfolding U_def[symmetric] *[THEN sym] o_def
proof- fix A assume A:"A \<in> sets (sigma_algebra.vimage_algebra borel U (p2e ::_ \<Rightarrow> 'a))"
hence *:"A \<subseteq> extensional {..<DIM('a)}" unfolding U_def by auto
- from A guess B unfolding borel.in_vimage_algebra U_def .. note B=this
- have "(p2e ` A::'a set) \<in> sets borel" unfolding B apply(subst Int_left_commute)
- apply(subst Int_absorb1) unfolding p2e_inv_extensional[of B,THEN sym] using B(1) by auto
+ from A guess B unfolding borel.in_vimage_algebra U_def ..
+ then have "(p2e ` A::'a set) \<in> sets borel"
+ by (simp add: p2e_inv_extensional[of B, symmetric])
from lmeasure_measure_eq_borel_prod[OF this] show "lmeasure (p2e ` A::'a set) =
finite_product_sigma_finite.measure (\<lambda>x. borel) (\<lambda>x. lmeasure) {..<DIM('a)} A"
unfolding e2p_p2e'[OF *] .
--- a/src/HOL/Probability/Positive_Extended_Real.thy Thu Dec 09 17:25:43 2010 +0100
+++ b/src/HOL/Probability/Positive_Extended_Real.thy Thu Dec 09 17:26:08 2010 +0100
@@ -260,6 +260,9 @@
qed
end
+lemma Real_minus_abs[simp]: "Real (- \<bar>x\<bar>) = 0"
+ by simp
+
lemma pextreal_plus_eq_\<omega>[simp]: "(a :: pextreal) + b = \<omega> \<longleftrightarrow> a = \<omega> \<or> b = \<omega>"
by (cases a, cases b) auto
--- a/src/HOL/Probability/Probability_Space.thy Thu Dec 09 17:25:43 2010 +0100
+++ b/src/HOL/Probability/Probability_Space.thy Thu Dec 09 17:26:08 2010 +0100
@@ -352,7 +352,7 @@
show "sigma_algebra (sigma (pair_algebra MX MY))" by default
have sa: "sigma_algebra M" by default
show "(\<lambda>x. (X x, Y x)) \<in> measurable M (sigma (pair_algebra MX MY))"
- unfolding P.measurable_pair[OF sa] using assms by (simp add: comp_def)
+ unfolding P.measurable_pair_iff[OF sa] using assms by (simp add: comp_def)
qed
lemma (in prob_space) distribution_order:
@@ -410,8 +410,9 @@
assume A: "range A \<subseteq> sets XY.P" and df: "disjoint_family A"
have "(\<Sum>\<^isub>\<infinity>n. \<mu> (?X (A n))) = \<mu> (\<Union>x. ?X (A x))"
proof (intro measure_countably_additive)
- from assms have *: "(\<lambda>x. (X x, Y x)) \<in> measurable M XY.P"
- by (intro XY.measurable_prod_sigma) (simp_all add: comp_def, default)
+ have "sigma_algebra M" by default
+ then have *: "(\<lambda>x. (X x, Y x)) \<in> measurable M XY.P"
+ using assms by (simp add: XY.measurable_pair comp_def)
show "range (\<lambda>n. ?X (A n)) \<subseteq> events"
using measurable_sets[OF *] A by auto
show "disjoint_family (\<lambda>n. ?X (A n))"
@@ -503,7 +504,7 @@
show "finite_sigma_algebra (sigma (pair_algebra MX MY))" by default
have sa: "sigma_algebra M" by default
show "(\<lambda>x. (X x, Y x)) \<in> measurable M (sigma (pair_algebra MX MY))"
- unfolding P.measurable_pair[OF sa] using assms by (simp add: comp_def)
+ unfolding P.measurable_pair_iff[OF sa] using assms by (simp add: comp_def)
qed
lemma (in prob_space) finite_random_variable_imp_sets:
@@ -640,7 +641,7 @@
proof
fix x assume "x \<in> space XY.P"
moreover have "(\<lambda>x. (X x, Y x)) \<in> measurable M XY.P"
- using X Y by (subst XY.measurable_pair) (simp_all add: o_def, default)
+ using X Y by (intro XY.measurable_pair) (simp_all add: o_def, default)
ultimately have "(\<lambda>x. (X x, Y x)) -` {x} \<inter> space M \<in> sets M"
unfolding measurable_def by simp
then show "joint_distribution X Y {x} \<noteq> \<omega>"
@@ -1068,13 +1069,13 @@
show "\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. Z x = g (Y x)"
proof (intro ballI bexI)
- show "(SUP i. g i) \<in> borel_measurable M'"
+ show "(\<lambda>x. SUP i. g i x) \<in> borel_measurable M'"
using g by (auto intro: M'.borel_measurable_simple_function)
fix x assume "x \<in> space M"
have "Z x = (SUP i. f i) x" using `f \<up> Z` unfolding isoton_def by simp
- also have "\<dots> = (SUP i. g i) (Y x)" unfolding SUPR_fun_expand
+ also have "\<dots> = (SUP i. g i (Y x))" unfolding SUPR_apply
using g `x \<in> space M` by simp
- finally show "Z x = (SUP i. g i) (Y x)" .
+ finally show "Z x = (SUP i. g i (Y x))" .
qed
qed
--- a/src/HOL/Probability/Product_Measure.thy Thu Dec 09 17:25:43 2010 +0100
+++ b/src/HOL/Probability/Product_Measure.thy Thu Dec 09 17:26:08 2010 +0100
@@ -92,6 +92,12 @@
shows "a \<in> extensional (insert i I)"
using assms unfolding extensional_def by auto
+lemma merge_singleton[simp]: "i \<notin> I \<Longrightarrow> merge I x {i} y = restrict (x(i := y i)) (insert i I)"
+ unfolding merge_def by (auto simp: fun_eq_iff)
+
+lemma Pi_Int: "Pi I E \<inter> Pi I F = (\<Pi> i\<in>I. E i \<inter> F i)"
+ by auto
+
lemma PiE_Int: "(Pi\<^isub>E I A) \<inter> (Pi\<^isub>E I B) = Pi\<^isub>E I (\<lambda>x. A x \<inter> B x)"
by auto
@@ -107,6 +113,64 @@
lemma Pi_cancel_fupd[simp]: "i \<notin> I \<Longrightarrow> x(i := a) \<in> Pi I B \<longleftrightarrow> x \<in> Pi I B"
by (auto simp: Pi_def)
+lemma restrict_vimage:
+ assumes "I \<inter> J = {}"
+ shows "(\<lambda>x. (restrict x I, restrict x J)) -` (Pi\<^isub>E I E \<times> Pi\<^isub>E J F) = Pi (I \<union> J) (merge I E J F)"
+ using assms by (auto simp: restrict_Pi_cancel)
+
+lemma merge_vimage:
+ assumes "I \<inter> J = {}"
+ shows "(\<lambda>(x,y). merge I x J y) -` Pi\<^isub>E (I \<union> J) E = Pi I E \<times> Pi J E"
+ using assms by (auto simp: restrict_Pi_cancel)
+
+lemma restrict_fupd[simp]: "i \<notin> I \<Longrightarrow> restrict (f (i := x)) I = restrict f I"
+ by (auto simp: restrict_def intro!: ext)
+
+lemma merge_restrict[simp]:
+ "merge I (restrict x I) J y = merge I x J y"
+ "merge I x J (restrict y J) = merge I x J y"
+ unfolding merge_def by (auto intro!: ext)
+
+lemma merge_x_x_eq_restrict[simp]:
+ "merge I x J x = restrict x (I \<union> J)"
+ unfolding merge_def by (auto intro!: ext)
+
+lemma Pi_fupd_iff: "i \<in> I \<Longrightarrow> f \<in> Pi I (B(i := A)) \<longleftrightarrow> f \<in> Pi (I - {i}) B \<and> f i \<in> A"
+ apply auto
+ apply (drule_tac x=x in Pi_mem)
+ apply (simp_all split: split_if_asm)
+ apply (drule_tac x=i in Pi_mem)
+ apply (auto dest!: Pi_mem)
+ done
+
+lemma Pi_UN:
+ fixes A :: "nat \<Rightarrow> 'i \<Rightarrow> 'a set"
+ assumes "finite I" and mono: "\<And>i n m. i \<in> I \<Longrightarrow> n \<le> m \<Longrightarrow> A n i \<subseteq> A m i"
+ shows "(\<Union>n. Pi I (A n)) = (\<Pi> i\<in>I. \<Union>n. A n i)"
+proof (intro set_eqI iffI)
+ fix f assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
+ then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i" by auto
+ from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)" by auto
+ obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k"
+ using `finite I` finite_nat_set_iff_bounded_le[of "n`I"] by auto
+ have "f \<in> Pi I (A k)"
+ proof (intro Pi_I)
+ fix i assume "i \<in> I"
+ from mono[OF this, of "n i" k] k[OF this] n[OF this]
+ show "f i \<in> A k i" by auto
+ qed
+ then show "f \<in> (\<Union>n. Pi I (A n))" by auto
+qed auto
+
+lemma PiE_cong:
+ assumes "\<And>i. i\<in>I \<Longrightarrow> A i = B i"
+ shows "Pi\<^isub>E I A = Pi\<^isub>E I B"
+ using assms by (auto intro!: Pi_cong)
+
+lemma restrict_upd[simp]:
+ "i \<notin> I \<Longrightarrow> (restrict f I)(i := y) = restrict (f(i := y)) (insert i I)"
+ by (auto simp: fun_eq_iff)
+
section "Binary products"
definition
@@ -134,6 +198,14 @@
"space (pair_algebra A B) = space A \<times> space B"
by (simp add: pair_algebra_def)
+lemma sets_pair_algebra: "sets (pair_algebra N M) = (\<lambda>(x, y). x \<times> y) ` (sets N \<times> sets M)"
+ unfolding pair_algebra_def by auto
+
+lemma pair_algebra_sets_into_space:
+ assumes "sets M \<subseteq> Pow (space M)" "sets N \<subseteq> Pow (space N)"
+ shows "sets (pair_algebra M N) \<subseteq> Pow (space (pair_algebra M N))"
+ using assms by (auto simp: pair_algebra_def)
+
lemma pair_algebra_Int_snd:
assumes "sets S1 \<subseteq> Pow (space S1)"
shows "pair_algebra S1 (algebra.restricted_space S2 A) =
@@ -176,7 +248,7 @@
then show ?fst ?snd by auto
qed
-lemma (in pair_sigma_algebra) measurable_pair:
+lemma (in pair_sigma_algebra) measurable_pair_iff:
assumes "sigma_algebra M"
shows "f \<in> measurable M P \<longleftrightarrow>
(fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2"
@@ -205,42 +277,11 @@
qed
qed
-lemma (in pair_sigma_algebra) measurable_prod_sigma:
+lemma (in pair_sigma_algebra) measurable_pair:
assumes "sigma_algebra M"
- assumes 1: "(fst \<circ> f) \<in> measurable M M1" and 2: "(snd \<circ> f) \<in> measurable M M2"
+ assumes "(fst \<circ> f) \<in> measurable M M1" "(snd \<circ> f) \<in> measurable M M2"
shows "f \<in> measurable M P"
-proof -
- interpret M: sigma_algebra M by fact
- from 1 have fn1: "fst \<circ> f \<in> space M \<rightarrow> space M1"
- and q1: "\<forall>y\<in>sets M1. (fst \<circ> f) -` y \<inter> space M \<in> sets M"
- by (auto simp add: measurable_def)
- from 2 have fn2: "snd \<circ> f \<in> space M \<rightarrow> space M2"
- and q2: "\<forall>y\<in>sets M2. (snd \<circ> f) -` y \<inter> space M \<in> sets M"
- by (auto simp add: measurable_def)
- show ?thesis
- proof (rule M.measurable_sigma)
- show "sets E \<subseteq> Pow (space E)"
- using M1.space_closed M2.space_closed
- by (auto simp add: sigma_algebra_iff pair_algebra_def)
- next
- show "f \<in> space M \<rightarrow> space E"
- by (simp add: space_pair_algebra) (rule prod_final [OF fn1 fn2])
- next
- fix z
- assume z: "z \<in> sets E"
- thus "f -` z \<inter> space M \<in> sets M"
- proof (auto simp add: pair_algebra_def vimage_Times)
- fix x y
- assume x: "x \<in> sets M1" and y: "y \<in> sets M2"
- have "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M =
- ((fst \<circ> f) -` x \<inter> space M) \<inter> ((snd \<circ> f) -` y \<inter> space M)"
- by blast
- also have "... \<in> sets M" using x y q1 q2
- by blast
- finally show "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M \<in> sets M" .
- qed
- qed
-qed
+ unfolding measurable_pair_iff[OF assms(1)] using assms(2,3) by simp
lemma pair_algebraE:
assumes "X \<in> sets (pair_algebra M1 M2)"
@@ -726,11 +767,11 @@
then have F_borel: "\<And>i. F i \<in> borel_measurable P"
and F_mono: "\<And>i x. F i x \<le> F (Suc i) x"
and F_SUPR: "\<And>x. (SUP i. F i x) = f x"
- unfolding isoton_def le_fun_def SUPR_fun_expand
+ unfolding isoton_fun_expand unfolding isoton_def le_fun_def
by (auto intro: borel_measurable_simple_function)
note sf = simple_function_cut[OF F(1)]
- then have "(SUP i. ?C (F i)) \<in> borel_measurable M1"
- using F(1) by (auto intro!: M1.borel_measurable_SUP)
+ then have "(\<lambda>x. SUP i. ?C (F i) x) \<in> borel_measurable M1"
+ using F(1) by auto
moreover
{ fix x assume "x \<in> space M1"
have isotone: "(\<lambda> i y. F i (x, y)) \<up> (\<lambda>y. f (x, y))"
@@ -742,7 +783,7 @@
by (simp add: isoton_def) }
note SUPR_C = this
ultimately show "?C f \<in> borel_measurable M1"
- unfolding SUPR_fun_expand by (simp cong: measurable_cong)
+ by (simp cong: measurable_cong)
have "positive_integral (\<lambda>x. SUP i. F i x) = (SUP i. positive_integral (F i))"
using F_borel F_mono
by (auto intro!: positive_integral_monotone_convergence_SUP[symmetric])
@@ -1003,10 +1044,25 @@
sublocale finite_product_sigma_algebra \<subseteq> sigma_algebra P
using product_algebra_into_space by (rule sigma_algebra_sigma)
+lemma product_algebraE:
+ assumes "A \<in> sets (product_algebra M I)"
+ obtains E where "A = Pi\<^isub>E I E" "E \<in> (\<Pi> i\<in>I. sets (M i))"
+ using assms unfolding product_algebra_def by auto
+
+lemma product_algebraI[intro]:
+ assumes "E \<in> (\<Pi> i\<in>I. sets (M i))"
+ shows "Pi\<^isub>E I E \<in> sets (product_algebra M I)"
+ using assms unfolding product_algebra_def by auto
+
lemma space_product_algebra[simp]:
"space (product_algebra M I) = Pi\<^isub>E I (\<lambda>i. space (M i))"
unfolding product_algebra_def by simp
+lemma product_algebra_sets_into_space:
+ assumes "\<And>i. i\<in>I \<Longrightarrow> sets (M i) \<subseteq> Pow (space (M i))"
+ shows "sets (product_algebra M I) \<subseteq> Pow (space (product_algebra M I))"
+ using assms by (auto simp: product_algebra_def) blast
+
lemma (in finite_product_sigma_algebra) P_empty:
"I = {} \<Longrightarrow> P = \<lparr> space = {\<lambda>k. undefined}, sets = { {}, {\<lambda>k. undefined} }\<rparr>"
unfolding product_algebra_def by (simp add: sigma_def image_constant)
@@ -1015,34 +1071,122 @@
"\<lbrakk> \<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i) \<rbrakk> \<Longrightarrow> Pi\<^isub>E I A \<in> sets P"
by (auto simp: product_algebra_def sets_sigma intro!: sigma_sets.Basic)
-lemma bij_betw_prod_fold:
- assumes "i \<notin> I"
- shows "bij_betw (\<lambda>x. (x(i:=undefined), x i)) (\<Pi>\<^isub>E j\<in>insert i I. space (M j)) ((\<Pi>\<^isub>E j\<in>I. space (M j)) \<times> space (M i))"
- (is "bij_betw ?f ?P ?F")
- using `i \<notin> I`
-proof (unfold bij_betw_def, intro conjI set_eqI iffI)
- show "inj_on ?f ?P"
- proof (safe intro!: inj_onI ext)
- fix a b x assume "a(i:=undefined) = b(i:=undefined)" "a i = b i"
- then show "a x = b x"
- by (cases "x = i") (auto simp: fun_eq_iff split: split_if_asm)
+lemma (in product_sigma_algebra) bij_inv_restrict_merge:
+ assumes [simp]: "I \<inter> J = {}"
+ shows "bij_inv
+ (space (sigma (product_algebra M (I \<union> J))))
+ (space (sigma (pair_algebra (product_algebra M I) (product_algebra M J))))
+ (\<lambda>x. (restrict x I, restrict x J)) (\<lambda>(x, y). merge I x J y)"
+ by (rule bij_invI) (auto simp: space_pair_algebra extensional_restrict)
+
+lemma (in product_sigma_algebra) bij_inv_singleton:
+ "bij_inv (space (sigma (product_algebra M {i}))) (space (M i))
+ (\<lambda>x. x i) (\<lambda>x. (\<lambda>j\<in>{i}. x))"
+ by (rule bij_invI) (auto simp: restrict_def extensional_def fun_eq_iff)
+
+lemma (in product_sigma_algebra) bij_inv_restrict_insert:
+ assumes [simp]: "i \<notin> I"
+ shows "bij_inv
+ (space (sigma (product_algebra M (insert i I))))
+ (space (sigma (pair_algebra (product_algebra M I) (M i))))
+ (\<lambda>x. (restrict x I, x i)) (\<lambda>(x, y). x(i := y))"
+ by (rule bij_invI) (auto simp: space_pair_algebra extensional_restrict)
+
+lemma (in product_sigma_algebra) measurable_restrict_on_generating:
+ assumes [simp]: "I \<inter> J = {}"
+ shows "(\<lambda>x. (restrict x I, restrict x J)) \<in> measurable
+ (product_algebra M (I \<union> J))
+ (pair_algebra (product_algebra M I) (product_algebra M J))"
+ (is "?R \<in> measurable ?IJ ?P")
+proof (unfold measurable_def, intro CollectI conjI ballI)
+ show "?R \<in> space ?IJ \<rightarrow> space ?P" by (auto simp: space_pair_algebra)
+ { fix F E assume "E \<in> (\<Pi> i\<in>I. sets (M i))" "F \<in> (\<Pi> i\<in>J. sets (M i))"
+ then have "Pi (I \<union> J) (merge I E J F) \<inter> (\<Pi>\<^isub>E i\<in>I \<union> J. space (M i)) =
+ Pi\<^isub>E (I \<union> J) (merge I E J F)"
+ using M.sets_into_space by auto blast+ }
+ note this[simp]
+ show "\<And>A. A \<in> sets ?P \<Longrightarrow> ?R -` A \<inter> space ?IJ \<in> sets ?IJ"
+ by (force elim!: pair_algebraE product_algebraE
+ simp del: vimage_Int simp: restrict_vimage merge_vimage space_pair_algebra)
+ qed
+
+lemma (in product_sigma_algebra) measurable_merge_on_generating:
+ assumes [simp]: "I \<inter> J = {}"
+ shows "(\<lambda>(x, y). merge I x J y) \<in> measurable
+ (pair_algebra (product_algebra M I) (product_algebra M J))
+ (product_algebra M (I \<union> J))"
+ (is "?M \<in> measurable ?P ?IJ")
+proof (unfold measurable_def, intro CollectI conjI ballI)
+ show "?M \<in> space ?P \<rightarrow> space ?IJ" by (auto simp: space_pair_algebra)
+ { fix E assume "E \<in> (\<Pi> i\<in>I. sets (M i))" "E \<in> (\<Pi> i\<in>J. sets (M i))"
+ then have "Pi I E \<times> Pi J E \<inter> (\<Pi>\<^isub>E i\<in>I. space (M i)) \<times> (\<Pi>\<^isub>E i\<in>J. space (M i)) =
+ Pi\<^isub>E I E \<times> Pi\<^isub>E J E"
+ using M.sets_into_space by auto blast+ }
+ note this[simp]
+ show "\<And>A. A \<in> sets ?IJ \<Longrightarrow> ?M -` A \<inter> space ?P \<in> sets ?P"
+ by (force elim!: pair_algebraE product_algebraE
+ simp del: vimage_Int simp: restrict_vimage merge_vimage space_pair_algebra)
qed
-next
- fix X assume *: "X \<in> ?F" show "X \<in> ?f ` ?P"
- proof (cases X)
- case (Pair a b) with * `i \<notin> I` show ?thesis
- by (auto intro!: image_eqI[where x="a (i := b)"] ext simp: extensional_def)
- qed
-qed auto
+
+lemma (in product_sigma_algebra) measurable_singleton_on_generator:
+ "(\<lambda>x. \<lambda>j\<in>{i}. x) \<in> measurable (M i) (product_algebra M {i})"
+ (is "?f \<in> measurable _ ?P")
+proof (unfold measurable_def, intro CollectI conjI)
+ show "?f \<in> space (M i) \<rightarrow> space ?P" by auto
+ have "\<And>E. E i \<in> sets (M i) \<Longrightarrow> ?f -` Pi\<^isub>E {i} E \<inter> space (M i) = E i"
+ using M.sets_into_space by auto
+ then show "\<forall>A \<in> sets ?P. ?f -` A \<inter> space (M i) \<in> sets (M i)"
+ by (auto elim!: product_algebraE)
+qed
+
+lemma (in product_sigma_algebra) measurable_component_on_generator:
+ assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (product_algebra M I) (M i)"
+ (is "?f \<in> measurable ?P _")
+proof (unfold measurable_def, intro CollectI conjI ballI)
+ show "?f \<in> space ?P \<rightarrow> space (M i)" using `i \<in> I` by auto
+ fix A assume "A \<in> sets (M i)"
+ moreover then have "(\<lambda>x. x i) -` A \<inter> (\<Pi>\<^isub>E i\<in>I. space (M i)) =
+ (\<Pi>\<^isub>E j\<in>I. if i = j then A else space (M j))"
+ using M.sets_into_space `i \<in> I`
+ by (fastsimp dest: Pi_mem split: split_if_asm)
+ ultimately show "?f -` A \<inter> space ?P \<in> sets ?P"
+ by (auto intro!: product_algebraI)
+qed
-lemma borel_measurable_product_component:
- assumes "i \<in> I"
- shows "(\<lambda>x. x i) \<in> borel_measurable (sigma (product_algebra (\<lambda>x. borel) I))"
-proof -
- have *: "\<And>A. (\<lambda>x. x i) -` A \<inter> extensional I = (\<Pi>\<^isub>E j\<in>I. if j = i then A else UNIV)"
- using `i \<in> I` by (auto elim!: PiE)
- show ?thesis
- by (auto simp: * measurable_def product_algebra_def)
+lemma (in product_sigma_algebra) measurable_restrict_singleton_on_generating:
+ assumes [simp]: "i \<notin> I"
+ shows "(\<lambda>x. (restrict x I, x i)) \<in> measurable
+ (product_algebra M (insert i I))
+ (pair_algebra (product_algebra M I) (M i))"
+ (is "?R \<in> measurable ?I ?P")
+proof (unfold measurable_def, intro CollectI conjI ballI)
+ show "?R \<in> space ?I \<rightarrow> space ?P" by (auto simp: space_pair_algebra)
+ { fix E F assume "E \<in> (\<Pi> i\<in>I. sets (M i))" "F \<in> sets (M i)"
+ then have "(\<lambda>x. (restrict x I, x i)) -` (Pi\<^isub>E I E \<times> F) \<inter> (\<Pi>\<^isub>E i\<in>insert i I. space (M i)) =
+ Pi\<^isub>E (insert i I) (E(i := F))"
+ using M.sets_into_space using `i\<notin>I` by (auto simp: restrict_Pi_cancel) blast+ }
+ note this[simp]
+ show "\<And>A. A \<in> sets ?P \<Longrightarrow> ?R -` A \<inter> space ?I \<in> sets ?I"
+ by (force elim!: pair_algebraE product_algebraE
+ simp del: vimage_Int simp: space_pair_algebra)
+qed
+
+lemma (in product_sigma_algebra) measurable_merge_singleton_on_generating:
+ assumes [simp]: "i \<notin> I"
+ shows "(\<lambda>(x, y). x(i := y)) \<in> measurable
+ (pair_algebra (product_algebra M I) (M i))
+ (product_algebra M (insert i I))"
+ (is "?M \<in> measurable ?P ?IJ")
+proof (unfold measurable_def, intro CollectI conjI ballI)
+ show "?M \<in> space ?P \<rightarrow> space ?IJ" by (auto simp: space_pair_algebra)
+ { fix E assume "E \<in> (\<Pi> i\<in>I. sets (M i))" "E i \<in> sets (M i)"
+ then have "(\<lambda>(x, y). x(i := y)) -` Pi\<^isub>E (insert i I) E \<inter> (\<Pi>\<^isub>E i\<in>I. space (M i)) \<times> space (M i) =
+ Pi\<^isub>E I E \<times> E i"
+ using M.sets_into_space by auto blast+ }
+ note this[simp]
+ show "\<And>A. A \<in> sets ?IJ \<Longrightarrow> ?M -` A \<inter> space ?P \<in> sets ?P"
+ by (force elim!: pair_algebraE product_algebraE
+ simp del: vimage_Int simp: space_pair_algebra)
qed
section "Generating set generates also product algebra"
@@ -1108,38 +1252,6 @@
by (simp add: pair_algebra_def sigma_def)
qed
-lemma Pi_fupd_iff: "i \<in> I \<Longrightarrow> f \<in> Pi I (B(i := A)) \<longleftrightarrow> f \<in> Pi (I - {i}) B \<and> f i \<in> A"
- apply auto
- apply (drule_tac x=x in Pi_mem)
- apply (simp_all split: split_if_asm)
- apply (drule_tac x=i in Pi_mem)
- apply (auto dest!: Pi_mem)
- done
-
-lemma Pi_UN:
- fixes A :: "nat \<Rightarrow> 'i \<Rightarrow> 'a set"
- assumes "finite I" and mono: "\<And>i n m. i \<in> I \<Longrightarrow> n \<le> m \<Longrightarrow> A n i \<subseteq> A m i"
- shows "(\<Union>n. Pi I (A n)) = (\<Pi> i\<in>I. \<Union>n. A n i)"
-proof (intro set_eqI iffI)
- fix f assume "f \<in> (\<Pi> i\<in>I. \<Union>n. A n i)"
- then have "\<forall>i\<in>I. \<exists>n. f i \<in> A n i" by auto
- from bchoice[OF this] obtain n where n: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> (A (n i) i)" by auto
- obtain k where k: "\<And>i. i \<in> I \<Longrightarrow> n i \<le> k"
- using `finite I` finite_nat_set_iff_bounded_le[of "n`I"] by auto
- have "f \<in> Pi I (A k)"
- proof (intro Pi_I)
- fix i assume "i \<in> I"
- from mono[OF this, of "n i" k] k[OF this] n[OF this]
- show "f i \<in> A k i" by auto
- qed
- then show "f \<in> (\<Union>n. Pi I (A n))" by auto
-qed auto
-
-lemma PiE_cong:
- assumes "\<And>i. i\<in>I \<Longrightarrow> A i = B i"
- shows "Pi\<^isub>E I A = Pi\<^isub>E I B"
- using assms by (auto intro!: Pi_cong)
-
lemma sigma_product_algebra_sigma_eq:
assumes "finite I"
assumes isotone: "\<And>i. i \<in> I \<Longrightarrow> (S i) \<up> (space (E i))"
@@ -1209,150 +1321,163 @@
by (simp add: product_algebra_def sigma_def)
qed
-lemma (in finite_product_sigma_algebra) pair_sigma_algebra_finite_product_space:
- "sigma (pair_algebra P (M i)) = sigma (pair_algebra G (M i))"
-proof -
- have "sigma (pair_algebra P (M i)) = sigma (pair_algebra P (sigma (M i)))" by simp
- also have "\<dots> = sigma (pair_algebra G (M i))"
- proof (rule pair_sigma_algebra_sigma)
- show "(\<lambda>_. \<Pi>\<^isub>E i\<in>I. space (M i)) \<up> space G"
- "(\<lambda>_. space (M i)) \<up> space (M i)"
- by (simp_all add: isoton_const)
- show "range (\<lambda>_. \<Pi>\<^isub>E i\<in>I. space (M i)) \<subseteq> sets G" "range (\<lambda>_. space (M i)) \<subseteq> sets (M i)"
- by (auto intro!: image_eqI[where x="\<lambda>i\<in>I. space (M i)"] dest: Pi_mem
- simp: product_algebra_def)
- show "sets G \<subseteq> Pow (space G)" "sets (M i) \<subseteq> Pow (space (M i))"
- using product_algebra_into_space M.sets_into_space by auto
- qed
- finally show ?thesis .
-qed
-
-lemma sets_pair_algebra: "sets (pair_algebra N M) = (\<lambda>(x, y). x \<times> y) ` (sets N \<times> sets M)"
- unfolding pair_algebra_def by auto
-
-lemma (in finite_product_sigma_algebra) sigma_pair_algebra_sigma_eq:
+lemma (in product_sigma_algebra) sigma_pair_algebra_sigma_eq:
"sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))) =
sigma (pair_algebra (product_algebra M I) (product_algebra M J))"
using M.sets_into_space
by (intro pair_sigma_algebra_sigma[of "\<lambda>_. \<Pi>\<^isub>E i\<in>I. space (M i)", of _ "\<lambda>_. \<Pi>\<^isub>E i\<in>J. space (M i)"])
(auto simp: isoton_const product_algebra_def, blast+)
+lemma (in product_sigma_algebra) sigma_pair_algebra_product_singleton:
+ "sigma (pair_algebra (sigma (product_algebra M I)) (M i)) =
+ sigma (pair_algebra (product_algebra M I) (M i))"
+ using M.sets_into_space apply (subst M.sigma_eq[symmetric])
+ by (intro pair_sigma_algebra_sigma[of "\<lambda>_. \<Pi>\<^isub>E i\<in>I. space (M i)" _ "\<lambda>_. space (M i)"])
+ (auto simp: isoton_const product_algebra_def, blast+)
+
+lemma (in product_sigma_algebra) measurable_restrict:
+ assumes [simp]: "I \<inter> J = {}"
+ shows "(\<lambda>x. (restrict x I, restrict x J)) \<in> measurable
+ (sigma (product_algebra M (I \<union> J)))
+ (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))"
+ unfolding sigma_pair_algebra_sigma_eq using M.sets_into_space
+ by (intro measurable_sigma_sigma measurable_restrict_on_generating
+ pair_algebra_sets_into_space product_algebra_sets_into_space)
+ auto
+
+lemma (in product_sigma_algebra) measurable_merge:
+ assumes [simp]: "I \<inter> J = {}"
+ shows "(\<lambda>(x, y). merge I x J y) \<in> measurable
+ (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))
+ (sigma (product_algebra M (I \<union> J)))"
+ unfolding sigma_pair_algebra_sigma_eq using M.sets_into_space
+ by (intro measurable_sigma_sigma measurable_merge_on_generating
+ pair_algebra_sets_into_space product_algebra_sets_into_space)
+ auto
+
lemma (in product_sigma_algebra) product_product_vimage_algebra:
- assumes [simp]: "I \<inter> J = {}" and "finite I" "finite J"
+ assumes [simp]: "I \<inter> J = {}"
shows "sigma_algebra.vimage_algebra
(sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))
- (space (product_algebra M (I \<union> J))) (\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))) =
+ (space (sigma (product_algebra M (I \<union> J)))) (\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))) =
sigma (product_algebra M (I \<union> J))"
- (is "sigma_algebra.vimage_algebra _ (space ?IJ) ?f = sigma ?IJ")
-proof -
- have "finite (I \<union> J)" using assms by auto
- interpret I: finite_product_sigma_algebra M I by default fact
- interpret J: finite_product_sigma_algebra M J by default fact
- interpret IJ: finite_product_sigma_algebra M "I \<union> J" by default fact
- interpret pair_sigma_algebra I.P J.P by default
+ unfolding sigma_pair_algebra_sigma_eq using sets_into_space
+ by (intro vimage_algebra_sigma[OF bij_inv_restrict_merge]
+ pair_algebra_sets_into_space product_algebra_sets_into_space
+ measurable_merge_on_generating measurable_restrict_on_generating)
+ auto
+
+lemma (in product_sigma_algebra) pair_product_product_vimage_algebra:
+ assumes [simp]: "I \<inter> J = {}"
+ shows "sigma_algebra.vimage_algebra (sigma (product_algebra M (I \<union> J)))
+ (space (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))) (\<lambda>(x,y). merge I x J y) =
+ (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))"
+ unfolding sigma_pair_algebra_sigma_eq using sets_into_space
+ by (intro vimage_algebra_sigma[OF bij_inv_restrict_merge[symmetric]]
+ pair_algebra_sets_into_space product_algebra_sets_into_space
+ measurable_merge_on_generating measurable_restrict_on_generating)
+ auto
+
+lemma (in product_sigma_algebra) pair_product_singleton_vimage_algebra:
+ assumes [simp]: "i \<notin> I"
+ shows "sigma_algebra.vimage_algebra (sigma (pair_algebra (sigma (product_algebra M I)) (M i)))
+ (space (sigma (product_algebra M (insert i I)))) (\<lambda>x. (restrict x I, x i)) =
+ (sigma (product_algebra M (insert i I)))"
+ unfolding sigma_pair_algebra_product_singleton using sets_into_space
+ by (intro vimage_algebra_sigma[OF bij_inv_restrict_insert]
+ pair_algebra_sets_into_space product_algebra_sets_into_space
+ measurable_merge_singleton_on_generating measurable_restrict_singleton_on_generating)
+ auto
- show "vimage_algebra (space ?IJ) ?f = sigma ?IJ"
- unfolding I.sigma_pair_algebra_sigma_eq
- proof (rule vimage_algebra_sigma)
- from M.sets_into_space
- show "sets (pair_algebra I.G J.G) \<subseteq> Pow (space (pair_algebra I.G J.G))"
- by (auto simp: sets_pair_algebra space_pair_algebra product_algebra_def) blast+
- show "?f \<in> space IJ.G \<rightarrow> space (pair_algebra I.G J.G)"
- by (auto simp: space_pair_algebra product_algebra_def)
- let ?F = "\<lambda>A. ?f -` A \<inter> (space IJ.G)"
- let ?s = "\<lambda>I. Pi\<^isub>E I ` (\<Pi> i\<in>I. sets (M i))"
- { fix A assume "A \<in> sets IJ.G"
- then obtain F where A: "A = Pi\<^isub>E (I \<union> J) F" "F \<in> (\<Pi> i\<in>I. sets (M i))" "F \<in> (\<Pi> i\<in>J. sets (M i))"
- by (auto simp: product_algebra_def)
- show "A \<in> ?F ` sets (pair_algebra I.G J.G)"
- using A M.sets_into_space
- by (auto simp: restrict_Pi_cancel product_algebra_def
- intro!: image_eqI[where x="Pi\<^isub>E I F \<times> Pi\<^isub>E J F"]) blast+ }
- { fix A assume "A \<in> sets (pair_algebra I.G J.G)"
- then obtain E F where A: "A = Pi\<^isub>E I E \<times> Pi\<^isub>E J F" "E \<in> (\<Pi> i\<in>I. sets (M i))" "F \<in> (\<Pi> i\<in>J. sets (M i))"
- by (auto simp: product_algebra_def sets_pair_algebra)
- then show "?F A \<in> sets IJ.G"
- using A M.sets_into_space
- by (auto simp: restrict_Pi_cancel product_algebra_def
- intro!: image_eqI[where x="merge I E J F"]) blast+ }
- qed
-qed
+lemma (in product_sigma_algebra) singleton_vimage_algebra:
+ "sigma_algebra.vimage_algebra (sigma (product_algebra M {i})) (space (M i)) (\<lambda>x. \<lambda>j\<in>{i}. x) = M i"
+ using sets_into_space
+ by (intro vimage_algebra_sigma[of "M i", unfolded M.sigma_eq, OF bij_inv_singleton[symmetric]]
+ product_algebra_sets_into_space measurable_singleton_on_generator measurable_component_on_generator)
+ auto
+
+lemma (in product_sigma_algebra) measurable_restrict_iff:
+ assumes IJ[simp]: "I \<inter> J = {}"
+ shows "f \<in> measurable (sigma (pair_algebra
+ (sigma (product_algebra M I)) (sigma (product_algebra M J)))) M' \<longleftrightarrow>
+ (\<lambda>x. f (restrict x I, restrict x J)) \<in> measurable (sigma (product_algebra M (I \<union> J))) M'"
+ using M.sets_into_space
+ apply (subst pair_product_product_vimage_algebra[OF IJ, symmetric])
+ apply (subst sigma_pair_algebra_sigma_eq)
+ apply (subst sigma_algebra.measurable_vimage_iff_inv[OF _
+ bij_inv_restrict_merge[symmetric]])
+ apply (intro sigma_algebra_sigma product_algebra_sets_into_space)
+ by auto
-lemma (in finite_product_sigma_algebra) sigma_pair_algebra_sigma_M_eq:
- "sigma (pair_algebra P (M i)) = sigma (pair_algebra G (M i))"
+lemma (in product_sigma_algebra) measurable_merge_iff:
+ assumes IJ: "I \<inter> J = {}"
+ shows "f \<in> measurable (sigma (product_algebra M (I \<union> J))) M' \<longleftrightarrow>
+ (\<lambda>(x, y). f (merge I x J y)) \<in>
+ measurable (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J)))) M'"
+ unfolding measurable_restrict_iff[OF IJ]
+ by (rule measurable_cong) (auto intro!: arg_cong[where f=f] simp: extensional_restrict)
+
+lemma (in product_sigma_algebra) measurable_component:
+ assumes "i \<in> I" and f: "f \<in> measurable (M i) M'"
+ shows "(\<lambda>x. f (x i)) \<in> measurable (sigma (product_algebra M I)) M'"
+ (is "?f \<in> measurable ?P M'")
proof -
- have "sigma (pair_algebra P (sigma (M i))) = sigma (pair_algebra G (M i))"
- using M.sets_into_space
- by (intro pair_sigma_algebra_sigma[of "\<lambda>_. \<Pi>\<^isub>E i\<in>I. space (M i)", of _ "\<lambda>_. space (M i)"])
- (auto simp: isoton_const product_algebra_def, blast+)
- then show ?thesis by simp
+ have "f \<circ> (\<lambda>x. x i) \<in> measurable ?P M'"
+ apply (rule measurable_comp[OF _ f])
+ using measurable_up_sigma[of "product_algebra M I" "M i"]
+ using measurable_component_on_generator[OF `i \<in> I`]
+ by auto
+ then show "?f \<in> measurable ?P M'" by (simp add: comp_def)
qed
-lemma (in product_sigma_algebra) product_singleton_vimage_algebra_eq:
- assumes [simp]: "i \<notin> I" "finite I"
- shows "sigma_algebra.vimage_algebra
- (sigma (pair_algebra (sigma (product_algebra M I)) (M i)))
- (space (product_algebra M (insert i I))) (\<lambda>x. ((\<lambda>i\<in>I. x i), x i)) =
- sigma (product_algebra M (insert i I))"
- (is "sigma_algebra.vimage_algebra _ (space ?I') ?f = sigma ?I'")
-proof -
- have "finite (insert i I)" using assms by auto
- interpret I: finite_product_sigma_algebra M I by default fact
- interpret I': finite_product_sigma_algebra M "insert i I" by default fact
- interpret pair_sigma_algebra I.P "M i" by default
- show "vimage_algebra (space ?I') ?f = sigma ?I'"
- unfolding I.sigma_pair_algebra_sigma_M_eq
- proof (rule vimage_algebra_sigma)
- from M.sets_into_space
- show "sets (pair_algebra I.G (M i)) \<subseteq> Pow (space (pair_algebra I.G (M i)))"
- by (auto simp: sets_pair_algebra space_pair_algebra product_algebra_def) blast
- show "?f \<in> space I'.G \<rightarrow> space (pair_algebra I.G (M i))"
- by (auto simp: space_pair_algebra product_algebra_def)
- let ?F = "\<lambda>A. ?f -` A \<inter> (space I'.G)"
- { fix A assume "A \<in> sets I'.G"
- then obtain F where A: "A = Pi\<^isub>E (insert i I) F" "F \<in> (\<Pi> i\<in>I. sets (M i))" "F i \<in> sets (M i)"
- by (auto simp: product_algebra_def)
- show "A \<in> ?F ` sets (pair_algebra I.G (M i))"
- using A M.sets_into_space
- by (auto simp: restrict_Pi_cancel product_algebra_def
- intro!: image_eqI[where x="Pi\<^isub>E I F \<times> F i"]) blast+ }
- { fix A assume "A \<in> sets (pair_algebra I.G (M i))"
- then obtain E F where A: "A = Pi\<^isub>E I E \<times> F" "E \<in> (\<Pi> i\<in>I. sets (M i))" "F \<in> sets (M i)"
- by (auto simp: product_algebra_def sets_pair_algebra)
- then show "?F A \<in> sets I'.G"
- using A M.sets_into_space
- by (auto simp: restrict_Pi_cancel product_algebra_def
- intro!: image_eqI[where x="E(i:= F)"]) blast+ }
+lemma (in product_sigma_algebra) measurable_component_singleton:
+ "(\<lambda>x. f (x i)) \<in> measurable (sigma (product_algebra M {i})) M' \<longleftrightarrow>
+ f \<in> measurable (M i) M'"
+ using sets_into_space
+ apply (subst singleton_vimage_algebra[symmetric])
+ apply (subst sigma_algebra.measurable_vimage_iff_inv[OF _ bij_inv_singleton[symmetric]])
+ by (auto intro!: sigma_algebra_sigma product_algebra_sets_into_space)
+
+lemma (in product_sigma_algebra) measurable_component_iff:
+ assumes "i \<in> I" and not_empty: "\<forall>i\<in>I. space (M i) \<noteq> {}"
+ shows "(\<lambda>x. f (x i)) \<in> measurable (sigma (product_algebra M I)) M' \<longleftrightarrow>
+ f \<in> measurable (M i) M'"
+ (is "?f \<in> measurable ?P M' \<longleftrightarrow> _")
+proof
+ assume "f \<in> measurable (M i) M'" then show "?f \<in> measurable ?P M'"
+ by (rule measurable_component[OF `i \<in> I`])
+next
+ assume f: "?f \<in> measurable ?P M'"
+ def t \<equiv> "\<lambda>i. SOME x. x \<in> space (M i)"
+ have t: "\<And>i. i\<in>I \<Longrightarrow> t i \<in> space (M i)"
+ unfolding t_def using not_empty by (rule_tac someI_ex) auto
+ have "?f \<circ> (\<lambda>x. (\<lambda>j\<in>I. if j = i then x else t j)) \<in> measurable (M i) M'"
+ (is "?f \<circ> ?t \<in> measurable _ _")
+ proof (rule measurable_comp[OF _ f])
+ have "?t \<in> measurable (M i) (product_algebra M I)"
+ proof (unfold measurable_def, intro CollectI conjI ballI)
+ from t show "?t \<in> space (M i) \<rightarrow> (space (product_algebra M I))" by auto
+ next
+ fix A assume A: "A \<in> sets (product_algebra M I)"
+ { fix E assume "E \<in> (\<Pi> i\<in>I. sets (M i))"
+ then have "?t -` Pi\<^isub>E I E \<inter> space (M i) = (if (\<forall>j\<in>I-{i}. t j \<in> E j) then E i else {})"
+ using `i \<in> I` sets_into_space by (auto dest: Pi_mem[where B=E]) }
+ note * = this
+ with A `i \<in> I` show "?t -` A \<inter> space (M i) \<in> sets (M i)"
+ by (auto elim!: product_algebraE simp del: vimage_Int)
+ qed
+ also have "\<dots> \<subseteq> measurable (M i) (sigma (product_algebra M I))"
+ using M.sets_into_space by (intro measurable_subset) (auto simp: product_algebra_def, blast)
+ finally show "?t \<in> measurable (M i) (sigma (product_algebra M I))" .
qed
+ then show "f \<in> measurable (M i) M'" unfolding comp_def using `i \<in> I` by simp
qed
-lemma restrict_fupd[simp]: "i \<notin> I \<Longrightarrow> restrict (f (i := x)) I = restrict f I"
- by (auto simp: restrict_def intro!: ext)
-
-lemma bij_betw_restrict_I_i:
- "i \<notin> I \<Longrightarrow> bij_betw (\<lambda>x. (restrict x I, x i))
- (space (product_algebra M (insert i I)))
- (space (pair_algebra (sigma (product_algebra M I)) (M i)))"
- by (intro bij_betwI[where g="(\<lambda>(x,y). x(i:=y))"])
- (auto simp: space_pair_algebra extensional_def intro!: ext)
-
-lemma (in product_sigma_algebra) product_singleton_vimage_algebra_inv_eq:
- assumes [simp]: "i \<notin> I" "finite I"
- shows "sigma_algebra.vimage_algebra
- (sigma (product_algebra M (insert i I)))
- (space (pair_algebra (sigma (product_algebra M I)) (M i))) (\<lambda>(x,y). x(i:=y)) =
- sigma (pair_algebra (sigma (product_algebra M I)) (M i))"
-proof -
- have "finite (insert i I)" using `finite I` by auto
- interpret I: finite_product_sigma_algebra M I by default fact
- interpret I': finite_product_sigma_algebra M "insert i I" by default fact
- interpret pair_sigma_algebra I.P "M i" by default
- show ?thesis
- unfolding product_singleton_vimage_algebra_eq[OF assms, symmetric]
- using bij_betw_restrict_I_i[OF `i \<notin> I`, of M]
- by (rule vimage_vimage_inv[unfolded space_sigma])
- (auto simp: space_pair_algebra product_algebra_def dest: extensional_restrict)
-qed
+lemma (in product_sigma_algebra) measurable_singleton:
+ shows "f \<in> measurable (sigma (product_algebra M {i})) M' \<longleftrightarrow>
+ (\<lambda>x. f (\<lambda>j\<in>{i}. x)) \<in> measurable (M i) M'"
+ using sets_into_space unfolding measurable_component_singleton[symmetric]
+ by (auto intro!: measurable_cong arg_cong[where f=f] simp: fun_eq_iff extensional_def)
locale product_sigma_finite =
fixes M :: "'i \<Rightarrow> 'a algebra" and \<mu> :: "'i \<Rightarrow> 'a set \<Rightarrow> pextreal"
@@ -1427,9 +1552,10 @@
let ?h = "\<lambda>x. (restrict x I, x i)"
let ?\<nu> = "\<lambda>A. P.pair_measure (?h ` A)"
interpret I': measure_space "sigma (product_algebra M (insert i I))" ?\<nu>
- unfolding product_singleton_vimage_algebra_eq[OF `i \<notin> I` `finite I`, symmetric]
- using bij_betw_restrict_I_i[OF `i \<notin> I`, of M]
- by (intro P.measure_space_isomorphic) auto
+ apply (subst pair_product_singleton_vimage_algebra[OF `i \<notin> I`, symmetric])
+ apply (intro P.measure_space_isomorphic bij_inv_bij_betw)
+ unfolding sigma_pair_algebra_product_singleton
+ by (rule bij_inv_restrict_insert[OF `i \<notin> I`])
show ?case
proof (intro exI[of _ ?\<nu>] conjI ballI)
{ fix A assume A: "A \<in> (\<Pi> i\<in>insert i I. sets (M i))"
@@ -1512,6 +1638,17 @@
"product_integral I \<equiv>
measure_space.integral (sigma (product_algebra M I)) (product_measure I)"
+abbreviation (in product_sigma_finite)
+ "product_integrable I \<equiv>
+ measure_space.integrable (sigma (product_algebra M I)) (product_measure I)"
+
+lemma (in product_sigma_finite) product_measure_empty[simp]:
+ "product_measure {} {\<lambda>x. undefined} = 1"
+proof -
+ interpret finite_product_sigma_finite M \<mu> "{}" by default auto
+ from measure_times[of "\<lambda>x. {}"] show ?thesis by simp
+qed
+
lemma (in product_sigma_finite) positive_integral_empty:
"product_positive_integral {} f = f (\<lambda>k. undefined)"
proof -
@@ -1528,46 +1665,6 @@
qed
qed
-lemma merge_restrict[simp]:
- "merge I (restrict x I) J y = merge I x J y"
- "merge I x J (restrict y J) = merge I x J y"
- unfolding merge_def by (auto intro!: ext)
-
-lemma merge_x_x_eq_restrict[simp]:
- "merge I x J x = restrict x (I \<union> J)"
- unfolding merge_def by (auto intro!: ext)
-
-lemma bij_betw_restrict_I_J:
- "I \<inter> J = {} \<Longrightarrow> bij_betw (\<lambda>x. (restrict x I, restrict x J))
- (space (product_algebra M (I \<union> J)))
- (space (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J))))"
- by (intro bij_betwI[where g="\<lambda>(x,y). merge I x J y"])
- (auto dest: extensional_restrict simp: space_pair_algebra)
-
-lemma (in product_sigma_algebra) product_product_vimage_algebra_eq:
- assumes [simp]: "I \<inter> J = {}" and "finite I" "finite J"
- shows "sigma_algebra.vimage_algebra
- (sigma (product_algebra M (I \<union> J)))
- (space (sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J)))))
- (\<lambda>(x, y). merge I x J y) =
- sigma (pair_algebra (sigma (product_algebra M I)) (sigma (product_algebra M J)))"
- (is "sigma_algebra.vimage_algebra ?IJ ?S ?m = ?P")
-proof -
- interpret I: finite_product_sigma_algebra M I by default fact
- interpret J: finite_product_sigma_algebra M J by default fact
- have "finite (I \<union> J)" using assms by auto
- interpret IJ: finite_product_sigma_algebra M "I \<union> J" by default fact
- interpret P: pair_sigma_algebra I.P J.P by default
-
- let ?g = "\<lambda>x. (restrict x I, restrict x J)"
- let ?f = "\<lambda>(x, y). merge I x J y"
- show "IJ.vimage_algebra (space P.P) ?f = P.P"
- using bij_betw_restrict_I_J[OF `I \<inter> J = {}`]
- by (subst P.vimage_vimage_inv[of ?g "space IJ.G" ?f,
- unfolded product_product_vimage_algebra[OF assms]])
- (auto simp: pair_algebra_def dest: extensional_restrict)
-qed
-
lemma (in product_sigma_finite) measure_fold:
assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
assumes A: "A \<in> sets (sigma (product_algebra M (I \<union> J)))"
@@ -1598,9 +1695,10 @@
show "range ?F \<subseteq> sets IJ.G" using F by (simp add: image_subset_iff product_algebra_def)
show "?F \<up> space IJ.G " using F(2) by simp
show "measure_space IJ.P (\<lambda>A. P.pair_measure (?f ` A))"
- unfolding product_product_vimage_algebra[OF IJ fin, symmetric]
- using bij_betw_restrict_I_J[OF IJ, of M]
- by (auto intro!: P.measure_space_isomorphic)
+ apply (subst product_product_vimage_algebra[OF IJ, symmetric])
+ apply (intro P.measure_space_isomorphic bij_inv_bij_betw)
+ unfolding sigma_pair_algebra_sigma_eq
+ by (rule bij_inv_restrict_merge[OF `I \<inter> J = {}`])
show "measure_space IJ.P IJ.measure" by fact
next
fix A assume "A \<in> sets IJ.G"
@@ -1640,14 +1738,16 @@
interpret P: pair_sigma_finite I.P I.measure J.P J.measure by default
let ?f = "\<lambda>x. ((\<lambda>i\<in>I. x i), (\<lambda>i\<in>J. x i))"
have P_borel: "(\<lambda>x. f (case x of (x, y) \<Rightarrow> merge I x J y)) \<in> borel_measurable P.P"
- by (subst product_product_vimage_algebra_eq[OF IJ fin, symmetric])
- (auto simp: space_pair_algebra intro!: IJ.measurable_vimage f)
+ unfolding case_prod_distrib measurable_merge_iff[OF IJ, symmetric] using f .
+ have bij: "bij_betw ?f (space IJ.P) (space P.P)"
+ unfolding sigma_pair_algebra_sigma_eq
+ by (intro bij_inv_bij_betw) (rule bij_inv_restrict_merge[OF IJ])
have "IJ.positive_integral f = IJ.positive_integral (\<lambda>x. f (restrict x (I \<union> J)))"
by (auto intro!: IJ.positive_integral_cong arg_cong[where f=f] dest!: extensional_restrict)
also have "\<dots> = I.positive_integral (\<lambda>x. J.positive_integral (\<lambda>y. f (merge I x J y)))"
unfolding P.positive_integral_fst_measurable[OF P_borel, simplified]
- unfolding P.positive_integral_vimage[unfolded space_sigma, OF bij_betw_restrict_I_J[OF IJ]]
- unfolding product_product_vimage_algebra[OF IJ fin]
+ unfolding P.positive_integral_vimage[OF bij]
+ unfolding product_product_vimage_algebra[OF IJ]
apply simp
apply (rule IJ.positive_integral_cong_measure[symmetric])
apply (rule measure_fold)
@@ -1687,6 +1787,59 @@
qed simp
qed
+lemma (in product_sigma_finite) product_positive_integral_insert:
+ assumes [simp]: "finite I" "i \<notin> I"
+ and f: "f \<in> borel_measurable (sigma (product_algebra M (insert i I)))"
+ shows "product_positive_integral (insert i I) f
+ = product_positive_integral I (\<lambda>x. M.positive_integral i (\<lambda>y. f (x(i:=y))))"
+proof -
+ interpret I: finite_product_sigma_finite M \<mu> I by default auto
+ interpret i: finite_product_sigma_finite M \<mu> "{i}" by default auto
+ interpret P: pair_sigma_algebra I.P i.P ..
+ have IJ: "I \<inter> {i} = {}" by auto
+ show ?thesis
+ unfolding product_positive_integral_fold[OF IJ, simplified, OF f]
+ proof (rule I.positive_integral_cong, subst product_positive_integral_singleton)
+ fix x assume x: "x \<in> space I.P"
+ let "?f y" = "f (restrict (x(i := y)) (insert i I))"
+ have f'_eq: "\<And>y. ?f y = f (x(i := y))"
+ using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def)
+ note fP = f[unfolded measurable_merge_iff[OF IJ, simplified]]
+ show "?f \<in> borel_measurable (M i)"
+ using P.measurable_pair_image_snd[OF fP x]
+ unfolding measurable_singleton f'_eq by (simp add: f'_eq)
+ show "M.positive_integral i ?f = M.positive_integral i (\<lambda>y. f (x(i := y)))"
+ unfolding f'_eq by simp
+ qed
+qed
+
+lemma (in product_sigma_finite) product_positive_integral_setprod:
+ fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> pextreal"
+ assumes "finite I" and borel: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
+ shows "product_positive_integral I (\<lambda>x. (\<Prod>i\<in>I. f i (x i))) =
+ (\<Prod>i\<in>I. M.positive_integral i (f i))"
+using assms proof induct
+ case empty
+ interpret finite_product_sigma_finite M \<mu> "{}" by default auto
+ then show ?case by simp
+next
+ case (insert i I)
+ note `finite I`[intro, simp]
+ interpret I: finite_product_sigma_finite M \<mu> I by default auto
+ have *: "\<And>x y. (\<Prod>j\<in>I. f j (if j = i then y else x j)) = (\<Prod>j\<in>I. f j (x j))"
+ using insert by (auto intro!: setprod_cong)
+ have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow>
+ (\<lambda>x. (\<Prod>i\<in>J. f i (x i))) \<in> borel_measurable (sigma (product_algebra M J))"
+ using sets_into_space insert
+ by (intro sigma_algebra.borel_measurable_pextreal_setprod
+ sigma_algebra_sigma product_algebra_sets_into_space
+ measurable_component)
+ auto
+ show ?case
+ by (simp add: product_positive_integral_insert[OF insert(1,2) prod])
+ (simp add: insert I.positive_integral_cmult M.positive_integral_multc * prod subset_insertI)
+qed
+
lemma (in product_sigma_finite) product_integral_singleton:
assumes f: "f \<in> borel_measurable (M i)"
shows "product_integral {i} (\<lambda>x. f (x i)) = M.integral i f"
@@ -1700,45 +1853,6 @@
unfolding *[THEN product_positive_integral_singleton] ..
qed
-lemma (in product_sigma_finite) borel_measurable_merge_iff:
- assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
- shows "f \<in> measurable (sigma (pair_algebra
- (sigma (product_algebra M I)) (sigma (product_algebra M J)))) M' \<longleftrightarrow>
- (\<lambda>x. f (restrict x I, restrict x J)) \<in> measurable (sigma (product_algebra M (I \<union> J))) M'"
-proof -
- interpret I: finite_product_sigma_finite M \<mu> I by default fact
- interpret J: finite_product_sigma_finite M \<mu> J by default fact
- have "finite (I \<union> J)" using fin by auto
- interpret IJ: finite_product_sigma_finite M \<mu> "I \<union> J" by default fact
- interpret P: pair_sigma_finite I.P I.measure J.P J.measure by default
- let ?f = "\<lambda>x. (restrict x I, restrict x J)"
- let ?S = "space (product_algebra M (I \<union> J))"
- { fix p assume p: "p \<in> space (pair_algebra I.P J.P)"
- have "?f (the_inv_into ?S ?f p) = p"
- proof (intro f_the_inv_into_f[where f="?f"] inj_onI ext)
- fix x y t assume "x \<in> ?S" "y \<in> ?S" "?f x = ?f y"
- show "x t = y t"
- proof cases
- assume "t \<in> I \<union> J" then show ?thesis using `?f x = ?f y`
- by (auto simp: restrict_def fun_eq_iff split: split_if_asm)
- next
- assume "t \<notin> I \<union> J" then show ?thesis
- using `x \<in> ?S` `y \<in> ?S` by (auto simp: space_pair_algebra extensional_def)
- qed
- next
- show "p \<in> ?f ` ?S" using p
- by (intro image_eqI[of _ _ "merge I (fst p) J (snd p)"])
- (auto simp: space_pair_algebra extensional_restrict)
- qed }
- note restrict = this
- show ?thesis
- apply (subst product_product_vimage_algebra[OF assms, symmetric])
- apply (subst P.measurable_vimage_iff_inv)
- using bij_betw_restrict_I_J[OF IJ, of M] apply simp
- apply (rule measurable_cong)
- by (auto simp del: space_product_algebra simp: restrict)
-qed
-
lemma (in product_sigma_finite) product_integral_fold:
assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
and f: "measure_space.integrable (sigma (product_algebra M (I \<union> J))) (product_measure (I \<union> J)) f"
@@ -1761,7 +1875,7 @@
then have f'_borel:
"(\<lambda>x. Real (?f x)) \<in> borel_measurable P.P"
"(\<lambda>x. Real (- ?f x)) \<in> borel_measurable P.P"
- unfolding borel_measurable_merge_iff[OF IJ fin]
+ unfolding measurable_restrict_iff[OF IJ]
by simp_all
have PI:
"P.positive_integral (\<lambda>x. Real (?f x)) = IJ.positive_integral (\<lambda>x. Real (f x))"
@@ -1771,7 +1885,7 @@
by simp_all
have "P.integrable ?f" using `IJ.integrable f`
unfolding P.integrable_def IJ.integrable_def
- unfolding borel_measurable_merge_iff[OF IJ fin]
+ unfolding measurable_restrict_iff[OF IJ]
using f_restrict PI by simp_all
show ?thesis
unfolding P.integrable_fst_measurable(2)[OF `P.integrable ?f`, simplified]
@@ -1779,6 +1893,84 @@
unfolding PI by simp
qed
+lemma (in product_sigma_finite) product_integral_insert:
+ assumes [simp]: "finite I" "i \<notin> I"
+ and f: "measure_space.integrable (sigma (product_algebra M (insert i I))) (product_measure (insert i I)) f"
+ shows "product_integral (insert i I) f
+ = product_integral I (\<lambda>x. M.integral i (\<lambda>y. f (x(i:=y))))"
+proof -
+ interpret I: finite_product_sigma_finite M \<mu> I by default auto
+ interpret I': finite_product_sigma_finite M \<mu> "insert i I" by default auto
+ interpret i: finite_product_sigma_finite M \<mu> "{i}" by default auto
+ interpret P: pair_sigma_algebra I.P i.P ..
+ have IJ: "I \<inter> {i} = {}" by auto
+ show ?thesis
+ unfolding product_integral_fold[OF IJ, simplified, OF f]
+ proof (rule I.integral_cong, subst product_integral_singleton)
+ fix x assume x: "x \<in> space I.P"
+ let "?f y" = "f (restrict (x(i := y)) (insert i I))"
+ have f'_eq: "\<And>y. ?f y = f (x(i := y))"
+ using x by (auto intro!: arg_cong[where f=f] simp: fun_eq_iff extensional_def)
+ have "f \<in> borel_measurable I'.P" using f unfolding I'.integrable_def by auto
+ note fP = this[unfolded measurable_merge_iff[OF IJ, simplified]]
+ show "?f \<in> borel_measurable (M i)"
+ using P.measurable_pair_image_snd[OF fP x]
+ unfolding measurable_singleton f'_eq by (simp add: f'_eq)
+ show "M.integral i ?f = M.integral i (\<lambda>y. f (x(i := y)))"
+ unfolding f'_eq by simp
+ qed
+qed
+
+lemma (in product_sigma_finite) product_integrable_setprod:
+ fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> real"
+ assumes [simp]: "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> M.integrable i (f i)"
+ shows "product_integrable I (\<lambda>x. (\<Prod>i\<in>I. f i (x i)))" (is "product_integrable I ?f")
+proof -
+ interpret finite_product_sigma_finite M \<mu> I by default fact
+ have f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
+ using integrable unfolding M.integrable_def by auto
+ then have borel: "?f \<in> borel_measurable P"
+ by (intro borel_measurable_setprod measurable_component) auto
+ moreover have "integrable (\<lambda>x. \<bar>\<Prod>i\<in>I. f i (x i)\<bar>)"
+ proof (unfold integrable_def, intro conjI)
+ show "(\<lambda>x. abs (?f x)) \<in> borel_measurable P"
+ using borel by auto
+ have "positive_integral (\<lambda>x. Real (abs (?f x))) =
+ positive_integral (\<lambda>x. \<Prod>i\<in>I. Real (abs (f i (x i))))"
+ by (simp add: Real_setprod abs_setprod)
+ also have "\<dots> = (\<Prod>i\<in>I. M.positive_integral i (\<lambda>x. Real (abs (f i x))))"
+ using f by (subst product_positive_integral_setprod) auto
+ also have "\<dots> < \<omega>"
+ using integrable[THEN M.integrable_abs]
+ unfolding pextreal_less_\<omega> setprod_\<omega> M.integrable_def by simp
+ finally show "positive_integral (\<lambda>x. Real (abs (?f x))) \<noteq> \<omega>" by auto
+ show "positive_integral (\<lambda>x. Real (- abs (?f x))) \<noteq> \<omega>" by simp
+ qed
+ ultimately show ?thesis
+ by (rule integrable_abs_iff[THEN iffD1])
+qed
+
+lemma (in product_sigma_finite) product_integral_setprod:
+ fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> real"
+ assumes "finite I" "I \<noteq> {}" and integrable: "\<And>i. i \<in> I \<Longrightarrow> M.integrable i (f i)"
+ shows "product_integral I (\<lambda>x. (\<Prod>i\<in>I. f i (x i))) = (\<Prod>i\<in>I. M.integral i (f i))"
+using assms proof (induct rule: finite_ne_induct)
+ case (singleton i)
+ then show ?case by (simp add: product_integral_singleton integrable_def)
+next
+ case (insert i I)
+ then have iI: "finite (insert i I)" by auto
+ then have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow>
+ product_integrable J (\<lambda>x. (\<Prod>i\<in>J. f i (x i)))"
+ by (intro product_integrable_setprod insert(5)) (auto intro: finite_subset)
+ interpret I: finite_product_sigma_finite M \<mu> I by default fact
+ have *: "\<And>x y. (\<Prod>j\<in>I. f j (if j = i then y else x j)) = (\<Prod>j\<in>I. f j (x j))"
+ using `i \<notin> I` by (auto intro!: setprod_cong)
+ show ?case
+ unfolding product_integral_insert[OF insert(1,3) prod[OF subset_refl]]
+ by (simp add: * insert integral_multc I.integral_cmult[OF prod] subset_insertI)
+qed
+
section "Products on finite spaces"
lemma sigma_sets_pair_algebra_finite:
--- a/src/HOL/Probability/Radon_Nikodym.thy Thu Dec 09 17:25:43 2010 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy Thu Dec 09 17:26:08 2010 +0100
@@ -323,9 +323,10 @@
{ fix f g assume "f \<up> g" and f: "\<And>i. f i \<in> G"
have "g \<in> G" unfolding G_def
proof safe
- from `f \<up> g` have [simp]: "g = (SUP i. f i)" unfolding isoton_def by simp
+ from `f \<up> g` have [simp]: "g = (\<lambda>x. SUP i. f i x)"
+ unfolding isoton_def fun_eq_iff SUPR_apply by simp
have f_borel: "\<And>i. f i \<in> borel_measurable M" using f unfolding G_def by simp
- thus "g \<in> borel_measurable M" by (auto intro!: borel_measurable_SUP)
+ thus "g \<in> borel_measurable M" by auto
fix A assume "A \<in> sets M"
hence "\<And>i. (\<lambda>x. f i x * indicator A x) \<in> borel_measurable M"
using f_borel by (auto intro!: borel_measurable_indicator)
@@ -1103,42 +1104,36 @@
unfolding eq[OF A, symmetric] RN_deriv(2)[OF \<nu> A, symmetric] ..
qed
-lemma the_inv_into_in:
- assumes "inj_on f A" and x: "x \<in> f`A"
- shows "the_inv_into A f x \<in> A"
- using assms by (auto simp: the_inv_into_f_f)
-
lemma (in sigma_finite_measure) RN_deriv_vimage:
fixes f :: "'b \<Rightarrow> 'a"
- assumes f: "bij_betw f S (space M)"
+ assumes f: "bij_inv S (space M) f g"
assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
shows "AE x.
- sigma_finite_measure.RN_deriv (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>A. \<nu> (f ` A)) (the_inv_into S f x) = RN_deriv \<nu> x"
+ sigma_finite_measure.RN_deriv (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>A. \<nu> (f ` A)) (g x) = RN_deriv \<nu> x"
proof (rule RN_deriv_unique[OF \<nu>])
interpret sf: sigma_finite_measure "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
- using f by (rule sigma_finite_measure_isomorphic)
+ using f by (rule sigma_finite_measure_isomorphic[OF bij_inv_bij_betw(1)])
interpret \<nu>: measure_space M \<nu> using \<nu>(1) .
have \<nu>': "measure_space (vimage_algebra S f) (\<lambda>A. \<nu> (f ` A))"
- using f by (rule \<nu>.measure_space_isomorphic)
+ using f by (rule \<nu>.measure_space_isomorphic[OF bij_inv_bij_betw(1)])
{ fix A assume "A \<in> sets M" then have "f ` (f -` A \<inter> S) = A"
- using sets_into_space f[unfolded bij_betw_def]
+ using sets_into_space f[THEN bij_inv_bij_betw(1), unfolded bij_betw_def]
by (intro image_vimage_inter_eq[where T="space M"]) auto }
note A_f = this
then have ac: "sf.absolutely_continuous (\<lambda>A. \<nu> (f ` A))"
using \<nu>(2) by (auto simp: sf.absolutely_continuous_def absolutely_continuous_def)
- show "(\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (the_inv_into S f x)) \<in> borel_measurable M"
+ show "(\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x)) \<in> borel_measurable M"
using sf.RN_deriv(1)[OF \<nu>' ac]
unfolding measurable_vimage_iff_inv[OF f] comp_def .
fix A assume "A \<in> sets M"
- then have *: "\<And>x. x \<in> space M \<Longrightarrow> indicator (f -` A \<inter> S) (the_inv_into S f x) = (indicator A x :: pextreal)"
- using f[unfolded bij_betw_def]
- unfolding indicator_def by (auto simp: f_the_inv_into_f the_inv_into_in)
+ then have *: "\<And>x. x \<in> space M \<Longrightarrow> indicator (f -` A \<inter> S) (g x) = (indicator A x :: pextreal)"
+ using f by (auto simp: bij_inv_def indicator_def)
have "\<nu> (f ` (f -` A \<inter> S)) = sf.positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) x * indicator (f -` A \<inter> S) x)"
using `A \<in> sets M` by (force intro!: sf.RN_deriv(2)[OF \<nu>' ac])
- also have "\<dots> = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (the_inv_into S f x) * indicator A x)"
+ also have "\<dots> = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
unfolding positive_integral_vimage_inv[OF f]
by (simp add: * cong: positive_integral_cong)
- finally show "\<nu> A = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (the_inv_into S f x) * indicator A x)"
+ finally show "\<nu> A = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
unfolding A_f[OF `A \<in> sets M`] .
qed
--- a/src/HOL/Probability/Sigma_Algebra.thy Thu Dec 09 17:25:43 2010 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy Thu Dec 09 17:26:08 2010 +0100
@@ -806,13 +806,6 @@
(simp_all add: f_the_inv_into_f cong: measurable_cong)
qed
-lemma (in sigma_algebra) measurable_vimage_iff_inv:
- fixes f :: "'b \<Rightarrow> 'a" assumes f: "bij_betw f S (space M)"
- shows "g \<in> measurable (vimage_algebra S f) M' \<longleftrightarrow> (g \<circ> the_inv_into S f) \<in> measurable M M'"
- unfolding measurable_vimage_iff[OF f]
- using f[unfolded bij_betw_def]
- by (auto intro!: measurable_cong simp add: the_inv_into_f_f)
-
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"
@@ -871,22 +864,6 @@
qed
qed
-lemma vimage_algebra_sigma:
- assumes E: "sets E \<subseteq> Pow (space E)"
- and f: "f \<in> space F \<rightarrow> space E"
- and "\<And>A. A \<in> sets F \<Longrightarrow> A \<in> (\<lambda>X. f -` X \<inter> space F) ` sets E"
- and "\<And>A. A \<in> sets E \<Longrightarrow> f -` A \<inter> space F \<in> sets F"
- shows "sigma_algebra.vimage_algebra (sigma E) (space 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"
- using assms by auto
- show "vimage_algebra (space F) f = sigma F"
- unfolding vimage_algebra_def using assms
- by (simp add: sigma_def eq sigma_sets_vimage)
-qed
-
section {* Conditional space *}
definition (in algebra)
@@ -1420,6 +1397,8 @@
using E by simp
qed
+subsection "Sigma algebras on finite sets"
+
locale finite_sigma_algebra = sigma_algebra +
assumes finite_space: "finite (space M)"
and sets_eq_Pow[simp]: "sets M = Pow (space M)"
@@ -1438,4 +1417,92 @@
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 "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