changeset 39092 98de40859858 parent 38656 d5d342611edb child 39097 943c7b348524
```--- a/src/HOL/Probability/Radon_Nikodym.thy	Fri Aug 27 16:23:51 2010 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Thu Sep 02 17:12:40 2010 +0200
@@ -2,201 +2,6 @@
imports Lebesgue_Integration
begin

-  assumes "finite I" "A ` I \<subseteq> sets M"
-  shows "\<mu> (\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. \<mu> (A i))"
-using assms proof induct
-  case (insert i I)
-  then have "(\<Union>i\<in>I. A i) \<in> sets M" by (auto intro: finite_UN)
-  then have "\<mu> (\<Union>i\<in>insert i I. A i) \<le> \<mu> (A i) + \<mu> (\<Union>i\<in>I. A i)"
-  also have "\<dots> \<le> (\<Sum>i\<in>insert i I. \<mu> (A i))"
-    using insert by (auto intro!: add_left_mono)
-  finally show ?case .
-qed simp
-
-lemma (in sigma_algebra) borel_measurable_restricted:
-  fixes f :: "'a \<Rightarrow> pinfreal" assumes "A \<in> sets M"
-  shows "f \<in> borel_measurable (M\<lparr> space := A, sets := op \<inter> A ` sets M \<rparr>) \<longleftrightarrow>
-    (\<lambda>x. f x * indicator A x) \<in> borel_measurable M"
-    (is "f \<in> borel_measurable ?R \<longleftrightarrow> ?f \<in> borel_measurable M")
-proof -
-  interpret R: sigma_algebra ?R by (rule restricted_sigma_algebra[OF `A \<in> sets M`])
-  have *: "f \<in> borel_measurable ?R \<longleftrightarrow> ?f \<in> borel_measurable ?R"
-    by (auto intro!: measurable_cong)
-  show ?thesis unfolding *
-    unfolding in_borel_measurable_borel_space
-  proof (simp, safe)
-    fix S :: "pinfreal set" assume "S \<in> sets borel_space"
-      "\<forall>S\<in>sets borel_space. ?f -` S \<inter> A \<in> op \<inter> A ` sets M"
-    then have "?f -` S \<inter> A \<in> op \<inter> A ` sets M" by auto
-    then have f: "?f -` S \<inter> A \<in> sets M"
-      using `A \<in> sets M` sets_into_space by fastsimp
-    show "?f -` S \<inter> space M \<in> sets M"
-    proof cases
-      assume "0 \<in> S"
-      then have "?f -` S \<inter> space M = ?f -` S \<inter> A \<union> (space M - A)"
-        using `A \<in> sets M` sets_into_space by auto
-      then show ?thesis using f `A \<in> sets M` by (auto intro!: Un Diff)
-    next
-      assume "0 \<notin> S"
-      then have "?f -` S \<inter> space M = ?f -` S \<inter> A"
-        using `A \<in> sets M` sets_into_space
-        by (auto simp: indicator_def split: split_if_asm)
-      then show ?thesis using f by auto
-    qed
-  next
-    fix S :: "pinfreal set" assume "S \<in> sets borel_space"
-      "\<forall>S\<in>sets borel_space. ?f -` S \<inter> space M \<in> sets M"
-    then have f: "?f -` S \<inter> space M \<in> sets M" by auto
-    then show "?f -` S \<inter> A \<in> op \<inter> A ` sets M"
-      using `A \<in> sets M` sets_into_space
-      apply (rule bexI[OF _ f])
-      by auto
-  qed
-qed
-
-lemma (in sigma_algebra) simple_function_eq_borel_measurable:
-  fixes f :: "'a \<Rightarrow> pinfreal"
-  shows "simple_function f \<longleftrightarrow>
-    finite (f`space M) \<and> f \<in> borel_measurable M"
-  using simple_function_borel_measurable[of f]
-    borel_measurable_simple_function[of f]
-  by (fastsimp simp: simple_function_def)
-
-lemma (in measure_space) simple_function_restricted:
-  fixes f :: "'a \<Rightarrow> pinfreal" assumes "A \<in> sets M"
-  shows "sigma_algebra.simple_function (M\<lparr> space := A, sets := op \<inter> A ` sets M \<rparr>) f \<longleftrightarrow> simple_function (\<lambda>x. f x * indicator A x)"
-    (is "sigma_algebra.simple_function ?R f \<longleftrightarrow> simple_function ?f")
-proof -
-  interpret R: sigma_algebra ?R by (rule restricted_sigma_algebra[OF `A \<in> sets M`])
-  have "finite (f`A) \<longleftrightarrow> finite (?f`space M)"
-  proof cases
-    assume "A = space M"
-    then have "f`A = ?f`space M" by (fastsimp simp: image_iff)
-    then show ?thesis by simp
-  next
-    assume "A \<noteq> space M"
-    then obtain x where x: "x \<in> space M" "x \<notin> A"
-      using sets_into_space `A \<in> sets M` by auto
-    have *: "?f`space M = f`A \<union> {0}"
-    proof (auto simp add: image_iff)
-      show "\<exists>x\<in>space M. f x = 0 \<or> indicator A x = 0"
-        using x by (auto intro!: bexI[of _ x])
-    next
-      fix x assume "x \<in> A"
-      then show "\<exists>y\<in>space M. f x = f y * indicator A y"
-        using `A \<in> sets M` sets_into_space by (auto intro!: bexI[of _ x])
-    next
-      fix x
-      assume "indicator A x \<noteq> (0::pinfreal)"
-      then have "x \<in> A" by (auto simp: indicator_def split: split_if_asm)
-      moreover assume "x \<in> space M" "\<forall>y\<in>A. ?f x \<noteq> f y"
-      ultimately show "f x = 0" by auto
-    qed
-    then show ?thesis by auto
-  qed
-  then show ?thesis
-    unfolding simple_function_eq_borel_measurable
-      R.simple_function_eq_borel_measurable
-    unfolding borel_measurable_restricted[OF `A \<in> sets M`]
-    by auto
-qed
-
-lemma (in measure_space) simple_integral_restricted:
-  assumes "A \<in> sets M"
-  assumes sf: "simple_function (\<lambda>x. f x * indicator A x)"
-  shows "measure_space.simple_integral (M\<lparr> space := A, sets := op \<inter> A ` sets M \<rparr>) \<mu> f = simple_integral (\<lambda>x. f x * indicator A x)"
-    (is "_ = simple_integral ?f")
-  unfolding measure_space.simple_integral_def[OF restricted_measure_space[OF `A \<in> sets M`]]
-  unfolding simple_integral_def
-proof (simp, safe intro!: setsum_mono_zero_cong_left)
-  from sf show "finite (?f ` space M)"
-    unfolding simple_function_def by auto
-next
-  fix x assume "x \<in> A"
-  then show "f x \<in> ?f ` space M"
-    using sets_into_space `A \<in> sets M` by (auto intro!: image_eqI[of _ _ x])
-next
-  fix x assume "x \<in> space M" "?f x \<notin> f`A"
-  then have "x \<notin> A" by (auto simp: image_iff)
-  then show "?f x * \<mu> (?f -` {?f x} \<inter> space M) = 0" by simp
-next
-  fix x assume "x \<in> A"
-  then have "f x \<noteq> 0 \<Longrightarrow>
-    f -` {f x} \<inter> A = ?f -` {f x} \<inter> space M"
-    using `A \<in> sets M` sets_into_space
-    by (auto simp: indicator_def split: split_if_asm)
-  then show "f x * \<mu> (f -` {f x} \<inter> A) =
-    f x * \<mu> (?f -` {f x} \<inter> space M)"
-    unfolding pinfreal_mult_cancel_left by auto
-qed
-
-lemma (in measure_space) positive_integral_restricted:
-  assumes "A \<in> sets M"
-  shows "measure_space.positive_integral (M\<lparr> space := A, sets := op \<inter> A ` sets M \<rparr>) \<mu> f = positive_integral (\<lambda>x. f x * indicator A x)"
-    (is "measure_space.positive_integral ?R \<mu> f = positive_integral ?f")
-proof -
-  have msR: "measure_space ?R \<mu>" by (rule restricted_measure_space[OF `A \<in> sets M`])
-  then interpret R: measure_space ?R \<mu> .
-  have saR: "sigma_algebra ?R" by fact
-  have *: "R.positive_integral f = R.positive_integral ?f"
-    by (auto intro!: R.positive_integral_cong)
-  show ?thesis
-    unfolding * R.positive_integral_def positive_integral_def
-    unfolding simple_function_restricted[OF `A \<in> sets M`]
-    apply (rule arg_cong[where f=Sup])
-  proof (auto simp: image_iff simple_integral_restricted[OF `A \<in> sets M`])
-    fix g assume "simple_function (\<lambda>x. g x * indicator A x)"
-      "g \<le> f" "\<forall>x\<in>A. \<omega> \<noteq> g x"
-    then show "\<exists>x. simple_function x \<and> x \<le> (\<lambda>x. f x * indicator A x) \<and> (\<forall>y\<in>space M. \<omega> \<noteq> x y) \<and>
-      simple_integral (\<lambda>x. g x * indicator A x) = simple_integral x"
-      apply (rule_tac exI[of _ "\<lambda>x. g x * indicator A x"])
-      by (auto simp: indicator_def le_fun_def)
-  next
-    fix g assume g: "simple_function g" "g \<le> (\<lambda>x. f x * indicator A x)"
-      "\<forall>x\<in>space M. \<omega> \<noteq> g x"
-    then have *: "(\<lambda>x. g x * indicator A x) = g"
-      "\<And>x. g x * indicator A x = g x"
-      "\<And>x. g x \<le> f x"
-      by (auto simp: le_fun_def expand_fun_eq indicator_def split: split_if_asm)
-    from g show "\<exists>x. simple_function (\<lambda>xa. x xa * indicator A xa) \<and> x \<le> f \<and> (\<forall>xa\<in>A. \<omega> \<noteq> x xa) \<and>
-      simple_integral g = simple_integral (\<lambda>xa. x xa * indicator A xa)"
-      using `A \<in> sets M`[THEN sets_into_space]
-      apply (rule_tac exI[of _ "\<lambda>x. g x * indicator A x"])
-      by (fastsimp simp: le_fun_def *)
-  qed
-qed
-
-lemma (in sigma_algebra) borel_measurable_psuminf:
-  assumes "\<And>i. f i \<in> borel_measurable M"
-  shows "(\<lambda>x. (\<Sum>\<^isub>\<infinity> i. f i x)) \<in> borel_measurable M"
-  using assms unfolding psuminf_def
-  by (auto intro!: borel_measurable_SUP[unfolded SUPR_fun_expand])
-
-lemma (in sigma_finite_measure) disjoint_sigma_finite:
-  "\<exists>A::nat\<Rightarrow>'a set. range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and>
-    (\<forall>i. \<mu> (A i) \<noteq> \<omega>) \<and> disjoint_family A"
-proof -
-  obtain A :: "nat \<Rightarrow> 'a set" where
-    range: "range A \<subseteq> sets M" and
-    space: "(\<Union>i. A i) = space M" and
-    measure: "\<And>i. \<mu> (A i) \<noteq> \<omega>"
-    using sigma_finite by auto
-
-  note range' = range_disjointed_sets[OF range] range
-
-  { fix i
-    have "\<mu> (disjointed A i) \<le> \<mu> (A i)"
-      using range' disjointed_subset[of A i] by (auto intro!: measure_mono)
-    then have "\<mu> (disjointed A i) \<noteq> \<omega>"
-      using measure[of i] by auto }
-  with disjoint_family_disjointed UN_disjointed_eq[of A] space range'
-  show ?thesis by (auto intro!: exI[of _ "disjointed A"])
-qed
-
lemma (in sigma_finite_measure) Ex_finite_integrable_function:
shows "\<exists>h\<in>borel_measurable M. positive_integral h \<noteq> \<omega> \<and> (\<forall>x\<in>space M. 0 < h x \<and> h x < \<omega>)"
proof -
@@ -206,7 +11,6 @@
measure: "\<And>i. \<mu> (A i) \<noteq> \<omega>" and
disjoint: "disjoint_family A"
using disjoint_sigma_finite by auto
-
let "?B i" = "2^Suc i * \<mu> (A i)"
have "\<forall>i. \<exists>x. 0 < x \<and> x < inverse (?B i)"
proof
@@ -225,20 +29,22 @@
qed
from choice[OF this] obtain n where n: "\<And>i. 0 < n i"
"\<And>i. n i < inverse (2^Suc i * \<mu> (A i))" by auto
-
let "?h x" = "\<Sum>\<^isub>\<infinity> i. n i * indicator (A i) x"
show ?thesis
proof (safe intro!: bexI[of _ ?h] del: notI)
-    have "positive_integral ?h = (\<Sum>\<^isub>\<infinity> i. n i * \<mu> (A i))"
-      apply (subst positive_integral_psuminf)
-      using range apply (fastsimp intro!: borel_measurable_pinfreal_times borel_measurable_const borel_measurable_indicator)
-      apply (subst positive_integral_cmult_indicator)
-      using range by auto
+    have "\<And>i. A i \<in> sets M"
+      using range by fastsimp+
+    then have "positive_integral ?h = (\<Sum>\<^isub>\<infinity> i. n i * \<mu> (A i))"
+      by (simp add: positive_integral_psuminf positive_integral_cmult_indicator)
also have "\<dots> \<le> (\<Sum>\<^isub>\<infinity> i. Real ((1 / 2)^Suc i))"
proof (rule psuminf_le)
fix N show "n N * \<mu> (A N) \<le> Real ((1 / 2) ^ Suc N)"
using measure[of N] n[of N]
-        by (cases "n N") (auto simp: pinfreal_noteq_omega_Ex field_simps zero_le_mult_iff mult_le_0_iff mult_less_0_iff power_less_zero_eq power_le_zero_eq inverse_eq_divide less_divide_eq power_divide split: split_if_asm)
+        by (cases "n N")
+           (auto simp: pinfreal_noteq_omega_Ex field_simps zero_le_mult_iff
+                       mult_le_0_iff mult_less_0_iff power_less_zero_eq
+                       power_le_zero_eq inverse_eq_divide less_divide_eq
+                       power_divide split: split_if_asm)
qed
also have "\<dots> = Real 1"
by (rule suminf_imp_psuminf, rule power_half_series, auto)
@@ -251,7 +57,7 @@
then show "0 < ?h x" and "?h x < \<omega>" using n[of i] by auto
next
show "?h \<in> borel_measurable M" using range
-      by (auto intro!: borel_measurable_psuminf borel_measurable_pinfreal_times borel_measurable_indicator)
+      by (auto intro!: borel_measurable_psuminf borel_measurable_pinfreal_times)
qed
qed

@@ -370,7 +176,7 @@

interpret M': finite_measure M s by fact

-  let "?r S" = "M\<lparr> space := S, sets := (\<lambda>C. S \<inter> C)`sets M\<rparr>"
+  let "?r S" = "restricted_space S"

{ fix S n
assume S: "S \<in> sets M"
@@ -838,7 +644,7 @@
= (f x * indicator (Q i) x) * indicator A x"
unfolding indicator_def by auto

-    have fm: "finite_measure (M\<lparr>space := Q i, sets := op \<inter> (Q i) ` sets M\<rparr>) \<mu>"
+    have fm: "finite_measure (restricted_space (Q i)) \<mu>"
(is "finite_measure ?R \<mu>") by (rule restricted_finite_measure[OF Q_sets[of i]])
then interpret R: finite_measure ?R .
have fmv: "finite_measure ?R \<nu>"
@@ -935,47 +741,6 @@
qed
qed

-lemma (in measure_space) positive_integral_translated_density:
-  assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
-  shows "measure_space.positive_integral M (\<lambda>A. positive_integral (\<lambda>x. f x * indicator A x)) g =
-    positive_integral (\<lambda>x. f x * g x)" (is "measure_space.positive_integral M ?T _ = _")
-proof -
-  from measure_space_density[OF assms(1)]
-  interpret T: measure_space M ?T .
-
-  from borel_measurable_implies_simple_function_sequence[OF assms(2)]
-  obtain G where G: "\<And>i. simple_function (G i)" "G \<up> g" by blast
-  note G_borel = borel_measurable_simple_function[OF this(1)]
-
-  from T.positive_integral_isoton[OF `G \<up> g` G_borel]
-  have *: "(\<lambda>i. T.positive_integral (G i)) \<up> T.positive_integral g" .
-
-  { fix i
-    have [simp]: "finite (G i ` space M)"
-      using G(1) unfolding simple_function_def by auto
-    have "T.positive_integral (G i) = T.simple_integral (G i)"
-      using G T.positive_integral_eq_simple_integral by simp
-    also have "\<dots> = positive_integral (\<lambda>x. f x * (\<Sum>y\<in>G i`space M. y * indicator (G i -` {y} \<inter> space M) x))"
-      apply (subst positive_integral_cmult[symmetric])
-      using G_borel assms(1) apply (fastsimp intro: borel_measurable_indicator borel_measurable_vimage)
-      apply (subst positive_integral_setsum[symmetric])
-      using G_borel assms(1) apply (fastsimp intro: borel_measurable_indicator borel_measurable_vimage)
-      by (simp add: setsum_right_distrib field_simps)
-    also have "\<dots> = positive_integral (\<lambda>x. f x * G i x)"
-      by (auto intro!: positive_integral_cong
-               simp: indicator_def if_distrib setsum_cases)
-    finally have "T.positive_integral (G i) = positive_integral (\<lambda>x. f x * G i x)" . }
-  with * have eq_Tg: "(\<lambda>i. positive_integral (\<lambda>x. f x * G i x)) \<up> T.positive_integral g" by simp
-
-  from G(2) have "(\<lambda>i x. f x * G i x) \<up> (\<lambda>x. f x * g x)"
-    unfolding isoton_fun_expand by (auto intro!: isoton_cmult_right)
-  then have "(\<lambda>i. positive_integral (\<lambda>x. f x * G i x)) \<up> positive_integral (\<lambda>x. f x * g x)"
-    using assms(1) G_borel by (auto intro!: positive_integral_isoton borel_measurable_pinfreal_times)
-  with eq_Tg show "T.positive_integral g = positive_integral (\<lambda>x. f x * g x)"
-    unfolding isoton_def by simp
-qed
-