# HG changeset patch
# User Andreas Lochbihler
# Date 1447233220 -3600
# Node ID 64e6d712af165cd5b8409dc7f1a39e767466b3dc
# Parent  ec580491c5d27f0f72b48873902514f1bd0ea773
add lemmas

diff -r ec580491c5d2 -r 64e6d712af16 src/HOL/Library/Indicator_Function.thy
--- 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)"
diff -r ec580491c5d2 -r 64e6d712af16 src/HOL/Probability/Measure_Space.thy
--- 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
diff -r ec580491c5d2 -r 64e6d712af16 src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
--- 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
diff -r ec580491c5d2 -r 64e6d712af16 src/HOL/Probability/Sigma_Algebra.thy
--- 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> {}"