# HG changeset patch # User hoelzl # Date 1349863953 -7200 # Node ID 8d5668f73c428bc6ce2fde75482a1e3ae5dfe782 # Parent 28066863284cdc2fc460c088b7017cac4234cebe induction prove for positive_integral_density diff -r 28066863284c -r 8d5668f73c42 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: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) -next - case (seq U) - moreover then have "incseq (\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 \ measurable M M'" @@ -2532,61 +2527,53 @@ (auto elim: eventually_elim2) qed -lemma positive_integral_density: +lemma positive_integral_density': assumes f: "f \ borel_measurable M" "AE x in M. 0 \ f x" - assumes g': "g' \ borel_measurable M" - shows "integral\<^isup>P (density M f) g' = (\\<^isup>+ x. f x * g' x \M)" -proof - - def g \ "\x. max 0 (g' x)" - then have g: "g \ borel_measurable M" "AE x in M. 0 \ 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 = "\y x. indicator (G i -` {y} \ space M) x" - { fix x assume *: "x \ space M" "0 \ f x" "0 \ g x" - then have [simp]: "G i ` space M \ {y. G i x = y \ x \ space M} = {G i x}" by auto - from * G' G have "(\y\G i`space M. y * (f x * ?I y x)) = f x * (\y\G i`space M. (y * ?I y x))" - by (subst setsum_ereal_right_distrib) (auto simp: ac_simps) - also have "\ = f x * G i x" - by (simp add: indicator_def if_distrib setsum_cases) - finally have "(\y\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 "\ = (\y\G i`space M. y * (\\<^isup>+x. f x * ?I y x \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 "\ = (\y\G i`space M. (\\<^isup>+x. y * (f x * ?I y x) \M))" - using f G' G by (auto intro!: setsum_cong positive_integral_cmult[symmetric]) - also have "\ = (\\<^isup>+x. (\y\G i`space M. y * (f x * ?I y x)) \M)" - using f G' G by (auto intro!: positive_integral_setsum[symmetric]) - finally have "integral\<^isup>P (density M f) (G i) = (\\<^isup>+x. f x * G i x \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 "\ = (SUP i. (\\<^isup>+x. f x * G i x \M))" by simp - also have "\ = (\\<^isup>+x. (SUP i. f x * G i x) \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 "\ = (\\<^isup>+x. f x * g x \M)" using f G' G g - by (intro positive_integral_cong_AE) - (auto simp add: SUPR_ereal_cmult split: split_max) - also have "\ = (\\<^isup>+x. f x * g' x \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' = (\\<^isup>+x. f x * g' x \M)" - unfolding g_def positive_integral_max_0 . + assumes g: "g \ borel_measurable M" "AE x in M. 0 \ g x" + shows "integral\<^isup>P (density M f) g = (\\<^isup>+ x. f x * g x \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 +next + case (set A) then show ?case + by (simp add: emeasure_density f) +next + case (mult u c) + moreover have "\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) +next + case (add u v) + moreover then have "\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]) +next + 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 qed +lemma positive_integral_density: + "f \ borel_measurable M \ AE x in M. 0 \ f x \ g' \ borel_measurable M \ + integral\<^isup>P (density M f) g' = (\\<^isup>+ x. f x * g' x \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 \ borel_measurable M" "AE x in M. 0 \ f x" and g: "g \ borel_measurable M"