--- a/src/HOL/Probability/Binary_Product_Measure.thy Wed Jun 15 22:19:03 2016 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Thu Jun 16 23:03:27 2016 +0200
@@ -37,12 +37,6 @@
unfolding pair_measure_def using pair_measure_closed[of A B]
by (rule sets_measure_of)
-lemma sets_pair_in_sets:
- assumes N: "space A \<times> space B = space N"
- assumes "\<And>a b. a \<in> sets A \<Longrightarrow> b \<in> sets B \<Longrightarrow> a \<times> b \<in> sets N"
- shows "sets (A \<Otimes>\<^sub>M B) \<subseteq> sets N"
- using assms by (auto intro!: sets.sigma_sets_subset simp: sets_pair_measure N)
-
lemma sets_pair_measure_cong[measurable_cong, cong]:
"sets M1 = sets M1' \<Longrightarrow> sets M2 = sets M2' \<Longrightarrow> sets (M1 \<Otimes>\<^sub>M M2) = sets (M1' \<Otimes>\<^sub>M M2')"
unfolding sets_pair_measure by (simp cong: sets_eq_imp_space_eq)
@@ -122,23 +116,45 @@
and measurable_snd'': "(\<lambda>x. f (snd x)) \<in> measurable (P \<Otimes>\<^sub>M M) N"
by simp_all
+lemma sets_pair_in_sets:
+ assumes "\<And>a b. a \<in> sets A \<Longrightarrow> b \<in> sets B \<Longrightarrow> a \<times> b \<in> sets N"
+ shows "sets (A \<Otimes>\<^sub>M B) \<subseteq> sets N"
+ unfolding sets_pair_measure
+ by (intro sets.sigma_sets_subset') (auto intro!: assms)
+
lemma sets_pair_eq_sets_fst_snd:
- "sets (A \<Otimes>\<^sub>M B) = sets (Sup_sigma {vimage_algebra (space A \<times> space B) fst A, vimage_algebra (space A \<times> space B) snd B})"
- (is "?P = sets (Sup_sigma {?fst, ?snd})")
+ "sets (A \<Otimes>\<^sub>M B) = sets (Sup {vimage_algebra (space A \<times> space B) fst A, vimage_algebra (space A \<times> space B) snd B})"
+ (is "?P = sets (Sup {?fst, ?snd})")
proof -
{ fix a b assume ab: "a \<in> sets A" "b \<in> sets B"
then have "a \<times> b = (fst -` a \<inter> (space A \<times> space B)) \<inter> (snd -` b \<inter> (space A \<times> space B))"
by (auto dest: sets.sets_into_space)
- also have "\<dots> \<in> sets (Sup_sigma {?fst, ?snd})"
- using ab by (auto intro: in_Sup_sigma in_vimage_algebra)
- finally have "a \<times> b \<in> sets (Sup_sigma {?fst, ?snd})" . }
+ also have "\<dots> \<in> sets (Sup {?fst, ?snd})"
+ apply (rule sets.Int)
+ apply (rule in_sets_Sup)
+ apply auto []
+ apply (rule insertI1)
+ apply (auto intro: ab in_vimage_algebra) []
+ apply (rule in_sets_Sup)
+ apply auto []
+ apply (rule insertI2)
+ apply (auto intro: ab in_vimage_algebra)
+ done
+ finally have "a \<times> b \<in> sets (Sup {?fst, ?snd})" . }
moreover have "sets ?fst \<subseteq> sets (A \<Otimes>\<^sub>M B)"
by (rule sets_image_in_sets) (auto simp: space_pair_measure[symmetric])
moreover have "sets ?snd \<subseteq> sets (A \<Otimes>\<^sub>M B)"
by (rule sets_image_in_sets) (auto simp: space_pair_measure)
ultimately show ?thesis
- by (intro antisym[of "sets A" for A] sets_Sup_in_sets sets_pair_in_sets )
- (auto simp add: space_Sup_sigma space_pair_measure)
+ apply (intro antisym[of "sets A" for A] sets_Sup_in_sets sets_pair_in_sets)
+ apply simp
+ apply simp
+ apply simp
+ apply (elim disjE)
+ apply (simp add: space_pair_measure)
+ apply (simp add: space_pair_measure)
+ apply (auto simp add: space_pair_measure)
+ done
qed
lemma measurable_pair_iff:
@@ -597,11 +613,10 @@
have [simp]: "snd \<in> X \<times> Y \<rightarrow> Y" "fst \<in> X \<times> Y \<rightarrow> X"
by auto
let ?XY = "{{fst -` a \<inter> X \<times> Y | a. a \<in> A}, {snd -` b \<inter> X \<times> Y | b. b \<in> B}}"
- have "sets ?P =
- sets (\<Squnion>\<^sub>\<sigma> xy\<in>?XY. sigma (X \<times> Y) xy)"
+ have "sets ?P = sets (SUP xy:?XY. sigma (X \<times> Y) xy)"
by (simp add: vimage_algebra_sigma sets_pair_eq_sets_fst_snd A B)
also have "\<dots> = sets (sigma (X \<times> Y) (\<Union>?XY))"
- by (intro Sup_sigma_sigma arg_cong[where f=sets]) auto
+ by (intro Sup_sigma arg_cong[where f=sets]) auto
also have "\<dots> = sets ?S"
proof (intro arg_cong[where f=sets] sigma_eqI sigma_sets_eqI)
show "\<Union>?XY \<subseteq> Pow (X \<times> Y)" "{a \<times> b |a b. a \<in> A \<and> b \<in> B} \<subseteq> Pow (X \<times> Y)"
--- a/src/HOL/Probability/Embed_Measure.thy Wed Jun 15 22:19:03 2016 +0200
+++ b/src/HOL/Probability/Embed_Measure.thy Thu Jun 16 23:03:27 2016 +0200
@@ -241,20 +241,25 @@
have fg[simp]: "\<And>A. inj_on (map_prod f g) A" "\<And>A. inj_on f A" "\<And>A. inj_on g A"
using f g by (auto simp: inj_on_def)
+ note complete_lattice_class.Sup_insert[simp del] ccSup_insert[simp del] SUP_insert[simp del]
+ ccSUP_insert[simp del]
show sets: "sets ?L = sets (embed_measure (M \<Otimes>\<^sub>M N) (map_prod f g))"
unfolding map_prod_def[symmetric]
apply (simp add: sets_pair_eq_sets_fst_snd sets_embed_eq_vimage_algebra
cong: vimage_algebra_cong)
- apply (subst vimage_algebra_Sup_sigma)
+ apply (subst sets_vimage_Sup_eq[where Y="space (M \<Otimes>\<^sub>M N)"])
apply (simp_all add: space_pair_measure[symmetric])
apply (auto simp add: the_inv_into_f_f
simp del: map_prod_simp
del: prod_fun_imageE) []
+ apply auto []
+ apply (subst image_insert)
+ apply simp
apply (subst (1 2 3 4 ) vimage_algebra_vimage_algebra_eq)
apply (simp_all add: the_inv_into_in_Pi Pi_iff[of snd] Pi_iff[of fst] space_pair_measure)
apply (simp_all add: Pi_iff[of snd] Pi_iff[of fst] the_inv_into_in_Pi vimage_algebra_vimage_algebra_eq
space_pair_measure[symmetric] map_prod_image[symmetric])
- apply (intro arg_cong[where f=sets] arg_cong[where f=Sup_sigma] arg_cong2[where f=insert] vimage_algebra_cong)
+ apply (intro arg_cong[where f=sets] arg_cong[where f=Sup] arg_cong2[where f=insert] vimage_algebra_cong)
apply (auto simp: map_prod_image the_inv_into_f_f
simp del: map_prod_simp del: prod_fun_imageE)
apply (simp_all add: the_inv_into_f_f space_pair_measure)
@@ -270,6 +275,19 @@
sigma_finite_measure.emeasure_pair_measure_Times)
qed (insert assms, simp_all add: sigma_finite_embed_measure)
+lemma mono_embed_measure:
+ "space M = space M' \<Longrightarrow> sets M \<subseteq> sets M' \<Longrightarrow> sets (embed_measure M f) \<subseteq> sets (embed_measure M' f)"
+ unfolding embed_measure_def
+ apply (subst (1 2) sets_measure_of)
+ apply (blast dest: sets.sets_into_space)
+ apply (blast dest: sets.sets_into_space)
+ apply simp
+ apply (intro sigma_sets_mono')
+ apply safe
+ apply (simp add: subset_eq)
+ apply metis
+ done
+
lemma density_embed_measure:
assumes inj: "inj f" and Mg[measurable]: "g \<in> borel_measurable (embed_measure M f)"
shows "density (embed_measure M f) g = embed_measure (density M (g \<circ> f)) f" (is "?M1 = ?M2")
--- a/src/HOL/Probability/Finite_Product_Measure.thy Wed Jun 15 22:19:03 2016 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Thu Jun 16 23:03:27 2016 +0200
@@ -389,8 +389,12 @@
qed
lemma sets_PiM_eq_proj:
- "I \<noteq> {} \<Longrightarrow> sets (PiM I M) = sets (\<Squnion>\<^sub>\<sigma> i\<in>I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. space (M i)) (\<lambda>x. x i) (M i))"
- apply (simp add: sets_PiM_single sets_Sup_sigma)
+ "I \<noteq> {} \<Longrightarrow> sets (PiM I M) = sets (SUP i:I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. space (M i)) (\<lambda>x. x i) (M i))"
+ apply (simp add: sets_PiM_single)
+ apply (subst sets_Sup_eq[where X="\<Pi>\<^sub>E i\<in>I. space (M i)"])
+ apply auto []
+ apply auto []
+ apply simp
apply (subst SUP_cong[OF refl])
apply (rule sets_vimage_algebra2)
apply auto []
@@ -418,10 +422,10 @@
let ?F = "\<lambda>i. {(\<lambda>x. x i) -` A \<inter> Pi\<^sub>E I \<Omega> |A. A \<in> E i}"
assume "I \<noteq> {}"
then have "sets (Pi\<^sub>M I (\<lambda>i. sigma (\<Omega> i) (E i))) =
- sets (\<Squnion>\<^sub>\<sigma> i\<in>I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. \<Omega> i) (\<lambda>x. x i) (sigma (\<Omega> i) (E i)))"
+ sets (SUP i:I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. \<Omega> i) (\<lambda>x. x i) (sigma (\<Omega> i) (E i)))"
by (subst sets_PiM_eq_proj) (auto simp: space_measure_of_conv)
- also have "\<dots> = sets (\<Squnion>\<^sub>\<sigma> i\<in>I. sigma (Pi\<^sub>E I \<Omega>) (?F i))"
- using E by (intro SUP_sigma_cong arg_cong[where f=sets] vimage_algebra_sigma) auto
+ also have "\<dots> = sets (SUP i:I. sigma (Pi\<^sub>E I \<Omega>) (?F i))"
+ using E by (intro sets_SUP_cong arg_cong[where f=sets] vimage_algebra_sigma) auto
also have "\<dots> = sets (sigma (Pi\<^sub>E I \<Omega>) (\<Union>i\<in>I. ?F i))"
using \<open>I \<noteq> {}\<close> by (intro arg_cong[where f=sets] SUP_sigma_sigma) auto
also have "\<dots> = sets (sigma (Pi\<^sub>E I \<Omega>) P)"
--- a/src/HOL/Probability/Giry_Monad.thy Wed Jun 15 22:19:03 2016 +0200
+++ b/src/HOL/Probability/Giry_Monad.thy Thu Jun 16 23:03:27 2016 +0200
@@ -162,17 +162,17 @@
definition subprob_algebra :: "'a measure \<Rightarrow> 'a measure measure" where
"subprob_algebra K =
- (\<Squnion>\<^sub>\<sigma> A\<in>sets K. vimage_algebra {M. subprob_space M \<and> sets M = sets K} (\<lambda>M. emeasure M A) borel)"
+ (SUP A : sets K. vimage_algebra {M. subprob_space M \<and> sets M = sets K} (\<lambda>M. emeasure M A) borel)"
lemma space_subprob_algebra: "space (subprob_algebra A) = {M. subprob_space M \<and> sets M = sets A}"
- by (auto simp add: subprob_algebra_def space_Sup_sigma)
+ by (auto simp add: subprob_algebra_def space_Sup_eq_UN)
lemma subprob_algebra_cong: "sets M = sets N \<Longrightarrow> subprob_algebra M = subprob_algebra N"
by (simp add: subprob_algebra_def)
lemma measurable_emeasure_subprob_algebra[measurable]:
"a \<in> sets A \<Longrightarrow> (\<lambda>M. emeasure M a) \<in> borel_measurable (subprob_algebra A)"
- by (auto intro!: measurable_Sup_sigma1 measurable_vimage_algebra1 simp: subprob_algebra_def)
+ by (auto intro!: measurable_Sup1 measurable_vimage_algebra1 simp: subprob_algebra_def)
lemma measurable_measure_subprob_algebra[measurable]:
"a \<in> sets A \<Longrightarrow> (\<lambda>M. measure M a) \<in> borel_measurable (subprob_algebra A)"
@@ -227,7 +227,7 @@
(\<And>a. a \<in> space M \<Longrightarrow> sets (K a) = sets N) \<Longrightarrow>
(\<And>A. A \<in> sets N \<Longrightarrow> (\<lambda>a. emeasure (K a) A) \<in> borel_measurable M) \<Longrightarrow>
K \<in> measurable M (subprob_algebra N)"
- by (auto intro!: measurable_Sup_sigma2 measurable_vimage_algebra2 simp: subprob_algebra_def)
+ by (auto intro!: measurable_Sup2 measurable_vimage_algebra2 simp: subprob_algebra_def)
lemma measurable_submarkov:
"K \<in> measurable M (subprob_algebra M) \<longleftrightarrow>
@@ -1504,55 +1504,6 @@
finally show ?thesis .
qed
-section \<open>Measures form a $\omega$-chain complete partial order\<close>
-
-definition SUP_measure :: "(nat \<Rightarrow> 'a measure) \<Rightarrow> 'a measure" where
- "SUP_measure M = measure_of (\<Union>i. space (M i)) (\<Union>i. sets (M i)) (\<lambda>A. SUP i. emeasure (M i) A)"
-
-lemma
- assumes const: "\<And>i j. sets (M i) = sets (M j)"
- shows space_SUP_measure: "space (SUP_measure M) = space (M i)" (is ?sp)
- and sets_SUP_measure: "sets (SUP_measure M) = sets (M i)" (is ?st)
-proof -
- have "(\<Union>i. sets (M i)) = sets (M i)"
- using const by auto
- moreover have "(\<Union>i. space (M i)) = space (M i)"
- using const[THEN sets_eq_imp_space_eq] by auto
- moreover have "\<And>i. sets (M i) \<subseteq> Pow (space (M i))"
- by (auto dest: sets.sets_into_space)
- ultimately show ?sp ?st
- by (simp_all add: SUP_measure_def)
-qed
-
-lemma emeasure_SUP_measure:
- assumes const: "\<And>i j. sets (M i) = sets (M j)"
- and mono: "mono (\<lambda>i. emeasure (M i))"
- shows "emeasure (SUP_measure M) A = (SUP i. emeasure (M i) A)"
-proof cases
- assume "A \<in> sets (SUP_measure M)"
- show ?thesis
- proof (rule emeasure_measure_of[OF SUP_measure_def])
- show "countably_additive (sets (SUP_measure M)) (\<lambda>A. SUP i. emeasure (M i) A)"
- proof (rule countably_additiveI)
- fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets (SUP_measure M)"
- then have "\<And>i j. A i \<in> sets (M j)"
- using sets_SUP_measure[of M, OF const] by simp
- moreover assume "disjoint_family A"
- ultimately show "(\<Sum>i. SUP ia. emeasure (M ia) (A i)) = (SUP i. emeasure (M i) (\<Union>i. A i))"
- using suminf_SUP_eq
- using mono by (subst ennreal_suminf_SUP_eq) (auto simp: mono_def le_fun_def intro!: SUP_cong suminf_emeasure)
- qed
- show "positive (sets (SUP_measure M)) (\<lambda>A. SUP i. emeasure (M i) A)"
- by (auto simp: positive_def intro: SUP_upper2)
- show "(\<Union>i. sets (M i)) \<subseteq> Pow (\<Union>i. space (M i))"
- using sets.sets_into_space by auto
- qed fact
-next
- assume "A \<notin> sets (SUP_measure M)"
- with sets_SUP_measure[of M, OF const] show ?thesis
- by (simp add: emeasure_notin_sets)
-qed
-
lemma bind_return'': "sets M = sets N \<Longrightarrow> M \<bind> return N = M"
by (cases "space M = {}")
(simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return'
--- a/src/HOL/Probability/Measurable.thy Wed Jun 15 22:19:03 2016 +0200
+++ b/src/HOL/Probability/Measurable.thy Thu Jun 16 23:03:27 2016 +0200
@@ -266,7 +266,7 @@
unfolding finite_nat_set_iff_bounded by (simp add: Ball_def)
lemma measurable_Least[measurable]:
- assumes [measurable]: "(\<And>i::nat. (\<lambda>x. P i x) \<in> measurable M (count_space UNIV))"q
+ assumes [measurable]: "(\<And>i::nat. (\<lambda>x. P i x) \<in> measurable M (count_space UNIV))"
shows "(\<lambda>x. LEAST i. P i x) \<in> measurable M (count_space UNIV)"
unfolding measurable_def by (safe intro!: sets_Least) simp_all
--- a/src/HOL/Probability/Measure_Space.thy Wed Jun 15 22:19:03 2016 +0200
+++ b/src/HOL/Probability/Measure_Space.thy Thu Jun 16 23:03:27 2016 +0200
@@ -26,7 +26,7 @@
proof (rule SUP_eqI)
fix y :: ennreal assume "\<And>n. n \<in> UNIV \<Longrightarrow> (if i < n then f i else 0) \<le> y"
from this[of "Suc i"] show "f i \<le> y" by auto
- qed (insert assms, simp add: zero_le)
+ qed (insert assms, simp)
ultimately show ?thesis using assms
by (subst suminf_eq_SUP) (auto simp: indicator_def)
qed
@@ -325,7 +325,7 @@
by (auto simp: UN_disjointed_eq disjoint_family_disjointed)
moreover have "(\<lambda>n. (\<Sum>i<n. f (disjointed A i))) \<longlonglongrightarrow> (\<Sum>i. f (disjointed A i))"
using f(1)[unfolded positive_def] dA
- by (auto intro!: summable_LIMSEQ summableI)
+ by (auto intro!: summable_LIMSEQ)
from LIMSEQ_Suc[OF this]
have "(\<lambda>n. (\<Sum>i\<le>n. f (disjointed A i))) \<longlonglongrightarrow> (\<Sum>i. f (disjointed A i))"
unfolding lessThan_Suc_atMost .
@@ -1395,7 +1395,7 @@
qed (auto dest: sets.sets_into_space)
lemma measure_nonneg[simp]: "0 \<le> measure M A"
- unfolding measure_def by (auto simp: enn2real_nonneg)
+ unfolding measure_def by auto
lemma zero_less_measure_iff: "0 < measure M A \<longleftrightarrow> measure M A \<noteq> 0"
using measure_nonneg[of M A] by (auto simp add: le_less)
@@ -1418,13 +1418,13 @@
by (cases "A \<in> M") (auto simp: measure_notin_sets emeasure_notin_sets)
lemma enn2real_plus:"a < top \<Longrightarrow> b < top \<Longrightarrow> enn2real (a + b) = enn2real a + enn2real b"
- by (simp add: enn2real_def plus_ennreal.rep_eq real_of_ereal_add enn2ereal_nonneg less_top
+ by (simp add: enn2real_def plus_ennreal.rep_eq real_of_ereal_add less_top
del: real_of_ereal_enn2ereal)
lemma measure_Union:
"emeasure M A \<noteq> \<infinity> \<Longrightarrow> emeasure M B \<noteq> \<infinity> \<Longrightarrow> A \<in> sets M \<Longrightarrow> B \<in> sets M \<Longrightarrow> A \<inter> B = {} \<Longrightarrow>
measure M (A \<union> B) = measure M A + measure M B"
- by (simp add: measure_def enn2ereal_nonneg plus_emeasure[symmetric] enn2real_plus less_top)
+ by (simp add: measure_def plus_emeasure[symmetric] enn2real_plus less_top)
lemma disjoint_family_on_insert:
"i \<notin> I \<Longrightarrow> disjoint_family_on A (insert i I) \<longleftrightarrow> A i \<inter> (\<Union>i\<in>I. A i) = {} \<and> disjoint_family_on A I"
@@ -1462,8 +1462,7 @@
then have "emeasure M (A i) = ennreal ((measure M (A i)))"
using finite by (intro emeasure_eq_ennreal_measure) (auto simp: top_unique) }
ultimately show ?thesis using finite
- by (subst (asm) (2) emeasure_eq_ennreal_measure)
- (simp_all add: measure_nonneg)
+ by (subst (asm) (2) emeasure_eq_ennreal_measure) simp_all
qed
lemma measure_subadditive:
@@ -1494,7 +1493,7 @@
show ?thesis
using emeasure_subadditive_finite[OF A] fin
unfolding emeasure_eq_ennreal_measure[OF *]
- by (simp_all add: setsum_ennreal measure_nonneg setsum_nonneg emeasure_eq_ennreal_measure)
+ by (simp_all add: setsum_nonneg emeasure_eq_ennreal_measure)
qed
lemma measure_subadditive_countably:
@@ -2161,185 +2160,1124 @@
lemma scale_null_measure [simp]: "scale_measure r (null_measure M) = null_measure M"
by (rule measure_eqI) simp_all
-subsection \<open>Measures form a chain-complete partial order\<close>
+
+subsection \<open>Complete lattice structure on measures\<close>
+
+lemma (in finite_measure) finite_measure_Diff':
+ "A \<in> sets M \<Longrightarrow> B \<in> sets M \<Longrightarrow> measure M (A - B) = measure M A - measure M (A \<inter> B)"
+ using finite_measure_Diff[of A "A \<inter> B"] by (auto simp: Diff_Int)
+
+lemma (in finite_measure) finite_measure_Union':
+ "A \<in> sets M \<Longrightarrow> B \<in> sets M \<Longrightarrow> measure M (A \<union> B) = measure M A + measure M (B - A)"
+ using finite_measure_Union[of A "B - A"] by auto
+
+lemma finite_unsigned_Hahn_decomposition:
+ assumes "finite_measure M" "finite_measure N" and [simp]: "sets N = sets M"
+ shows "\<exists>Y\<in>sets M. (\<forall>X\<in>sets M. X \<subseteq> Y \<longrightarrow> N X \<le> M X) \<and> (\<forall>X\<in>sets M. X \<inter> Y = {} \<longrightarrow> M X \<le> N X)"
+proof -
+ interpret M: finite_measure M by fact
+ interpret N: finite_measure N by fact
+
+ define d where "d X = measure M X - measure N X" for X
+
+ have [intro]: "bdd_above (d`sets M)"
+ using sets.sets_into_space[of _ M]
+ by (intro bdd_aboveI[where M="measure M (space M)"])
+ (auto simp: d_def field_simps subset_eq intro!: add_increasing M.finite_measure_mono)
+
+ define \<gamma> where "\<gamma> = (SUP X:sets M. d X)"
+ have le_\<gamma>[intro]: "X \<in> sets M \<Longrightarrow> d X \<le> \<gamma>" for X
+ by (auto simp: \<gamma>_def intro!: cSUP_upper)
+
+ have "\<exists>f. \<forall>n. f n \<in> sets M \<and> d (f n) > \<gamma> - 1 / 2^n"
+ proof (intro choice_iff[THEN iffD1] allI)
+ fix n
+ have "\<exists>X\<in>sets M. \<gamma> - 1 / 2^n < d X"
+ unfolding \<gamma>_def by (intro less_cSUP_iff[THEN iffD1]) auto
+ then show "\<exists>y. y \<in> sets M \<and> \<gamma> - 1 / 2 ^ n < d y"
+ by auto
+ qed
+ then obtain E where [measurable]: "E n \<in> sets M" and E: "d (E n) > \<gamma> - 1 / 2^n" for n
+ by auto
+
+ define F where "F m n = (if m \<le> n then \<Inter>i\<in>{m..n}. E i else space M)" for m n
+
+ have [measurable]: "m \<le> n \<Longrightarrow> F m n \<in> sets M" for m n
+ by (auto simp: F_def)
+
+ have 1: "\<gamma> - 2 / 2 ^ m + 1 / 2 ^ n \<le> d (F m n)" if "m \<le> n" for m n
+ using that
+ proof (induct rule: dec_induct)
+ case base with E[of m] show ?case
+ by (simp add: F_def field_simps)
+ next
+ case (step i)
+ have F_Suc: "F m (Suc i) = F m i \<inter> E (Suc i)"
+ using \<open>m \<le> i\<close> by (auto simp: F_def le_Suc_eq)
+
+ have "\<gamma> + (\<gamma> - 2 / 2^m + 1 / 2 ^ Suc i) \<le> (\<gamma> - 1 / 2^Suc i) + (\<gamma> - 2 / 2^m + 1 / 2^i)"
+ by (simp add: field_simps)
+ also have "\<dots> \<le> d (E (Suc i)) + d (F m i)"
+ using E[of "Suc i"] by (intro add_mono step) auto
+ also have "\<dots> = d (E (Suc i)) + d (F m i - E (Suc i)) + d (F m (Suc i))"
+ using \<open>m \<le> i\<close> by (simp add: d_def field_simps F_Suc M.finite_measure_Diff' N.finite_measure_Diff')
+ also have "\<dots> = d (E (Suc i) \<union> F m i) + d (F m (Suc i))"
+ using \<open>m \<le> i\<close> by (simp add: d_def field_simps M.finite_measure_Union' N.finite_measure_Union')
+ also have "\<dots> \<le> \<gamma> + d (F m (Suc i))"
+ using \<open>m \<le> i\<close> by auto
+ finally show ?case
+ by auto
+ qed
+
+ define F' where "F' m = (\<Inter>i\<in>{m..}. E i)" for m
+ have F'_eq: "F' m = (\<Inter>i. F m (i + m))" for m
+ by (fastforce simp: le_iff_add[of m] F'_def F_def)
+
+ have [measurable]: "F' m \<in> sets M" for m
+ by (auto simp: F'_def)
+
+ have \<gamma>_le: "\<gamma> - 0 \<le> d (\<Union>m. F' m)"
+ proof (rule LIMSEQ_le)
+ show "(\<lambda>n. \<gamma> - 2 / 2 ^ n) \<longlonglongrightarrow> \<gamma> - 0"
+ by (intro tendsto_intros LIMSEQ_divide_realpow_zero) auto
+ have "incseq F'"
+ by (auto simp: incseq_def F'_def)
+ then show "(\<lambda>m. d (F' m)) \<longlonglongrightarrow> d (\<Union>m. F' m)"
+ unfolding d_def
+ by (intro tendsto_diff M.finite_Lim_measure_incseq N.finite_Lim_measure_incseq) auto
+
+ have "\<gamma> - 2 / 2 ^ m + 0 \<le> d (F' m)" for m
+ proof (rule LIMSEQ_le)
+ have *: "decseq (\<lambda>n. F m (n + m))"
+ by (auto simp: decseq_def F_def)
+ show "(\<lambda>n. d (F m n)) \<longlonglongrightarrow> d (F' m)"
+ unfolding d_def F'_eq
+ by (rule LIMSEQ_offset[where k=m])
+ (auto intro!: tendsto_diff M.finite_Lim_measure_decseq N.finite_Lim_measure_decseq *)
+ show "(\<lambda>n. \<gamma> - 2 / 2 ^ m + 1 / 2 ^ n) \<longlonglongrightarrow> \<gamma> - 2 / 2 ^ m + 0"
+ by (intro tendsto_add LIMSEQ_divide_realpow_zero tendsto_const) auto
+ show "\<exists>N. \<forall>n\<ge>N. \<gamma> - 2 / 2 ^ m + 1 / 2 ^ n \<le> d (F m n)"
+ using 1[of m] by (intro exI[of _ m]) auto
+ qed
+ then show "\<exists>N. \<forall>n\<ge>N. \<gamma> - 2 / 2 ^ n \<le> d (F' n)"
+ by auto
+ qed
+
+ show ?thesis
+ proof (safe intro!: bexI[of _ "\<Union>m. F' m"])
+ fix X assume [measurable]: "X \<in> sets M" and X: "X \<subseteq> (\<Union>m. F' m)"
+ have "d (\<Union>m. F' m) - d X = d ((\<Union>m. F' m) - X)"
+ using X by (auto simp: d_def M.finite_measure_Diff N.finite_measure_Diff)
+ also have "\<dots> \<le> \<gamma>"
+ by auto
+ finally have "0 \<le> d X"
+ using \<gamma>_le by auto
+ then show "emeasure N X \<le> emeasure M X"
+ by (auto simp: d_def M.emeasure_eq_measure N.emeasure_eq_measure)
+ next
+ fix X assume [measurable]: "X \<in> sets M" and X: "X \<inter> (\<Union>m. F' m) = {}"
+ then have "d (\<Union>m. F' m) + d X = d (X \<union> (\<Union>m. F' m))"
+ by (auto simp: d_def M.finite_measure_Union N.finite_measure_Union)
+ also have "\<dots> \<le> \<gamma>"
+ by auto
+ finally have "d X \<le> 0"
+ using \<gamma>_le by auto
+ then show "emeasure M X \<le> emeasure N X"
+ by (auto simp: d_def M.emeasure_eq_measure N.emeasure_eq_measure)
+ qed auto
+qed
+
+lemma unsigned_Hahn_decomposition:
+ assumes [simp]: "sets N = sets M" and [measurable]: "A \<in> sets M"
+ and [simp]: "emeasure M A \<noteq> top" "emeasure N A \<noteq> top"
+ shows "\<exists>Y\<in>sets M. Y \<subseteq> A \<and> (\<forall>X\<in>sets M. X \<subseteq> Y \<longrightarrow> N X \<le> M X) \<and> (\<forall>X\<in>sets M. X \<subseteq> A \<longrightarrow> X \<inter> Y = {} \<longrightarrow> M X \<le> N X)"
+proof -
+ have "\<exists>Y\<in>sets (restrict_space M A).
+ (\<forall>X\<in>sets (restrict_space M A). X \<subseteq> Y \<longrightarrow> (restrict_space N A) X \<le> (restrict_space M A) X) \<and>
+ (\<forall>X\<in>sets (restrict_space M A). X \<inter> Y = {} \<longrightarrow> (restrict_space M A) X \<le> (restrict_space N A) X)"
+ proof (rule finite_unsigned_Hahn_decomposition)
+ show "finite_measure (restrict_space M A)" "finite_measure (restrict_space N A)"
+ by (auto simp: space_restrict_space emeasure_restrict_space less_top intro!: finite_measureI)
+ qed (simp add: sets_restrict_space)
+ then guess Y ..
+ then show ?thesis
+ apply (intro bexI[of _ Y] conjI ballI conjI)
+ apply (simp_all add: sets_restrict_space emeasure_restrict_space)
+ apply safe
+ subgoal for X Z
+ by (erule ballE[of _ _ X]) (auto simp add: Int_absorb1)
+ subgoal for X Z
+ by (erule ballE[of _ _ X]) (auto simp add: Int_absorb1 ac_simps)
+ apply auto
+ done
+qed
+
+text \<open>
+ Define a lexicographical order on @{type measure}, in the order space, sets and measure. The parts
+ of the lexicographical order are point-wise ordered.
+\<close>
instantiation measure :: (type) order_bot
begin
-definition bot_measure :: "'a measure" where
- "bot_measure = sigma {} {{}}"
-
-lemma space_bot[simp]: "space bot = {}"
- unfolding bot_measure_def by (rule space_measure_of) auto
-
-lemma sets_bot[simp]: "sets bot = {{}}"
- unfolding bot_measure_def by (subst sets_measure_of) auto
-
-lemma emeasure_bot[simp]: "emeasure bot = (\<lambda>x. 0)"
- unfolding bot_measure_def by (rule emeasure_sigma)
-
inductive less_eq_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
- "sets N = sets M \<Longrightarrow> (\<And>A. A \<in> sets M \<Longrightarrow> emeasure M A \<le> emeasure N A) \<Longrightarrow> less_eq_measure M N"
-| "less_eq_measure bot N"
+ "space M \<subset> space N \<Longrightarrow> less_eq_measure M N"
+| "space M = space N \<Longrightarrow> sets M \<subset> sets N \<Longrightarrow> less_eq_measure M N"
+| "space M = space N \<Longrightarrow> sets M = sets N \<Longrightarrow> emeasure M \<le> emeasure N \<Longrightarrow> less_eq_measure M N"
+
+lemma le_measure_iff:
+ "M \<le> N \<longleftrightarrow> (if space M = space N then
+ if sets M = sets N then emeasure M \<le> emeasure N else sets M \<subseteq> sets N else space M \<subseteq> space N)"
+ by (auto elim: less_eq_measure.cases intro: less_eq_measure.intros)
definition less_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
"less_measure M N \<longleftrightarrow> (M \<le> N \<and> \<not> N \<le> M)"
-instance
-proof (standard, goal_cases)
- case 1 then show ?case
- unfolding less_measure_def ..
-next
- case (2 M) then show ?case
- by (intro less_eq_measure.intros) auto
-next
- case (3 M N L) then show ?case
- apply (safe elim!: less_eq_measure.cases)
- apply (simp_all add: less_eq_measure.intros)
- apply (rule less_eq_measure.intros)
- apply simp
- apply (blast intro: order_trans) []
- unfolding less_eq_measure.simps
- apply (rule disjI2)
- apply simp
- apply (rule measure_eqI)
- apply (auto intro!: antisym)
- done
-next
- case (4 M N) then show ?case
- apply (safe elim!: less_eq_measure.cases intro!: measure_eqI)
- apply simp
- apply simp
- apply (blast intro: antisym)
- apply (simp)
- apply simp
- done
-qed (rule less_eq_measure.intros)
-end
-
-lemma le_emeasureD: "M \<le> N \<Longrightarrow> emeasure M A \<le> emeasure N A"
- by (cases "A \<in> sets M") (auto elim!: less_eq_measure.cases simp: emeasure_notin_sets)
-
-lemma le_sets: "N \<le> M \<Longrightarrow> sets N \<le> sets M"
- unfolding less_eq_measure.simps by auto
-
-instantiation measure :: (type) ccpo
-begin
-
-definition Sup_measure :: "'a measure set \<Rightarrow> 'a measure" where
- "Sup_measure A = measure_of (SUP a:A. space a) (SUP a:A. sets a) (SUP a:A. emeasure a)"
+definition bot_measure :: "'a measure" where
+ "bot_measure = sigma {} {}"
lemma
- assumes A: "Complete_Partial_Order.chain op \<le> A" and a: "a \<noteq> bot" "a \<in> A"
- shows space_Sup: "space (Sup A) = space a"
- and sets_Sup: "sets (Sup A) = sets a"
+ shows space_bot[simp]: "space bot = {}"
+ and sets_bot[simp]: "sets bot = {{}}"
+ and emeasure_bot[simp]: "emeasure bot X = 0"
+ by (auto simp: bot_measure_def sigma_sets_empty_eq emeasure_sigma)
+
+instance
+proof standard
+ show "bot \<le> a" for a :: "'a measure"
+ by (simp add: le_measure_iff bot_measure_def sigma_sets_empty_eq emeasure_sigma le_fun_def)
+qed (auto simp: le_measure_iff less_measure_def split: if_split_asm intro: measure_eqI)
+
+end
+
+lemma le_measure: "sets M = sets N \<Longrightarrow> M \<le> N \<longleftrightarrow> (\<forall>A\<in>sets M. emeasure M A \<le> emeasure N A)"
+ apply (auto simp: le_measure_iff le_fun_def dest: sets_eq_imp_space_eq)
+ subgoal for X
+ by (cases "X \<in> sets M") (auto simp: emeasure_notin_sets)
+ done
+
+definition sup_measure' :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
+where
+ "sup_measure' A B = measure_of (space A) (sets A) (\<lambda>X. SUP Y:sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y))"
+
+lemma assumes [simp]: "sets B = sets A"
+ shows space_sup_measure'[simp]: "space (sup_measure' A B) = space A"
+ and sets_sup_measure'[simp]: "sets (sup_measure' A B) = sets A"
+ using sets_eq_imp_space_eq[OF assms] by (simp_all add: sup_measure'_def)
+
+lemma emeasure_sup_measure':
+ assumes sets_eq[simp]: "sets B = sets A" and [simp, intro]: "X \<in> sets A"
+ shows "emeasure (sup_measure' A B) X = (SUP Y:sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y))"
+ (is "_ = ?S X")
proof -
- have sets: "(SUP a:A. sets a) = sets a"
- proof (intro antisym SUP_least)
- fix a' show "a' \<in> A \<Longrightarrow> sets a' \<subseteq> sets a"
- using a chainD[OF A, of a a'] by (auto elim!: less_eq_measure.cases)
- qed (insert \<open>a\<in>A\<close>, auto)
- have space: "(SUP a:A. space a) = space a"
- proof (intro antisym SUP_least)
- fix a' show "a' \<in> A \<Longrightarrow> space a' \<subseteq> space a"
- using a chainD[OF A, of a a'] by (intro sets_le_imp_space_le) (auto elim!: less_eq_measure.cases)
- qed (insert \<open>a\<in>A\<close>, auto)
- show "space (Sup A) = space a"
- unfolding Sup_measure_def sets space sets.space_measure_of_eq ..
- show "sets (Sup A) = sets a"
- unfolding Sup_measure_def sets space sets.sets_measure_of_eq ..
+ note sets_eq_imp_space_eq[OF sets_eq, simp]
+ show ?thesis
+ using sup_measure'_def
+ proof (rule emeasure_measure_of)
+ let ?d = "\<lambda>X Y. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y)"
+ show "countably_additive (sets (sup_measure' A B)) (\<lambda>X. SUP Y : sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y))"
+ proof (rule countably_additiveI, goal_cases)
+ case (1 X)
+ then have [measurable]: "\<And>i. X i \<in> sets A" and "disjoint_family X"
+ by auto
+ have "(\<Sum>i. ?S (X i)) = (SUP Y:sets A. \<Sum>i. ?d (X i) Y)"
+ proof (rule ennreal_suminf_SUP_eq_directed)
+ fix J :: "nat set" and a b assume "finite J" and [measurable]: "a \<in> sets A" "b \<in> sets A"
+ have "\<exists>c\<in>sets A. c \<subseteq> X i \<and> (\<forall>a\<in>sets A. ?d (X i) a \<le> ?d (X i) c)" for i
+ proof cases
+ assume "emeasure A (X i) = top \<or> emeasure B (X i) = top"
+ then show ?thesis
+ proof
+ assume "emeasure A (X i) = top" then show ?thesis
+ by (intro bexI[of _ "X i"]) auto
+ next
+ assume "emeasure B (X i) = top" then show ?thesis
+ by (intro bexI[of _ "{}"]) auto
+ qed
+ next
+ assume finite: "\<not> (emeasure A (X i) = top \<or> emeasure B (X i) = top)"
+ then have "\<exists>Y\<in>sets A. Y \<subseteq> X i \<and> (\<forall>C\<in>sets A. C \<subseteq> Y \<longrightarrow> B C \<le> A C) \<and> (\<forall>C\<in>sets A. C \<subseteq> X i \<longrightarrow> C \<inter> Y = {} \<longrightarrow> A C \<le> B C)"
+ using unsigned_Hahn_decomposition[of B A "X i"] by simp
+ then obtain Y where [measurable]: "Y \<in> sets A" and [simp]: "Y \<subseteq> X i"
+ and B_le_A: "\<And>C. C \<in> sets A \<Longrightarrow> C \<subseteq> Y \<Longrightarrow> B C \<le> A C"
+ and A_le_B: "\<And>C. C \<in> sets A \<Longrightarrow> C \<subseteq> X i \<Longrightarrow> C \<inter> Y = {} \<Longrightarrow> A C \<le> B C"
+ by auto
+
+ show ?thesis
+ proof (intro bexI[of _ Y] ballI conjI)
+ fix a assume [measurable]: "a \<in> sets A"
+ have *: "(X i \<inter> a \<inter> Y \<union> (X i \<inter> a - Y)) = X i \<inter> a" "(X i - a) \<inter> Y \<union> (X i - a - Y) = X i \<inter> - a"
+ for a Y by auto
+ then have "?d (X i) a =
+ (A (X i \<inter> a \<inter> Y) + A (X i \<inter> a \<inter> - Y)) + (B (X i \<inter> - a \<inter> Y) + B (X i \<inter> - a \<inter> - Y))"
+ by (subst (1 2) plus_emeasure) (auto simp: Diff_eq[symmetric])
+ also have "\<dots> \<le> (A (X i \<inter> a \<inter> Y) + B (X i \<inter> a \<inter> - Y)) + (A (X i \<inter> - a \<inter> Y) + B (X i \<inter> - a \<inter> - Y))"
+ by (intro add_mono order_refl B_le_A A_le_B) (auto simp: Diff_eq[symmetric])
+ also have "\<dots> \<le> (A (X i \<inter> Y \<inter> a) + A (X i \<inter> Y \<inter> - a)) + (B (X i \<inter> - Y \<inter> a) + B (X i \<inter> - Y \<inter> - a))"
+ by (simp add: ac_simps)
+ also have "\<dots> \<le> A (X i \<inter> Y) + B (X i \<inter> - Y)"
+ by (subst (1 2) plus_emeasure) (auto simp: Diff_eq[symmetric] *)
+ finally show "?d (X i) a \<le> ?d (X i) Y" .
+ qed auto
+ qed
+ then obtain C where [measurable]: "C i \<in> sets A" and "C i \<subseteq> X i"
+ and C: "\<And>a. a \<in> sets A \<Longrightarrow> ?d (X i) a \<le> ?d (X i) (C i)" for i
+ by metis
+ have *: "X i \<inter> (\<Union>i. C i) = X i \<inter> C i" for i
+ proof safe
+ fix x j assume "x \<in> X i" "x \<in> C j"
+ moreover have "i = j \<or> X i \<inter> X j = {}"
+ using \<open>disjoint_family X\<close> by (auto simp: disjoint_family_on_def)
+ ultimately show "x \<in> C i"
+ using \<open>C i \<subseteq> X i\<close> \<open>C j \<subseteq> X j\<close> by auto
+ qed auto
+ have **: "X i \<inter> - (\<Union>i. C i) = X i \<inter> - C i" for i
+ proof safe
+ fix x j assume "x \<in> X i" "x \<notin> C i" "x \<in> C j"
+ moreover have "i = j \<or> X i \<inter> X j = {}"
+ using \<open>disjoint_family X\<close> by (auto simp: disjoint_family_on_def)
+ ultimately show False
+ using \<open>C i \<subseteq> X i\<close> \<open>C j \<subseteq> X j\<close> by auto
+ qed auto
+ show "\<exists>c\<in>sets A. \<forall>i\<in>J. ?d (X i) a \<le> ?d (X i) c \<and> ?d (X i) b \<le> ?d (X i) c"
+ apply (intro bexI[of _ "\<Union>i. C i"])
+ unfolding * **
+ apply (intro C ballI conjI)
+ apply auto
+ done
+ qed
+ also have "\<dots> = ?S (\<Union>i. X i)"
+ unfolding UN_extend_simps(4)
+ by (auto simp add: suminf_add[symmetric] Diff_eq[symmetric] simp del: UN_simps
+ intro!: SUP_cong arg_cong2[where f="op +"] suminf_emeasure
+ disjoint_family_on_bisimulation[OF \<open>disjoint_family X\<close>])
+ finally show "(\<Sum>i. ?S (X i)) = ?S (\<Union>i. X i)" .
+ qed
+ qed (auto dest: sets.sets_into_space simp: positive_def intro!: SUP_const)
qed
-lemma emeasure_Sup:
- assumes A: "Complete_Partial_Order.chain op \<le> A" "A \<noteq> {}"
- assumes "X \<in> sets (Sup A)"
- shows "emeasure (Sup A) X = (SUP a:A. emeasure a) X"
-proof (rule emeasure_measure_of[OF Sup_measure_def])
- show "countably_additive (sets (Sup A)) (SUP a:A. emeasure a)"
- unfolding countably_additive_def
- proof safe
- fix F :: "nat \<Rightarrow> 'a set" assume F: "range F \<subseteq> sets (Sup A)" "disjoint_family F"
- show "(\<Sum>i. (SUP a:A. emeasure a) (F i)) = SUPREMUM A emeasure (UNION UNIV F)"
- unfolding SUP_apply
+lemma le_emeasure_sup_measure'1:
+ assumes "sets B = sets A" "X \<in> sets A" shows "emeasure A X \<le> emeasure (sup_measure' A B) X"
+ by (subst emeasure_sup_measure'[OF assms]) (auto intro!: SUP_upper2[of "X"] assms)
+
+lemma le_emeasure_sup_measure'2:
+ assumes "sets B = sets A" "X \<in> sets A" shows "emeasure B X \<le> emeasure (sup_measure' A B) X"
+ by (subst emeasure_sup_measure'[OF assms]) (auto intro!: SUP_upper2[of "{}"] assms)
+
+lemma emeasure_sup_measure'_le2:
+ assumes [simp]: "sets B = sets C" "sets A = sets C" and [measurable]: "X \<in> sets C"
+ assumes A: "\<And>Y. Y \<subseteq> X \<Longrightarrow> Y \<in> sets A \<Longrightarrow> emeasure A Y \<le> emeasure C Y"
+ assumes B: "\<And>Y. Y \<subseteq> X \<Longrightarrow> Y \<in> sets A \<Longrightarrow> emeasure B Y \<le> emeasure C Y"
+ shows "emeasure (sup_measure' A B) X \<le> emeasure C X"
+proof (subst emeasure_sup_measure')
+ show "(SUP Y:sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y)) \<le> emeasure C X"
+ unfolding \<open>sets A = sets C\<close>
+ proof (intro SUP_least)
+ fix Y assume [measurable]: "Y \<in> sets C"
+ have [simp]: "X \<inter> Y \<union> (X - Y) = X"
+ by auto
+ have "emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y) \<le> emeasure C (X \<inter> Y) + emeasure C (X \<inter> - Y)"
+ by (intro add_mono A B) (auto simp: Diff_eq[symmetric])
+ also have "\<dots> = emeasure C X"
+ by (subst plus_emeasure) (auto simp: Diff_eq[symmetric])
+ finally show "emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y) \<le> emeasure C X" .
+ qed
+qed simp_all
+
+definition sup_lexord :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b::order) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+where
+ "sup_lexord A B k s c =
+ (if k A = k B then c else if \<not> k A \<le> k B \<and> \<not> k B \<le> k A then s else if k B \<le> k A then A else B)"
+
+lemma sup_lexord:
+ "(k A < k B \<Longrightarrow> P B) \<Longrightarrow> (k B < k A \<Longrightarrow> P A) \<Longrightarrow> (k A = k B \<Longrightarrow> P c) \<Longrightarrow>
+ (\<not> k B \<le> k A \<Longrightarrow> \<not> k A \<le> k B \<Longrightarrow> P s) \<Longrightarrow> P (sup_lexord A B k s c)"
+ by (auto simp: sup_lexord_def)
+
+lemmas le_sup_lexord = sup_lexord[where P="\<lambda>a. c \<le> a" for c]
+
+lemma sup_lexord1: "k A = k B \<Longrightarrow> sup_lexord A B k s c = c"
+ by (simp add: sup_lexord_def)
+
+lemma sup_lexord_commute: "sup_lexord A B k s c = sup_lexord B A k s c"
+ by (auto simp: sup_lexord_def)
+
+lemma sigma_sets_le_sets_iff: "(sigma_sets (space x) \<A> \<subseteq> sets x) = (\<A> \<subseteq> sets x)"
+ using sets.sigma_sets_subset[of \<A> x] by auto
+
+lemma sigma_le_iff: "\<A> \<subseteq> Pow \<Omega> \<Longrightarrow> sigma \<Omega> \<A> \<le> x \<longleftrightarrow> (\<Omega> \<subseteq> space x \<and> (space x = \<Omega> \<longrightarrow> \<A> \<subseteq> sets x))"
+ by (cases "\<Omega> = space x")
+ (simp_all add: eq_commute[of _ "sets x"] le_measure_iff emeasure_sigma le_fun_def
+ sigma_sets_superset_generator sigma_sets_le_sets_iff)
+
+instantiation measure :: (type) semilattice_sup
+begin
+
+definition sup_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
+where
+ "sup_measure A B =
+ sup_lexord A B space (sigma (space A \<union> space B) {})
+ (sup_lexord A B sets (sigma (space A) (sets A \<union> sets B)) (sup_measure' A B))"
+
+instance
+proof
+ fix x y z :: "'a measure"
+ show "x \<le> sup x y"
+ unfolding sup_measure_def
+ proof (intro le_sup_lexord)
+ assume "space x = space y"
+ then have *: "sets x \<union> sets y \<subseteq> Pow (space x)"
+ using sets.space_closed by auto
+ assume "\<not> sets y \<subseteq> sets x" "\<not> sets x \<subseteq> sets y"
+ then have "sets x \<subset> sets x \<union> sets y"
+ by auto
+ also have "\<dots> \<le> sigma (space x) (sets x \<union> sets y)"
+ by (subst sets_measure_of[OF *]) (rule sigma_sets_superset_generator)
+ finally show "x \<le> sigma (space x) (sets x \<union> sets y)"
+ by (simp add: space_measure_of[OF *] less_eq_measure.intros(2))
+ next
+ assume "\<not> space y \<subseteq> space x" "\<not> space x \<subseteq> space y"
+ then show "x \<le> sigma (space x \<union> space y) {}"
+ by (intro less_eq_measure.intros) auto
+ next
+ assume "sets x = sets y" then show "x \<le> sup_measure' x y"
+ by (simp add: le_measure le_emeasure_sup_measure'1)
+ qed (auto intro: less_eq_measure.intros)
+ show "y \<le> sup x y"
+ unfolding sup_measure_def
+ proof (intro le_sup_lexord)
+ assume **: "space x = space y"
+ then have *: "sets x \<union> sets y \<subseteq> Pow (space y)"
+ using sets.space_closed by auto
+ assume "\<not> sets y \<subseteq> sets x" "\<not> sets x \<subseteq> sets y"
+ then have "sets y \<subset> sets x \<union> sets y"
+ by auto
+ also have "\<dots> \<le> sigma (space y) (sets x \<union> sets y)"
+ by (subst sets_measure_of[OF *]) (rule sigma_sets_superset_generator)
+ finally show "y \<le> sigma (space x) (sets x \<union> sets y)"
+ by (simp add: ** space_measure_of[OF *] less_eq_measure.intros(2))
+ next
+ assume "\<not> space y \<subseteq> space x" "\<not> space x \<subseteq> space y"
+ then show "y \<le> sigma (space x \<union> space y) {}"
+ by (intro less_eq_measure.intros) auto
+ next
+ assume "sets x = sets y" then show "y \<le> sup_measure' x y"
+ by (simp add: le_measure le_emeasure_sup_measure'2)
+ qed (auto intro: less_eq_measure.intros)
+ show "x \<le> y \<Longrightarrow> z \<le> y \<Longrightarrow> sup x z \<le> y"
+ unfolding sup_measure_def
+ proof (intro sup_lexord[where P="\<lambda>x. x \<le> y"])
+ assume "x \<le> y" "z \<le> y" and [simp]: "space x = space z" "sets x = sets z"
+ from \<open>x \<le> y\<close> show "sup_measure' x z \<le> y"
+ proof cases
+ case 1 then show ?thesis
+ by (intro less_eq_measure.intros(1)) simp
+ next
+ case 2 then show ?thesis
+ by (intro less_eq_measure.intros(2)) simp_all
+ next
+ case 3 with \<open>z \<le> y\<close> \<open>x \<le> y\<close> show ?thesis
+ by (auto simp add: le_measure intro!: emeasure_sup_measure'_le2)
+ qed
+ next
+ assume **: "x \<le> y" "z \<le> y" "space x = space z" "\<not> sets z \<subseteq> sets x" "\<not> sets x \<subseteq> sets z"
+ then have *: "sets x \<union> sets z \<subseteq> Pow (space x)"
+ using sets.space_closed by auto
+ show "sigma (space x) (sets x \<union> sets z) \<le> y"
+ unfolding sigma_le_iff[OF *] using ** by (auto simp: le_measure_iff split: if_split_asm)
+ next
+ assume "x \<le> y" "z \<le> y" "\<not> space z \<subseteq> space x" "\<not> space x \<subseteq> space z"
+ then have "space x \<subseteq> space y" "space z \<subseteq> space y"
+ by (auto simp: le_measure_iff split: if_split_asm)
+ then show "sigma (space x \<union> space z) {} \<le> y"
+ by (simp add: sigma_le_iff)
+ qed
+qed
+
+end
+
+lemma space_empty_eq_bot: "space a = {} \<longleftrightarrow> a = bot"
+ using space_empty[of a] by (auto intro!: measure_eqI)
+
+interpretation sup_measure: comm_monoid_set sup "bot :: 'a measure"
+ proof qed (auto intro!: antisym)
+
+lemma sup_measure_F_mono':
+ "finite J \<Longrightarrow> finite I \<Longrightarrow> sup_measure.F id I \<le> sup_measure.F id (I \<union> J)"
+proof (induction J rule: finite_induct)
+ case empty then show ?case
+ by simp
+next
+ case (insert i J)
+ show ?case
+ proof cases
+ assume "i \<in> I" with insert show ?thesis
+ by (auto simp: insert_absorb)
+ next
+ assume "i \<notin> I"
+ have "sup_measure.F id I \<le> sup_measure.F id (I \<union> J)"
+ by (intro insert)
+ also have "\<dots> \<le> sup_measure.F id (insert i (I \<union> J))"
+ using insert \<open>i \<notin> I\<close> by (subst sup_measure.insert) auto
+ finally show ?thesis
+ by auto
+ qed
+qed
+
+lemma sup_measure_F_mono: "finite I \<Longrightarrow> J \<subseteq> I \<Longrightarrow> sup_measure.F id J \<le> sup_measure.F id I"
+ using sup_measure_F_mono'[of I J] by (auto simp: finite_subset Un_absorb1)
+
+lemma sets_eq_iff_bounded: "A \<le> B \<Longrightarrow> B \<le> C \<Longrightarrow> sets A = sets C \<Longrightarrow> sets B = sets A"
+ by (auto dest: sets_eq_imp_space_eq simp add: le_measure_iff split: if_split_asm)
+
+lemma sets_sup: "sets A = sets M \<Longrightarrow> sets B = sets M \<Longrightarrow> sets (sup A B) = sets M"
+ by (auto simp add: sup_measure_def sup_lexord_def dest: sets_eq_imp_space_eq)
+
+lemma sets_sup_measure_F:
+ "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> sets i = sets M) \<Longrightarrow> sets (sup_measure.F id I) = sets M"
+ by (induction I rule: finite_ne_induct) (simp_all add: sets_sup)
+
+lemma le_measureD1: "A \<le> B \<Longrightarrow> space A \<le> space B"
+ by (auto simp: le_measure_iff split: if_split_asm)
+
+lemma le_measureD2: "A \<le> B \<Longrightarrow> space A = space B \<Longrightarrow> sets A \<le> sets B"
+ by (auto simp: le_measure_iff split: if_split_asm)
+
+lemma le_measureD3: "A \<le> B \<Longrightarrow> sets A = sets B \<Longrightarrow> emeasure A X \<le> emeasure B X"
+ by (auto simp: le_measure_iff le_fun_def dest: sets_eq_imp_space_eq split: if_split_asm)
+
+definition Sup_measure' :: "'a measure set \<Rightarrow> 'a measure"
+where
+ "Sup_measure' M = measure_of (\<Union>a\<in>M. space a) (\<Union>a\<in>M. sets a)
+ (\<lambda>X. (SUP P:{P. finite P \<and> P \<subseteq> M }. sup_measure.F id P X))"
+
+lemma UN_space_closed: "UNION S sets \<subseteq> Pow (UNION S space)"
+ using sets.space_closed by auto
+
+lemma space_Sup_measure'2: "space (Sup_measure' M) = (\<Union>m\<in>M. space m)"
+ unfolding Sup_measure'_def by (intro space_measure_of[OF UN_space_closed])
+
+lemma sets_Sup_measure'2: "sets (Sup_measure' M) = sigma_sets (\<Union>m\<in>M. space m) (\<Union>m\<in>M. sets m)"
+ unfolding Sup_measure'_def by (intro sets_measure_of[OF UN_space_closed])
+
+lemma sets_Sup_measure':
+ assumes sets_eq[simp]: "\<And>m. m \<in> M \<Longrightarrow> sets m = sets A" and "M \<noteq> {}"
+ shows "sets (Sup_measure' M) = sets A"
+ using sets_eq[THEN sets_eq_imp_space_eq, simp] \<open>M \<noteq> {}\<close> by (simp add: Sup_measure'_def)
+
+lemma space_Sup_measure':
+ assumes sets_eq[simp]: "\<And>m. m \<in> M \<Longrightarrow> sets m = sets A" and "M \<noteq> {}"
+ shows "space (Sup_measure' M) = space A"
+ using sets_eq[THEN sets_eq_imp_space_eq, simp] \<open>M \<noteq> {}\<close>
+ by (simp add: Sup_measure'_def )
+
+lemma emeasure_Sup_measure':
+ assumes sets_eq[simp]: "\<And>m. m \<in> M \<Longrightarrow> sets m = sets A" and "X \<in> sets A" "M \<noteq> {}"
+ shows "emeasure (Sup_measure' M) X = (SUP P:{P. finite P \<and> P \<subseteq> M}. sup_measure.F id P X)"
+ (is "_ = ?S X")
+ using Sup_measure'_def
+proof (rule emeasure_measure_of)
+ note sets_eq[THEN sets_eq_imp_space_eq, simp]
+ have *: "sets (Sup_measure' M) = sets A" "space (Sup_measure' M) = space A"
+ using \<open>M \<noteq> {}\<close> by (simp_all add: Sup_measure'_def)
+ let ?\<mu> = "sup_measure.F id"
+ show "countably_additive (sets (Sup_measure' M)) ?S"
+ proof (rule countably_additiveI, goal_cases)
+ case (1 F)
+ then have **: "range F \<subseteq> sets A"
+ by (auto simp: *)
+ show "(\<Sum>i. ?S (F i)) = ?S (\<Union>i. F i)"
proof (subst ennreal_suminf_SUP_eq_directed)
- fix N i j assume "i \<in> A" "j \<in> A"
- with A(1)
- show "\<exists>k\<in>A. \<forall>n\<in>N. emeasure i (F n) \<le> emeasure k (F n) \<and> emeasure j (F n) \<le> emeasure k (F n)"
- by (blast elim: chainE dest: le_emeasureD)
+ fix i j and N :: "nat set" assume ij: "i \<in> {P. finite P \<and> P \<subseteq> M}" "j \<in> {P. finite P \<and> P \<subseteq> M}"
+ have "(i \<noteq> {} \<longrightarrow> sets (?\<mu> i) = sets A) \<and> (j \<noteq> {} \<longrightarrow> sets (?\<mu> j) = sets A) \<and>
+ (i \<noteq> {} \<or> j \<noteq> {} \<longrightarrow> sets (?\<mu> (i \<union> j)) = sets A)"
+ using ij by (intro impI sets_sup_measure_F conjI) auto
+ then have "?\<mu> j (F n) \<le> ?\<mu> (i \<union> j) (F n) \<and> ?\<mu> i (F n) \<le> ?\<mu> (i \<union> j) (F n)" for n
+ using ij
+ by (cases "i = {}"; cases "j = {}")
+ (auto intro!: le_measureD3 sup_measure_F_mono simp: sets_sup_measure_F
+ simp del: id_apply)
+ with ij show "\<exists>k\<in>{P. finite P \<and> P \<subseteq> M}. \<forall>n\<in>N. ?\<mu> i (F n) \<le> ?\<mu> k (F n) \<and> ?\<mu> j (F n) \<le> ?\<mu> k (F n)"
+ by (safe intro!: bexI[of _ "i \<union> j"]) auto
next
- show "(SUP n:A. \<Sum>i. emeasure n (F i)) = (SUP y:A. emeasure y (UNION UNIV F))"
+ show "(SUP P : {P. finite P \<and> P \<subseteq> M}. \<Sum>n. ?\<mu> P (F n)) = (SUP P : {P. finite P \<and> P \<subseteq> M}. ?\<mu> P (UNION UNIV F))"
proof (intro SUP_cong refl)
- fix a assume "a \<in> A" then show "(\<Sum>i. emeasure a (F i)) = emeasure a (UNION UNIV F)"
- using sets_Sup[OF A(1), of a] F by (cases "a = bot") (auto simp: suminf_emeasure)
+ fix i assume i: "i \<in> {P. finite P \<and> P \<subseteq> M}"
+ show "(\<Sum>n. ?\<mu> i (F n)) = ?\<mu> i (UNION UNIV F)"
+ proof cases
+ assume "i \<noteq> {}" with i ** show ?thesis
+ apply (intro suminf_emeasure \<open>disjoint_family F\<close>)
+ apply (subst sets_sup_measure_F[OF _ _ sets_eq])
+ apply auto
+ done
+ qed simp
qed
qed
qed
-qed (insert \<open>A \<noteq> {}\<close> \<open>X \<in> sets (Sup A)\<close>, auto simp: positive_def dest: sets.sets_into_space intro: SUP_upper2)
+ show "positive (sets (Sup_measure' M)) ?S"
+ by (auto simp: positive_def bot_ennreal[symmetric])
+ show "X \<in> sets (Sup_measure' M)"
+ using assms * by auto
+qed (rule UN_space_closed)
+
+definition Sup_lexord :: "('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> ('a set \<Rightarrow> 'a) \<Rightarrow> ('a set \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> 'a"
+where
+ "Sup_lexord k c s A = (let U = (SUP a:A. k a) in if \<exists>a\<in>A. k a = U then c {a\<in>A. k a = U} else s A)"
+
+lemma Sup_lexord:
+ "(\<And>a S. a \<in> A \<Longrightarrow> k a = (SUP a:A. k a) \<Longrightarrow> S = {a'\<in>A. k a' = k a} \<Longrightarrow> P (c S)) \<Longrightarrow> ((\<And>a. a \<in> A \<Longrightarrow> k a \<noteq> (SUP a:A. k a)) \<Longrightarrow> P (s A)) \<Longrightarrow>
+ P (Sup_lexord k c s A)"
+ by (auto simp: Sup_lexord_def Let_def)
+
+lemma Sup_lexord1:
+ assumes A: "A \<noteq> {}" "(\<And>a. a \<in> A \<Longrightarrow> k a = (\<Union>a\<in>A. k a))" "P (c A)"
+ shows "P (Sup_lexord k c s A)"
+ unfolding Sup_lexord_def Let_def
+proof (clarsimp, safe)
+ show "\<forall>a\<in>A. k a \<noteq> (\<Union>x\<in>A. k x) \<Longrightarrow> P (s A)"
+ by (metis assms(1,2) ex_in_conv)
+next
+ fix a assume "a \<in> A" "k a = (\<Union>x\<in>A. k x)"
+ then have "{a \<in> A. k a = (\<Union>x\<in>A. k x)} = {a \<in> A. k a = k a}"
+ by (metis A(2)[symmetric])
+ then show "P (c {a \<in> A. k a = (\<Union>x\<in>A. k x)})"
+ by (simp add: A(3))
+qed
+
+instantiation measure :: (type) complete_lattice
+begin
+
+definition Sup_measure :: "'a measure set \<Rightarrow> 'a measure"
+where
+ "Sup_measure = Sup_lexord space (Sup_lexord sets Sup_measure'
+ (\<lambda>U. sigma (\<Union>u\<in>U. space u) (\<Union>u\<in>U. sets u))) (\<lambda>U. sigma (\<Union>u\<in>U. space u) {})"
+
+definition Inf_measure :: "'a measure set \<Rightarrow> 'a measure"
+where
+ "Inf_measure A = Sup {x. \<forall>a\<in>A. x \<le> a}"
+
+definition inf_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
+where
+ "inf_measure a b = Inf {a, b}"
+
+definition top_measure :: "'a measure"
+where
+ "top_measure = Inf {}"
instance
proof
- fix A and x :: "'a measure" assume A: "Complete_Partial_Order.chain op \<le> A" and x: "x \<in> A"
- show "x \<le> Sup A"
- proof cases
- assume "x \<noteq> bot"
- show ?thesis
- proof
- show "sets (Sup A) = sets x"
- using A \<open>x \<noteq> bot\<close> x by (rule sets_Sup)
- with x show "\<And>a. a \<in> sets x \<Longrightarrow> emeasure x a \<le> emeasure (Sup A) a"
- by (subst emeasure_Sup[OF A]) (auto intro: SUP_upper)
+ note UN_space_closed [simp]
+ show upper: "x \<le> Sup A" if x: "x \<in> A" for x :: "'a measure" and A
+ unfolding Sup_measure_def
+ proof (intro Sup_lexord[where P="\<lambda>y. x \<le> y"])
+ assume "\<And>a. a \<in> A \<Longrightarrow> space a \<noteq> (\<Union>a\<in>A. space a)"
+ from this[OF \<open>x \<in> A\<close>] \<open>x \<in> A\<close> show "x \<le> sigma (\<Union>a\<in>A. space a) {}"
+ by (intro less_eq_measure.intros) auto
+ next
+ fix a S assume "a \<in> A" and a: "space a = (\<Union>a\<in>A. space a)" and S: "S = {a' \<in> A. space a' = space a}"
+ and neq: "\<And>aa. aa \<in> S \<Longrightarrow> sets aa \<noteq> (\<Union>a\<in>S. sets a)"
+ have sp_a: "space a = (UNION S space)"
+ using \<open>a\<in>A\<close> by (auto simp: S)
+ show "x \<le> sigma (UNION S space) (UNION S sets)"
+ proof cases
+ assume [simp]: "space x = space a"
+ have "sets x \<subset> (\<Union>a\<in>S. sets a)"
+ using \<open>x\<in>A\<close> neq[of x] by (auto simp: S)
+ also have "\<dots> \<subseteq> sigma_sets (\<Union>x\<in>S. space x) (\<Union>x\<in>S. sets x)"
+ by (rule sigma_sets_superset_generator)
+ finally show ?thesis
+ by (intro less_eq_measure.intros(2)) (simp_all add: sp_a)
+ next
+ assume "space x \<noteq> space a"
+ moreover have "space x \<le> space a"
+ unfolding a using \<open>x\<in>A\<close> by auto
+ ultimately show ?thesis
+ by (intro less_eq_measure.intros) (simp add: less_le sp_a)
qed
- qed simp
-next
- fix A and x :: "'a measure" assume A: "Complete_Partial_Order.chain op \<le> A" and x: "\<And>z. z \<in> A \<Longrightarrow> z \<le> x"
- consider "A = {}" | "A = {bot}" | x where "x\<in>A" "x \<noteq> bot"
- by blast
- then show "Sup A \<le> x"
- proof cases
- assume "A = {}"
- moreover have "Sup ({}::'a measure set) = bot"
- by (auto simp add: Sup_measure_def sigma_sets_empty_eq intro!: measure_eqI)
- ultimately show ?thesis
- by simp
next
- assume "A = {bot}"
- moreover have "Sup ({bot}::'a measure set) = bot"
- by (auto simp add: Sup_measure_def sigma_sets_empty_eq intro!: measure_eqI)
- ultimately show ?thesis
- by simp
+ fix a b S S' assume "a \<in> A" and a: "space a = (\<Union>a\<in>A. space a)" and S: "S = {a' \<in> A. space a' = space a}"
+ and "b \<in> S" and b: "sets b = (\<Union>a\<in>S. sets a)" and S': "S' = {a' \<in> S. sets a' = sets b}"
+ then have "S' \<noteq> {}" "space b = space a"
+ by auto
+ have sets_eq: "\<And>x. x \<in> S' \<Longrightarrow> sets x = sets b"
+ by (auto simp: S')
+ note sets_eq[THEN sets_eq_imp_space_eq, simp]
+ have *: "sets (Sup_measure' S') = sets b" "space (Sup_measure' S') = space b"
+ using \<open>S' \<noteq> {}\<close> by (simp_all add: Sup_measure'_def sets_eq)
+ show "x \<le> Sup_measure' S'"
+ proof cases
+ assume "x \<in> S"
+ with \<open>b \<in> S\<close> have "space x = space b"
+ by (simp add: S)
+ show ?thesis
+ proof cases
+ assume "x \<in> S'"
+ show "x \<le> Sup_measure' S'"
+ proof (intro le_measure[THEN iffD2] ballI)
+ show "sets x = sets (Sup_measure' S')"
+ using \<open>x\<in>S'\<close> * by (simp add: S')
+ fix X assume "X \<in> sets x"
+ show "emeasure x X \<le> emeasure (Sup_measure' S') X"
+ proof (subst emeasure_Sup_measure'[OF _ \<open>X \<in> sets x\<close>])
+ show "emeasure x X \<le> (SUP P : {P. finite P \<and> P \<subseteq> S'}. emeasure (sup_measure.F id P) X)"
+ using \<open>x\<in>S'\<close> by (intro SUP_upper2[where i="{x}"]) auto
+ qed (insert \<open>x\<in>S'\<close> S', auto)
+ qed
+ next
+ assume "x \<notin> S'"
+ then have "sets x \<noteq> sets b"
+ using \<open>x\<in>S\<close> by (auto simp: S')
+ moreover have "sets x \<le> sets b"
+ using \<open>x\<in>S\<close> unfolding b by auto
+ ultimately show ?thesis
+ using * \<open>x \<in> S\<close>
+ by (intro less_eq_measure.intros(2))
+ (simp_all add: * \<open>space x = space b\<close> less_le)
+ qed
+ next
+ assume "x \<notin> S"
+ with \<open>x\<in>A\<close> \<open>x \<notin> S\<close> \<open>space b = space a\<close> show ?thesis
+ by (intro less_eq_measure.intros)
+ (simp_all add: * less_le a SUP_upper S)
+ qed
+ qed
+ show least: "Sup A \<le> x" if x: "\<And>z. z \<in> A \<Longrightarrow> z \<le> x" for x :: "'a measure" and A
+ unfolding Sup_measure_def
+ proof (intro Sup_lexord[where P="\<lambda>y. y \<le> x"])
+ assume "\<And>a. a \<in> A \<Longrightarrow> space a \<noteq> (\<Union>a\<in>A. space a)"
+ show "sigma (UNION A space) {} \<le> x"
+ using x[THEN le_measureD1] by (subst sigma_le_iff) auto
next
- fix a assume "a \<in> A" "a \<noteq> bot"
- then have "a \<le> x" "x \<noteq> bot" "a \<noteq> bot"
- using x[OF \<open>a \<in> A\<close>] by (auto simp: bot_unique)
- then have "sets x = sets a"
- by (auto elim: less_eq_measure.cases)
-
- show "Sup A \<le> x"
- proof (rule less_eq_measure.intros)
- show "sets x = sets (Sup A)"
- by (subst sets_Sup[OF A \<open>a \<noteq> bot\<close> \<open>a \<in> A\<close>]) fact
+ fix a S assume "a \<in> A" "space a = (\<Union>a\<in>A. space a)" and S: "S = {a' \<in> A. space a' = space a}"
+ "\<And>a. a \<in> S \<Longrightarrow> sets a \<noteq> (\<Union>a\<in>S. sets a)"
+ have "UNION S space \<subseteq> space x"
+ using S le_measureD1[OF x] by auto
+ moreover
+ have "UNION S space = space a"
+ using \<open>a\<in>A\<close> S by auto
+ then have "space x = UNION S space \<Longrightarrow> UNION S sets \<subseteq> sets x"
+ using \<open>a \<in> A\<close> le_measureD2[OF x] by (auto simp: S)
+ ultimately show "sigma (UNION S space) (UNION S sets) \<le> x"
+ by (subst sigma_le_iff) simp_all
+ next
+ fix a b S S' assume "a \<in> A" and a: "space a = (\<Union>a\<in>A. space a)" and S: "S = {a' \<in> A. space a' = space a}"
+ and "b \<in> S" and b: "sets b = (\<Union>a\<in>S. sets a)" and S': "S' = {a' \<in> S. sets a' = sets b}"
+ then have "S' \<noteq> {}" "space b = space a"
+ by auto
+ have sets_eq: "\<And>x. x \<in> S' \<Longrightarrow> sets x = sets b"
+ by (auto simp: S')
+ note sets_eq[THEN sets_eq_imp_space_eq, simp]
+ have *: "sets (Sup_measure' S') = sets b" "space (Sup_measure' S') = space b"
+ using \<open>S' \<noteq> {}\<close> by (simp_all add: Sup_measure'_def sets_eq)
+ show "Sup_measure' S' \<le> x"
+ proof cases
+ assume "space x = space a"
+ show ?thesis
+ proof cases
+ assume **: "sets x = sets b"
+ show ?thesis
+ proof (intro le_measure[THEN iffD2] ballI)
+ show ***: "sets (Sup_measure' S') = sets x"
+ by (simp add: * **)
+ fix X assume "X \<in> sets (Sup_measure' S')"
+ show "emeasure (Sup_measure' S') X \<le> emeasure x X"
+ unfolding ***
+ proof (subst emeasure_Sup_measure'[OF _ \<open>X \<in> sets (Sup_measure' S')\<close>])
+ show "(SUP P : {P. finite P \<and> P \<subseteq> S'}. emeasure (sup_measure.F id P) X) \<le> emeasure x X"
+ proof (safe intro!: SUP_least)
+ fix P assume P: "finite P" "P \<subseteq> S'"
+ show "emeasure (sup_measure.F id P) X \<le> emeasure x X"
+ proof cases
+ assume "P = {}" then show ?thesis
+ by auto
+ next
+ assume "P \<noteq> {}"
+ from P have "finite P" "P \<subseteq> A"
+ unfolding S' S by (simp_all add: subset_eq)
+ then have "sup_measure.F id P \<le> x"
+ by (induction P) (auto simp: x)
+ moreover have "sets (sup_measure.F id P) = sets x"
+ using \<open>finite P\<close> \<open>P \<noteq> {}\<close> \<open>P \<subseteq> S'\<close> \<open>sets x = sets b\<close>
+ by (intro sets_sup_measure_F) (auto simp: S')
+ ultimately show "emeasure (sup_measure.F id P) X \<le> emeasure x X"
+ by (rule le_measureD3)
+ qed
+ qed
+ show "m \<in> S' \<Longrightarrow> sets m = sets (Sup_measure' S')" for m
+ unfolding * by (simp add: S')
+ qed fact
+ qed
+ next
+ assume "sets x \<noteq> sets b"
+ moreover have "sets b \<le> sets x"
+ unfolding b S using x[THEN le_measureD2] \<open>space x = space a\<close> by auto
+ ultimately show "Sup_measure' S' \<le> x"
+ using \<open>space x = space a\<close> \<open>b \<in> S\<close>
+ by (intro less_eq_measure.intros(2)) (simp_all add: * S)
+ qed
next
- fix X assume "X \<in> sets (Sup A)"
- then have "emeasure (Sup A) X \<le> (SUP a:A. emeasure a X)"
- using \<open>a\<in>A\<close> by (subst emeasure_Sup[OF A _]) auto
- also have "\<dots> \<le> emeasure x X"
- by (intro SUP_least le_emeasureD x)
- finally show "emeasure (Sup A) X \<le> emeasure x X" .
+ assume "space x \<noteq> space a"
+ then have "space a < space x"
+ using le_measureD1[OF x[OF \<open>a\<in>A\<close>]] by auto
+ then show "Sup_measure' S' \<le> x"
+ by (intro less_eq_measure.intros) (simp add: * \<open>space b = space a\<close>)
qed
qed
+ show "Sup {} = (bot::'a measure)" "Inf {} = (top::'a measure)"
+ by (auto intro!: antisym least simp: top_measure_def)
+ show lower: "x \<in> A \<Longrightarrow> Inf A \<le> x" for x :: "'a measure" and A
+ unfolding Inf_measure_def by (intro least) auto
+ show greatest: "(\<And>z. z \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> x \<le> Inf A" for x :: "'a measure" and A
+ unfolding Inf_measure_def by (intro upper) auto
+ show "inf x y \<le> x" "inf x y \<le> y" "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> inf y z" for x y z :: "'a measure"
+ by (auto simp: inf_measure_def intro!: lower greatest)
qed
+
end
-lemma
- assumes A: "Complete_Partial_Order.chain op \<le> (f ` A)" and a: "a \<in> A" "f a \<noteq> bot"
- shows space_SUP: "space (SUP M:A. f M) = space (f a)"
- and sets_SUP: "sets (SUP M:A. f M) = sets (f a)"
-by(rule space_Sup[OF A a(2) imageI[OF a(1)]] sets_Sup[OF A a(2) imageI[OF a(1)]])+
+lemma sets_SUP:
+ assumes "\<And>x. x \<in> I \<Longrightarrow> sets (M x) = sets N"
+ shows "I \<noteq> {} \<Longrightarrow> sets (SUP i:I. M i) = sets N"
+ unfolding Sup_measure_def
+ using assms assms[THEN sets_eq_imp_space_eq]
+ sets_Sup_measure'[where A=N and M="M`I"]
+ by (intro Sup_lexord1[where P="\<lambda>x. sets x = sets N"]) auto
lemma emeasure_SUP:
- assumes A: "Complete_Partial_Order.chain op \<le> (f ` A)" "A \<noteq> {}"
- assumes "X \<in> sets (SUP M:A. f M)"
- shows "emeasure (SUP M:A. f M) X = (SUP M:A. emeasure (f M)) X"
-using \<open>X \<in> _\<close> by(subst emeasure_Sup[OF A(1)]; simp add: A)
+ assumes sets: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets N" "X \<in> sets N" "I \<noteq> {}"
+ shows "emeasure (SUP i:I. M i) X = (SUP J:{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emeasure (SUP i:J. M i) X)"
+proof -
+ have eq: "finite J \<Longrightarrow> sup_measure.F id J = (SUP i:J. i)" for J :: "'b measure set"
+ by (induction J rule: finite_induct) auto
+ have 1: "J \<noteq> {} \<Longrightarrow> J \<subseteq> I \<Longrightarrow> sets (SUP x:J. M x) = sets N" for J
+ by (intro sets_SUP sets) (auto )
+
+ from \<open>I \<noteq> {}\<close> obtain i where "i\<in>I" by auto
+ have "Sup_measure' (M`I) X = (SUP P:{P. finite P \<and> P \<subseteq> M`I}. sup_measure.F id P X)"
+ using sets by (intro emeasure_Sup_measure') auto
+ also have "Sup_measure' (M`I) = (SUP i:I. M i)"
+ unfolding Sup_measure_def using \<open>I \<noteq> {}\<close> sets sets(1)[THEN sets_eq_imp_space_eq]
+ by (intro Sup_lexord1[where P="\<lambda>x. _ = x"]) auto
+ also have "(SUP P:{P. finite P \<and> P \<subseteq> M`I}. sup_measure.F id P X) =
+ (SUP J:{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. (SUP i:J. M i) X)"
+ proof (intro SUP_eq)
+ fix J assume "J \<in> {P. finite P \<and> P \<subseteq> M`I}"
+ then obtain J' where J': "J' \<subseteq> I" "finite J'" and J: "J = M`J'" and "finite J"
+ using finite_subset_image[of J M I] by auto
+ show "\<exists>j\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. sup_measure.F id J X \<le> (SUP i:j. M i) X"
+ proof cases
+ assume "J' = {}" with \<open>i \<in> I\<close> show ?thesis
+ by (auto simp add: J)
+ next
+ assume "J' \<noteq> {}" with J J' show ?thesis
+ by (intro bexI[of _ "J'"]) (auto simp add: eq simp del: id_apply)
+ qed
+ next
+ fix J assume J: "J \<in> {P. P \<noteq> {} \<and> finite P \<and> P \<subseteq> I}"
+ show "\<exists>J'\<in>{J. finite J \<and> J \<subseteq> M`I}. (SUP i:J. M i) X \<le> sup_measure.F id J' X"
+ using J by (intro bexI[of _ "M`J"]) (auto simp add: eq simp del: id_apply)
+ qed
+ finally show ?thesis .
+qed
+
+lemma emeasure_SUP_chain:
+ assumes sets: "\<And>i. i \<in> A \<Longrightarrow> sets (M i) = sets N" "X \<in> sets N"
+ assumes ch: "Complete_Partial_Order.chain op \<le> (M ` A)" and "A \<noteq> {}"
+ shows "emeasure (SUP i:A. M i) X = (SUP i:A. emeasure (M i) X)"
+proof (subst emeasure_SUP[OF sets \<open>A \<noteq> {}\<close>])
+ show "(SUP J:{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> A}. emeasure (SUPREMUM J M) X) = (SUP i:A. emeasure (M i) X)"
+ proof (rule SUP_eq)
+ fix J assume "J \<in> {J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> A}"
+ then have J: "Complete_Partial_Order.chain op \<le> (M ` J)" "finite J" "J \<noteq> {}" and "J \<subseteq> A"
+ using ch[THEN chain_subset, of "M`J"] by auto
+ with in_chain_finite[OF J(1)] obtain j where "j \<in> J" "(SUP j:J. M j) = M j"
+ by auto
+ with \<open>J \<subseteq> A\<close> show "\<exists>j\<in>A. emeasure (SUPREMUM J M) X \<le> emeasure (M j) X"
+ by auto
+ next
+ fix j assume "j\<in>A" then show "\<exists>i\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> A}. emeasure (M j) X \<le> emeasure (SUPREMUM i M) X"
+ by (intro bexI[of _ "{j}"]) auto
+ qed
+qed
+
+subsubsection \<open>Supremum of a set of $\sigma$-algebras\<close>
+
+lemma space_Sup_eq_UN: "space (Sup M) = (\<Union>x\<in>M. space x)"
+ unfolding Sup_measure_def
+ apply (intro Sup_lexord[where P="\<lambda>x. space x = _"])
+ apply (subst space_Sup_measure'2)
+ apply auto []
+ apply (subst space_measure_of[OF UN_space_closed])
+ apply auto
+ done
+
+lemma sets_Sup_eq:
+ assumes *: "\<And>m. m \<in> M \<Longrightarrow> space m = X" and "M \<noteq> {}"
+ shows "sets (Sup M) = sigma_sets X (\<Union>x\<in>M. sets x)"
+ unfolding Sup_measure_def
+ apply (rule Sup_lexord1)
+ apply fact
+ apply (simp add: assms)
+ apply (rule Sup_lexord)
+ subgoal premises that for a S
+ unfolding that(3) that(2)[symmetric]
+ using that(1)
+ apply (subst sets_Sup_measure'2)
+ apply (intro arg_cong2[where f=sigma_sets])
+ apply (auto simp: *)
+ done
+ apply (subst sets_measure_of[OF UN_space_closed])
+ apply (simp add: assms)
+ done
+
+lemma in_sets_Sup: "(\<And>m. m \<in> M \<Longrightarrow> space m = X) \<Longrightarrow> m \<in> M \<Longrightarrow> A \<in> sets m \<Longrightarrow> A \<in> sets (Sup M)"
+ by (subst sets_Sup_eq[where X=X]) auto
+
+lemma Sup_lexord_rel:
+ assumes "\<And>i. i \<in> I \<Longrightarrow> k (A i) = k (B i)"
+ "R (c (A ` {a \<in> I. k (B a) = (SUP x:I. k (B x))})) (c (B ` {a \<in> I. k (B a) = (SUP x:I. k (B x))}))"
+ "R (s (A`I)) (s (B`I))"
+ shows "R (Sup_lexord k c s (A`I)) (Sup_lexord k c s (B`I))"
+proof -
+ have "A ` {a \<in> I. k (B a) = (SUP x:I. k (B x))} = {a \<in> A ` I. k a = (SUP x:I. k (B x))}"
+ using assms(1) by auto
+ moreover have "B ` {a \<in> I. k (B a) = (SUP x:I. k (B x))} = {a \<in> B ` I. k a = (SUP x:I. k (B x))}"
+ by auto
+ ultimately show ?thesis
+ using assms by (auto simp: Sup_lexord_def Let_def)
+qed
+
+lemma sets_SUP_cong:
+ assumes eq: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i)" shows "sets (SUP i:I. M i) = sets (SUP i:I. N i)"
+ unfolding Sup_measure_def
+ using eq eq[THEN sets_eq_imp_space_eq]
+ apply (intro Sup_lexord_rel[where R="\<lambda>x y. sets x = sets y"])
+ apply simp
+ apply simp
+ apply (simp add: sets_Sup_measure'2)
+ apply (intro arg_cong2[where f="\<lambda>x y. sets (sigma x y)"])
+ apply auto
+ done
+
+lemma sets_Sup_in_sets:
+ assumes "M \<noteq> {}"
+ assumes "\<And>m. m \<in> M \<Longrightarrow> space m = space N"
+ assumes "\<And>m. m \<in> M \<Longrightarrow> sets m \<subseteq> sets N"
+ shows "sets (Sup M) \<subseteq> sets N"
+proof -
+ have *: "UNION M space = space N"
+ using assms by auto
+ show ?thesis
+ unfolding * using assms by (subst sets_Sup_eq[of M "space N"]) (auto intro!: sets.sigma_sets_subset)
+qed
+
+lemma measurable_Sup1:
+ assumes m: "m \<in> M" and f: "f \<in> measurable m N"
+ and const_space: "\<And>m n. m \<in> M \<Longrightarrow> n \<in> M \<Longrightarrow> space m = space n"
+ shows "f \<in> measurable (Sup M) N"
+proof -
+ have "space (Sup M) = space m"
+ using m by (auto simp add: space_Sup_eq_UN dest: const_space)
+ then show ?thesis
+ using m f unfolding measurable_def by (auto intro: in_sets_Sup[OF const_space])
+qed
+
+lemma measurable_Sup2:
+ assumes M: "M \<noteq> {}"
+ assumes f: "\<And>m. m \<in> M \<Longrightarrow> f \<in> measurable N m"
+ and const_space: "\<And>m n. m \<in> M \<Longrightarrow> n \<in> M \<Longrightarrow> space m = space n"
+ shows "f \<in> measurable N (Sup M)"
+proof -
+ from M obtain m where "m \<in> M" by auto
+ have space_eq: "\<And>n. n \<in> M \<Longrightarrow> space n = space m"
+ by (intro const_space \<open>m \<in> M\<close>)
+ have "f \<in> measurable N (sigma (\<Union>m\<in>M. space m) (\<Union>m\<in>M. sets m))"
+ proof (rule measurable_measure_of)
+ show "f \<in> space N \<rightarrow> UNION M space"
+ using measurable_space[OF f] M by auto
+ qed (auto intro: measurable_sets f dest: sets.sets_into_space)
+ also have "measurable N (sigma (\<Union>m\<in>M. space m) (\<Union>m\<in>M. sets m)) = measurable N (Sup M)"
+ apply (intro measurable_cong_sets refl)
+ apply (subst sets_Sup_eq[OF space_eq M])
+ apply simp
+ apply (subst sets_measure_of[OF UN_space_closed])
+ apply (simp add: space_eq M)
+ done
+ finally show ?thesis .
+qed
+
+lemma sets_Sup_sigma:
+ assumes [simp]: "M \<noteq> {}" and M: "\<And>m. m \<in> M \<Longrightarrow> m \<subseteq> Pow \<Omega>"
+ shows "sets (SUP m:M. sigma \<Omega> m) = sets (sigma \<Omega> (\<Union>M))"
+proof -
+ { fix a m assume "a \<in> sigma_sets \<Omega> m" "m \<in> M"
+ then have "a \<in> sigma_sets \<Omega> (\<Union>M)"
+ by induction (auto intro: sigma_sets.intros) }
+ then show "sets (SUP m:M. sigma \<Omega> m) = sets (sigma \<Omega> (\<Union>M))"
+ apply (subst sets_Sup_eq[where X="\<Omega>"])
+ apply (auto simp add: M) []
+ apply auto []
+ apply (simp add: space_measure_of_conv M Union_least)
+ apply (rule sigma_sets_eqI)
+ apply auto
+ done
+qed
+
+lemma Sup_sigma:
+ assumes [simp]: "M \<noteq> {}" and M: "\<And>m. m \<in> M \<Longrightarrow> m \<subseteq> Pow \<Omega>"
+ shows "(SUP m:M. sigma \<Omega> m) = (sigma \<Omega> (\<Union>M))"
+proof (intro antisym SUP_least)
+ have *: "\<Union>M \<subseteq> Pow \<Omega>"
+ using M by auto
+ show "sigma \<Omega> (\<Union>M) \<le> (SUP m:M. sigma \<Omega> m)"
+ proof (intro less_eq_measure.intros(3))
+ show "space (sigma \<Omega> (\<Union>M)) = space (SUP m:M. sigma \<Omega> m)"
+ "sets (sigma \<Omega> (\<Union>M)) = sets (SUP m:M. sigma \<Omega> m)"
+ using sets_Sup_sigma[OF assms] sets_Sup_sigma[OF assms, THEN sets_eq_imp_space_eq]
+ by auto
+ qed (simp add: emeasure_sigma le_fun_def)
+ fix m assume "m \<in> M" then show "sigma \<Omega> m \<le> sigma \<Omega> (\<Union>M)"
+ by (subst sigma_le_iff) (auto simp add: M *)
+qed
+
+lemma SUP_sigma_sigma:
+ "M \<noteq> {} \<Longrightarrow> (\<And>m. m \<in> M \<Longrightarrow> f m \<subseteq> Pow \<Omega>) \<Longrightarrow> (SUP m:M. sigma \<Omega> (f m)) = sigma \<Omega> (\<Union>m\<in>M. f m)"
+ using Sup_sigma[of "f`M" \<Omega>] by auto
+
+lemma sets_vimage_Sup_eq:
+ assumes *: "M \<noteq> {}" "f \<in> X \<rightarrow> Y" "\<And>m. m \<in> M \<Longrightarrow> space m = Y"
+ shows "sets (vimage_algebra X f (Sup M)) = sets (SUP m : M. vimage_algebra X f m)"
+ (is "?IS = ?SI")
+proof
+ show "?IS \<subseteq> ?SI"
+ apply (intro sets_image_in_sets measurable_Sup2)
+ apply (simp add: space_Sup_eq_UN *)
+ apply (simp add: *)
+ apply (intro measurable_Sup1)
+ apply (rule imageI)
+ apply assumption
+ apply (rule measurable_vimage_algebra1)
+ apply (auto simp: *)
+ done
+ show "?SI \<subseteq> ?IS"
+ apply (intro sets_Sup_in_sets)
+ apply (auto simp: *) []
+ apply (auto simp: *) []
+ apply (elim imageE)
+ apply simp
+ apply (rule sets_image_in_sets)
+ apply simp
+ apply (simp add: measurable_def)
+ apply (simp add: * space_Sup_eq_UN sets_vimage_algebra2)
+ apply (auto intro: in_sets_Sup[OF *(3)])
+ done
+qed
+
+lemma restrict_space_eq_vimage_algebra':
+ "sets (restrict_space M \<Omega>) = sets (vimage_algebra (\<Omega> \<inter> space M) (\<lambda>x. x) M)"
+proof -
+ have *: "{A \<inter> (\<Omega> \<inter> space M) |A. A \<in> sets M} = {A \<inter> \<Omega> |A. A \<in> sets M}"
+ using sets.sets_into_space[of _ M] by blast
+
+ show ?thesis
+ unfolding restrict_space_def
+ by (subst sets_measure_of)
+ (auto simp add: image_subset_iff sets_vimage_algebra * dest: sets.sets_into_space intro!: arg_cong2[where f=sigma_sets])
+qed
+
+lemma sigma_le_sets:
+ assumes [simp]: "A \<subseteq> Pow X" shows "sets (sigma X A) \<subseteq> sets N \<longleftrightarrow> X \<in> sets N \<and> A \<subseteq> sets N"
+proof
+ have "X \<in> sigma_sets X A" "A \<subseteq> sigma_sets X A"
+ by (auto intro: sigma_sets_top)
+ moreover assume "sets (sigma X A) \<subseteq> sets N"
+ ultimately show "X \<in> sets N \<and> A \<subseteq> sets N"
+ by auto
+next
+ assume *: "X \<in> sets N \<and> A \<subseteq> sets N"
+ { fix Y assume "Y \<in> sigma_sets X A" from this * have "Y \<in> sets N"
+ by induction auto }
+ then show "sets (sigma X A) \<subseteq> sets N"
+ by auto
+qed
+
+lemma measurable_iff_sets:
+ "f \<in> measurable M N \<longleftrightarrow> (f \<in> space M \<rightarrow> space N \<and> sets (vimage_algebra (space M) f N) \<subseteq> sets M)"
+proof -
+ have *: "{f -` A \<inter> space M |A. A \<in> sets N} \<subseteq> Pow (space M)"
+ by auto
+ show ?thesis
+ unfolding measurable_def
+ by (auto simp add: vimage_algebra_def sigma_le_sets[OF *])
+qed
+
+lemma sets_vimage_algebra_space: "X \<in> sets (vimage_algebra X f M)"
+ using sets.top[of "vimage_algebra X f M"] by simp
+
+lemma measurable_mono:
+ assumes N: "sets N' \<le> sets N" "space N = space N'"
+ assumes M: "sets M \<le> sets M'" "space M = space M'"
+ shows "measurable M N \<subseteq> measurable M' N'"
+ unfolding measurable_def
+proof safe
+ fix f A assume "f \<in> space M \<rightarrow> space N" "A \<in> sets N'"
+ moreover assume "\<forall>y\<in>sets N. f -` y \<inter> space M \<in> sets M" note this[THEN bspec, of A]
+ ultimately show "f -` A \<inter> space M' \<in> sets M'"
+ using assms by auto
+qed (insert N M, auto)
+
+lemma measurable_Sup_measurable:
+ assumes f: "f \<in> space N \<rightarrow> A"
+ shows "f \<in> measurable N (Sup {M. space M = A \<and> f \<in> measurable N M})"
+proof (rule measurable_Sup2)
+ show "{M. space M = A \<and> f \<in> measurable N M} \<noteq> {}"
+ using f unfolding ex_in_conv[symmetric]
+ by (intro exI[of _ "sigma A {}"]) (auto intro!: measurable_measure_of)
+qed auto
+
+lemma (in sigma_algebra) sigma_sets_subset':
+ assumes a: "a \<subseteq> M" "\<Omega>' \<in> M"
+ shows "sigma_sets \<Omega>' a \<subseteq> M"
+proof
+ show "x \<in> M" if x: "x \<in> sigma_sets \<Omega>' a" for x
+ using x by (induct rule: sigma_sets.induct) (insert a, auto)
+qed
+
+lemma in_sets_SUP: "i \<in> I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> space (M i) = Y) \<Longrightarrow> X \<in> sets (M i) \<Longrightarrow> X \<in> sets (SUP i:I. M i)"
+ by (intro in_sets_Sup[where X=Y]) auto
+
+lemma measurable_SUP1:
+ "i \<in> I \<Longrightarrow> f \<in> measurable (M i) N \<Longrightarrow> (\<And>m n. m \<in> I \<Longrightarrow> n \<in> I \<Longrightarrow> space (M m) = space (M n)) \<Longrightarrow>
+ f \<in> measurable (SUP i:I. M i) N"
+ by (auto intro: measurable_Sup1)
+
+lemma sets_image_in_sets':
+ assumes X: "X \<in> sets N"
+ assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> f -` A \<inter> X \<in> sets N"
+ shows "sets (vimage_algebra X f M) \<subseteq> sets N"
+ unfolding sets_vimage_algebra
+ by (rule sets.sigma_sets_subset') (auto intro!: measurable_sets X f)
+
+lemma mono_vimage_algebra:
+ "sets M \<le> sets N \<Longrightarrow> sets (vimage_algebra X f M) \<subseteq> sets (vimage_algebra X f N)"
+ using sets.top[of "sigma X {f -` A \<inter> X |A. A \<in> sets N}"]
+ unfolding vimage_algebra_def
+ apply (subst (asm) space_measure_of)
+ apply auto []
+ apply (subst sigma_le_sets)
+ apply auto
+ done
+
+lemma mono_restrict_space: "sets M \<le> sets N \<Longrightarrow> sets (restrict_space M X) \<subseteq> sets (restrict_space N X)"
+ unfolding sets_restrict_space by (rule image_mono)
+
+lemma sets_eq_bot: "sets M = {{}} \<longleftrightarrow> M = bot"
+ apply safe
+ apply (intro measure_eqI)
+ apply auto
+ done
+
+lemma sets_eq_bot2: "{{}} = sets M \<longleftrightarrow> M = bot"
+ using sets_eq_bot[of M] by blast
end
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Wed Jun 15 22:19:03 2016 +0200
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Thu Jun 16 23:03:27 2016 +0200
@@ -1525,6 +1525,18 @@
subsection \<open>Integral under concrete measures\<close>
+lemma nn_integral_mono_measure:
+ assumes "sets M = sets N" "M \<le> N" shows "nn_integral M f \<le> nn_integral N f"
+ unfolding nn_integral_def
+proof (intro SUP_subset_mono)
+ note \<open>sets M = sets N\<close>[simp] \<open>sets M = sets N\<close>[THEN sets_eq_imp_space_eq, simp]
+ show "{g. simple_function M g \<and> g \<le> f} \<subseteq> {g. simple_function N g \<and> g \<le> f}"
+ by (simp add: simple_function_def)
+ show "integral\<^sup>S M x \<le> integral\<^sup>S N x" for x
+ using le_measureD3[OF \<open>M \<le> N\<close>]
+ by (auto simp add: simple_integral_def intro!: setsum_mono mult_mono)
+qed
+
lemma nn_integral_empty:
assumes "space M = {}"
shows "nn_integral M f = 0"
@@ -1534,6 +1546,9 @@
thus ?thesis by simp
qed
+lemma nn_integral_bot[simp]: "nn_integral bot f = 0"
+ by (simp add: nn_integral_empty)
+
subsubsection \<open>Distributions\<close>
lemma nn_integral_distr:
--- a/src/HOL/Probability/Radon_Nikodym.thy Wed Jun 15 22:19:03 2016 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy Thu Jun 16 23:03:27 2016 +0200
@@ -8,155 +8,6 @@
imports Bochner_Integration
begin
-lemma (in finite_measure) finite_measure_Diff':
- "A \<in> sets M \<Longrightarrow> B \<in> sets M \<Longrightarrow> measure M (A - B) = measure M A - measure M (A \<inter> B)"
- using finite_measure_Diff[of A "A \<inter> B"] by (auto simp: Diff_Int)
-
-lemma (in finite_measure) finite_measure_Union':
- "A \<in> sets M \<Longrightarrow> B \<in> sets M \<Longrightarrow> measure M (A \<union> B) = measure M A + measure M (B - A)"
- using finite_measure_Union[of A "B - A"] by auto
-
-lemma finite_unsigned_Hahn_decomposition:
- assumes "finite_measure M" "finite_measure N" and [simp]: "sets N = sets M"
- shows "\<exists>Y\<in>sets M. (\<forall>X\<in>sets M. X \<subseteq> Y \<longrightarrow> N X \<le> M X) \<and> (\<forall>X\<in>sets M. X \<inter> Y = {} \<longrightarrow> M X \<le> N X)"
-proof -
- interpret M: finite_measure M by fact
- interpret N: finite_measure N by fact
-
- define d where "d X = measure M X - measure N X" for X
-
- have [intro]: "bdd_above (d`sets M)"
- using sets.sets_into_space[of _ M]
- by (intro bdd_aboveI[where M="measure M (space M)"])
- (auto simp: d_def field_simps subset_eq intro!: add_increasing M.finite_measure_mono)
-
- define \<gamma> where "\<gamma> = (SUP X:sets M. d X)"
- have le_\<gamma>[intro]: "X \<in> sets M \<Longrightarrow> d X \<le> \<gamma>" for X
- by (auto simp: \<gamma>_def intro!: cSUP_upper)
-
- have "\<exists>f. \<forall>n. f n \<in> sets M \<and> d (f n) > \<gamma> - 1 / 2^n"
- proof (intro choice_iff[THEN iffD1] allI)
- fix n
- have "\<exists>X\<in>sets M. \<gamma> - 1 / 2^n < d X"
- unfolding \<gamma>_def by (intro less_cSUP_iff[THEN iffD1]) auto
- then show "\<exists>y. y \<in> sets M \<and> \<gamma> - 1 / 2 ^ n < d y"
- by auto
- qed
- then obtain E where [measurable]: "E n \<in> sets M" and E: "d (E n) > \<gamma> - 1 / 2^n" for n
- by auto
-
- define F where "F m n = (if m \<le> n then \<Inter>i\<in>{m..n}. E i else space M)" for m n
-
- have [measurable]: "m \<le> n \<Longrightarrow> F m n \<in> sets M" for m n
- by (auto simp: F_def)
-
- have 1: "\<gamma> - 2 / 2 ^ m + 1 / 2 ^ n \<le> d (F m n)" if "m \<le> n" for m n
- using that
- proof (induct rule: dec_induct)
- case base with E[of m] show ?case
- by (simp add: F_def field_simps)
- next
- case (step i)
- have F_Suc: "F m (Suc i) = F m i \<inter> E (Suc i)"
- using \<open>m \<le> i\<close> by (auto simp: F_def le_Suc_eq)
-
- have "\<gamma> + (\<gamma> - 2 / 2^m + 1 / 2 ^ Suc i) \<le> (\<gamma> - 1 / 2^Suc i) + (\<gamma> - 2 / 2^m + 1 / 2^i)"
- by (simp add: field_simps)
- also have "\<dots> \<le> d (E (Suc i)) + d (F m i)"
- using E[of "Suc i"] by (intro add_mono step) auto
- also have "\<dots> = d (E (Suc i)) + d (F m i - E (Suc i)) + d (F m (Suc i))"
- using \<open>m \<le> i\<close> by (simp add: d_def field_simps F_Suc M.finite_measure_Diff' N.finite_measure_Diff')
- also have "\<dots> = d (E (Suc i) \<union> F m i) + d (F m (Suc i))"
- using \<open>m \<le> i\<close> by (simp add: d_def field_simps M.finite_measure_Union' N.finite_measure_Union')
- also have "\<dots> \<le> \<gamma> + d (F m (Suc i))"
- using \<open>m \<le> i\<close> by auto
- finally show ?case
- by auto
- qed
-
- define F' where "F' m = (\<Inter>i\<in>{m..}. E i)" for m
- have F'_eq: "F' m = (\<Inter>i. F m (i + m))" for m
- by (fastforce simp: le_iff_add[of m] F'_def F_def)
-
- have [measurable]: "F' m \<in> sets M" for m
- by (auto simp: F'_def)
-
- have \<gamma>_le: "\<gamma> - 0 \<le> d (\<Union>m. F' m)"
- proof (rule LIMSEQ_le)
- show "(\<lambda>n. \<gamma> - 2 / 2 ^ n) \<longlonglongrightarrow> \<gamma> - 0"
- by (intro tendsto_intros LIMSEQ_divide_realpow_zero) auto
- have "incseq F'"
- by (auto simp: incseq_def F'_def)
- then show "(\<lambda>m. d (F' m)) \<longlonglongrightarrow> d (\<Union>m. F' m)"
- unfolding d_def
- by (intro tendsto_diff M.finite_Lim_measure_incseq N.finite_Lim_measure_incseq) auto
-
- have "\<gamma> - 2 / 2 ^ m + 0 \<le> d (F' m)" for m
- proof (rule LIMSEQ_le)
- have *: "decseq (\<lambda>n. F m (n + m))"
- by (auto simp: decseq_def F_def)
- show "(\<lambda>n. d (F m n)) \<longlonglongrightarrow> d (F' m)"
- unfolding d_def F'_eq
- by (rule LIMSEQ_offset[where k=m])
- (auto intro!: tendsto_diff M.finite_Lim_measure_decseq N.finite_Lim_measure_decseq *)
- show "(\<lambda>n. \<gamma> - 2 / 2 ^ m + 1 / 2 ^ n) \<longlonglongrightarrow> \<gamma> - 2 / 2 ^ m + 0"
- by (intro tendsto_add LIMSEQ_divide_realpow_zero tendsto_const) auto
- show "\<exists>N. \<forall>n\<ge>N. \<gamma> - 2 / 2 ^ m + 1 / 2 ^ n \<le> d (F m n)"
- using 1[of m] by (intro exI[of _ m]) auto
- qed
- then show "\<exists>N. \<forall>n\<ge>N. \<gamma> - 2 / 2 ^ n \<le> d (F' n)"
- by auto
- qed
-
- show ?thesis
- proof (safe intro!: bexI[of _ "\<Union>m. F' m"])
- fix X assume [measurable]: "X \<in> sets M" and X: "X \<subseteq> (\<Union>m. F' m)"
- have "d (\<Union>m. F' m) - d X = d ((\<Union>m. F' m) - X)"
- using X by (auto simp: d_def M.finite_measure_Diff N.finite_measure_Diff)
- also have "\<dots> \<le> \<gamma>"
- by auto
- finally have "0 \<le> d X"
- using \<gamma>_le by auto
- then show "emeasure N X \<le> emeasure M X"
- by (auto simp: d_def M.emeasure_eq_measure N.emeasure_eq_measure)
- next
- fix X assume [measurable]: "X \<in> sets M" and X: "X \<inter> (\<Union>m. F' m) = {}"
- then have "d (\<Union>m. F' m) + d X = d (X \<union> (\<Union>m. F' m))"
- by (auto simp: d_def M.finite_measure_Union N.finite_measure_Union)
- also have "\<dots> \<le> \<gamma>"
- by auto
- finally have "d X \<le> 0"
- using \<gamma>_le by auto
- then show "emeasure M X \<le> emeasure N X"
- by (auto simp: d_def M.emeasure_eq_measure N.emeasure_eq_measure)
- qed auto
-qed
-
-lemma unsigned_Hahn_decomposition:
- assumes [simp]: "sets N = sets M" and [measurable]: "A \<in> sets M"
- and [simp]: "emeasure M A \<noteq> top" "emeasure N A \<noteq> top"
- shows "\<exists>Y\<in>sets M. Y \<subseteq> A \<and> (\<forall>X\<in>sets M. X \<subseteq> Y \<longrightarrow> N X \<le> M X) \<and> (\<forall>X\<in>sets M. X \<subseteq> A \<longrightarrow> X \<inter> Y = {} \<longrightarrow> M X \<le> N X)"
-proof -
- have "\<exists>Y\<in>sets (restrict_space M A).
- (\<forall>X\<in>sets (restrict_space M A). X \<subseteq> Y \<longrightarrow> (restrict_space N A) X \<le> (restrict_space M A) X) \<and>
- (\<forall>X\<in>sets (restrict_space M A). X \<inter> Y = {} \<longrightarrow> (restrict_space M A) X \<le> (restrict_space N A) X)"
- proof (rule finite_unsigned_Hahn_decomposition)
- show "finite_measure (restrict_space M A)" "finite_measure (restrict_space N A)"
- by (auto simp: space_restrict_space emeasure_restrict_space less_top intro!: finite_measureI)
- qed (simp add: sets_restrict_space)
- then guess Y ..
- then show ?thesis
- apply (intro bexI[of _ Y] conjI ballI conjI)
- apply (simp_all add: sets_restrict_space emeasure_restrict_space)
- apply safe
- subgoal for X Z
- by (erule ballE[of _ _ X]) (auto simp add: Int_absorb1)
- subgoal for X Z
- by (erule ballE[of _ _ X]) (auto simp add: Int_absorb1 ac_simps)
- apply auto
- done
-qed
-
definition diff_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
where
"diff_measure M N = measure_of (space M) (sets M) (\<lambda>A. emeasure M A - emeasure N A)"
--- a/src/HOL/Probability/SPMF.thy Wed Jun 15 22:19:03 2016 +0200
+++ b/src/HOL/Probability/SPMF.thy Thu Jun 16 23:03:27 2016 +0200
@@ -302,7 +302,7 @@
finally show ?thesis .
qed
-lemma integral_measure_spmf:
+lemma integral_measure_spmf:
assumes "integrable (measure_spmf p) f"
shows "(\<integral> x. f x \<partial>measure_spmf p) = \<integral> x. spmf p x * f x \<partial>count_space UNIV"
proof -
@@ -340,7 +340,7 @@
proof(rule neq_top_trans)
show "(SUP i. ennreal (spmf (Y i) x)) \<le> 1" by(rule SUP_least)(simp add: pmf_le_1)
qed simp
-
+
lemma SUP_emeasure_spmf_neq_top: "(SUP p:Y. emeasure (measure_spmf p) A) \<noteq> \<top>"
proof(rule neq_top_trans)
show "(SUP p:Y. emeasure (measure_spmf p) A) \<le> 1"
@@ -453,7 +453,7 @@
lemma set_map_spmf [simp]: "set_spmf (map_spmf f p) = f ` set_spmf p"
by(simp add: set_spmf_def image_bind bind_image o_def Option.option.set_map)
-
+
lemma map_spmf_cong:
"\<lbrakk> p = q; \<And>x. x \<in> set_spmf q \<Longrightarrow> f x = g x \<rbrakk>
\<Longrightarrow> map_spmf f p = map_spmf g q"
@@ -576,7 +576,7 @@
by(simp add: sets_bind[where N="count_space UNIV"] space_measure_spmf)
next
fix A :: "'a set"
- have "emeasure ?lhs A = \<integral>\<^sup>+ x. emeasure (measure_spmf (f x)) A \<partial>measure_pmf p"
+ have "emeasure ?lhs A = \<integral>\<^sup>+ x. emeasure (measure_spmf (f x)) A \<partial>measure_pmf p"
by(simp add: measure_spmf_def emeasure_distr space_restrict_space emeasure_restrict_space bind_spmf_def)
also have "\<dots> = emeasure ?rhs A"
by(simp add: emeasure_bind[where N="count_space UNIV"] space_measure_spmf space_subprob_algebra)
@@ -591,13 +591,13 @@
next
fix A :: "'a set"
let ?A = "the -` A \<inter> range Some"
- have "emeasure ?lhs A = \<integral>\<^sup>+ x. emeasure (measure_pmf (case x of None \<Rightarrow> return_pmf None | Some x \<Rightarrow> f x)) ?A \<partial>measure_pmf p"
+ have "emeasure ?lhs A = \<integral>\<^sup>+ x. emeasure (measure_pmf (case x of None \<Rightarrow> return_pmf None | Some x \<Rightarrow> f x)) ?A \<partial>measure_pmf p"
by(simp add: measure_spmf_def emeasure_distr space_restrict_space emeasure_restrict_space bind_spmf_def)
also have "\<dots> = \<integral>\<^sup>+ x. emeasure (measure_pmf (f (the x))) ?A * indicator (range Some) x \<partial>measure_pmf p"
by(rule nn_integral_cong)(auto split: option.split simp add: indicator_def)
also have "\<dots> = \<integral>\<^sup>+ x. emeasure (measure_spmf (f x)) A \<partial>measure_spmf p"
by(simp add: measure_spmf_def nn_integral_distr nn_integral_restrict_space emeasure_distr space_restrict_space emeasure_restrict_space)
- also have "\<dots> = emeasure ?rhs A"
+ also have "\<dots> = emeasure ?rhs A"
by(simp add: emeasure_bind[where N="count_space UNIV"] space_measure_spmf space_subprob_algebra)
finally show "emeasure ?lhs A = emeasure ?rhs A" .
qed
@@ -663,7 +663,7 @@
lemma rel_spmf_mono:
"\<lbrakk>rel_spmf A f g; \<And>x y. A x y \<Longrightarrow> B x y \<rbrakk> \<Longrightarrow> rel_spmf B f g"
-apply(erule rel_pmf_mono)
+apply(erule rel_pmf_mono)
using option.rel_mono[of A B] by(simp add: le_fun_def)
lemma rel_spmf_mono_strong:
@@ -684,7 +684,7 @@
lemma rel_spmfE [elim?, consumes 1, case_names rel_spmf]:
assumes "rel_spmf P p q"
- obtains pq where
+ obtains pq where
"\<And>x y. (x, y) \<in> set_spmf pq \<Longrightarrow> P x y"
"p = map_spmf fst pq"
"q = map_spmf snd pq"
@@ -847,7 +847,7 @@
lemma weight_spmf_nonneg: "weight_spmf p \<ge> 0"
by(fact measure_nonneg)
-lemma (in finite_measure) integrable_weight_spmf [simp]:
+lemma (in finite_measure) integrable_weight_spmf [simp]:
"(\<lambda>x. weight_spmf (f x)) \<in> borel_measurable M \<Longrightarrow> integrable M (\<lambda>x. weight_spmf (f x))"
by(rule integrable_const_bound[where B=1])(simp_all add: weight_spmf_nonneg weight_spmf_le_1)
@@ -1068,7 +1068,7 @@
and refl: "\<And>x. x \<in> set_spmf p \<Longrightarrow> R x x"
shows "ord_spmf R p q"
proof(rule rel_pmf.intros)
- define pq where "pq = embed_pmf
+ define pq where "pq = embed_pmf
(\<lambda>(x, y). case x of Some x' \<Rightarrow> (case y of Some y' \<Rightarrow> if x' = y' then spmf p x' else 0 | None \<Rightarrow> 0)
| None \<Rightarrow> (case y of None \<Rightarrow> pmf q None | Some y' \<Rightarrow> spmf q y' - spmf p y'))"
(is "_ = embed_pmf ?f")
@@ -1077,8 +1077,8 @@
have integral: "(\<integral>\<^sup>+ xy. ?f xy \<partial>count_space UNIV) = 1" (is "nn_integral ?M _ = _")
proof -
have "(\<integral>\<^sup>+ xy. ?f xy \<partial>count_space UNIV) =
- \<integral>\<^sup>+ xy. ennreal (?f xy) * indicator {(None, None)} xy +
- ennreal (?f xy) * indicator (range (\<lambda>x. (None, Some x))) xy +
+ \<integral>\<^sup>+ xy. ennreal (?f xy) * indicator {(None, None)} xy +
+ ennreal (?f xy) * indicator (range (\<lambda>x. (None, Some x))) xy +
ennreal (?f xy) * indicator (range (\<lambda>x. (Some x, Some x))) xy \<partial>?M"
by(rule nn_integral_cong)(auto split: split_indicator option.splits if_split_asm)
also have "\<dots> = (\<integral>\<^sup>+ xy. ?f xy * indicator {(None, None)} xy \<partial>?M) +
@@ -1132,8 +1132,8 @@
then show ?thesis using Some by simp
next
case None
- have "(\<integral>\<^sup>+ y. pmf pq (None, y) \<partial>count_space UNIV) =
- (\<integral>\<^sup>+ y. ennreal (pmf pq (None, Some (the y))) * indicator (range Some) y +
+ have "(\<integral>\<^sup>+ y. pmf pq (None, y) \<partial>count_space UNIV) =
+ (\<integral>\<^sup>+ y. ennreal (pmf pq (None, Some (the y))) * indicator (range Some) y +
ennreal (pmf pq (None, None)) * indicator {None} y \<partial>count_space UNIV)"
by(rule nn_integral_cong)(auto split: split_indicator)
also have "\<dots> = (\<integral>\<^sup>+ y. ennreal (pmf pq (None, Some (the y))) \<partial>count_space (range Some)) + pmf pq (None, None)"
@@ -1170,8 +1170,8 @@
then show ?thesis using None by simp
next
case (Some y)
- have "(\<integral>\<^sup>+ x. pmf pq (x, Some y) \<partial>count_space UNIV) =
- (\<integral>\<^sup>+ x. ennreal (pmf pq (x, Some y)) * indicator (range Some) x +
+ have "(\<integral>\<^sup>+ x. pmf pq (x, Some y) \<partial>count_space UNIV) =
+ (\<integral>\<^sup>+ x. ennreal (pmf pq (x, Some y)) * indicator (range Some) x +
ennreal (pmf pq (None, Some y)) * indicator {None} x \<partial>count_space UNIV)"
by(rule nn_integral_cong)(auto split: split_indicator)
also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (pmf pq (x, Some y)) * indicator (range Some) x \<partial>count_space UNIV) + pmf pq (None, Some y)"
@@ -1215,8 +1215,7 @@
by(auto intro!: nn_integral_mono split: split_indicator dest: ord_spmf_eq_leD simp add: nn_integral_measure_spmf nn_integral_indicator[symmetric])
lemma ord_spmf_eqD_measure_spmf: "ord_spmf op = p q \<Longrightarrow> measure_spmf p \<le> measure_spmf q"
-by(rule less_eq_measure.intros)(simp_all add: ord_spmf_eqD_emeasure)
-
+ by (subst le_measure) (auto simp: ord_spmf_eqD_emeasure)
subsection \<open>CCPO structure for the flat ccpo @{term "ord_option op ="}\<close>
@@ -1224,7 +1223,7 @@
definition lub_spmf :: "'a spmf"
where "lub_spmf = embed_spmf (\<lambda>x. enn2real (SUP p : Y. ennreal (spmf p x)))"
- \<comment> \<open>We go through @{typ ennreal} to have a sensible definition even if @{term Y} is empty.\<close>
+ \<comment> \<open>We go through @{typ ennreal} to have a sensible definition even if @{term Y} is empty.\<close>
lemma lub_spmf_empty [simp]: "SPMF.lub_spmf {} = return_pmf None"
by(simp add: SPMF.lub_spmf_def bot_ereal_def)
@@ -1259,18 +1258,18 @@
proof(rule spmf_eqI)
fix i
from le have le': "\<And>x. spmf p x \<le> spmf q x" by(rule ord_spmf_eq_leD)
- have "(\<integral>\<^sup>+ x. ennreal (spmf q x) - spmf p x \<partial>count_space UNIV) =
+ have "(\<integral>\<^sup>+ x. ennreal (spmf q x) - spmf p x \<partial>count_space UNIV) =
(\<integral>\<^sup>+ x. spmf q x \<partial>count_space UNIV) - (\<integral>\<^sup>+ x. spmf p x \<partial>count_space UNIV)"
by(subst nn_integral_diff)(simp_all add: AE_count_space le' nn_integral_spmf_neq_top)
also have "\<dots> = (1 - pmf q None) - (1 - pmf p None)" unfolding pmf_None_eq_weight_spmf
by(simp add: weight_spmf_eq_nn_integral_spmf[symmetric] ennreal_minus)
also have "\<dots> = 0" using None by simp
- finally have "\<And>x. spmf q x \<le> spmf p x"
+ finally have "\<And>x. spmf q x \<le> spmf p x"
by(simp add: nn_integral_0_iff_AE AE_count_space ennreal_minus ennreal_eq_0_iff)
with le' show "spmf p i = spmf q i" by(rule antisym)
qed
-lemma ord_spmf_eqD_pmf_None:
+lemma ord_spmf_eqD_pmf_None:
assumes "ord_spmf op = x y"
shows "pmf x None \<ge> pmf y None"
using assms
@@ -1283,7 +1282,7 @@
Chains on @{typ "'a spmf"} maintain countable support.
Thanks to Johannes Hölzl for the proof idea.
\<close>
-lemma spmf_chain_countable: "countable (\<Union>p\<in>Y. set_spmf p)"
+lemma spmf_chain_countable: "countable (\<Union>p\<in>Y. set_spmf p)"
proof(cases "Y = {}")
case Y: False
show ?thesis
@@ -1295,13 +1294,13 @@
next
case False
define N :: "'a option pmf \<Rightarrow> real" where "N p = pmf p None" for p
-
+
have N_less_imp_le_spmf: "\<lbrakk> x \<in> Y; y \<in> Y; N y < N x \<rbrakk> \<Longrightarrow> ord_spmf op = x y" for x y
using chainD[OF chain, of x y] ord_spmf_eqD_pmf_None[of x y] ord_spmf_eqD_pmf_None[of y x]
by (auto simp: N_def)
have N_eq_imp_eq: "\<lbrakk> x \<in> Y; y \<in> Y; N y = N x \<rbrakk> \<Longrightarrow> x = y" for x y
using chainD[OF chain, of x y] by(auto simp add: N_def dest: ord_spmf_eq_pmf_None_eq)
-
+
have NC: "N ` Y \<noteq> {}" "bdd_below (N ` Y)"
using \<open>Y \<noteq> {}\<close> by(auto intro!: bdd_belowI[of _ 0] simp: N_def)
have NC_less: "Inf (N ` Y) < N x" if "x \<in> Y" for x unfolding cInf_less_iff[OF NC]
@@ -1314,12 +1313,12 @@
by cases(auto dest: N_less_imp_le_spmf N_eq_imp_eq intro: ord_spmf_reflI) }
with False \<open>x \<in> Y\<close> show False by blast
qed
-
+
from NC have "Inf (N ` Y) \<in> closure (N ` Y)" by (intro closure_contains_Inf)
then obtain X' where "\<And>n. X' n \<in> N ` Y" and X': "X' \<longlonglongrightarrow> Inf (N ` Y)"
unfolding closure_sequential by auto
then obtain X where X: "\<And>n. X n \<in> Y" and "X' = (\<lambda>n. N (X n))" unfolding image_iff Bex_def by metis
-
+
with X' have seq: "(\<lambda>n. N (X n)) \<longlonglongrightarrow> Inf (N ` Y)" by simp
have "(\<Union>x \<in> Y. set_spmf x) \<subseteq> (\<Union>n. set_spmf (X n))"
proof(rule UN_least)
@@ -1343,7 +1342,7 @@
let ?B = "\<Union>p\<in>Y. set_spmf p"
have countable: "countable ?B" by(rule spmf_chain_countable)
- have "(\<integral>\<^sup>+ x. (SUP p:Y. ennreal (spmf p x)) \<partial>count_space UNIV) =
+ have "(\<integral>\<^sup>+ x. (SUP p:Y. ennreal (spmf p x)) \<partial>count_space UNIV) =
(\<integral>\<^sup>+ x. (SUP p:Y. ennreal (spmf p x) * indicator ?B x) \<partial>count_space UNIV)"
by(intro nn_integral_cong SUP_cong)(auto split: split_indicator simp add: spmf_eq_0_set_spmf)
also have "\<dots> = (\<integral>\<^sup>+ x. (SUP p:Y. ennreal (spmf p x)) \<partial>count_space ?B)"
@@ -1481,8 +1480,10 @@
from assms obtain p where p: "p \<in> Y" by auto
from chain have chain': "Complete_Partial_Order.chain op \<le> (measure_spmf ` Y)"
by(rule chain_imageI)(rule ord_spmf_eqD_measure_spmf)
- show "sets ?lhs = sets ?rhs" and "emeasure ?lhs A = emeasure ?rhs A" for A
- using chain' Y p by(simp_all add: sets_SUP emeasure_SUP emeasure_lub_spmf)
+ show "sets ?lhs = sets ?rhs"
+ using Y by (subst sets_SUP) auto
+ show "emeasure ?lhs A = emeasure ?rhs A" for A
+ using chain' Y p by (subst emeasure_SUP_chain) (auto simp: emeasure_lub_spmf)
qed
end
@@ -1552,11 +1553,11 @@
ultimately show "ord_spmf op = (bind_spmf (B f) (\<lambda>y. C y f)) (bind_spmf (B g) (\<lambda>y'. C y' g))"
by(rule bind_spmf_mono')
qed
-
+
lemma monotone_bind_spmf1: "monotone (ord_spmf op =) (ord_spmf op =) (\<lambda>y. bind_spmf y g)"
by(rule monotoneI)(simp add: bind_spmf_mono' ord_spmf_reflI)
-lemma monotone_bind_spmf2:
+lemma monotone_bind_spmf2:
assumes g: "\<And>x. monotone ord (ord_spmf op =) (\<lambda>y. g y x)"
shows "monotone ord (ord_spmf op =) (\<lambda>y. bind_spmf p (g y))"
by(rule monotoneI)(auto intro: bind_spmf_mono' monotoneD[OF g] ord_spmf_reflI)
@@ -1611,7 +1612,7 @@
using chain by(rule chain_imageI)(auto simp add: le_fun_def dest: ord_spmf_eq_leD monotoneD[OF g] intro!: mult_left_mono)
have chain''': "Complete_Partial_Order.chain (ord_spmf op =) ((\<lambda>p. bind_spmf x (\<lambda>y. g y p)) ` Y)"
using chain by(rule chain_imageI)(rule monotone_bind_spmf2[OF g, THEN monotoneD])
-
+
have "ennreal (spmf ?lhs i) = \<integral>\<^sup>+ y. (SUP p:Y. ennreal (spmf x y * spmf (g y p) i)) \<partial>count_space (set_spmf x)"
by(simp add: ennreal_spmf_bind ennreal_spmf_lub_spmf[OF chain'] Y nn_integral_measure_spmf' SUP_mult_left_ennreal ennreal_mult)
also have "\<dots> = (SUP p:Y. \<integral>\<^sup>+ y. ennreal (spmf x y * spmf (g y p) i) \<partial>count_space (set_spmf x))"
@@ -1707,7 +1708,7 @@
locale rel_spmf_characterisation =
assumes rel_pmf_measureI:
- "\<And>(R :: 'a option \<Rightarrow> 'b option \<Rightarrow> bool) p q.
+ "\<And>(R :: 'a option \<Rightarrow> 'b option \<Rightarrow> bool) p q.
(\<And>A. measure (measure_pmf p) A \<le> measure (measure_pmf q) {y. \<exists>x\<in>A. R x y})
\<Longrightarrow> rel_pmf R p q"
\<comment> \<open>This assumption is shown to hold in general in the AFP entry \<open>MFMC_Countable\<close>.\<close>
@@ -1911,7 +1912,7 @@
subsection \<open>Subprobability distributions of sets\<close>
definition spmf_of_set :: "'a set \<Rightarrow> 'a spmf"
-where
+where
"spmf_of_set A = (if finite A \<and> A \<noteq> {} then spmf_of_pmf (pmf_of_set A) else return_pmf None)"
lemma spmf_of_set: "spmf (spmf_of_set A) x = indicator A x / card A"
@@ -1933,7 +1934,7 @@
"inj_on f A \<Longrightarrow> map_spmf f (spmf_of_set A) = spmf_of_set (f ` A)"
by(auto simp add: spmf_of_set_def map_pmf_of_set_inj dest: finite_imageD)
-lemma spmf_of_pmf_pmf_of_set [simp]:
+lemma spmf_of_pmf_pmf_of_set [simp]:
"\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> spmf_of_pmf (pmf_of_set A) = spmf_of_set A"
by(simp add: spmf_of_set_def)
@@ -2001,7 +2002,7 @@
lemma rel_pmf_of_set_bij:
assumes f: "bij_betw f A B"
and A: "A \<noteq> {}" "finite A"
- and B: "B \<noteq> {}" "finite B"
+ and B: "B \<noteq> {}" "finite B"
and R: "\<And>x. x \<in> A \<Longrightarrow> R x (f x)"
shows "rel_pmf R (pmf_of_set A) (pmf_of_set B)"
proof(rule pmf.rel_mono_strong)
@@ -2056,7 +2057,7 @@
by(auto intro: arg_cong[where f=card])
also have "\<dots> = (if i then card (B \<inter> A) / card B else (card B - card (B \<inter> A)) / card B)"
by(auto simp add: card_Diff_subset_Int assms)
- also have "\<dots> = ennreal (spmf ?rhs i)"
+ also have "\<dots> = ennreal (spmf ?rhs i)"
by(simp add: assms card_gt_0_iff field_simps card_mono Int_commute of_nat_diff)
finally show "spmf ?lhs i = spmf ?rhs i" by simp
qed
@@ -2233,7 +2234,7 @@
apply(auto simp add: max_def min_def ennreal_mult[symmetric] not_le ennreal_lt_0)
done
-lemma measure_spmf_scale_spmf':
+lemma measure_spmf_scale_spmf':
"r \<le> 1 \<Longrightarrow> measure_spmf (scale_spmf r p) = scale_measure r (measure_spmf p)"
unfolding measure_spmf_scale_spmf
apply(cases "weight_spmf p > 0")
@@ -2250,7 +2251,7 @@
lemma scale_spmf_0 [simp]: "scale_spmf 0 p = return_pmf None"
by(rule spmf_eqI)(simp add: spmf_scale_spmf min_def max_def weight_spmf_le_0)
-lemma bind_scale_spmf:
+lemma bind_scale_spmf:
assumes r: "r \<le> 1"
shows "bind_spmf (scale_spmf r p) f = bind_spmf p (\<lambda>x. scale_spmf r (f x))"
(is "?lhs = ?rhs")
@@ -2262,7 +2263,7 @@
thus "spmf ?lhs x = spmf ?rhs x" by simp
qed
-lemma scale_bind_spmf:
+lemma scale_bind_spmf:
assumes "r \<le> 1"
shows "scale_spmf r (bind_spmf p f) = bind_spmf p (\<lambda>x. scale_spmf r (f x))"
(is "?lhs = ?rhs")
@@ -2298,7 +2299,7 @@
lemma set_scale_spmf' [simp]: "0 < r \<Longrightarrow> set_spmf (scale_spmf r p) = set_spmf p"
by(simp add: set_scale_spmf)
-lemma rel_spmf_scaleI:
+lemma rel_spmf_scaleI:
assumes "r > 0 \<Longrightarrow> rel_spmf A p q"
shows "rel_spmf A (scale_spmf r p) (scale_spmf r q)"
proof(cases "r > 0")
@@ -2319,7 +2320,7 @@
thus ?thesis by(auto simp add: min_def max_def ennreal_mult[symmetric] split: if_split_asm)
qed
-lemma weight_scale_spmf' [simp]:
+lemma weight_scale_spmf' [simp]:
"\<lbrakk> 0 \<le> r; r \<le> 1 \<rbrakk> \<Longrightarrow> weight_spmf (scale_spmf r p) = r * weight_spmf p"
by(simp add: weight_scale_spmf max_def min_def)(metis antisym_conv mult_left_le order_trans weight_spmf_le_1)
@@ -2327,7 +2328,7 @@
"pmf (scale_spmf k p) None = 1 - min 1 (max 0 k * (1 - pmf p None))"
unfolding pmf_None_eq_weight_spmf by(simp add: weight_scale_spmf)
-lemma scale_scale_spmf:
+lemma scale_scale_spmf:
"scale_spmf r (scale_spmf r' p) = scale_spmf (r * max 0 (min (inverse (weight_spmf p)) r')) p"
(is "?lhs = ?rhs")
proof(rule spmf_eqI)
@@ -2432,7 +2433,7 @@
lemma set_pair_spmf [simp]: "set_spmf (pair_spmf p q) = set_spmf p \<times> set_spmf q"
by(auto 4 3 simp add: pair_spmf_def set_spmf_bind_pmf bind_UNION in_set_spmf intro: rev_bexI split: option.splits)
-
+
lemma spmf_pair [simp]: "spmf (pair_spmf p q) (x, y) = spmf p x * spmf q y" (is "?lhs = ?rhs")
proof -
have "ennreal ?lhs = \<integral>\<^sup>+ a. \<integral>\<^sup>+ b. indicator {(x, y)} (a, b) \<partial>measure_spmf q \<partial>measure_spmf p"
@@ -2483,8 +2484,8 @@
by(simp add: pair_spmf_return_spmf1)
lemma rel_pair_spmf_prod:
- "rel_spmf (rel_prod A B) (pair_spmf p q) (pair_spmf p' q') \<longleftrightarrow>
- rel_spmf A (scale_spmf (weight_spmf q) p) (scale_spmf (weight_spmf q') p') \<and>
+ "rel_spmf (rel_prod A B) (pair_spmf p q) (pair_spmf p' q') \<longleftrightarrow>
+ rel_spmf A (scale_spmf (weight_spmf q) p) (scale_spmf (weight_spmf q') p') \<and>
rel_spmf B (scale_spmf (weight_spmf p) q) (scale_spmf (weight_spmf p') q')"
(is "?lhs \<longleftrightarrow> ?rhs" is "_ \<longleftrightarrow> ?A \<and> ?B" is "_ \<longleftrightarrow> rel_spmf _ ?p ?p' \<and> rel_spmf _ ?q ?q'")
proof(intro iffI conjI)
@@ -2506,7 +2507,7 @@
moreover have "(weight_spmf p * weight_spmf q) * (weight_spmf p * weight_spmf q) \<le> (1 * 1) * (1 * 1)"
by(intro mult_mono)(simp_all add: weight_spmf_nonneg weight_spmf_le_1)
ultimately have "(weight_spmf p * weight_spmf q) * (weight_spmf p * weight_spmf q) = 1" by simp
- hence *: "weight_spmf p * weight_spmf q = 1"
+ hence *: "weight_spmf p * weight_spmf q = 1"
by(metis antisym_conv less_le mult_less_cancel_left1 weight_pair_spmf weight_spmf_le_1 weight_spmf_nonneg)
hence "weight_spmf p = 1" by(metis antisym_conv mult_left_le weight_spmf_le_1 weight_spmf_nonneg)
moreover with * have "weight_spmf q = 1" by simp
@@ -2526,7 +2527,7 @@
have [simp]: "snd \<circ> ?f = map_prod snd snd" by(simp add: fun_eq_iff)
from \<open>?rhs\<close> have eq: "weight_spmf p * weight_spmf q = weight_spmf p' * weight_spmf q'"
by(auto dest!: rel_spmf_weightD simp add: weight_spmf_le_1 weight_spmf_nonneg)
-
+
have "map_spmf snd ?pq = scale_spmf ?r (pair_spmf ?p' ?q')"
by(simp add: pair_map_spmf[symmetric] p' q' map_scale_spmf spmf.map_comp)
also have "\<dots> = pair_spmf p' q'" using full[of p' q'] eq
@@ -2546,24 +2547,24 @@
let ?f = "(\<lambda>((x, y), (x', y')). (x, x'))"
let ?pq = "map_spmf ?f pq"
have [simp]: "fst \<circ> ?f = fst \<circ> fst" by(simp add: split_def o_def)
- show "map_spmf fst ?pq = scale_spmf (weight_spmf q) p" using pq
+ show "map_spmf fst ?pq = scale_spmf (weight_spmf q) p" using pq
by(simp add: spmf.map_comp)(simp add: spmf.map_comp[symmetric])
have [simp]: "snd \<circ> ?f = fst \<circ> snd" by(simp add: split_def o_def)
- show "map_spmf snd ?pq = scale_spmf (weight_spmf q') p'" using pq'
+ show "map_spmf snd ?pq = scale_spmf (weight_spmf q') p'" using pq'
by(simp add: spmf.map_comp)(simp add: spmf.map_comp[symmetric])
qed(auto dest: * )
-
+
show ?B
proof
let ?f = "(\<lambda>((x, y), (x', y')). (y, y'))"
let ?pq = "map_spmf ?f pq"
have [simp]: "fst \<circ> ?f = snd \<circ> fst" by(simp add: split_def o_def)
- show "map_spmf fst ?pq = scale_spmf (weight_spmf p) q" using pq
+ show "map_spmf fst ?pq = scale_spmf (weight_spmf p) q" using pq
by(simp add: spmf.map_comp)(simp add: spmf.map_comp[symmetric])
have [simp]: "snd \<circ> ?f = snd \<circ> snd" by(simp add: split_def o_def)
- show "map_spmf snd ?pq = scale_spmf (weight_spmf p') q'" using pq'
+ show "map_spmf snd ?pq = scale_spmf (weight_spmf p') q'" using pq'
by(simp add: spmf.map_comp)(simp add: spmf.map_comp[symmetric])
qed(auto dest: * )
qed
@@ -2650,7 +2651,7 @@
lemma rel_spmf_try_spmf:
"\<lbrakk> rel_spmf R p p'; \<not> lossless_spmf p' \<Longrightarrow> rel_spmf R q q' \<rbrakk>
\<Longrightarrow> rel_spmf R (TRY p ELSE q) (TRY p' ELSE q')"
-unfolding try_spmf_def
+unfolding try_spmf_def
apply(rule rel_pmf_bindI[where R="\<lambda>x y. rel_option R x y \<and> x \<in> set_pmf p \<and> y \<in> set_pmf p'"])
apply(erule pmf.rel_mono_strong; simp)
apply(auto split: option.split simp add: lossless_iff_set_pmf_None)
--- a/src/HOL/Probability/Sigma_Algebra.thy Wed Jun 15 22:19:03 2016 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy Thu Jun 16 23:03:27 2016 +0200
@@ -2002,86 +2002,6 @@
using emeasure_extend_measure[OF M _ _ ms(2,3), of "(i,j)"] eq ms(1) \<open>I i j\<close>
by (auto simp: subset_eq)
-subsubsection \<open>Supremum of a set of $\sigma$-algebras\<close>
-
-definition "Sup_sigma M = sigma (\<Union>x\<in>M. space x) (\<Union>x\<in>M. sets x)"
-
-syntax
- "_SUP_sigma" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>\<^sub>\<sigma> _\<in>_./ _)" [0, 0, 10] 10)
-
-translations
- "\<Squnion>\<^sub>\<sigma> x\<in>A. B" == "CONST Sup_sigma ((\<lambda>x. B) ` A)"
-
-lemma space_Sup_sigma: "space (Sup_sigma M) = (\<Union>x\<in>M. space x)"
- unfolding Sup_sigma_def by (rule space_measure_of) (auto dest: sets.sets_into_space)
-
-lemma sets_Sup_sigma: "sets (Sup_sigma M) = sigma_sets (\<Union>x\<in>M. space x) (\<Union>x\<in>M. sets x)"
- unfolding Sup_sigma_def by (rule sets_measure_of) (auto dest: sets.sets_into_space)
-
-lemma in_Sup_sigma: "m \<in> M \<Longrightarrow> A \<in> sets m \<Longrightarrow> A \<in> sets (Sup_sigma M)"
- unfolding sets_Sup_sigma by auto
-
-lemma SUP_sigma_cong:
- assumes *: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i)" shows "sets (\<Squnion>\<^sub>\<sigma> i\<in>I. M i) = sets (\<Squnion>\<^sub>\<sigma> i\<in>I. N i)"
- using * sets_eq_imp_space_eq[OF *] by (simp add: Sup_sigma_def)
-
-lemma sets_Sup_in_sets:
- assumes "M \<noteq> {}"
- assumes "\<And>m. m \<in> M \<Longrightarrow> space m = space N"
- assumes "\<And>m. m \<in> M \<Longrightarrow> sets m \<subseteq> sets N"
- shows "sets (Sup_sigma M) \<subseteq> sets N"
-proof -
- have *: "UNION M space = space N"
- using assms by auto
- show ?thesis
- unfolding sets_Sup_sigma * using assms by (auto intro!: sets.sigma_sets_subset)
-qed
-
-lemma measurable_Sup_sigma1:
- assumes m: "m \<in> M" and f: "f \<in> measurable m N"
- and const_space: "\<And>m n. m \<in> M \<Longrightarrow> n \<in> M \<Longrightarrow> space m = space n"
- shows "f \<in> measurable (Sup_sigma M) N"
-proof -
- have "space (Sup_sigma M) = space m"
- using m by (auto simp add: space_Sup_sigma dest: const_space)
- then show ?thesis
- using m f unfolding measurable_def by (auto intro: in_Sup_sigma)
-qed
-
-lemma measurable_Sup_sigma2:
- assumes M: "M \<noteq> {}"
- assumes f: "\<And>m. m \<in> M \<Longrightarrow> f \<in> measurable N m"
- shows "f \<in> measurable N (Sup_sigma M)"
- unfolding Sup_sigma_def
-proof (rule measurable_measure_of)
- show "f \<in> space N \<rightarrow> UNION M space"
- using measurable_space[OF f] M by auto
-qed (auto intro: measurable_sets f dest: sets.sets_into_space)
-
-lemma Sup_sigma_sigma:
- assumes [simp]: "M \<noteq> {}" and M: "\<And>m. m \<in> M \<Longrightarrow> m \<subseteq> Pow \<Omega>"
- shows "(\<Squnion>\<^sub>\<sigma> m\<in>M. sigma \<Omega> m) = sigma \<Omega> (\<Union>M)"
-proof (rule measure_eqI)
- { fix a m assume "a \<in> sigma_sets \<Omega> m" "m \<in> M"
- then have "a \<in> sigma_sets \<Omega> (\<Union>M)"
- by induction (auto intro: sigma_sets.intros) }
- then show "sets (\<Squnion>\<^sub>\<sigma> m\<in>M. sigma \<Omega> m) = sets (sigma \<Omega> (\<Union>M))"
- apply (simp add: sets_Sup_sigma space_measure_of_conv M Union_least)
- apply (rule sigma_sets_eqI)
- apply auto
- done
-qed (simp add: Sup_sigma_def emeasure_sigma)
-
-lemma SUP_sigma_sigma:
- assumes M: "M \<noteq> {}" "\<And>m. m \<in> M \<Longrightarrow> f m \<subseteq> Pow \<Omega>"
- shows "(\<Squnion>\<^sub>\<sigma> m\<in>M. sigma \<Omega> (f m)) = sigma \<Omega> (\<Union>m\<in>M. f m)"
-proof -
- have "Sup_sigma (sigma \<Omega> ` f ` M) = sigma \<Omega> (\<Union>(f ` M))"
- using M by (intro Sup_sigma_sigma) auto
- then show ?thesis
- by (simp add: image_image)
-qed
-
subsection \<open>The smallest $\sigma$-algebra regarding a function\<close>
definition
@@ -2157,31 +2077,6 @@
by (simp add: sets_vimage_algebra2 ex_simps[symmetric] vimage_comp comp_def del: ex_simps)
qed (simp add: vimage_algebra_def emeasure_sigma)
-lemma sets_vimage_Sup_eq:
- assumes *: "M \<noteq> {}" "\<And>m. m \<in> M \<Longrightarrow> f \<in> X \<rightarrow> space m"
- shows "sets (vimage_algebra X f (Sup_sigma M)) = sets (\<Squnion>\<^sub>\<sigma> m \<in> M. vimage_algebra X f m)"
- (is "?IS = ?SI")
-proof
- show "?IS \<subseteq> ?SI"
- by (intro sets_image_in_sets measurable_Sup_sigma2 measurable_Sup_sigma1)
- (auto simp: space_Sup_sigma measurable_vimage_algebra1 *)
- { fix m assume "m \<in> M"
- moreover then have "f \<in> X \<rightarrow> space (Sup_sigma M)" "f \<in> X \<rightarrow> space m"
- using * by (auto simp: space_Sup_sigma)
- ultimately have "f \<in> measurable (vimage_algebra X f (Sup_sigma M)) m"
- by (auto simp add: measurable_def sets_vimage_algebra2 intro: in_Sup_sigma) }
- then show "?SI \<subseteq> ?IS"
- by (auto intro!: sets_image_in_sets sets_Sup_in_sets del: subsetI simp: *)
-qed
-
-lemma vimage_algebra_Sup_sigma:
- assumes [simp]: "MM \<noteq> {}" and "\<And>M. M \<in> MM \<Longrightarrow> f \<in> X \<rightarrow> space M"
- shows "vimage_algebra X f (Sup_sigma MM) = Sup_sigma (vimage_algebra X f ` MM)"
-proof (rule measure_eqI)
- show "sets (vimage_algebra X f (Sup_sigma MM)) = sets (Sup_sigma (vimage_algebra X f ` MM))"
- using assms by (rule sets_vimage_Sup_eq)
-qed (simp add: vimage_algebra_def Sup_sigma_def emeasure_sigma)
-
subsubsection \<open>Restricted Space Sigma Algebra\<close>
definition restrict_space where
--- a/src/HOL/Probability/Stream_Space.thy Wed Jun 15 22:19:03 2016 +0200
+++ b/src/HOL/Probability/Stream_Space.thy Thu Jun 16 23:03:27 2016 +0200
@@ -94,16 +94,16 @@
shows "(\<lambda>x. f x ## g x) \<in> measurable N (stream_space M)"
by (rule measurable_stream_space2) (simp add: Stream_snth)
-lemma measurable_smap[measurable]:
+lemma measurable_smap[measurable]:
assumes X[measurable]: "X \<in> measurable N M"
shows "smap X \<in> measurable (stream_space N) (stream_space M)"
by (rule measurable_stream_space2) simp
-lemma measurable_stake[measurable]:
+lemma measurable_stake[measurable]:
"stake i \<in> measurable (stream_space (count_space UNIV)) (count_space (UNIV :: 'a::countable list set))"
by (induct i) auto
-lemma measurable_shift[measurable]:
+lemma measurable_shift[measurable]:
assumes f: "f \<in> measurable N (stream_space M)"
assumes [measurable]: "g \<in> measurable N (stream_space M)"
shows "(\<lambda>x. stake n (f x) @- g x) \<in> measurable N (stream_space M)"
@@ -168,7 +168,7 @@
lemma (in prob_space) nn_integral_stream_space:
assumes [measurable]: "f \<in> borel_measurable (stream_space M)"
shows "(\<integral>\<^sup>+X. f X \<partial>stream_space M) = (\<integral>\<^sup>+x. (\<integral>\<^sup>+X. f (x ## X) \<partial>stream_space M) \<partial>M)"
-proof -
+proof -
interpret S: sequence_space M ..
interpret P: pair_sigma_finite M "\<Pi>\<^sub>M i::nat\<in>UNIV. M" ..
@@ -230,7 +230,7 @@
apply (simp add: AE_iff_nn_integral[symmetric])
done
qed
-
+
lemma (in prob_space) AE_stream_all:
assumes [measurable]: "Measurable.pred M P" and P: "AE x in M. P x"
shows "AE x in stream_space M. stream_all P x"
@@ -271,14 +271,14 @@
assumes sets: "\<And>i. (\<lambda>x. x !! i) \<in> measurable N M"
shows "sets (stream_space M) \<subseteq> sets N"
unfolding stream_space_def sets_distr
- by (auto intro!: sets_image_in_sets measurable_Sup_sigma2 measurable_vimage_algebra2 del: subsetI equalityI
+ by (auto intro!: sets_image_in_sets measurable_Sup2 measurable_vimage_algebra2 del: subsetI equalityI
simp add: sets_PiM_eq_proj snth_in space sets cong: measurable_cong_sets)
lemma sets_stream_space_eq: "sets (stream_space M) =
- sets (\<Squnion>\<^sub>\<sigma> i\<in>UNIV. vimage_algebra (streams (space M)) (\<lambda>s. s !! i) M)"
+ sets (SUP i:UNIV. vimage_algebra (streams (space M)) (\<lambda>s. s !! i) M)"
by (auto intro!: sets_stream_space_in_sets sets_Sup_in_sets sets_image_in_sets
- measurable_Sup_sigma1 snth_in measurable_vimage_algebra1 del: subsetI
- simp: space_Sup_sigma space_stream_space)
+ measurable_Sup1 snth_in measurable_vimage_algebra1 del: subsetI
+ simp: space_Sup_eq_UN space_stream_space)
lemma sets_restrict_stream_space:
assumes S[measurable]: "S \<in> sets M"
@@ -288,17 +288,17 @@
apply (simp add: space_stream_space streams_mono2)
apply (subst vimage_algebra_cong[OF refl refl sets_stream_space_eq])
apply (subst sets_stream_space_eq)
- apply (subst sets_vimage_Sup_eq)
+ apply (subst sets_vimage_Sup_eq[where Y="streams (space M)"])
apply simp
+ apply auto []
apply (auto intro: streams_mono) []
+ apply auto []
apply (simp add: image_image space_restrict_space)
- apply (intro SUP_sigma_cong)
apply (simp add: vimage_algebra_cong[OF refl refl restrict_space_eq_vimage_algebra])
apply (subst (1 2) vimage_algebra_vimage_algebra_eq)
- apply (auto simp: streams_mono snth_in)
+ apply (auto simp: streams_mono snth_in )
done
-
primrec sstart :: "'a set \<Rightarrow> 'a list \<Rightarrow> 'a stream set" where
"sstart S [] = streams S"
| [simp del]: "sstart S (x # xs) = op ## x ` sstart S xs"