# HG changeset patch
# User hoelzl
# Date 1349863952 -7200
# Node ID 28066863284cdc2fc460c088b7017cac4234cebe
# Parent  182fa22e7ee8c1c8bb0a71e4d719971ca17fe0e1
add induction rules for simple functions and for Borel measurable functions

diff -r 182fa22e7ee8 -r 28066863284c src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Wed Oct 10 12:12:32 2012 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Wed Oct 10 12:12:32 2012 +0200
@@ -391,8 +391,8 @@
   assumes u: "simple_function M u" and nn: "AE x in M. 0 \<le> u x"
   assumes cong: "\<And>f g. simple_function M f \<Longrightarrow> simple_function M g \<Longrightarrow> (AE x in M. f x = g x) \<Longrightarrow> P f \<Longrightarrow> P g"
   assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)"
-  assumes mult: "\<And>u c. 0 \<le> c \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)"
-  assumes add: "\<And>u v. P u \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)"
+  assumes mult: "\<And>u c. 0 \<le> c \<Longrightarrow> simple_function M u \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)"
+  assumes add: "\<And>u v. simple_function M u \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> simple_function M v \<Longrightarrow> (\<And>x. 0 \<le> v x) \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)"
   shows "P u"
 proof -
   def v \<equiv> "max 0 \<circ> u"
@@ -426,7 +426,8 @@
     proof induct
       case empty show ?case
         using set[of "{}"] by (simp add: indicator_def[abs_def])
-    qed (auto intro!: add mult set simple_functionD v)
+    qed (auto intro!: add mult set simple_functionD v setsum_nonneg
+       simple_function_setsum)
   qed fact
 qed
 
@@ -435,17 +436,20 @@
   assumes u: "u \<in> borel_measurable M" "AE x in M. 0 \<le> u x"
   assumes cong: "\<And>f g. f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. f x = g x) \<Longrightarrow> P f \<Longrightarrow> P g"
   assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)"
-  assumes mult: "\<And>u c. 0 \<le> c \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)"
-  assumes add: "\<And>u v. P u \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)"
-  assumes seq: "\<And>U. (\<And>i. P (U i)) \<Longrightarrow> incseq U \<Longrightarrow> P (SUP i. U i)"
+  assumes mult: "\<And>u c. 0 \<le> c \<Longrightarrow> u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> P (\<lambda>x. c * u x)"
+  assumes add: "\<And>u v. u \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> u x) \<Longrightarrow> P u \<Longrightarrow> v \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 \<le> v x) \<Longrightarrow> P v \<Longrightarrow> P (\<lambda>x. v x + u x)"
+  assumes seq: "\<And>U. (\<And>i. U i \<in> borel_measurable M) \<Longrightarrow>  (\<And>i x. 0 \<le> U i x) \<Longrightarrow>  (\<And>i. P (U i)) \<Longrightarrow> incseq U \<Longrightarrow> P (SUP i. U i)"
   shows "P u"
   using u
 proof (induct rule: borel_measurable_implies_simple_function_sequence')
-  fix U assume "\<And>i. simple_function M (U i)" "incseq U" "\<And>i. \<infinity> \<notin> range (U i)" and
+  fix U assume U: "\<And>i. simple_function M (U i)" "incseq U" "\<And>i. \<infinity> \<notin> range (U i)" and
     sup: "\<And>x. (SUP i. U i x) = max 0 (u x)" and nn: "\<And>i x. 0 \<le> U i x"
   have u_eq: "max 0 \<circ> u = (SUP i. U i)" and "\<And>i. AE x in M. 0 \<le> U i x"
     using nn u sup by (auto simp: max_def)
   
+  from U have "\<And>i. U i \<in> borel_measurable M"
+    by (simp add: borel_measurable_simple_function)
+
   have "max 0 \<circ> u \<in> borel_measurable M" "u \<in> borel_measurable M"
     by (auto intro!: measurable_comp u borel_measurable_ereal_max simp: id_def[symmetric])
   moreover have "AE x in M. (max 0 \<circ> u) x = u x"
@@ -457,7 +461,7 @@
       using `simple_function M (U i)` `AE x in M. 0 \<le> U i x`
       by (induct rule: simple_function_induct_nn)
          (auto intro: set mult add cong dest!: borel_measurable_simple_function)
-  qed fact
+  qed fact+
   ultimately show "P u"
     by fact
 qed
@@ -777,32 +781,6 @@
   shows "integral\<^isup>S M f = (\<integral>\<^isup>Sx. f x * indicator S x \<partial>M)"
   using assms by (intro simple_integral_cong_AE) auto
 
-lemma simple_integral_distr:
-  assumes T: "T \<in> measurable M M'"
-    and f: "simple_function M' f"
-  shows "integral\<^isup>S (distr M M' T) f = (\<integral>\<^isup>S x. f (T x) \<partial>M)"
-  unfolding simple_integral_def
-proof (intro setsum_mono_zero_cong_right ballI)
-  show "(\<lambda>x. f (T x)) ` space M \<subseteq> f ` space (distr M M' T)"
-    using T unfolding measurable_def by auto
-  show "finite (f ` space (distr M M' T))"
-    using f unfolding simple_function_def by auto
-next
-  fix i assume "i \<in> f ` space (distr M M' T) - (\<lambda>x. f (T x)) ` space M"
-  then have "T -` (f -` {i} \<inter> space (distr M M' T)) \<inter> space M = {}" by (auto simp: image_iff)
-  with f[THEN simple_functionD(2), of "{i}"]
-  show "i * emeasure (distr M M' T) (f -` {i} \<inter> space (distr M M' T)) = 0"
-    using T by (simp add: emeasure_distr)
-next
-  fix i assume "i \<in> (\<lambda>x. f (T x)) ` space M"
-  then have "T -` (f -` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) -` {i} \<inter> space M"
-    using T unfolding measurable_def by auto
-  with f[THEN simple_functionD(2), of "{i}"] T
-  show "i * emeasure (distr M M' T) (f -` {i} \<inter> space (distr M M' T)) =
-      i * (emeasure M) ((\<lambda>x. f (T x)) -` {i} \<inter> space M)"
-    by (auto simp add: emeasure_distr)
-qed
-
 lemma simple_integral_cmult_indicator:
   assumes A: "A \<in> sets M"
   shows "(\<integral>\<^isup>Sx. c * indicator A x \<partial>M) = c * (emeasure M) A"
@@ -2330,45 +2308,43 @@
 
 section {* Distributions *}
 
-lemma simple_function_distr[simp]:
-  "simple_function (distr M M' T) f \<longleftrightarrow> simple_function M' (\<lambda>x. f x)"
- unfolding simple_function_def by simp
+lemma positive_integral_distr':
+  assumes T: "T \<in> measurable M M'"
+  and f: "f \<in> borel_measurable (distr M M' T)" "AE x in (distr M M' T). 0 \<le> f x"
+  shows "integral\<^isup>P (distr M M' T) f = (\<integral>\<^isup>+ x. f (T x) \<partial>M)"
+  using f 
+proof induct
+  case (cong f g)
+  then have eq: "AE x in (distr M M' T). g x = f x" "AE x in M. g (T x) = f (T x)"
+    by (auto dest: AE_distrD[OF T])
+  show ?case
+    apply (subst eq(1)[THEN positive_integral_cong_AE])
+    apply (subst eq(2)[THEN positive_integral_cong_AE])
+    apply fact
+    done
+next
+  case (set A)
+  then have eq: "\<And>x. x \<in> space M \<Longrightarrow> indicator A (T x) = indicator (T -` A \<inter> space M) x"
+    by (auto simp: indicator_def)
+  from set T show ?case
+    by (subst positive_integral_cong[OF eq])
+       (auto simp add: emeasure_distr intro!: positive_integral_indicator[symmetric] measurable_sets)
+next
+  case (seq U) 
+  moreover then have "incseq (\<lambda>i x. U i (T x))"
+    by (force simp: le_fun_def incseq_def)
+  ultimately show ?case
+    by (simp_all add: measurable_compose[OF T] positive_integral_monotone_convergence_SUP)
+qed (simp_all add: measurable_compose[OF T] T positive_integral_cmult positive_integral_add)
 
 lemma positive_integral_distr:
   assumes T: "T \<in> measurable M M'"
   and f: "f \<in> borel_measurable M'"
   shows "integral\<^isup>P (distr M M' T) f = (\<integral>\<^isup>+ x. f (T x) \<partial>M)"
-proof -
-  from borel_measurable_implies_simple_function_sequence'[OF f]
-  guess f' . note f' = this
-  then have f_distr: "\<And>i. simple_function (distr M M' T) (f' i)"
-    by simp
-  let ?f = "\<lambda>i x. f' i (T x)"
-  have inc: "incseq ?f" using f' by (force simp: le_fun_def incseq_def)
-  have sup: "\<And>x. (SUP i. ?f i x) = max 0 (f (T x))"
-    using f'(4) .
-  have sf: "\<And>i. simple_function M (\<lambda>x. f' i (T x))"
-    using simple_function_comp[OF T(1) f'(1)] .
-  show "integral\<^isup>P (distr M M' T) f = (\<integral>\<^isup>+ x. f (T x) \<partial>M)"
-    using
-      positive_integral_monotone_convergence_simple[OF f'(2,5) f_distr]
-      positive_integral_monotone_convergence_simple[OF inc f'(5) sf]
-    by (simp add: positive_integral_max_0 simple_integral_distr[OF T f'(1)] f')
-qed
-
-lemma integral_distr:
-  assumes T: "T \<in> measurable M M'"
-  assumes f: "f \<in> borel_measurable M'"
-  shows "integral\<^isup>L (distr M M' T) f = (\<integral>x. f (T x) \<partial>M)"
-proof -
-  from measurable_comp[OF T, of f borel]
-  have borel: "(\<lambda>x. ereal (f x)) \<in> borel_measurable M'" "(\<lambda>x. ereal (- f x)) \<in> borel_measurable M'"
-    and "(\<lambda>x. f (T x)) \<in> borel_measurable M"
-    using f by (auto simp: comp_def)
-  then show ?thesis
-    using f unfolding lebesgue_integral_def integrable_def
-    by (auto simp: borel[THEN positive_integral_distr[OF T]])
-qed
+  apply (subst (1 2) positive_integral_max_0[symmetric])
+  apply (rule positive_integral_distr')
+  apply (auto simp: f T)
+  done
 
 lemma integrable_distr_eq:
   assumes T: "T \<in> measurable M M'" "f \<in> borel_measurable M'"