--- a/src/HOL/Library/Extended_Real.thy Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Library/Extended_Real.thy Thu Jan 22 14:51:08 2015 +0100
@@ -1606,6 +1606,42 @@
using zero_neq_one by blast
qed
+lemma ereal_Sup:
+ assumes *: "\<bar>SUP a:A. ereal a\<bar> \<noteq> \<infinity>"
+ shows "ereal (Sup A) = (SUP a:A. ereal a)"
+proof (rule antisym)
+ obtain r where r: "ereal r = (SUP a:A. ereal a)" "A \<noteq> {}"
+ using * by (force simp: bot_ereal_def)
+ then have upper: "\<And>a. a \<in> A \<Longrightarrow> a \<le> r"
+ by (auto intro!: SUP_upper simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
+
+ show "ereal (Sup A) \<le> (SUP a:A. ereal a)"
+ using upper by (simp add: r[symmetric] cSup_least[OF `A \<noteq> {}`])
+ show "(SUP a:A. ereal a) \<le> ereal (Sup A)"
+ using upper `A \<noteq> {}` by (intro SUP_least) (auto intro!: cSup_upper bdd_aboveI)
+qed
+
+lemma ereal_SUP: "\<bar>SUP a:A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (SUP a:A. f a) = (SUP a:A. ereal (f a))"
+ using ereal_Sup[of "f`A"] by auto
+
+lemma ereal_Inf:
+ assumes *: "\<bar>INF a:A. ereal a\<bar> \<noteq> \<infinity>"
+ shows "ereal (Inf A) = (INF a:A. ereal a)"
+proof (rule antisym)
+ obtain r where r: "ereal r = (INF a:A. ereal a)" "A \<noteq> {}"
+ using * by (force simp: top_ereal_def)
+ then have lower: "\<And>a. a \<in> A \<Longrightarrow> r \<le> a"
+ by (auto intro!: INF_lower simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
+
+ show "(INF a:A. ereal a) \<le> ereal (Inf A)"
+ using lower by (simp add: r[symmetric] cInf_greatest[OF `A \<noteq> {}`])
+ show "ereal (Inf A) \<le> (INF a:A. ereal a)"
+ using lower `A \<noteq> {}` by (intro INF_greatest) (auto intro!: cInf_lower bdd_belowI)
+qed
+
+lemma ereal_INF: "\<bar>INF a:A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (INF a:A. f a) = (INF a:A. ereal (f a))"
+ using ereal_Inf[of "f`A"] by auto
+
lemma ereal_Sup_uminus_image_eq: "Sup (uminus ` S::ereal set) = - Inf S"
by (auto intro!: SUP_eqI
simp: Ball_def[symmetric] ereal_uminus_le_reorder le_Inf_iff
@@ -1705,28 +1741,37 @@
using assms by (cases e) auto
qed
+lemma SUP_PInfty:
+ fixes f :: "'a \<Rightarrow> ereal"
+ assumes "\<And>n::nat. \<exists>i\<in>A. ereal (real n) \<le> f i"
+ shows "(SUP i:A. f i) = \<infinity>"
+ unfolding SUP_def Sup_eq_top_iff[where 'a=ereal, unfolded top_ereal_def]
+ apply simp
+proof safe
+ fix x :: ereal
+ assume "x \<noteq> \<infinity>"
+ show "\<exists>i\<in>A. x < f i"
+ proof (cases x)
+ case PInf
+ with `x \<noteq> \<infinity>` show ?thesis
+ by simp
+ next
+ case MInf
+ with assms[of "0"] show ?thesis
+ by force
+ next
+ case (real r)
+ with less_PInf_Ex_of_nat[of x] obtain n :: nat where "x < ereal (real n)"
+ by auto
+ moreover obtain i where "i \<in> A" "ereal (real n) \<le> f i"
+ using assms ..
+ ultimately show ?thesis
+ by (auto intro!: bexI[of _ i])
+ qed
+qed
+
lemma SUP_nat_Infty: "(SUP i::nat. ereal (real i)) = \<infinity>"
-proof -
- {
- fix x :: ereal
- assume "x \<noteq> \<infinity>"
- then have "\<exists>k::nat. x < ereal (real k)"
- proof (cases x)
- case MInf
- then show ?thesis
- by (intro exI[of _ 0]) auto
- next
- case (real r)
- moreover obtain k :: nat where "r < real k"
- using ex_less_of_nat by (auto simp: real_eq_of_nat)
- ultimately show ?thesis
- by auto
- qed simp
- }
- then show ?thesis
- using SUP_eq_top_iff[of UNIV "\<lambda>n::nat. ereal (real n)"]
- by (auto simp: top_ereal_def)
-qed
+ by (rule SUP_PInfty) auto
lemma Inf_less:
fixes x :: ereal
@@ -1930,35 +1975,6 @@
shows "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> 0 \<le> c \<Longrightarrow> (SUP i:I. c + f i) = c + SUPREMUM I f"
using SUP_ereal_add_left[of I f c] by (simp add: add_ac)
-lemma SUP_PInfty:
- fixes f :: "'a \<Rightarrow> ereal"
- assumes "\<And>n::nat. \<exists>i\<in>A. ereal (real n) \<le> f i"
- shows "(SUP i:A. f i) = \<infinity>"
- unfolding SUP_def Sup_eq_top_iff[where 'a=ereal, unfolded top_ereal_def]
- apply simp
-proof safe
- fix x :: ereal
- assume "x \<noteq> \<infinity>"
- show "\<exists>i\<in>A. x < f i"
- proof (cases x)
- case PInf
- with `x \<noteq> \<infinity>` show ?thesis
- by simp
- next
- case MInf
- with assms[of "0"] show ?thesis
- by force
- next
- case (real r)
- with less_PInf_Ex_of_nat[of x] obtain n :: nat where "x < ereal (real n)"
- by auto
- moreover obtain i where "i \<in> A" "ereal (real n) \<le> f i"
- using assms ..
- ultimately show ?thesis
- by (auto intro!: bexI[of _ i])
- qed
-qed
-
lemma Sup_countable_SUP:
assumes "A \<noteq> {}"
shows "\<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> A \<and> Sup A = SUPREMUM UNIV f"
@@ -2664,13 +2680,6 @@
by (cases rule: ereal3_cases[of a b c])
(auto simp add: field_simps not_le mult_le_0_iff mult_less_0_iff)
-lemma ereal_pos_le_distrib:
- fixes a b c :: ereal
- assumes "c \<ge> 0"
- shows "c * (a + b) \<le> c * a + c * b"
- using assms
- by (cases rule: ereal3_cases[of a b c]) (auto simp add: field_simps)
-
lemma ereal_max_mono: "(a::ereal) \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> max a c \<le> max b d"
by (metis sup_ereal_def sup_mono)
--- a/src/HOL/Library/FuncSet.thy Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Library/FuncSet.thy Thu Jan 22 14:51:08 2015 +0100
@@ -405,16 +405,20 @@
lemma fun_upd_in_PiE: "x \<notin> S \<Longrightarrow> f \<in> PiE (insert x S) T \<Longrightarrow> f(x := undefined) \<in> PiE S T"
unfolding PiE_def extensional_def by auto
-lemma PiE_insert_eq:
- assumes "x \<notin> S"
- shows "PiE (insert x S) T = (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
+lemma PiE_insert_eq: "PiE (insert x S) T = (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
proof -
{
- fix f assume "f \<in> PiE (insert x S) T"
+ fix f assume "f \<in> PiE (insert x S) T" "x \<notin> S"
with assms have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
by (auto intro!: image_eqI[where x="(f x, f(x := undefined))"] intro: fun_upd_in_PiE PiE_mem)
}
- then show ?thesis
+ moreover
+ {
+ fix f assume "f \<in> PiE (insert x S) T" "x \<in> S"
+ with assms have "f \<in> (\<lambda>(y, g). g(x := y)) ` (T x \<times> PiE S T)"
+ by (auto intro!: image_eqI[where x="(f x, f)"] intro: fun_upd_in_PiE PiE_mem simp: insert_absorb)
+ }
+ ultimately show ?thesis
using assms by (auto intro: PiE_fun_upd)
qed
--- a/src/HOL/Library/Product_Vector.thy Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Library/Product_Vector.thy Thu Jan 22 14:51:08 2015 +0100
@@ -538,4 +538,8 @@
end
+lemma inner_Pair_0: "inner x (0, b) = inner (snd x) b" "inner x (a, 0) = inner (fst x) a"
+ by (cases x, simp)+
+
+
end
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Thu Jan 22 14:51:08 2015 +0100
@@ -1175,6 +1175,16 @@
lemma suminf_ereal_finite: "summable f \<Longrightarrow> (\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
by (auto simp: sums_ereal[symmetric] summable_def sums_unique[symmetric])
+lemma suminf_ereal_finite_neg:
+ assumes "summable f"
+ shows "(\<Sum>x. ereal (f x)) \<noteq> -\<infinity>"
+proof-
+ from assms obtain x where "f sums x" by blast
+ hence "(\<lambda>x. ereal (f x)) sums ereal x" by (simp add: sums_ereal)
+ from sums_unique[OF this] have "(\<Sum>x. ereal (f x)) = ereal x" ..
+ thus "(\<Sum>x. ereal (f x)) \<noteq> -\<infinity>" by simp_all
+qed
+
subsection {* monoset *}
definition (in order) mono_set:
@@ -1364,4 +1374,8 @@
lemma ereal_indicator_nonneg[simp, intro]: "0 \<le> (indicator A x ::ereal)"
unfolding indicator_def by auto
+lemma indicator_inter_arith_ereal: "indicator A x * indicator B x = (indicator (A \<inter> B) x :: ereal)"
+ by (simp split: split_indicator)
+
+
end
--- a/src/HOL/Multivariate_Analysis/Integration.thy Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Thu Jan 22 14:51:08 2015 +0100
@@ -481,6 +481,35 @@
and "interval_lowerbound (cbox a b) = a"
using assms unfolding box_ne_empty by auto
+
+lemma interval_upperbound_Times:
+ assumes "A \<noteq> {}" and "B \<noteq> {}"
+ shows "interval_upperbound (A \<times> B) = (interval_upperbound A, interval_upperbound B)"
+proof-
+ from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
+ have "(\<Sum>i\<in>Basis. (SUP x:A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x:A. x \<bullet> i) *\<^sub>R i)"
+ by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
+ moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
+ have "(\<Sum>i\<in>Basis. (SUP x:A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x:B. x \<bullet> i) *\<^sub>R i)"
+ by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
+ ultimately show ?thesis unfolding interval_upperbound_def
+ by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod)
+qed
+
+lemma interval_lowerbound_Times:
+ assumes "A \<noteq> {}" and "B \<noteq> {}"
+ shows "interval_lowerbound (A \<times> B) = (interval_lowerbound A, interval_lowerbound B)"
+proof-
+ from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
+ have "(\<Sum>i\<in>Basis. (INF x:A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x:A. x \<bullet> i) *\<^sub>R i)"
+ by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
+ moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
+ have "(\<Sum>i\<in>Basis. (INF x:A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x:B. x \<bullet> i) *\<^sub>R i)"
+ by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
+ ultimately show ?thesis unfolding interval_lowerbound_def
+ by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod)
+qed
+
subsection {* Content (length, area, volume...) of an interval. *}
definition "content (s::('a::euclidean_space) set) =
@@ -619,6 +648,20 @@
lemma content_lt_nz: "0 < content (cbox a b) \<longleftrightarrow> content (cbox a b) \<noteq> 0"
unfolding content_pos_lt_eq content_eq_0 unfolding not_ex not_le by fastforce
+lemma content_times[simp]: "content (A \<times> B) = content A * content B"
+proof (cases "A \<times> B = {}")
+ let ?ub1 = "interval_upperbound" and ?lb1 = "interval_lowerbound"
+ let ?ub2 = "interval_upperbound" and ?lb2 = "interval_lowerbound"
+ assume nonempty: "A \<times> B \<noteq> {}"
+ hence "content (A \<times> B) = (\<Prod>i\<in>Basis. (?ub1 A, ?ub2 B) \<bullet> i - (?lb1 A, ?lb2 B) \<bullet> i)"
+ unfolding content_def by (simp add: interval_upperbound_Times interval_lowerbound_Times)
+ also have "... = content A * content B" unfolding content_def using nonempty
+ apply (subst Basis_prod_def, subst setprod.union_disjoint, force, force, force, simp)
+ apply (subst (1 2) setprod.reindex, auto intro: inj_onI)
+ done
+ finally show ?thesis .
+qed (auto simp: content_def)
+
subsection {* The notion of a gauge --- simply an open set containing the point. *}
--- a/src/HOL/Probability/Bochner_Integration.thy Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Probability/Bochner_Integration.thy Thu Jan 22 14:51:08 2015 +0100
@@ -2059,6 +2059,41 @@
by (subst lebesgue_integral_count_space_finite_support)
(auto intro!: setsum.mono_neutral_cong_left)
+lemma integrable_count_space_nat_iff:
+ fixes f :: "nat \<Rightarrow> _::{banach,second_countable_topology}"
+ shows "integrable (count_space UNIV) f \<longleftrightarrow> summable (\<lambda>x. norm (f x))"
+ by (auto simp add: integrable_iff_bounded nn_integral_count_space_nat summable_ereal suminf_ereal_finite)
+
+lemma sums_integral_count_space_nat:
+ fixes f :: "nat \<Rightarrow> _::{banach,second_countable_topology}"
+ assumes *: "integrable (count_space UNIV) f"
+ shows "f sums (integral\<^sup>L (count_space UNIV) f)"
+proof -
+ let ?f = "\<lambda>n i. indicator {n} i *\<^sub>R f i"
+ have f': "\<And>n i. ?f n i = indicator {n} i *\<^sub>R f n"
+ by (auto simp: fun_eq_iff split: split_indicator)
+
+ have "(\<lambda>i. \<integral>n. ?f i n \<partial>count_space UNIV) sums \<integral> n. (\<Sum>i. ?f i n) \<partial>count_space UNIV"
+ proof (rule sums_integral)
+ show "\<And>i. integrable (count_space UNIV) (?f i)"
+ using * by (intro integrable_mult_indicator) auto
+ show "AE n in count_space UNIV. summable (\<lambda>i. norm (?f i n))"
+ using summable_finite[of "{n}" "\<lambda>i. norm (?f i n)" for n] by simp
+ show "summable (\<lambda>i. \<integral> n. norm (?f i n) \<partial>count_space UNIV)"
+ using * by (subst f') (simp add: integrable_count_space_nat_iff)
+ qed
+ also have "(\<integral> n. (\<Sum>i. ?f i n) \<partial>count_space UNIV) = (\<integral>n. f n \<partial>count_space UNIV)"
+ using suminf_finite[of "{n}" "\<lambda>i. ?f i n" for n] by (auto intro!: integral_cong)
+ also have "(\<lambda>i. \<integral>n. ?f i n \<partial>count_space UNIV) = f"
+ by (subst f') simp
+ finally show ?thesis .
+qed
+
+lemma integral_count_space_nat:
+ fixes f :: "nat \<Rightarrow> _::{banach,second_countable_topology}"
+ shows "integrable (count_space UNIV) f \<Longrightarrow> integral\<^sup>L (count_space UNIV) f = (\<Sum>x. f x)"
+ using sums_integral_count_space_nat by (rule sums_unique)
+
subsection {* Point measure *}
lemma lebesgue_integral_point_measure_finite:
@@ -2076,6 +2111,20 @@
apply (auto simp: AE_count_space integrable_count_space)
done
+subsection {* Lebesgue integration on @{const null_measure} *}
+
+lemma has_bochner_integral_null_measure_iff[iff]:
+ "has_bochner_integral (null_measure M) f 0 \<longleftrightarrow> f \<in> borel_measurable M"
+ by (auto simp add: has_bochner_integral.simps simple_bochner_integral_def[abs_def]
+ intro!: exI[of _ "\<lambda>n x. 0"] simple_bochner_integrable.intros)
+
+lemma integrable_null_measure_iff[iff]: "integrable (null_measure M) f \<longleftrightarrow> f \<in> borel_measurable M"
+ by (auto simp add: integrable.simps)
+
+lemma integral_null_measure[simp]: "integral\<^sup>L (null_measure M) f = 0"
+ by (cases "integrable (null_measure M) f")
+ (auto simp add: not_integrable_integral_eq has_bochner_integral_integral_eq)
+
subsection {* Legacy lemmas for the real-valued Lebesgue integral *}
lemma real_lebesgue_integral_def:
--- a/src/HOL/Probability/Finite_Product_Measure.thy Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Thu Jan 22 14:51:08 2015 +0100
@@ -180,6 +180,37 @@
translations
"PIM x:I. M" == "CONST PiM I (%x. M)"
+lemma extend_measure_cong:
+ assumes "\<Omega> = \<Omega>'" "I = I'" "G = G'" "\<And>i. i \<in> I' \<Longrightarrow> \<mu> i = \<mu>' i"
+ shows "extend_measure \<Omega> I G \<mu> = extend_measure \<Omega>' I' G' \<mu>'"
+ unfolding extend_measure_def by (auto simp add: assms)
+
+lemma Pi_cong_sets:
+ "\<lbrakk>I = J; \<And>x. x \<in> I \<Longrightarrow> M x = N x\<rbrakk> \<Longrightarrow> Pi I M = Pi J N"
+ unfolding Pi_def by auto
+
+lemma PiM_cong:
+ assumes "I = J" "\<And>x. x \<in> I \<Longrightarrow> M x = N x"
+ shows "PiM I M = PiM J N"
+unfolding PiM_def
+proof (rule extend_measure_cong)
+ case goal1 show ?case using assms
+ by (subst assms(1), intro PiE_cong[of J "\<lambda>i. space (M i)" "\<lambda>i. space (N i)"]) simp_all
+next
+ case goal2
+ have "\<And>K. K \<subseteq> J \<Longrightarrow> (\<Pi> j\<in>K. sets (M j)) = (\<Pi> j\<in>K. sets (N j))"
+ using assms by (intro Pi_cong_sets) auto
+ thus ?case by (auto simp: assms)
+next
+ case goal3 show ?case using assms
+ by (intro ext) (auto simp: prod_emb_def dest: PiE_mem)
+next
+ case (goal4 x)
+ thus ?case using assms
+ by (auto intro!: setprod.cong split: split_if_asm)
+qed
+
+
lemma prod_algebra_sets_into_space:
"prod_algebra I M \<subseteq> Pow (\<Pi>\<^sub>E i\<in>I. space (M i))"
by (auto simp: prod_emb_def prod_algebra_def)
@@ -624,6 +655,17 @@
lemma measurable_restrict_subset: "J \<subseteq> L \<Longrightarrow> (\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)"
by (intro measurable_restrict measurable_component_singleton) auto
+lemma measurable_restrict_subset':
+ assumes "J \<subseteq> L" "\<And>x. x \<in> J \<Longrightarrow> sets (M x) = sets (N x)"
+ shows "(\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J N)"
+proof-
+ from assms(1) have "(\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)"
+ by (rule measurable_restrict_subset)
+ also from assms(2) have "measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M) = measurable (Pi\<^sub>M L M) (Pi\<^sub>M J N)"
+ by (intro sets_PiM_cong measurable_cong_sets) simp_all
+ finally show ?thesis .
+qed
+
lemma measurable_prod_emb[intro, simp]:
"J \<subseteq> L \<Longrightarrow> X \<in> sets (Pi\<^sub>M J M) \<Longrightarrow> prod_emb L M J X \<in> sets (Pi\<^sub>M L M)"
unfolding prod_emb_def space_PiM[symmetric]
@@ -945,6 +987,17 @@
qed
qed
+lemma (in product_sigma_finite) product_nn_integral_insert_rev:
+ assumes I[simp]: "finite I" "i \<notin> I"
+ and [measurable]: "f \<in> borel_measurable (Pi\<^sub>M (insert i I) M)"
+ shows "integral\<^sup>N (Pi\<^sub>M (insert i I) M) f = (\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x(i := y)) \<partial>(Pi\<^sub>M I M)) \<partial>(M i))"
+ apply (subst product_nn_integral_insert[OF assms])
+ apply (rule pair_sigma_finite.Fubini')
+ apply intro_locales []
+ apply (rule sigma_finite[OF I(1)])
+ apply measurable
+ done
+
lemma (in product_sigma_finite) product_nn_integral_setprod:
fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> ereal"
assumes "finite I" and borel: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
@@ -969,6 +1022,23 @@
done
qed (simp add: space_PiM)
+lemma (in product_sigma_finite) product_nn_integral_pair:
+ assumes [measurable]: "split f \<in> borel_measurable (M x \<Otimes>\<^sub>M M y)"
+ assumes xy: "x \<noteq> y"
+ shows "(\<integral>\<^sup>+\<sigma>. f (\<sigma> x) (\<sigma> y) \<partial>PiM {x, y} M) = (\<integral>\<^sup>+z. f (fst z) (snd z) \<partial>(M x \<Otimes>\<^sub>M M y))"
+proof-
+ interpret psm: pair_sigma_finite "M x" "M y"
+ unfolding pair_sigma_finite_def using sigma_finite_measures by simp_all
+ have "{x, y} = {y, x}" by auto
+ also have "(\<integral>\<^sup>+\<sigma>. f (\<sigma> x) (\<sigma> y) \<partial>PiM {y, x} M) = (\<integral>\<^sup>+y. \<integral>\<^sup>+\<sigma>. f (\<sigma> x) y \<partial>PiM {x} M \<partial>M y)"
+ using xy by (subst product_nn_integral_insert_rev) simp_all
+ also have "... = (\<integral>\<^sup>+y. \<integral>\<^sup>+x. f x y \<partial>M x \<partial>M y)"
+ by (intro nn_integral_cong, subst product_nn_integral_singleton) simp_all
+ also have "... = (\<integral>\<^sup>+z. f (fst z) (snd z) \<partial>(M x \<Otimes>\<^sub>M M y))"
+ by (subst psm.nn_integral_snd[symmetric]) simp_all
+ finally show ?thesis .
+qed
+
lemma (in product_sigma_finite) distr_component:
"distr (M i) (Pi\<^sub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^sub>M {i} M" (is "?D = ?P")
proof (intro measure_eqI[symmetric])
--- a/src/HOL/Probability/Giry_Monad.thy Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy Thu Jan 22 14:51:08 2015 +0100
@@ -32,6 +32,9 @@
"prob_space M \<Longrightarrow> subprob_space M"
by (rule subprob_spaceI) (simp_all add: prob_space.emeasure_space_1 prob_space.not_empty)
+lemma subprob_space_imp_sigma_finite: "subprob_space M \<Longrightarrow> sigma_finite_measure M"
+ unfolding subprob_space_def finite_measure_def by simp
+
sublocale prob_space \<subseteq> subprob_space
by (rule subprob_spaceI) (simp_all add: emeasure_space_1 not_empty)
@@ -123,6 +126,10 @@
by (simp add: space_pair_measure)
qed
+lemma subprob_space_null_measure_iff:
+ "subprob_space (null_measure M) \<longleftrightarrow> space M \<noteq> {}"
+ by (auto intro!: subprob_spaceI dest: subprob_space.subprob_not_empty)
+
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)"
@@ -1250,4 +1257,18 @@
by (simp add: emeasure_notin_sets)
qed
+lemma bind_return'': "sets M = sets N \<Longrightarrow> M \<guillemotright>= return N = M"
+ by (cases "space M = {}")
+ (simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return'
+ cong: subprob_algebra_cong)
+
+lemma (in prob_space) distr_const[simp]:
+ "c \<in> space N \<Longrightarrow> distr M N (\<lambda>x. c) = return N c"
+ by (rule measure_eqI) (auto simp: emeasure_distr emeasure_space_1)
+
+lemma return_count_space_eq_density:
+ "return (count_space M) x = density (count_space M) (indicator {x})"
+ by (rule measure_eqI)
+ (auto simp: indicator_inter_arith_ereal emeasure_density split: split_indicator)
+
end
--- a/src/HOL/Probability/Lebesgue_Measure.thy Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Thu Jan 22 14:51:08 2015 +0100
@@ -529,6 +529,23 @@
thus ?thesis by (auto simp add: emeasure_le_0_iff)
qed
+lemma countable_imp_null_set_lborel: "countable A \<Longrightarrow> A \<in> null_sets lborel"
+ by (simp add: null_sets_def emeasure_lborel_countable sets.countable)
+
+lemma finite_imp_null_set_lborel: "finite A \<Longrightarrow> A \<in> null_sets lborel"
+ by (intro countable_imp_null_set_lborel countable_finite)
+
+lemma lborel_neq_count_space[simp]: "lborel \<noteq> count_space (A::('a::ordered_euclidean_space) set)"
+proof
+ assume asm: "lborel = count_space A"
+ have "space lborel = UNIV" by simp
+ hence [simp]: "A = UNIV" by (subst (asm) asm) (simp only: space_count_space)
+ have "emeasure lborel {undefined::'a} = 1"
+ by (subst asm, subst emeasure_count_space_finite) auto
+ moreover have "emeasure lborel {undefined} \<noteq> 1" by simp
+ ultimately show False by contradiction
+qed
+
subsection {* Affine transformation on the Lebesgue-Borel *}
lemma lborel_eqI:
@@ -651,11 +668,59 @@
unfolding has_bochner_integral_iff lborel_integrable_real_affine_iff
by (simp_all add: lborel_integral_real_affine[symmetric] divideR_right cong: conj_cong)
+lemma lborel_distr_uminus: "distr lborel borel uminus = (lborel :: real measure)"
+ by (subst lborel_real_affine[of "-1" 0])
+ (auto simp: density_1 one_ereal_def[symmetric])
+
+lemma lborel_distr_mult:
+ assumes "(c::real) \<noteq> 0"
+ shows "distr lborel borel (op * c) = density lborel (\<lambda>_. inverse \<bar>c\<bar>)"
+proof-
+ have "distr lborel borel (op * c) = distr lborel lborel (op * c)" by (simp cong: distr_cong)
+ also from assms have "... = density lborel (\<lambda>_. inverse \<bar>c\<bar>)"
+ by (subst lborel_real_affine[of "inverse c" 0]) (auto simp: o_def distr_density_distr)
+ finally show ?thesis .
+qed
+
+lemma lborel_distr_mult':
+ assumes "(c::real) \<noteq> 0"
+ shows "lborel = density (distr lborel borel (op * c)) (\<lambda>_. abs c)"
+proof-
+ have "lborel = density lborel (\<lambda>_. 1)" by (rule density_1[symmetric])
+ also from assms have "(\<lambda>_. 1 :: ereal) = (\<lambda>_. inverse (abs c) * abs c)" by (intro ext) simp
+ also have "density lborel ... = density (density lborel (\<lambda>_. inverse (abs c))) (\<lambda>_. abs c)"
+ by (subst density_density_eq) auto
+ also from assms have "density lborel (\<lambda>_. inverse (abs c)) = distr lborel borel (op * c)"
+ by (rule lborel_distr_mult[symmetric])
+ finally show ?thesis .
+qed
+
+lemma lborel_distr_plus: "distr lborel borel (op + c) = (lborel :: real measure)"
+ by (subst lborel_real_affine[of 1 c]) (auto simp: density_1 one_ereal_def[symmetric])
+
interpretation lborel!: sigma_finite_measure lborel
by (rule sigma_finite_lborel)
interpretation lborel_pair: pair_sigma_finite lborel lborel ..
+lemma lborel_prod:
+ "lborel \<Otimes>\<^sub>M lborel = (lborel :: ('a::euclidean_space \<times> 'b::euclidean_space) measure)"
+proof (rule lborel_eqI[symmetric], clarify)
+ fix la ua :: 'a and lb ub :: 'b
+ assume lu: "\<And>a b. (a, b) \<in> Basis \<Longrightarrow> (la, lb) \<bullet> (a, b) \<le> (ua, ub) \<bullet> (a, b)"
+ have [simp]:
+ "\<And>b. b \<in> Basis \<Longrightarrow> la \<bullet> b \<le> ua \<bullet> b"
+ "\<And>b. b \<in> Basis \<Longrightarrow> lb \<bullet> b \<le> ub \<bullet> b"
+ "inj_on (\<lambda>u. (u, 0)) Basis" "inj_on (\<lambda>u. (0, u)) Basis"
+ "(\<lambda>u. (u, 0)) ` Basis \<inter> (\<lambda>u. (0, u)) ` Basis = {}"
+ "box (la, lb) (ua, ub) = box la ua \<times> box lb ub"
+ using lu[of _ 0] lu[of 0] by (auto intro!: inj_onI simp add: Basis_prod_def ball_Un box_def)
+ show "emeasure (lborel \<Otimes>\<^sub>M lborel) (box (la, lb) (ua, ub)) =
+ ereal (setprod (op \<bullet> ((ua, ub) - (la, lb))) Basis)"
+ by (simp add: lborel.emeasure_pair_measure_Times Basis_prod_def setprod.union_disjoint
+ setprod.reindex)
+qed (simp add: borel_prod[symmetric])
+
(* FIXME: conversion in measurable prover *)
lemma lborelD_Collect[measurable (raw)]: "{x\<in>space borel. P x} \<in> sets borel \<Longrightarrow> {x\<in>space lborel. P x} \<in> sets lborel" by simp
lemma lborelD[measurable (raw)]: "A \<in> sets borel \<Longrightarrow> A \<in> sets lborel" by simp
--- a/src/HOL/Probability/Measure_Space.thy Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Probability/Measure_Space.thy Thu Jan 22 14:51:08 2015 +0100
@@ -1928,5 +1928,23 @@
finally show "emeasure M X = emeasure N X" .
qed fact
+subsection {* Null measure *}
+
+definition "null_measure M = sigma (space M) (sets M)"
+
+lemma space_null_measure[simp]: "space (null_measure M) = space M"
+ by (simp add: null_measure_def)
+
+lemma sets_null_measure[simp, measurable_cong]: "sets (null_measure M) = sets M"
+ by (simp add: null_measure_def)
+
+lemma emeasure_null_measure[simp]: "emeasure (null_measure M) X = 0"
+ by (cases "X \<in> sets M", rule emeasure_measure_of)
+ (auto simp: positive_def countably_additive_def emeasure_notin_sets null_measure_def
+ dest: sets.sets_into_space)
+
+lemma measure_null_measure[simp]: "measure (null_measure M) X = 0"
+ by (simp add: measure_def)
+
end
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Thu Jan 22 14:51:08 2015 +0100
@@ -1951,6 +1951,11 @@
shows "(\<integral>\<^sup>+x. f x \<partial>count_space X) = (\<integral>\<^sup>+x. f x * indicator X x \<partial>count_space UNIV)"
by (simp add: nn_integral_restrict_space[symmetric] restrict_count_space)
+lemma nn_integral_count_space_eq:
+ "(\<And>x. x \<in> A - B \<Longrightarrow> f x = 0) \<Longrightarrow> (\<And>x. x \<in> B - A \<Longrightarrow> f x = 0) \<Longrightarrow>
+ (\<integral>\<^sup>+x. f x \<partial>count_space A) = (\<integral>\<^sup>+x. f x \<partial>count_space B)"
+ by (auto simp: nn_integral_count_space_indicator intro!: nn_integral_cong split: split_indicator)
+
lemma nn_integral_ge_point:
assumes "x \<in> A"
shows "p x \<le> \<integral>\<^sup>+ x. p x \<partial>count_space A"
@@ -2194,6 +2199,23 @@
using f g by (subst density_density_eq) auto
qed
+lemma density_1: "density M (\<lambda>_. 1) = M"
+ by (intro measure_eqI) (auto simp: emeasure_density)
+
+lemma emeasure_density_add:
+ assumes X: "X \<in> sets M"
+ assumes Mf[measurable]: "f \<in> borel_measurable M"
+ assumes Mg[measurable]: "g \<in> borel_measurable M"
+ assumes nonnegf: "\<And>x. x \<in> space M \<Longrightarrow> f x \<ge> 0"
+ assumes nonnegg: "\<And>x. x \<in> space M \<Longrightarrow> g x \<ge> 0"
+ shows "emeasure (density M f) X + emeasure (density M g) X =
+ emeasure (density M (\<lambda>x. f x + g x)) X"
+ using assms
+ apply (subst (1 2 3) emeasure_density, simp_all) []
+ apply (subst nn_integral_add[symmetric], simp_all) []
+ apply (intro nn_integral_cong, simp split: split_indicator)
+ done
+
subsubsection {* Point measure *}
definition point_measure :: "'a set \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> 'a measure" where
@@ -2351,6 +2373,21 @@
unfolding uniform_measure_def by (simp add: AE_density)
qed
+subsubsection {* Null measure *}
+
+lemma null_measure_eq_density: "null_measure M = density M (\<lambda>_. 0)"
+ by (intro measure_eqI) (simp_all add: emeasure_density)
+
+lemma nn_integral_null_measure[simp]: "(\<integral>\<^sup>+x. f x \<partial>null_measure M) = 0"
+ by (auto simp add: nn_integral_def simple_integral_def SUP_constant bot_ereal_def le_fun_def
+ intro!: exI[of _ "\<lambda>x. 0"])
+
+lemma density_null_measure[simp]: "density (null_measure M) f = null_measure M"
+proof (intro measure_eqI)
+ fix A show "emeasure (density (null_measure M) f) A = emeasure (null_measure M) A"
+ by (simp add: density_def) (simp only: null_measure_def[symmetric] emeasure_null_measure)
+qed simp
+
subsubsection {* Uniform count measure *}
definition "uniform_count_measure A = point_measure A (\<lambda>x. 1 / card A)"
--- a/src/HOL/Probability/Probability_Mass_Function.thy Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Thu Jan 22 14:51:08 2015 +0100
@@ -12,16 +12,6 @@
"~~/src/HOL/Library/Multiset"
begin
-lemma bind_return'': "sets M = sets N \<Longrightarrow> M \<guillemotright>= return N = M"
- by (cases "space M = {}")
- (simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return'
- cong: subprob_algebra_cong)
-
-
-lemma (in prob_space) distr_const[simp]:
- "c \<in> space N \<Longrightarrow> distr M N (\<lambda>x. c) = return N c"
- by (rule measure_eqI) (auto simp: emeasure_distr emeasure_space_1)
-
lemma (in finite_measure) countable_support:
"countable {x. measure M {x} \<noteq> 0}"
proof cases
@@ -214,8 +204,7 @@
by (subst emeasure_eq_setsum_singleton) (auto simp: emeasure_pmf_single)
lemma measure_measure_pmf_finite: "finite S \<Longrightarrow> measure (measure_pmf M) S = setsum (pmf M) S"
-using emeasure_measure_pmf_finite[of S M]
-by(simp add: measure_pmf.emeasure_eq_measure)
+ using emeasure_measure_pmf_finite[of S M] by(simp add: measure_pmf.emeasure_eq_measure)
lemma nn_integral_measure_pmf_support:
fixes f :: "'a \<Rightarrow> ereal"
@@ -759,33 +748,34 @@
intro!: measure_pmf.integrable_const_bound[where B=1])
done
+
lemma measurable_pair_restrict_pmf2:
assumes "countable A"
- assumes "\<And>y. y \<in> A \<Longrightarrow> (\<lambda>x. f (x, y)) \<in> measurable M L"
- shows "f \<in> measurable (M \<Otimes>\<^sub>M restrict_space (measure_pmf N) A) L"
- apply (subst measurable_cong_sets)
- apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
- apply (simp_all add: restrict_count_space)
- apply (subst split_eta[symmetric])
- unfolding measurable_split_conv
- apply (rule measurable_compose_countable'[OF _ measurable_snd `countable A`])
- apply (rule measurable_compose[OF measurable_fst])
- apply fact
- done
+ assumes [measurable]: "\<And>y. y \<in> A \<Longrightarrow> (\<lambda>x. f (x, y)) \<in> measurable M L"
+ shows "f \<in> measurable (M \<Otimes>\<^sub>M restrict_space (measure_pmf N) A) L" (is "f \<in> measurable ?M _")
+proof -
+ have [measurable_cong]: "sets (restrict_space (count_space UNIV) A) = sets (count_space A)"
+ by (simp add: restrict_count_space)
+
+ show ?thesis
+ by (intro measurable_compose_countable'[where f="\<lambda>a b. f (fst b, a)" and g=snd and I=A,
+ unfolded pair_collapse] assms)
+ measurable
+qed
lemma measurable_pair_restrict_pmf1:
assumes "countable A"
- assumes "\<And>x. x \<in> A \<Longrightarrow> (\<lambda>y. f (x, y)) \<in> measurable N L"
+ assumes [measurable]: "\<And>x. x \<in> A \<Longrightarrow> (\<lambda>y. f (x, y)) \<in> measurable N L"
shows "f \<in> measurable (restrict_space (measure_pmf M) A \<Otimes>\<^sub>M N) L"
- apply (subst measurable_cong_sets)
- apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
- apply (simp_all add: restrict_count_space)
- apply (subst split_eta[symmetric])
- unfolding measurable_split_conv
- apply (rule measurable_compose_countable'[OF _ measurable_fst `countable A`])
- apply (rule measurable_compose[OF measurable_snd])
- apply fact
- done
+proof -
+ have [measurable_cong]: "sets (restrict_space (count_space UNIV) A) = sets (count_space A)"
+ by (simp add: restrict_count_space)
+
+ show ?thesis
+ by (intro measurable_compose_countable'[where f="\<lambda>a b. f (a, snd b)" and g=fst and I=A,
+ unfolded pair_collapse] assms)
+ measurable
+qed
lemma bind_commute_pmf: "bind_pmf A (\<lambda>x. bind_pmf B (C x)) = bind_pmf B (\<lambda>y. bind_pmf A (\<lambda>x. C x y))"
unfolding pmf_eq_iff pmf_bind
@@ -993,11 +983,6 @@
map_pmf fst pq = p; map_pmf snd pq = q \<rbrakk>
\<Longrightarrow> rel_pmf R p q"
-lemma nn_integral_count_space_eq:
- "(\<And>x. x \<in> A - B \<Longrightarrow> f x = 0) \<Longrightarrow> (\<And>x. x \<in> B - A \<Longrightarrow> f x = 0) \<Longrightarrow>
- (\<integral>\<^sup>+x. f x \<partial>count_space A) = (\<integral>\<^sup>+x. f x \<partial>count_space B)"
- by (auto simp: nn_integral_count_space_indicator intro!: nn_integral_cong split: split_indicator)
-
bnf pmf: "'a pmf" map: map_pmf sets: set_pmf bd : "natLeq" rel: rel_pmf
proof -
show "map_pmf id = id" by (rule map_pmf_id)
--- a/src/HOL/Probability/Probability_Measure.thy Thu Jan 22 13:21:45 2015 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy Thu Jan 22 14:51:08 2015 +0100
@@ -23,6 +23,9 @@
show "prob_space M" by default fact
qed
+lemma prob_space_imp_sigma_finite: "prob_space M \<Longrightarrow> sigma_finite_measure M"
+ unfolding prob_space_def finite_measure_def by simp
+
abbreviation (in prob_space) "events \<equiv> sets M"
abbreviation (in prob_space) "prob \<equiv> measure M"
abbreviation (in prob_space) "random_variable M' X \<equiv> X \<in> measurable M M'"