--- a/src/HOL/Library/Indicator_Function.thy Wed Nov 11 10:08:09 2015 +0100
+++ b/src/HOL/Library/Indicator_Function.thy Wed Nov 11 10:13:40 2015 +0100
@@ -60,6 +60,9 @@
lemma indicator_image: "inj f \<Longrightarrow> indicator (f ` X) (f x) = (indicator X x::_::zero_neq_one)"
by (auto simp: indicator_def inj_on_def)
+lemma indicator_vimage: "indicator (f -` A) x = indicator A (f x)"
+by(auto split: split_indicator)
+
lemma
fixes f :: "'a \<Rightarrow> 'b::semiring_1" assumes "finite A"
shows setsum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator B x) = (\<Sum>x \<in> A \<inter> B. f x)"
--- a/src/HOL/Probability/Measure_Space.thy Wed Nov 11 10:08:09 2015 +0100
+++ b/src/HOL/Probability/Measure_Space.thy Wed Nov 11 10:13:40 2015 +0100
@@ -1421,6 +1421,9 @@
using emeasure_nonneg[of M A]
by (cases "emeasure M A") (auto simp: measure_def)
+lemma max_0_ereal_measure [simp]: "max 0 (ereal (measure M X)) = ereal (measure M X)"
+by(simp add: max_def measure_nonneg)
+
lemma measure_Union:
assumes finite: "emeasure M A \<noteq> \<infinity>" "emeasure M B \<noteq> \<infinity>"
and measurable: "A \<in> sets M" "B \<in> sets M" "A \<inter> B = {}"
@@ -2100,6 +2103,9 @@
lemma measure_null_measure[simp]: "measure (null_measure M) X = 0"
by (simp add: measure_def)
+lemma null_measure_idem [simp]: "null_measure (null_measure M) = null_measure M"
+by(rule measure_eqI) simp_all
+
subsection \<open>Measures form a chain-complete partial order\<close>
instantiation measure :: (type) order_bot
@@ -2270,4 +2276,16 @@
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)"
+unfolding SUP_def by(rule space_Sup[OF A a(2) imageI[OF a(1)]] sets_Sup[OF A a(2) imageI[OF a(1)]])+
+
+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> unfolding SUP_def by(subst emeasure_Sup[OF A(1)]; simp add: A)
+
end
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Wed Nov 11 10:08:09 2015 +0100
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Wed Nov 11 10:13:40 2015 +0100
@@ -2710,4 +2710,13 @@
"finite A \<Longrightarrow> X \<subseteq> A \<Longrightarrow> measure (uniform_count_measure A) X = card X / card A"
by (simp add: emeasure_point_measure_finite uniform_count_measure_def measure_def)
+lemma space_uniform_count_measure_empty_iff [simp]:
+ "space (uniform_count_measure X) = {} \<longleftrightarrow> X = {}"
+by(simp add: space_uniform_count_measure)
+
+lemma sets_uniform_count_measure_eq_UNIV [simp]:
+ "sets (uniform_count_measure UNIV) = UNIV \<longleftrightarrow> True"
+ "UNIV = sets (uniform_count_measure UNIV) \<longleftrightarrow> True"
+by(simp_all add: sets_uniform_count_measure)
+
end
--- a/src/HOL/Probability/Sigma_Algebra.thy Wed Nov 11 10:08:09 2015 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy Wed Nov 11 10:13:40 2015 +0100
@@ -298,6 +298,10 @@
finally show ?thesis .
qed
+lemma (in sigma_algebra) countable_UN'':
+ "\<lbrakk> countable X; \<And>x y. x \<in> X \<Longrightarrow> A x \<in> M \<rbrakk> \<Longrightarrow> (\<Union>x\<in>X. A x) \<in> M"
+by(erule countable_UN')(auto)
+
lemma (in sigma_algebra) countable_INT [intro]:
fixes A :: "'i::countable \<Rightarrow> 'a set"
assumes A: "A`X \<subseteq> M" "X \<noteq> {}"