induction prove for positive_integral_density
Wed, 10 Oct 2012 12:12:33 +0200
changeset 49798 8d5668f73c42
parent 49797 28066863284c
child 49799 15ea98537c76
induction prove for positive_integral_density
--- 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:33 2012 +0200
@@ -2329,13 +2329,8 @@
   from set T show ?case
     by (subst positive_integral_cong[OF eq])
        (auto simp add: emeasure_distr intro!: positive_integral_indicator[symmetric] measurable_sets)
-  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)
+qed (simp_all add: measurable_compose[OF T] T positive_integral_cmult positive_integral_add
+                   positive_integral_monotone_convergence_SUP le_fun_def incseq_def)
 lemma positive_integral_distr:
   assumes T: "T \<in> measurable M M'"
@@ -2532,61 +2527,53 @@
        (auto elim: eventually_elim2)
-lemma positive_integral_density:
+lemma positive_integral_density':
   assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
-  assumes g': "g' \<in> borel_measurable M"
-  shows "integral\<^isup>P (density M f) g' = (\<integral>\<^isup>+ x. f x * g' x \<partial>M)"
-proof -
-  def g \<equiv> "\<lambda>x. max 0 (g' x)"
-  then have g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
-    using g' by auto
-  from borel_measurable_implies_simple_function_sequence'[OF g(1)] guess G . note G = this
-  note G' = borel_measurable_simple_function[OF this(1)] simple_functionD[OF G(1)]
-  note G'(2)[simp]
-  with G(4) f g have G_M': "AE x in density M f. (SUP i. G i x) = g x"
-    by (auto simp add: AE_density[OF f(1)] max_def)
-  { fix i
-    let ?I = "\<lambda>y x. indicator (G i -` {y} \<inter> space M) x"
-    { fix x assume *: "x \<in> space M" "0 \<le> f x" "0 \<le> g x"
-      then have [simp]: "G i ` space M \<inter> {y. G i x = y \<and> x \<in> space M} = {G i x}" by auto
-      from * G' G have "(\<Sum>y\<in>G i`space M. y * (f x * ?I y x)) = f x * (\<Sum>y\<in>G i`space M. (y * ?I y x))"
-        by (subst setsum_ereal_right_distrib) (auto simp: ac_simps)
-      also have "\<dots> = f x * G i x"
-        by (simp add: indicator_def if_distrib setsum_cases)
-      finally have "(\<Sum>y\<in>G i`space M. y * (f x * ?I y x)) = f x * G i x" . }
-    note to_singleton = this
-    have "integral\<^isup>P (density M f) (G i) = integral\<^isup>S (density M f) (G i)"
-      using G by (intro positive_integral_eq_simple_integral) simp_all
-    also have "\<dots> = (\<Sum>y\<in>G i`space M. y * (\<integral>\<^isup>+x. f x * ?I y x \<partial>M))"
-      using f G(1)
-      by (auto intro!: setsum_cong arg_cong2[where f="op *"] emeasure_density
-               simp: simple_function_def simple_integral_def)
-    also have "\<dots> = (\<Sum>y\<in>G i`space M. (\<integral>\<^isup>+x. y * (f x * ?I y x) \<partial>M))"
-      using f G' G by (auto intro!: setsum_cong positive_integral_cmult[symmetric])
-    also have "\<dots> = (\<integral>\<^isup>+x. (\<Sum>y\<in>G i`space M. y * (f x * ?I y x)) \<partial>M)"
-      using f G' G by (auto intro!: positive_integral_setsum[symmetric])
-    finally have "integral\<^isup>P (density M f) (G i) = (\<integral>\<^isup>+x. f x * G i x \<partial>M)"
-      using f g G' to_singleton by (auto intro!: positive_integral_cong_AE) }
-  note [simp] = this
-  have "integral\<^isup>P (density M f) g = (SUP i. integral\<^isup>P (density M f) (G i))" using G'(1) G_M'(1) G
-    using positive_integral_monotone_convergence_SUP[symmetric, OF `incseq G`, of "density M f"]
-    by (simp cong: positive_integral_cong_AE)
-  also have "\<dots> = (SUP i. (\<integral>\<^isup>+x. f x * G i x \<partial>M))" by simp
-  also have "\<dots> = (\<integral>\<^isup>+x. (SUP i. f x * G i x) \<partial>M)"
-    using f G' G(2)[THEN incseq_SucD] G
-    by (intro positive_integral_monotone_convergence_SUP_AE[symmetric])
-       (auto simp: ereal_mult_left_mono le_fun_def ereal_zero_le_0_iff)
-  also have "\<dots> = (\<integral>\<^isup>+x. f x * g x \<partial>M)" using f G' G g
-    by (intro positive_integral_cong_AE)
-       (auto simp add: SUPR_ereal_cmult split: split_max)
-  also have "\<dots> = (\<integral>\<^isup>+x. f x * g' x \<partial>M)"
-    using f(2)
-    by (subst (2) positive_integral_max_0[symmetric])
-       (auto simp: g_def max_def ereal_zero_le_0_iff intro!: positive_integral_cong_AE)
-  finally show "integral\<^isup>P (density M f) g' = (\<integral>\<^isup>+x. f x * g' x \<partial>M)"
-    unfolding g_def positive_integral_max_0 .
+  assumes g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
+  shows "integral\<^isup>P (density M f) g = (\<integral>\<^isup>+ x. f x * g x \<partial>M)"
+using g proof induct
+  case (cong u v)
+  then have eq: "AE x in density M f. v x = u x" "AE x in M. f x * v x = f x * u x"
+    by (auto simp: AE_density f)
+  show ?case
+    apply (subst positive_integral_cong_AE[OF eq(1)])
+    apply (subst positive_integral_cong_AE[OF eq(2)])
+    apply fact
+    done
+  case (set A) then show ?case
+    by (simp add: emeasure_density f)
+  case (mult u c)
+  moreover have "\<And>x. f x * (c * u x) = c * (f x * u x)" by (simp add: field_simps)
+  ultimately show ?case
+    by (simp add: f positive_integral_cmult)
+  case (add u v)
+  moreover then have "\<And>x. f x * (v x + u x) = f x * v x + f x * u x"
+    by (simp add: ereal_right_distrib)
+  moreover note f
+  ultimately show ?case
+    by (auto simp add: positive_integral_add ereal_zero_le_0_iff intro!: positive_integral_add[symmetric])
+  case (seq U)
+  from f(2) have eq: "AE x in M. f x * (SUP i. U i x) = (SUP i. f x * U i x)"
+    by eventually_elim (simp add: SUPR_ereal_cmult seq)
+  from seq f show ?case
+    apply (simp add: positive_integral_monotone_convergence_SUP)
+    apply (subst positive_integral_cong_AE[OF eq])
+    apply (subst positive_integral_monotone_convergence_SUP_AE)
+    apply (auto simp: incseq_def le_fun_def intro!: ereal_mult_left_mono)
+    done
+lemma positive_integral_density:
+  "f \<in> borel_measurable M \<Longrightarrow> AE x in M. 0 \<le> f x \<Longrightarrow> g' \<in> borel_measurable M \<Longrightarrow> 
+    integral\<^isup>P (density M f) g' = (\<integral>\<^isup>+ x. f x * g' x \<partial>M)"
+  by (subst (1 2) positive_integral_max_0[symmetric])
+     (auto intro!: positive_integral_cong_AE
+           simp: measurable_If max_def ereal_zero_le_0_iff positive_integral_density')
 lemma integral_density:
   assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
     and g: "g \<in> borel_measurable M"