# HG changeset patch
# User paulson
# Date 1257781815 0
# Node ID 40b44cb20c8c1c38b8515f7d704fb47d85a880c7
# Parent  535789c26230f227233352df4abd4de57000e598
New theory Probability/Borel.thy, and some associated lemmas

diff -r 535789c26230 -r 40b44cb20c8c src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Nov 09 11:34:22 2009 +0100
+++ b/src/HOL/IsaMakefile	Mon Nov 09 15:50:15 2009 +0000
@@ -1069,7 +1069,8 @@
   Probability/Sigma_Algebra.thy \
   Probability/SeriesPlus.thy \
   Probability/Caratheodory.thy \
-  Probability/Measure.thy
+  Probability/Measure.thy \
+  Probability/Borel.thy
 	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Probability
 
 
diff -r 535789c26230 -r 40b44cb20c8c src/HOL/Probability/Borel.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Borel.thy	Mon Nov 09 15:50:15 2009 +0000
@@ -0,0 +1,425 @@
+header {*Borel Sets*}
+
+theory Borel
+  imports Measure
+begin
+
+text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
+
+definition borel_space where
+  "borel_space = sigma (UNIV::real set) (range (\<lambda>a::real. {x. x \<le> a}))"
+
+definition borel_measurable where
+  "borel_measurable a = measurable a borel_space"
+
+definition indicator_fn where
+  "indicator_fn s = (\<lambda>x. if x \<in> s then 1 else (0::real))"
+
+definition mono_convergent where
+  "mono_convergent u f s \<equiv>
+	(\<forall>x m n. m \<le> n \<and> x \<in> s \<longrightarrow> u m x \<le> u n x) \<and>
+	(\<forall>x \<in> s. (\<lambda>i. u i x) ----> f x)"
+
+lemma in_borel_measurable:
+   "f \<in> borel_measurable M \<longleftrightarrow>
+    sigma_algebra M \<and>
+    (\<forall>s \<in> sets (sigma UNIV (range (\<lambda>a::real. {x. x \<le> a}))).
+      f -` s \<inter> space M \<in> sets M)"
+apply (auto simp add: borel_measurable_def measurable_def borel_space_def) 
+apply (metis PowD UNIV_I Un_commute sigma_algebra_sigma subset_Pow_Union subset_UNIV subset_Un_eq) 
+done
+
+lemma (in sigma_algebra) borel_measurable_const:
+   "(\<lambda>x. c) \<in> borel_measurable M"
+  by (auto simp add: in_borel_measurable prems)
+
+lemma (in sigma_algebra) borel_measurable_indicator:
+  assumes a: "a \<in> sets M"
+  shows "indicator_fn a \<in> borel_measurable M"
+apply (auto simp add: in_borel_measurable indicator_fn_def prems)
+apply (metis Diff_eq Int_commute a compl_sets) 
+done
+
+lemma Collect_eq: "{w \<in> X. f w \<le> a} = {w. f w \<le> a} \<inter> X"
+  by (metis Collect_conj_eq Collect_mem_eq Int_commute)
+
+lemma (in measure_space) borel_measurable_le_iff:
+   "f \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M)"
+proof 
+  assume f: "f \<in> borel_measurable M"
+  { fix a
+    have "{w \<in> space M. f w \<le> a} \<in> sets M" using f
+      apply (auto simp add: in_borel_measurable sigma_def Collect_eq)
+      apply (drule_tac x="{x. x \<le> a}" in bspec, auto)
+      apply (metis equalityE rangeI subsetD sigma_sets.Basic)  
+      done
+    }
+  thus "\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M" by blast
+next
+  assume "\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M"
+  thus "f \<in> borel_measurable M" 
+    apply (simp add: borel_measurable_def borel_space_def Collect_eq) 
+    apply (rule measurable_sigma, auto) 
+    done
+qed
+
+lemma Collect_less_le:
+     "{w \<in> X. f w < g w} = (\<Union>n. {w \<in> X. f w \<le> g w - inverse(real(Suc n))})"
+  proof auto
+    fix w
+    assume w: "f w < g w"
+    hence nz: "g w - f w \<noteq> 0"
+      by arith
+    with w have "real(Suc(natceiling(inverse(g w - f w)))) > inverse(g w - f w)"
+      by (metis lessI order_le_less_trans real_natceiling_ge real_of_nat_less_iff)       hence "inverse(real(Suc(natceiling(inverse(g w - f w)))))
+             < inverse(inverse(g w - f w))" 
+      by (metis less_iff_diff_less_0 less_imp_inverse_less linorder_neqE_ordered_idom nz positive_imp_inverse_positive real_le_anti_sym real_less_def w)
+    hence "inverse(real(Suc(natceiling(inverse(g w - f w))))) < g w - f w"
+      by (metis inverse_inverse_eq order_less_le_trans real_le_refl) 
+    thus "\<exists>n. f w \<le> g w - inverse(real(Suc n))" using w
+      by (rule_tac x="natceiling(inverse(g w - f w))" in exI, auto)
+  next
+    fix w n
+    assume le: "f w \<le> g w - inverse(real(Suc n))"
+    hence "0 < inverse(real(Suc n))"
+      by (metis inverse_real_of_nat_gt_zero)
+    thus "f w < g w" using le
+      by arith 
+  qed
+
+
+lemma (in sigma_algebra) sigma_le_less:
+  assumes M: "!!a::real. {w \<in> space M. f w \<le> a} \<in> sets M"
+  shows "{w \<in> space M. f w < a} \<in> sets M"
+proof -
+  show ?thesis using Collect_less_le [of "space M" f "\<lambda>x. a"]
+    by (auto simp add: countable_UN M) 
+qed
+
+lemma (in sigma_algebra) sigma_less_ge:
+  assumes M: "!!a::real. {w \<in> space M. f w < a} \<in> sets M"
+  shows "{w \<in> space M. a \<le> f w} \<in> sets M"
+proof -
+  have "{w \<in> space M. a \<le> f w} = space M - {w \<in> space M. f w < a}"
+    by auto
+  thus ?thesis using M
+    by auto
+qed
+
+lemma (in sigma_algebra) sigma_ge_gr:
+  assumes M: "!!a::real. {w \<in> space M. a \<le> f w} \<in> sets M"
+  shows "{w \<in> space M. a < f w} \<in> sets M"
+proof -
+  show ?thesis using Collect_less_le [of "space M" "\<lambda>x. a" f]
+    by (auto simp add: countable_UN le_diff_eq M) 
+qed
+
+lemma (in sigma_algebra) sigma_gr_le:
+  assumes M: "!!a::real. {w \<in> space M. a < f w} \<in> sets M"
+  shows "{w \<in> space M. f w \<le> a} \<in> sets M"
+proof -
+  have "{w \<in> space M. f w \<le> a} = space M - {w \<in> space M. a < f w}" 
+    by auto
+  thus ?thesis
+    by (simp add: M compl_sets)
+qed
+
+lemma (in measure_space) borel_measurable_gr_iff:
+   "f \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a < f w} \<in> sets M)"
+proof (auto simp add: borel_measurable_le_iff sigma_gr_le) 
+  fix u
+  assume M: "\<forall>a. {w \<in> space M. f w \<le> a} \<in> sets M"
+  have "{w \<in> space M. u < f w} = space M - {w \<in> space M. f w \<le> u}"
+    by auto
+  thus "{w \<in> space M. u < f w} \<in> sets M"
+    by (force simp add: compl_sets countable_UN M)
+qed
+
+lemma (in measure_space) borel_measurable_less_iff:
+   "f \<in> borel_measurable M = (\<forall>a. {w \<in> space M. f w < a} \<in> sets M)"
+proof (auto simp add: borel_measurable_le_iff sigma_le_less) 
+  fix u
+  assume M: "\<forall>a. {w \<in> space M. f w < a} \<in> sets M"
+  have "{w \<in> space M. f w \<le> u} = space M - {w \<in> space M. u < f w}"
+    by auto
+  thus "{w \<in> space M. f w \<le> u} \<in> sets M"
+    using Collect_less_le [of "space M" "\<lambda>x. u" f] 
+    by (force simp add: compl_sets countable_UN le_diff_eq sigma_less_ge M)
+qed
+
+lemma (in measure_space) borel_measurable_ge_iff:
+   "f \<in> borel_measurable M = (\<forall>a. {w \<in> space M. a \<le> f w} \<in> sets M)"
+proof (auto simp add: borel_measurable_less_iff sigma_le_less sigma_ge_gr sigma_gr_le) 
+  fix u
+  assume M: "\<forall>a. {w \<in> space M. f w < a} \<in> sets M"
+  have "{w \<in> space M. u \<le> f w} = space M - {w \<in> space M. f w < u}"
+    by auto
+  thus "{w \<in> space M. u \<le> f w} \<in> sets M"
+    by (force simp add: compl_sets countable_UN M)
+qed
+
+lemma (in measure_space) affine_borel_measurable:
+  assumes g: "g \<in> borel_measurable M"
+  shows "(\<lambda>x. a + (g x) * b) \<in> borel_measurable M"
+proof (cases rule: linorder_cases [of b 0])
+  case equal thus ?thesis
+    by (simp add: borel_measurable_const)
+next
+  case less
+    {
+      fix w c
+      have "a + g w * b \<le> c \<longleftrightarrow> g w * b \<le> c - a"
+        by auto
+      also have "... \<longleftrightarrow> (c-a)/b \<le> g w" using less
+        by (metis divide_le_eq less less_asym)
+      finally have "a + g w * b \<le> c \<longleftrightarrow> (c-a)/b \<le> g w" .
+    }
+    hence "\<And>w c. a + g w * b \<le> c \<longleftrightarrow> (c-a)/b \<le> g w" .
+    thus ?thesis using less g
+      by (simp add: borel_measurable_ge_iff [of g]) 
+         (simp add: borel_measurable_le_iff)
+next
+  case greater
+    hence 0: "\<And>x c. (g x * b \<le> c - a) \<longleftrightarrow> (g x \<le> (c - a) / b)"
+      by (metis mult_imp_le_div_pos le_divide_eq) 
+    have 1: "\<And>x c. (a + g x * b \<le> c) \<longleftrightarrow> (g x * b \<le> c - a)"
+      by auto
+    from greater g
+    show ?thesis
+      by (simp add: borel_measurable_le_iff 0 1) 
+qed
+
+definition
+  nat_to_rat_surj :: "nat \<Rightarrow> rat" where
+ "nat_to_rat_surj n = (let (i,j) = nat_to_nat2 n
+                       in Fract (nat_to_int_bij i) (nat_to_int_bij j))"
+
+lemma nat_to_rat_surj: "surj nat_to_rat_surj"
+proof (auto simp add: surj_def nat_to_rat_surj_def) 
+  fix y
+  show "\<exists>x. y = (\<lambda>(i, j). Fract (nat_to_int_bij i) (nat_to_int_bij j)) (nat_to_nat2 x)"
+  proof (cases y)
+    case (Fract a b)
+      obtain i where i: "nat_to_int_bij i = a" using surj_nat_to_int_bij
+        by (metis surj_def) 
+      obtain j where j: "nat_to_int_bij j = b" using surj_nat_to_int_bij
+        by (metis surj_def)
+      obtain n where n: "nat_to_nat2 n = (i,j)" using nat_to_nat2_surj
+        by (metis surj_def)
+
+      from Fract i j n show ?thesis
+        by (metis prod.cases prod_case_split)
+  qed
+qed
+
+lemma rats_enumeration: "\<rat> = range (of_rat o nat_to_rat_surj)" 
+  using nat_to_rat_surj
+  by (auto simp add: image_def surj_def) (metis Rats_cases) 
+
+lemma (in measure_space) borel_measurable_less_borel_measurable:
+  assumes f: "f \<in> borel_measurable M"
+  assumes g: "g \<in> borel_measurable M"
+  shows "{w \<in> space M. f w < g w} \<in> sets M"
+proof -
+  have "{w \<in> space M. f w < g w} =
+	(\<Union>r\<in>\<rat>. {w \<in> space M. f w < r} \<inter> {w \<in> space M. r < g w })"
+    by (auto simp add: Rats_dense_in_real)
+  thus ?thesis using f g 
+    by (simp add: borel_measurable_less_iff [of f]  
+                  borel_measurable_gr_iff [of g]) 
+       (blast intro: gen_countable_UN [OF rats_enumeration])
+qed
+ 
+lemma (in measure_space) borel_measurable_leq_borel_measurable:
+  assumes f: "f \<in> borel_measurable M"
+  assumes g: "g \<in> borel_measurable M"
+  shows "{w \<in> space M. f w \<le> g w} \<in> sets M"
+proof -
+  have "{w \<in> space M. f w \<le> g w} = space M - {w \<in> space M. g w < f w}" 
+    by auto 
+  thus ?thesis using f g 
+    by (simp add: borel_measurable_less_borel_measurable compl_sets)
+qed
+
+lemma (in measure_space) borel_measurable_eq_borel_measurable:
+  assumes f: "f \<in> borel_measurable M"
+  assumes g: "g \<in> borel_measurable M"
+  shows "{w \<in> space M. f w = g w} \<in> sets M"
+proof -
+  have "{w \<in> space M. f w = g w} =
+	{w \<in> space M. f w \<le> g w} \<inter> {w \<in> space M. g w \<le> f w}"
+    by auto
+  thus ?thesis using f g 
+    by (simp add: borel_measurable_leq_borel_measurable Int) 
+qed
+
+lemma (in measure_space) borel_measurable_neq_borel_measurable:
+  assumes f: "f \<in> borel_measurable M"
+  assumes g: "g \<in> borel_measurable M"
+  shows "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
+proof -
+  have "{w \<in> space M. f w \<noteq> g w} = space M - {w \<in> space M. f w = g w}"
+    by auto
+  thus ?thesis using f g 
+    by (simp add: borel_measurable_eq_borel_measurable compl_sets) 
+qed
+
+lemma (in measure_space) borel_measurable_plus_borel_measurable:
+  assumes f: "f \<in> borel_measurable M"
+  assumes g: "g \<in> borel_measurable M"
+  shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
+proof -
+  have 1:"!!a. {w \<in> space M. a \<le> f w + g w} = {w \<in> space M. a + (g w) * -1 \<le> f w}"
+    by auto
+  have "!!a. (\<lambda>w. a + (g w) * -1) \<in> borel_measurable M"
+    by (rule affine_borel_measurable [OF g]) 
+  hence "!!a. {w \<in> space M. (\<lambda>w. a + (g w) * -1)(w) \<le> f w} \<in> sets M" using f
+    by (rule borel_measurable_leq_borel_measurable) 
+  hence "!!a. {w \<in> space M. a \<le> f w + g w} \<in> sets M"
+    by (simp add: 1) 
+  thus ?thesis
+    by (simp add: borel_measurable_ge_iff) 
+qed
+
+
+lemma (in measure_space) borel_measurable_square:
+  assumes f: "f \<in> borel_measurable M"
+  shows "(\<lambda>x. (f x)^2) \<in> borel_measurable M"
+proof -
+  {
+    fix a
+    have "{w \<in> space M. (f w)\<twosuperior> \<le> a} \<in> sets M"
+    proof (cases rule: linorder_cases [of a 0])
+      case less
+      hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} = {}" 
+        by auto (metis less order_le_less_trans power2_less_0)
+      also have "... \<in> sets M"
+        by (rule empty_sets) 
+      finally show ?thesis .
+    next
+      case equal
+      hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} = 
+             {w \<in> space M. f w \<le> 0} \<inter> {w \<in> space M. 0 \<le> f w}"
+        by auto
+      also have "... \<in> sets M"
+        apply (insert f) 
+        apply (rule Int) 
+        apply (simp add: borel_measurable_le_iff)
+        apply (simp add: borel_measurable_ge_iff)
+        done
+      finally show ?thesis .
+    next
+      case greater
+      have "\<forall>x. (f x ^ 2 \<le> sqrt a ^ 2) = (- sqrt a  \<le> f x & f x \<le> sqrt a)"
+        by (metis abs_le_interval_iff abs_of_pos greater real_sqrt_abs
+                  real_sqrt_le_iff real_sqrt_power)
+      hence "{w \<in> space M. (f w)\<twosuperior> \<le> a} =
+             {w \<in> space M. -(sqrt a) \<le> f w} \<inter> {w \<in> space M. f w \<le> sqrt a}" 
+        using greater by auto
+      also have "... \<in> sets M"
+        apply (insert f) 
+        apply (rule Int) 
+        apply (simp add: borel_measurable_ge_iff)
+        apply (simp add: borel_measurable_le_iff)
+        done
+      finally show ?thesis .
+    qed
+  }
+  thus ?thesis by (auto simp add: borel_measurable_le_iff) 
+qed
+
+lemma times_eq_sum_squares:
+   fixes x::real
+   shows"x*y = ((x+y)^2)/4 - ((x-y)^ 2)/4"
+by (simp add: power2_eq_square ring_distribs diff_divide_distrib [symmetric]) 
+
+
+lemma (in measure_space) borel_measurable_uminus_borel_measurable:
+  assumes g: "g \<in> borel_measurable M"
+  shows "(\<lambda>x. - g x) \<in> borel_measurable M"
+proof -
+  have "(\<lambda>x. - g x) = (\<lambda>x. 0 + (g x) * -1)"
+    by simp
+  also have "... \<in> borel_measurable M" 
+    by (fast intro: affine_borel_measurable g) 
+  finally show ?thesis .
+qed
+
+lemma (in measure_space) borel_measurable_times_borel_measurable:
+  assumes f: "f \<in> borel_measurable M"
+  assumes g: "g \<in> borel_measurable M"
+  shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
+proof -
+  have 1: "(\<lambda>x. 0 + (f x + g x)\<twosuperior> * inverse 4) \<in> borel_measurable M"
+    by (fast intro: affine_borel_measurable borel_measurable_square 
+                    borel_measurable_plus_borel_measurable f g) 
+  have "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) = 
+        (\<lambda>x. 0 + ((f x + -g x) ^ 2 * inverse -4))"
+    by (simp add: Ring_and_Field.minus_divide_right) 
+  also have "... \<in> borel_measurable M" 
+    by (fast intro: affine_borel_measurable borel_measurable_square 
+                    borel_measurable_plus_borel_measurable 
+                    borel_measurable_uminus_borel_measurable f g)
+  finally have 2: "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) \<in> borel_measurable M" .
+  show ?thesis
+    apply (simp add: times_eq_sum_squares real_diff_def) 
+    using 1 2 apply (simp add: borel_measurable_plus_borel_measurable) 
+    done
+qed
+
+lemma (in measure_space) borel_measurable_diff_borel_measurable:
+  assumes f: "f \<in> borel_measurable M"
+  assumes g: "g \<in> borel_measurable M"
+  shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
+unfolding real_diff_def
+  by (fast intro: borel_measurable_plus_borel_measurable 
+                  borel_measurable_uminus_borel_measurable f g)
+
+lemma (in measure_space) mono_convergent_borel_measurable:
+  assumes u: "!!n. u n \<in> borel_measurable M"
+  assumes mc: "mono_convergent u f (space M)"
+  shows "f \<in> borel_measurable M"
+proof -
+  {
+    fix a
+    have 1: "!!w. w \<in> space M & f w <= a \<longleftrightarrow> w \<in> space M & (\<forall>i. u i w <= a)"
+      proof safe
+        fix w i
+        assume w: "w \<in> space M" and f: "f w \<le> a"
+        hence "u i w \<le> f w"
+          by (auto intro: SEQ.incseq_le
+                   simp add: incseq_def mc [unfolded mono_convergent_def])
+        thus "u i w \<le> a" using f
+          by auto
+      next
+        fix w 
+        assume w: "w \<in> space M" and u: "\<forall>i. u i w \<le> a"
+        thus "f w \<le> a"
+          by (metis LIMSEQ_le_const2 mc [unfolded mono_convergent_def])
+      qed
+    have "{w \<in> space M. f w \<le> a} = {w \<in> space M. (\<forall>i. u i w <= a)}"
+      by (simp add: 1)
+    also have "... = (\<Inter>i. {w \<in> space M. u i w \<le> a})" 
+      by auto
+    also have "...  \<in> sets M" using u
+      by (auto simp add: borel_measurable_le_iff intro: countable_INT) 
+    finally have "{w \<in> space M. f w \<le> a} \<in> sets M" .
+  }
+  thus ?thesis 
+    by (auto simp add: borel_measurable_le_iff) 
+qed
+
+lemma (in measure_space) borel_measurable_SIGMA_borel_measurable:
+  assumes s: "finite s"
+  shows "(!!i. i \<in> s ==> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) s) \<in> borel_measurable M" using s
+proof (induct s)
+  case empty
+  thus ?case
+    by (simp add: borel_measurable_const)
+next
+  case (insert x s)
+  thus ?case
+    by (auto simp add: borel_measurable_plus_borel_measurable) 
+qed
+
+end
diff -r 535789c26230 -r 40b44cb20c8c src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Mon Nov 09 11:34:22 2009 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Mon Nov 09 15:50:15 2009 +0000
@@ -71,7 +71,7 @@
   assumes countable_UN [intro]:
          "!!A. range A \<subseteq> sets M \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
 
-lemma (in sigma_algebra) countable_INT:
+lemma (in sigma_algebra) countable_INT [intro]:
   assumes a: "range a \<subseteq> sets M"
   shows "(\<Inter>i::nat. a i) \<in> sets M"
 proof -
@@ -83,6 +83,15 @@
   ultimately show ?thesis by metis
 qed
 
+lemma (in sigma_algebra) gen_countable_UN:
+  fixes f :: "nat \<Rightarrow> 'c"
+  shows  "I = range f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> (\<Union>x\<in>I. A x) \<in> sets M"
+by auto
+
+lemma (in sigma_algebra) gen_countable_INT:
+  fixes f :: "nat \<Rightarrow> 'c"
+  shows  "I = range f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> (\<Inter>x\<in>I. A x) \<in> sets M"
+by auto
 
 lemma algebra_Pow:
      "algebra (| space = sp, sets = Pow sp |)"
diff -r 535789c26230 -r 40b44cb20c8c src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Nov 09 11:34:22 2009 +0100
+++ b/src/HOL/Set.thy	Mon Nov 09 15:50:15 2009 +0000
@@ -1645,6 +1645,14 @@
 lemma image_vimage_eq [simp]: "f ` (f -` A) = A Int range f"
 by blast
 
+lemma vimage_const [simp]: "((\<lambda>x. c) -` A) = (if c \<in> A then UNIV else {})"
+  by auto
+
+lemma vimage_if [simp]: "((\<lambda>x. if x \<in> B then c else d) -` A) = 
+   (if c \<in> A then (if d \<in> A then UNIV else B)
+    else if d \<in> A then -B else {})"  
+  by (auto simp add: vimage_def) 
+
 lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B"
 by blast