# HG changeset patch
# User hoelzl
# Date 1349863955 -7200
# Node ID f3471f09bb86d0dcd08b198d02ed830249d5af6e
# Parent  a6678da5692c2600946a43b69ad8196a219f743d
add induction for real Borel measurable functions

diff -r a6678da5692c -r f3471f09bb86 src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Wed Oct 10 12:12:34 2012 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Wed Oct 10 12:12:35 2012 +0200
@@ -695,6 +695,69 @@
   qed
 qed
 
+lemma borel_measurable_real_induct[consumes 2, case_names cong set mult add seq, induct set: borel_measurable]:
+  fixes u :: "'a \<Rightarrow> real"
+  assumes u: "u \<in> borel_measurable M" "\<And>x. 0 \<le> u x"
+  assumes cong: "\<And>f g. f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> P g \<Longrightarrow> P f"
+  assumes set: "\<And>A. A \<in> sets M \<Longrightarrow> P (indicator A)"
+  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 u. (\<And>i. U i \<in> borel_measurable M) \<Longrightarrow> (\<And>i x. 0 \<le> U i x) \<Longrightarrow> (\<And>x. (\<lambda>i. U i x) ----> u x) \<Longrightarrow> (\<And>i. P (U i)) \<Longrightarrow> incseq U \<Longrightarrow> P u"
+  shows "P u"
+proof -
+  have "(\<lambda>x. ereal (u x)) \<in> borel_measurable M"
+    using u by auto
+  then obtain U where U: "\<And>i. simple_function M (U i)" "incseq U" "\<And>i. \<infinity> \<notin> range (U i)" and
+    "\<And>x. (SUP i. U i x) = max 0 (ereal (u x))" and nn: "\<And>i x. 0 \<le> U i x"
+    using borel_measurable_implies_simple_function_sequence'[of u M] by auto
+  then have u_eq: "\<And>x. ereal (u x) = (SUP i. U i x)"
+    using u by (auto simp: max_def)
+
+  have [simp]: "\<And>i x. U i x \<noteq> \<infinity>" using U by (auto simp: image_def eq_commute)
+
+  { fix i x have [simp]: "U i x \<noteq> -\<infinity>" using nn[of i x] by auto }
+  note this[simp]
+
+  show "P u"
+  proof (rule seq)
+    show "\<And>i. (\<lambda>x. real (U i x)) \<in> borel_measurable M"
+      using U by (auto intro: borel_measurable_simple_function)
+    show "\<And>i x. 0 \<le> real (U i x)"
+      using nn by (auto simp: real_of_ereal_pos)
+    show "incseq (\<lambda>i x. real (U i x))"
+      using U(2) by (auto simp: incseq_def image_iff le_fun_def intro!: real_of_ereal_positive_mono nn)
+    then show "\<And>x. (\<lambda>i. real (U i x)) ----> u x"
+      by (intro SUP_eq_LIMSEQ[THEN iffD1])
+         (auto simp: incseq_mono incseq_def le_fun_def u_eq ereal_real
+               intro!: arg_cong2[where f=SUPR] ext)
+    show "\<And>i. P (\<lambda>x. real (U i x))"
+    proof (rule cong)
+      fix x i assume x: "x \<in> space M"
+      have [simp]: "\<And>A x. real (indicator A x :: ereal) = indicator A x"
+        by (auto simp: indicator_def one_ereal_def)
+      { fix y assume "y \<in> U i ` space M"
+        then have "0 \<le> y" "y \<noteq> \<infinity>" using nn by auto
+        then have "\<bar>y * indicator (U i -` {y} \<inter> space M) x\<bar> \<noteq> \<infinity>"
+          by (auto simp: indicator_def) }
+      then show "real (U i x) = (\<Sum>y \<in> U i ` space M. real y * indicator (U i -` {y} \<inter> space M) x)"
+        unfolding simple_function_indicator_representation[OF U(1) x]
+        by (subst setsum_real_of_ereal[symmetric]) auto
+    next
+      fix i
+      have "finite (U i ` space M)" "\<And>x. x \<in> U i ` space M \<Longrightarrow> 0 \<le> x""\<And>x. x \<in> U i ` space M \<Longrightarrow> x \<noteq> \<infinity>"
+        using U(1) nn by (auto simp: simple_function_def)
+      then show "P (\<lambda>x. \<Sum>y \<in> U i ` space M. real y * indicator (U i -` {y} \<inter> space M) x)"
+      proof induct
+        case empty then show ?case
+          using set[of "{}"] by (simp add: indicator_def[abs_def])
+      qed (auto intro!: add mult set simple_functionD U setsum_nonneg borel_measurable_setsum mult_nonneg_nonneg real_of_ereal_pos)
+    qed (auto intro: borel_measurable_simple_function U simple_functionD intro!: borel_measurable_setsum borel_measurable_times)
+  qed
+qed
+
+lemma ereal_indicator: "ereal (indicator A x) = indicator A x"
+  by (auto simp: indicator_def one_ereal_def)
+
 lemma positive_integral_has_integral:
   fixes f :: "'a::ordered_euclidean_space \<Rightarrow> ereal"
   assumes f: "f \<in> borel_measurable lebesgue" "range f \<subseteq> {0..<\<infinity>}" "integral\<^isup>P lebesgue f \<noteq> \<infinity>"