src/HOL/Probability/Radon_Nikodym.thy
author hoelzl
Mon Aug 23 19:35:57 2010 +0200 (2010-08-23)
changeset 38656 d5d342611edb
child 39092 98de40859858
permissions -rw-r--r--
Rewrite the Probability theory.

Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.
     1 theory Radon_Nikodym
     2 imports Lebesgue_Integration
     3 begin
     4 
     5 lemma (in measure_space) measure_finitely_subadditive:
     6   assumes "finite I" "A ` I \<subseteq> sets M"
     7   shows "\<mu> (\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. \<mu> (A i))"
     8 using assms proof induct
     9   case (insert i I)
    10   then have "(\<Union>i\<in>I. A i) \<in> sets M" by (auto intro: finite_UN)
    11   then have "\<mu> (\<Union>i\<in>insert i I. A i) \<le> \<mu> (A i) + \<mu> (\<Union>i\<in>I. A i)"
    12     using insert by (simp add: measure_subadditive)
    13   also have "\<dots> \<le> (\<Sum>i\<in>insert i I. \<mu> (A i))"
    14     using insert by (auto intro!: add_left_mono)
    15   finally show ?case .
    16 qed simp
    17 
    18 lemma (in sigma_algebra) borel_measurable_restricted:
    19   fixes f :: "'a \<Rightarrow> pinfreal" assumes "A \<in> sets M"
    20   shows "f \<in> borel_measurable (M\<lparr> space := A, sets := op \<inter> A ` sets M \<rparr>) \<longleftrightarrow>
    21     (\<lambda>x. f x * indicator A x) \<in> borel_measurable M"
    22     (is "f \<in> borel_measurable ?R \<longleftrightarrow> ?f \<in> borel_measurable M")
    23 proof -
    24   interpret R: sigma_algebra ?R by (rule restricted_sigma_algebra[OF `A \<in> sets M`])
    25   have *: "f \<in> borel_measurable ?R \<longleftrightarrow> ?f \<in> borel_measurable ?R"
    26     by (auto intro!: measurable_cong)
    27   show ?thesis unfolding *
    28     unfolding in_borel_measurable_borel_space
    29   proof (simp, safe)
    30     fix S :: "pinfreal set" assume "S \<in> sets borel_space"
    31       "\<forall>S\<in>sets borel_space. ?f -` S \<inter> A \<in> op \<inter> A ` sets M"
    32     then have "?f -` S \<inter> A \<in> op \<inter> A ` sets M" by auto
    33     then have f: "?f -` S \<inter> A \<in> sets M"
    34       using `A \<in> sets M` sets_into_space by fastsimp
    35     show "?f -` S \<inter> space M \<in> sets M"
    36     proof cases
    37       assume "0 \<in> S"
    38       then have "?f -` S \<inter> space M = ?f -` S \<inter> A \<union> (space M - A)"
    39         using `A \<in> sets M` sets_into_space by auto
    40       then show ?thesis using f `A \<in> sets M` by (auto intro!: Un Diff)
    41     next
    42       assume "0 \<notin> S"
    43       then have "?f -` S \<inter> space M = ?f -` S \<inter> A"
    44         using `A \<in> sets M` sets_into_space
    45         by (auto simp: indicator_def split: split_if_asm)
    46       then show ?thesis using f by auto
    47     qed
    48   next
    49     fix S :: "pinfreal set" assume "S \<in> sets borel_space"
    50       "\<forall>S\<in>sets borel_space. ?f -` S \<inter> space M \<in> sets M"
    51     then have f: "?f -` S \<inter> space M \<in> sets M" by auto
    52     then show "?f -` S \<inter> A \<in> op \<inter> A ` sets M"
    53       using `A \<in> sets M` sets_into_space
    54       apply (simp add: image_iff)
    55       apply (rule bexI[OF _ f])
    56       by auto
    57   qed
    58 qed
    59 
    60 lemma (in sigma_algebra) simple_function_eq_borel_measurable:
    61   fixes f :: "'a \<Rightarrow> pinfreal"
    62   shows "simple_function f \<longleftrightarrow>
    63     finite (f`space M) \<and> f \<in> borel_measurable M"
    64   using simple_function_borel_measurable[of f]
    65     borel_measurable_simple_function[of f]
    66   by (fastsimp simp: simple_function_def)
    67 
    68 lemma (in measure_space) simple_function_restricted:
    69   fixes f :: "'a \<Rightarrow> pinfreal" assumes "A \<in> sets M"
    70   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)"
    71     (is "sigma_algebra.simple_function ?R f \<longleftrightarrow> simple_function ?f")
    72 proof -
    73   interpret R: sigma_algebra ?R by (rule restricted_sigma_algebra[OF `A \<in> sets M`])
    74   have "finite (f`A) \<longleftrightarrow> finite (?f`space M)"
    75   proof cases
    76     assume "A = space M"
    77     then have "f`A = ?f`space M" by (fastsimp simp: image_iff)
    78     then show ?thesis by simp
    79   next
    80     assume "A \<noteq> space M"
    81     then obtain x where x: "x \<in> space M" "x \<notin> A"
    82       using sets_into_space `A \<in> sets M` by auto
    83     have *: "?f`space M = f`A \<union> {0}"
    84     proof (auto simp add: image_iff)
    85       show "\<exists>x\<in>space M. f x = 0 \<or> indicator A x = 0"
    86         using x by (auto intro!: bexI[of _ x])
    87     next
    88       fix x assume "x \<in> A"
    89       then show "\<exists>y\<in>space M. f x = f y * indicator A y"
    90         using `A \<in> sets M` sets_into_space by (auto intro!: bexI[of _ x])
    91     next
    92       fix x
    93       assume "indicator A x \<noteq> (0::pinfreal)"
    94       then have "x \<in> A" by (auto simp: indicator_def split: split_if_asm)
    95       moreover assume "x \<in> space M" "\<forall>y\<in>A. ?f x \<noteq> f y"
    96       ultimately show "f x = 0" by auto
    97     qed
    98     then show ?thesis by auto
    99   qed
   100   then show ?thesis
   101     unfolding simple_function_eq_borel_measurable
   102       R.simple_function_eq_borel_measurable
   103     unfolding borel_measurable_restricted[OF `A \<in> sets M`]
   104     by auto
   105 qed
   106 
   107 lemma (in measure_space) simple_integral_restricted:
   108   assumes "A \<in> sets M"
   109   assumes sf: "simple_function (\<lambda>x. f x * indicator A x)"
   110   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)"
   111     (is "_ = simple_integral ?f")
   112   unfolding measure_space.simple_integral_def[OF restricted_measure_space[OF `A \<in> sets M`]]
   113   unfolding simple_integral_def
   114 proof (simp, safe intro!: setsum_mono_zero_cong_left)
   115   from sf show "finite (?f ` space M)"
   116     unfolding simple_function_def by auto
   117 next
   118   fix x assume "x \<in> A"
   119   then show "f x \<in> ?f ` space M"
   120     using sets_into_space `A \<in> sets M` by (auto intro!: image_eqI[of _ _ x])
   121 next
   122   fix x assume "x \<in> space M" "?f x \<notin> f`A"
   123   then have "x \<notin> A" by (auto simp: image_iff)
   124   then show "?f x * \<mu> (?f -` {?f x} \<inter> space M) = 0" by simp
   125 next
   126   fix x assume "x \<in> A"
   127   then have "f x \<noteq> 0 \<Longrightarrow>
   128     f -` {f x} \<inter> A = ?f -` {f x} \<inter> space M"
   129     using `A \<in> sets M` sets_into_space
   130     by (auto simp: indicator_def split: split_if_asm)
   131   then show "f x * \<mu> (f -` {f x} \<inter> A) =
   132     f x * \<mu> (?f -` {f x} \<inter> space M)"
   133     unfolding pinfreal_mult_cancel_left by auto
   134 qed
   135 
   136 lemma (in measure_space) positive_integral_restricted:
   137   assumes "A \<in> sets M"
   138   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)"
   139     (is "measure_space.positive_integral ?R \<mu> f = positive_integral ?f")
   140 proof -
   141   have msR: "measure_space ?R \<mu>" by (rule restricted_measure_space[OF `A \<in> sets M`])
   142   then interpret R: measure_space ?R \<mu> .
   143   have saR: "sigma_algebra ?R" by fact
   144   have *: "R.positive_integral f = R.positive_integral ?f"
   145     by (auto intro!: R.positive_integral_cong)
   146   show ?thesis
   147     unfolding * R.positive_integral_def positive_integral_def
   148     unfolding simple_function_restricted[OF `A \<in> sets M`]
   149     apply (simp add: SUPR_def)
   150     apply (rule arg_cong[where f=Sup])
   151   proof (auto simp: image_iff simple_integral_restricted[OF `A \<in> sets M`])
   152     fix g assume "simple_function (\<lambda>x. g x * indicator A x)"
   153       "g \<le> f" "\<forall>x\<in>A. \<omega> \<noteq> g x"
   154     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>
   155       simple_integral (\<lambda>x. g x * indicator A x) = simple_integral x"
   156       apply (rule_tac exI[of _ "\<lambda>x. g x * indicator A x"])
   157       by (auto simp: indicator_def le_fun_def)
   158   next
   159     fix g assume g: "simple_function g" "g \<le> (\<lambda>x. f x * indicator A x)"
   160       "\<forall>x\<in>space M. \<omega> \<noteq> g x"
   161     then have *: "(\<lambda>x. g x * indicator A x) = g"
   162       "\<And>x. g x * indicator A x = g x"
   163       "\<And>x. g x \<le> f x"
   164       by (auto simp: le_fun_def expand_fun_eq indicator_def split: split_if_asm)
   165     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>
   166       simple_integral g = simple_integral (\<lambda>xa. x xa * indicator A xa)"
   167       using `A \<in> sets M`[THEN sets_into_space]
   168       apply (rule_tac exI[of _ "\<lambda>x. g x * indicator A x"])
   169       by (fastsimp simp: le_fun_def *)
   170   qed
   171 qed
   172 
   173 lemma (in sigma_algebra) borel_measurable_psuminf:
   174   assumes "\<And>i. f i \<in> borel_measurable M"
   175   shows "(\<lambda>x. (\<Sum>\<^isub>\<infinity> i. f i x)) \<in> borel_measurable M"
   176   using assms unfolding psuminf_def
   177   by (auto intro!: borel_measurable_SUP[unfolded SUPR_fun_expand])
   178 
   179 lemma (in sigma_finite_measure) disjoint_sigma_finite:
   180   "\<exists>A::nat\<Rightarrow>'a set. range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and>
   181     (\<forall>i. \<mu> (A i) \<noteq> \<omega>) \<and> disjoint_family A"
   182 proof -
   183   obtain A :: "nat \<Rightarrow> 'a set" where
   184     range: "range A \<subseteq> sets M" and
   185     space: "(\<Union>i. A i) = space M" and
   186     measure: "\<And>i. \<mu> (A i) \<noteq> \<omega>"
   187     using sigma_finite by auto
   188 
   189   note range' = range_disjointed_sets[OF range] range
   190 
   191   { fix i
   192     have "\<mu> (disjointed A i) \<le> \<mu> (A i)"
   193       using range' disjointed_subset[of A i] by (auto intro!: measure_mono)
   194     then have "\<mu> (disjointed A i) \<noteq> \<omega>"
   195       using measure[of i] by auto }
   196   with disjoint_family_disjointed UN_disjointed_eq[of A] space range'
   197   show ?thesis by (auto intro!: exI[of _ "disjointed A"])
   198 qed
   199 
   200 lemma (in sigma_finite_measure) Ex_finite_integrable_function:
   201   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>)"
   202 proof -
   203   obtain A :: "nat \<Rightarrow> 'a set" where
   204     range: "range A \<subseteq> sets M" and
   205     space: "(\<Union>i. A i) = space M" and
   206     measure: "\<And>i. \<mu> (A i) \<noteq> \<omega>" and
   207     disjoint: "disjoint_family A"
   208     using disjoint_sigma_finite by auto
   209 
   210   let "?B i" = "2^Suc i * \<mu> (A i)"
   211   have "\<forall>i. \<exists>x. 0 < x \<and> x < inverse (?B i)"
   212   proof
   213     fix i show "\<exists>x. 0 < x \<and> x < inverse (?B i)"
   214     proof cases
   215       assume "\<mu> (A i) = 0"
   216       then show ?thesis by (auto intro!: exI[of _ 1])
   217     next
   218       assume not_0: "\<mu> (A i) \<noteq> 0"
   219       then have "?B i \<noteq> \<omega>" using measure[of i] by auto
   220       then have "inverse (?B i) \<noteq> 0" unfolding pinfreal_inverse_eq_0 by simp
   221       then show ?thesis using measure[of i] not_0
   222         by (auto intro!: exI[of _ "inverse (?B i) / 2"]
   223                  simp: pinfreal_noteq_omega_Ex zero_le_mult_iff zero_less_mult_iff mult_le_0_iff power_le_zero_eq)
   224     qed
   225   qed
   226   from choice[OF this] obtain n where n: "\<And>i. 0 < n i"
   227     "\<And>i. n i < inverse (2^Suc i * \<mu> (A i))" by auto
   228 
   229   let "?h x" = "\<Sum>\<^isub>\<infinity> i. n i * indicator (A i) x"
   230   show ?thesis
   231   proof (safe intro!: bexI[of _ ?h] del: notI)
   232     have "positive_integral ?h = (\<Sum>\<^isub>\<infinity> i. n i * \<mu> (A i))"
   233       apply (subst positive_integral_psuminf)
   234       using range apply (fastsimp intro!: borel_measurable_pinfreal_times borel_measurable_const borel_measurable_indicator)
   235       apply (subst positive_integral_cmult_indicator)
   236       using range by auto
   237     also have "\<dots> \<le> (\<Sum>\<^isub>\<infinity> i. Real ((1 / 2)^Suc i))"
   238     proof (rule psuminf_le)
   239       fix N show "n N * \<mu> (A N) \<le> Real ((1 / 2) ^ Suc N)"
   240         using measure[of N] n[of N]
   241         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)
   242     qed
   243     also have "\<dots> = Real 1"
   244       by (rule suminf_imp_psuminf, rule power_half_series, auto)
   245     finally show "positive_integral ?h \<noteq> \<omega>" by auto
   246   next
   247     fix x assume "x \<in> space M"
   248     then obtain i where "x \<in> A i" using space[symmetric] by auto
   249     from psuminf_cmult_indicator[OF disjoint, OF this]
   250     have "?h x = n i" by simp
   251     then show "0 < ?h x" and "?h x < \<omega>" using n[of i] by auto
   252   next
   253     show "?h \<in> borel_measurable M" using range
   254       by (auto intro!: borel_measurable_psuminf borel_measurable_pinfreal_times borel_measurable_indicator)
   255   qed
   256 qed
   257 
   258 definition (in measure_space)
   259   "absolutely_continuous \<nu> = (\<forall>N\<in>null_sets. \<nu> N = (0 :: pinfreal))"
   260 
   261 lemma (in finite_measure) Radon_Nikodym_aux_epsilon:
   262   fixes e :: real assumes "0 < e"
   263   assumes "finite_measure M s"
   264   shows "\<exists>A\<in>sets M. real (\<mu> (space M)) - real (s (space M)) \<le>
   265                     real (\<mu> A) - real (s A) \<and>
   266                     (\<forall>B\<in>sets M. B \<subseteq> A \<longrightarrow> - e < real (\<mu> B) - real (s B))"
   267 proof -
   268   let "?d A" = "real (\<mu> A) - real (s A)"
   269   interpret M': finite_measure M s by fact
   270 
   271   let "?A A" = "if (\<forall>B\<in>sets M. B \<subseteq> space M - A \<longrightarrow> -e < ?d B)
   272     then {}
   273     else (SOME B. B \<in> sets M \<and> B \<subseteq> space M - A \<and> ?d B \<le> -e)"
   274   def A \<equiv> "\<lambda>n. ((\<lambda>B. B \<union> ?A B) ^^ n) {}"
   275 
   276   have A_simps[simp]:
   277     "A 0 = {}"
   278     "\<And>n. A (Suc n) = (A n \<union> ?A (A n))" unfolding A_def by simp_all
   279 
   280   { fix A assume "A \<in> sets M"
   281     have "?A A \<in> sets M"
   282       by (auto intro!: someI2[of _ _ "\<lambda>A. A \<in> sets M"] simp: not_less) }
   283   note A'_in_sets = this
   284 
   285   { fix n have "A n \<in> sets M"
   286     proof (induct n)
   287       case (Suc n) thus "A (Suc n) \<in> sets M"
   288         using A'_in_sets[of "A n"] by (auto split: split_if_asm)
   289     qed (simp add: A_def) }
   290   note A_in_sets = this
   291   hence "range A \<subseteq> sets M" by auto
   292 
   293   { fix n B
   294     assume Ex: "\<exists>B. B \<in> sets M \<and> B \<subseteq> space M - A n \<and> ?d B \<le> -e"
   295     hence False: "\<not> (\<forall>B\<in>sets M. B \<subseteq> space M - A n \<longrightarrow> -e < ?d B)" by (auto simp: not_less)
   296     have "?d (A (Suc n)) \<le> ?d (A n) - e" unfolding A_simps if_not_P[OF False]
   297     proof (rule someI2_ex[OF Ex])
   298       fix B assume "B \<in> sets M \<and> B \<subseteq> space M - A n \<and> ?d B \<le> - e"
   299       hence "A n \<inter> B = {}" "B \<in> sets M" and dB: "?d B \<le> -e" by auto
   300       hence "?d (A n \<union> B) = ?d (A n) + ?d B"
   301         using `A n \<in> sets M` real_finite_measure_Union M'.real_finite_measure_Union by simp
   302       also have "\<dots> \<le> ?d (A n) - e" using dB by simp
   303       finally show "?d (A n \<union> B) \<le> ?d (A n) - e" .
   304     qed }
   305   note dA_epsilon = this
   306 
   307   { fix n have "?d (A (Suc n)) \<le> ?d (A n)"
   308     proof (cases "\<exists>B. B\<in>sets M \<and> B \<subseteq> space M - A n \<and> ?d B \<le> - e")
   309       case True from dA_epsilon[OF this] show ?thesis using `0 < e` by simp
   310     next
   311       case False
   312       hence "\<forall>B\<in>sets M. B \<subseteq> space M - A n \<longrightarrow> -e < ?d B" by (auto simp: not_le)
   313       thus ?thesis by simp
   314     qed }
   315   note dA_mono = this
   316 
   317   show ?thesis
   318   proof (cases "\<exists>n. \<forall>B\<in>sets M. B \<subseteq> space M - A n \<longrightarrow> -e < ?d B")
   319     case True then obtain n where B: "\<And>B. \<lbrakk> B \<in> sets M; B \<subseteq> space M - A n\<rbrakk> \<Longrightarrow> -e < ?d B" by blast
   320     show ?thesis
   321     proof (safe intro!: bexI[of _ "space M - A n"])
   322       fix B assume "B \<in> sets M" "B \<subseteq> space M - A n"
   323       from B[OF this] show "-e < ?d B" .
   324     next
   325       show "space M - A n \<in> sets M" by (rule compl_sets) fact
   326     next
   327       show "?d (space M) \<le> ?d (space M - A n)"
   328       proof (induct n)
   329         fix n assume "?d (space M) \<le> ?d (space M - A n)"
   330         also have "\<dots> \<le> ?d (space M - A (Suc n))"
   331           using A_in_sets sets_into_space dA_mono[of n]
   332             real_finite_measure_Diff[of "space M"]
   333             real_finite_measure_Diff[of "space M"]
   334             M'.real_finite_measure_Diff[of "space M"]
   335             M'.real_finite_measure_Diff[of "space M"]
   336           by (simp del: A_simps)
   337         finally show "?d (space M) \<le> ?d (space M - A (Suc n))" .
   338       qed simp
   339     qed
   340   next
   341     case False hence B: "\<And>n. \<exists>B. B\<in>sets M \<and> B \<subseteq> space M - A n \<and> ?d B \<le> - e"
   342       by (auto simp add: not_less)
   343     { fix n have "?d (A n) \<le> - real n * e"
   344       proof (induct n)
   345         case (Suc n) with dA_epsilon[of n, OF B] show ?case by (simp del: A_simps add: real_of_nat_Suc field_simps)
   346       qed simp } note dA_less = this
   347     have decseq: "decseq (\<lambda>n. ?d (A n))" unfolding decseq_eq_incseq
   348     proof (rule incseq_SucI)
   349       fix n show "- ?d (A n) \<le> - ?d (A (Suc n))" using dA_mono[of n] by auto
   350     qed
   351     from real_finite_continuity_from_below[of A] `range A \<subseteq> sets M`
   352       M'.real_finite_continuity_from_below[of A]
   353     have convergent: "(\<lambda>i. ?d (A i)) ----> ?d (\<Union>i. A i)"
   354       by (auto intro!: LIMSEQ_diff)
   355     obtain n :: nat where "- ?d (\<Union>i. A i) / e < real n" using reals_Archimedean2 by auto
   356     moreover from order_trans[OF decseq_le[OF decseq convergent] dA_less]
   357     have "real n \<le> - ?d (\<Union>i. A i) / e" using `0<e` by (simp add: field_simps)
   358     ultimately show ?thesis by auto
   359   qed
   360 qed
   361 
   362 lemma (in finite_measure) Radon_Nikodym_aux:
   363   assumes "finite_measure M s"
   364   shows "\<exists>A\<in>sets M. real (\<mu> (space M)) - real (s (space M)) \<le>
   365                     real (\<mu> A) - real (s A) \<and>
   366                     (\<forall>B\<in>sets M. B \<subseteq> A \<longrightarrow> 0 \<le> real (\<mu> B) - real (s B))"
   367 proof -
   368   let "?d A" = "real (\<mu> A) - real (s A)"
   369   let "?P A B n" = "A \<in> sets M \<and> A \<subseteq> B \<and> ?d B \<le> ?d A \<and> (\<forall>C\<in>sets M. C \<subseteq> A \<longrightarrow> - 1 / real (Suc n) < ?d C)"
   370 
   371   interpret M': finite_measure M s by fact
   372 
   373   let "?r S" = "M\<lparr> space := S, sets := (\<lambda>C. S \<inter> C)`sets M\<rparr>"
   374 
   375   { fix S n
   376     assume S: "S \<in> sets M"
   377     hence **: "\<And>X. X \<in> op \<inter> S ` sets M \<longleftrightarrow> X \<in> sets M \<and> X \<subseteq> S" by auto
   378     from M'.restricted_finite_measure[of S] restricted_finite_measure[of S] S
   379     have "finite_measure (?r S) \<mu>" "0 < 1 / real (Suc n)"
   380       "finite_measure (?r S) s" by auto
   381     from finite_measure.Radon_Nikodym_aux_epsilon[OF this] guess X ..
   382     hence "?P X S n"
   383     proof (simp add: **, safe)
   384       fix C assume C: "C \<in> sets M" "C \<subseteq> X" "X \<subseteq> S" and
   385         *: "\<forall>B\<in>sets M. S \<inter> B \<subseteq> X \<longrightarrow> - (1 / real (Suc n)) < ?d (S \<inter> B)"
   386       hence "C \<subseteq> S" "C \<subseteq> X" "S \<inter> C = C" by auto
   387       with *[THEN bspec, OF `C \<in> sets M`]
   388       show "- (1 / real (Suc n)) < ?d C" by auto
   389     qed
   390     hence "\<exists>A. ?P A S n" by auto }
   391   note Ex_P = this
   392 
   393   def A \<equiv> "nat_rec (space M) (\<lambda>n A. SOME B. ?P B A n)"
   394   have A_Suc: "\<And>n. A (Suc n) = (SOME B. ?P B (A n) n)" by (simp add: A_def)
   395   have A_0[simp]: "A 0 = space M" unfolding A_def by simp
   396 
   397   { fix i have "A i \<in> sets M" unfolding A_def
   398     proof (induct i)
   399       case (Suc i)
   400       from Ex_P[OF this, of i] show ?case unfolding nat_rec_Suc
   401         by (rule someI2_ex) simp
   402     qed simp }
   403   note A_in_sets = this
   404 
   405   { fix n have "?P (A (Suc n)) (A n) n"
   406       using Ex_P[OF A_in_sets] unfolding A_Suc
   407       by (rule someI2_ex) simp }
   408   note P_A = this
   409 
   410   have "range A \<subseteq> sets M" using A_in_sets by auto
   411 
   412   have A_mono: "\<And>i. A (Suc i) \<subseteq> A i" using P_A by simp
   413   have mono_dA: "mono (\<lambda>i. ?d (A i))" using P_A by (simp add: mono_iff_le_Suc)
   414   have epsilon: "\<And>C i. \<lbrakk> C \<in> sets M; C \<subseteq> A (Suc i) \<rbrakk> \<Longrightarrow> - 1 / real (Suc i) < ?d C"
   415       using P_A by auto
   416 
   417   show ?thesis
   418   proof (safe intro!: bexI[of _ "\<Inter>i. A i"])
   419     show "(\<Inter>i. A i) \<in> sets M" using A_in_sets by auto
   420     from `range A \<subseteq> sets M` A_mono
   421       real_finite_continuity_from_above[of A]
   422       M'.real_finite_continuity_from_above[of A]
   423     have "(\<lambda>i. ?d (A i)) ----> ?d (\<Inter>i. A i)" by (auto intro!: LIMSEQ_diff)
   424     thus "?d (space M) \<le> ?d (\<Inter>i. A i)" using mono_dA[THEN monoD, of 0 _]
   425       by (rule_tac LIMSEQ_le_const) (auto intro!: exI)
   426   next
   427     fix B assume B: "B \<in> sets M" "B \<subseteq> (\<Inter>i. A i)"
   428     show "0 \<le> ?d B"
   429     proof (rule ccontr)
   430       assume "\<not> 0 \<le> ?d B"
   431       hence "0 < - ?d B" by auto
   432       from ex_inverse_of_nat_Suc_less[OF this]
   433       obtain n where *: "?d B < - 1 / real (Suc n)"
   434         by (auto simp: real_eq_of_nat inverse_eq_divide field_simps)
   435       have "B \<subseteq> A (Suc n)" using B by (auto simp del: nat_rec_Suc)
   436       from epsilon[OF B(1) this] *
   437       show False by auto
   438     qed
   439   qed
   440 qed
   441 
   442 lemma (in finite_measure) Radon_Nikodym_finite_measure:
   443   assumes "finite_measure M \<nu>"
   444   assumes "absolutely_continuous \<nu>"
   445   shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
   446 proof -
   447   interpret M': finite_measure M \<nu> using assms(1) .
   448 
   449   def G \<equiv> "{g \<in> borel_measurable M. \<forall>A\<in>sets M. positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A}"
   450   have "(\<lambda>x. 0) \<in> G" unfolding G_def by auto
   451   hence "G \<noteq> {}" by auto
   452 
   453   { fix f g assume f: "f \<in> G" and g: "g \<in> G"
   454     have "(\<lambda>x. max (g x) (f x)) \<in> G" (is "?max \<in> G") unfolding G_def
   455     proof safe
   456       show "?max \<in> borel_measurable M" using f g unfolding G_def by auto
   457 
   458       let ?A = "{x \<in> space M. f x \<le> g x}"
   459       have "?A \<in> sets M" using f g unfolding G_def by auto
   460 
   461       fix A assume "A \<in> sets M"
   462       hence sets: "?A \<inter> A \<in> sets M" "(space M - ?A) \<inter> A \<in> sets M" using `?A \<in> sets M` by auto
   463       have union: "((?A \<inter> A) \<union> ((space M - ?A) \<inter> A)) = A"
   464         using sets_into_space[OF `A \<in> sets M`] by auto
   465 
   466       have "\<And>x. x \<in> space M \<Longrightarrow> max (g x) (f x) * indicator A x =
   467         g x * indicator (?A \<inter> A) x + f x * indicator ((space M - ?A) \<inter> A) x"
   468         by (auto simp: indicator_def max_def)
   469       hence "positive_integral (\<lambda>x. max (g x) (f x) * indicator A x) =
   470         positive_integral (\<lambda>x. g x * indicator (?A \<inter> A) x) +
   471         positive_integral (\<lambda>x. f x * indicator ((space M - ?A) \<inter> A) x)"
   472         using f g sets unfolding G_def
   473         by (auto cong: positive_integral_cong intro!: positive_integral_add borel_measurable_indicator)
   474       also have "\<dots> \<le> \<nu> (?A \<inter> A) + \<nu> ((space M - ?A) \<inter> A)"
   475         using f g sets unfolding G_def by (auto intro!: add_mono)
   476       also have "\<dots> = \<nu> A"
   477         using M'.measure_additive[OF sets] union by auto
   478       finally show "positive_integral (\<lambda>x. max (g x) (f x) * indicator A x) \<le> \<nu> A" .
   479     qed }
   480   note max_in_G = this
   481 
   482   { fix f g assume  "f \<up> g" and f: "\<And>i. f i \<in> G"
   483     have "g \<in> G" unfolding G_def
   484     proof safe
   485       from `f \<up> g` have [simp]: "g = (SUP i. f i)" unfolding isoton_def by simp
   486       have f_borel: "\<And>i. f i \<in> borel_measurable M" using f unfolding G_def by simp
   487       thus "g \<in> borel_measurable M" by (auto intro!: borel_measurable_SUP)
   488 
   489       fix A assume "A \<in> sets M"
   490       hence "\<And>i. (\<lambda>x. f i x * indicator A x) \<in> borel_measurable M"
   491         using f_borel by (auto intro!: borel_measurable_indicator)
   492       from positive_integral_isoton[OF isoton_indicator[OF `f \<up> g`] this]
   493       have SUP: "positive_integral (\<lambda>x. g x * indicator A x) =
   494           (SUP i. positive_integral (\<lambda>x. f i x * indicator A x))"
   495         unfolding isoton_def by simp
   496       show "positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A" unfolding SUP
   497         using f `A \<in> sets M` unfolding G_def by (auto intro!: SUP_leI)
   498     qed }
   499   note SUP_in_G = this
   500 
   501   let ?y = "SUP g : G. positive_integral g"
   502   have "?y \<le> \<nu> (space M)" unfolding G_def
   503   proof (safe intro!: SUP_leI)
   504     fix g assume "\<forall>A\<in>sets M. positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A"
   505     from this[THEN bspec, OF top] show "positive_integral g \<le> \<nu> (space M)"
   506       by (simp cong: positive_integral_cong)
   507   qed
   508   hence "?y \<noteq> \<omega>" using M'.finite_measure_of_space by auto
   509   from SUPR_countable_SUPR[OF this `G \<noteq> {}`] guess ys .. note ys = this
   510   hence "\<forall>n. \<exists>g. g\<in>G \<and> positive_integral g = ys n"
   511   proof safe
   512     fix n assume "range ys \<subseteq> positive_integral ` G"
   513     hence "ys n \<in> positive_integral ` G" by auto
   514     thus "\<exists>g. g\<in>G \<and> positive_integral g = ys n" by auto
   515   qed
   516   from choice[OF this] obtain gs where "\<And>i. gs i \<in> G" "\<And>n. positive_integral (gs n) = ys n" by auto
   517   hence y_eq: "?y = (SUP i. positive_integral (gs i))" using ys by auto
   518   let "?g i x" = "Max ((\<lambda>n. gs n x) ` {..i})"
   519   def f \<equiv> "SUP i. ?g i"
   520   have gs_not_empty: "\<And>i. (\<lambda>n. gs n x) ` {..i} \<noteq> {}" by auto
   521   { fix i have "?g i \<in> G"
   522     proof (induct i)
   523       case 0 thus ?case by simp fact
   524     next
   525       case (Suc i)
   526       with Suc gs_not_empty `gs (Suc i) \<in> G` show ?case
   527         by (auto simp add: atMost_Suc intro!: max_in_G)
   528     qed }
   529   note g_in_G = this
   530   have "\<And>x. \<forall>i. ?g i x \<le> ?g (Suc i) x"
   531     using gs_not_empty by (simp add: atMost_Suc)
   532   hence isoton_g: "?g \<up> f" by (simp add: isoton_def le_fun_def f_def)
   533   from SUP_in_G[OF this g_in_G] have "f \<in> G" .
   534   hence [simp, intro]: "f \<in> borel_measurable M" unfolding G_def by auto
   535 
   536   have "(\<lambda>i. positive_integral (?g i)) \<up> positive_integral f"
   537     using isoton_g g_in_G by (auto intro!: positive_integral_isoton simp: G_def f_def)
   538   hence "positive_integral f = (SUP i. positive_integral (?g i))"
   539     unfolding isoton_def by simp
   540   also have "\<dots> = ?y"
   541   proof (rule antisym)
   542     show "(SUP i. positive_integral (?g i)) \<le> ?y"
   543       using g_in_G by (auto intro!: exI Sup_mono simp: SUPR_def)
   544     show "?y \<le> (SUP i. positive_integral (?g i))" unfolding y_eq
   545       by (auto intro!: SUP_mono positive_integral_mono Max_ge)
   546   qed
   547   finally have int_f_eq_y: "positive_integral f = ?y" .
   548 
   549   let "?t A" = "\<nu> A - positive_integral (\<lambda>x. f x * indicator A x)"
   550 
   551   have "finite_measure M ?t"
   552   proof
   553     show "?t {} = 0" by simp
   554     show "?t (space M) \<noteq> \<omega>" using M'.finite_measure by simp
   555     show "countably_additive M ?t" unfolding countably_additive_def
   556     proof safe
   557       fix A :: "nat \<Rightarrow> 'a set"  assume A: "range A \<subseteq> sets M" "disjoint_family A"
   558       have "(\<Sum>\<^isub>\<infinity> n. positive_integral (\<lambda>x. f x * indicator (A n) x))
   559         = positive_integral (\<lambda>x. (\<Sum>\<^isub>\<infinity>n. f x * indicator (A n) x))"
   560         using `range A \<subseteq> sets M`
   561         by (rule_tac positive_integral_psuminf[symmetric]) (auto intro!: borel_measurable_indicator)
   562       also have "\<dots> = positive_integral (\<lambda>x. f x * indicator (\<Union>n. A n) x)"
   563         apply (rule positive_integral_cong)
   564         apply (subst psuminf_cmult_right)
   565         unfolding psuminf_indicator[OF `disjoint_family A`] ..
   566       finally have "(\<Sum>\<^isub>\<infinity> n. positive_integral (\<lambda>x. f x * indicator (A n) x))
   567         = positive_integral (\<lambda>x. f x * indicator (\<Union>n. A n) x)" .
   568       moreover have "(\<Sum>\<^isub>\<infinity>n. \<nu> (A n)) = \<nu> (\<Union>n. A n)"
   569         using M'.measure_countably_additive A by (simp add: comp_def)
   570       moreover have "\<And>i. positive_integral (\<lambda>x. f x * indicator (A i) x) \<le> \<nu> (A i)"
   571           using A `f \<in> G` unfolding G_def by auto
   572       moreover have v_fin: "\<nu> (\<Union>i. A i) \<noteq> \<omega>" using M'.finite_measure A by (simp add: countable_UN)
   573       moreover {
   574         have "positive_integral (\<lambda>x. f x * indicator (\<Union>i. A i) x) \<le> \<nu> (\<Union>i. A i)"
   575           using A `f \<in> G` unfolding G_def by (auto simp: countable_UN)
   576         also have "\<nu> (\<Union>i. A i) < \<omega>" using v_fin by (simp add: pinfreal_less_\<omega>)
   577         finally have "positive_integral (\<lambda>x. f x * indicator (\<Union>i. A i) x) \<noteq> \<omega>"
   578           by (simp add: pinfreal_less_\<omega>) }
   579       ultimately
   580       show "(\<Sum>\<^isub>\<infinity> n. ?t (A n)) = ?t (\<Union>i. A i)"
   581         apply (subst psuminf_minus) by simp_all
   582     qed
   583   qed
   584   then interpret M: finite_measure M ?t .
   585 
   586   have ac: "absolutely_continuous ?t" using `absolutely_continuous \<nu>` unfolding absolutely_continuous_def by auto
   587 
   588   have upper_bound: "\<forall>A\<in>sets M. ?t A \<le> 0"
   589   proof (rule ccontr)
   590     assume "\<not> ?thesis"
   591     then obtain A where A: "A \<in> sets M" and pos: "0 < ?t A"
   592       by (auto simp: not_le)
   593     note pos
   594     also have "?t A \<le> ?t (space M)"
   595       using M.measure_mono[of A "space M"] A sets_into_space by simp
   596     finally have pos_t: "0 < ?t (space M)" by simp
   597     moreover
   598     hence pos_M: "0 < \<mu> (space M)"
   599       using ac top unfolding absolutely_continuous_def by auto
   600     moreover
   601     have "positive_integral (\<lambda>x. f x * indicator (space M) x) \<le> \<nu> (space M)"
   602       using `f \<in> G` unfolding G_def by auto
   603     hence "positive_integral (\<lambda>x. f x * indicator (space M) x) \<noteq> \<omega>"
   604       using M'.finite_measure_of_space by auto
   605     moreover
   606     def b \<equiv> "?t (space M) / \<mu> (space M) / 2"
   607     ultimately have b: "b \<noteq> 0" "b \<noteq> \<omega>"
   608       using M'.finite_measure_of_space
   609       by (auto simp: pinfreal_inverse_eq_0 finite_measure_of_space)
   610 
   611     have "finite_measure M (\<lambda>A. b * \<mu> A)" (is "finite_measure M ?b")
   612     proof
   613       show "?b {} = 0" by simp
   614       show "?b (space M) \<noteq> \<omega>" using finite_measure_of_space b by auto
   615       show "countably_additive M ?b"
   616         unfolding countably_additive_def psuminf_cmult_right
   617         using measure_countably_additive by auto
   618     qed
   619 
   620     from M.Radon_Nikodym_aux[OF this]
   621     obtain A0 where "A0 \<in> sets M" and
   622       space_less_A0: "real (?t (space M)) - real (b * \<mu> (space M)) \<le> real (?t A0) - real (b * \<mu> A0)" and
   623       *: "\<And>B. \<lbrakk> B \<in> sets M ; B \<subseteq> A0 \<rbrakk> \<Longrightarrow> 0 \<le> real (?t B) - real (b * \<mu> B)" by auto
   624     { fix B assume "B \<in> sets M" "B \<subseteq> A0"
   625       with *[OF this] have "b * \<mu> B \<le> ?t B"
   626         using M'.finite_measure b finite_measure
   627         by (cases "b * \<mu> B", cases "?t B") (auto simp: field_simps) }
   628     note bM_le_t = this
   629 
   630     let "?f0 x" = "f x + b * indicator A0 x"
   631 
   632     { fix A assume A: "A \<in> sets M"
   633       hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
   634       have "positive_integral (\<lambda>x. ?f0 x  * indicator A x) =
   635         positive_integral (\<lambda>x. f x * indicator A x + b * indicator (A \<inter> A0) x)"
   636         by (auto intro!: positive_integral_cong simp: field_simps indicator_inter_arith)
   637       hence "positive_integral (\<lambda>x. ?f0 x * indicator A x) =
   638           positive_integral (\<lambda>x. f x * indicator A x) + b * \<mu> (A \<inter> A0)"
   639         using `A0 \<in> sets M` `A \<inter> A0 \<in> sets M` A
   640         by (simp add: borel_measurable_indicator positive_integral_add positive_integral_cmult_indicator) }
   641     note f0_eq = this
   642 
   643     { fix A assume A: "A \<in> sets M"
   644       hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
   645       have f_le_v: "positive_integral (\<lambda>x. f x * indicator A x) \<le> \<nu> A"
   646         using `f \<in> G` A unfolding G_def by auto
   647       note f0_eq[OF A]
   648       also have "positive_integral (\<lambda>x. f x * indicator A x) + b * \<mu> (A \<inter> A0) \<le>
   649           positive_integral (\<lambda>x. f x * indicator A x) + ?t (A \<inter> A0)"
   650         using bM_le_t[OF `A \<inter> A0 \<in> sets M`] `A \<in> sets M` `A0 \<in> sets M`
   651         by (auto intro!: add_left_mono)
   652       also have "\<dots> \<le> positive_integral (\<lambda>x. f x * indicator A x) + ?t A"
   653         using M.measure_mono[simplified, OF _ `A \<inter> A0 \<in> sets M` `A \<in> sets M`]
   654         by (auto intro!: add_left_mono)
   655       also have "\<dots> \<le> \<nu> A"
   656         using f_le_v M'.finite_measure[simplified, OF `A \<in> sets M`]
   657         by (cases "positive_integral (\<lambda>x. f x * indicator A x)", cases "\<nu> A", auto)
   658       finally have "positive_integral (\<lambda>x. ?f0 x * indicator A x) \<le> \<nu> A" . }
   659     hence "?f0 \<in> G" using `A0 \<in> sets M` unfolding G_def
   660       by (auto intro!: borel_measurable_indicator borel_measurable_pinfreal_add borel_measurable_pinfreal_times)
   661 
   662     have real: "?t (space M) \<noteq> \<omega>" "?t A0 \<noteq> \<omega>"
   663       "b * \<mu> (space M) \<noteq> \<omega>" "b * \<mu> A0 \<noteq> \<omega>"
   664       using `A0 \<in> sets M` b
   665         finite_measure[of A0] M.finite_measure[of A0]
   666         finite_measure_of_space M.finite_measure_of_space
   667       by auto
   668 
   669     have int_f_finite: "positive_integral f \<noteq> \<omega>"
   670       using M'.finite_measure_of_space pos_t unfolding pinfreal_zero_less_diff_iff
   671       by (auto cong: positive_integral_cong)
   672 
   673     have "?t (space M) > b * \<mu> (space M)" unfolding b_def
   674       apply (simp add: field_simps)
   675       apply (subst mult_assoc[symmetric])
   676       apply (subst pinfreal_mult_inverse)
   677       using finite_measure_of_space M'.finite_measure_of_space pos_t pos_M
   678       using pinfreal_mult_strict_right_mono[of "Real (1/2)" 1 "?t (space M)"]
   679       by simp_all
   680     hence  "0 < ?t (space M) - b * \<mu> (space M)"
   681       by (simp add: pinfreal_zero_less_diff_iff)
   682     also have "\<dots> \<le> ?t A0 - b * \<mu> A0"
   683       using space_less_A0 pos_M pos_t b real[unfolded pinfreal_noteq_omega_Ex] by auto
   684     finally have "b * \<mu> A0 < ?t A0" unfolding pinfreal_zero_less_diff_iff .
   685     hence "0 < ?t A0" by auto
   686     hence "0 < \<mu> A0" using ac unfolding absolutely_continuous_def
   687       using `A0 \<in> sets M` by auto
   688     hence "0 < b * \<mu> A0" using b by auto
   689 
   690     from int_f_finite this
   691     have "?y + 0 < positive_integral f + b * \<mu> A0" unfolding int_f_eq_y
   692       by (rule pinfreal_less_add)
   693     also have "\<dots> = positive_integral ?f0" using f0_eq[OF top] `A0 \<in> sets M` sets_into_space
   694       by (simp cong: positive_integral_cong)
   695     finally have "?y < positive_integral ?f0" by simp
   696 
   697     moreover from `?f0 \<in> G` have "positive_integral ?f0 \<le> ?y" by (auto intro!: le_SUPI)
   698     ultimately show False by auto
   699   qed
   700 
   701   show ?thesis
   702   proof (safe intro!: bexI[of _ f])
   703     fix A assume "A\<in>sets M"
   704     show "\<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
   705     proof (rule antisym)
   706       show "positive_integral (\<lambda>x. f x * indicator A x) \<le> \<nu> A"
   707         using `f \<in> G` `A \<in> sets M` unfolding G_def by auto
   708       show "\<nu> A \<le> positive_integral (\<lambda>x. f x * indicator A x)"
   709         using upper_bound[THEN bspec, OF `A \<in> sets M`]
   710          by (simp add: pinfreal_zero_le_diff)
   711     qed
   712   qed simp
   713 qed
   714 
   715 lemma (in finite_measure) Radon_Nikodym_finite_measure_infinite:
   716   assumes "measure_space M \<nu>"
   717   assumes "absolutely_continuous \<nu>"
   718   shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
   719 proof -
   720   interpret v: measure_space M \<nu> by fact
   721   let ?Q = "{Q\<in>sets M. \<nu> Q \<noteq> \<omega>}"
   722   let ?a = "SUP Q:?Q. \<mu> Q"
   723 
   724   have "{} \<in> ?Q" using v.empty_measure by auto
   725   then have Q_not_empty: "?Q \<noteq> {}" by blast
   726 
   727   have "?a \<le> \<mu> (space M)" using sets_into_space
   728     by (auto intro!: SUP_leI measure_mono top)
   729   then have "?a \<noteq> \<omega>" using finite_measure_of_space
   730     by auto
   731   from SUPR_countable_SUPR[OF this Q_not_empty]
   732   obtain Q'' where "range Q'' \<subseteq> \<mu> ` ?Q" and a: "?a = (SUP i::nat. Q'' i)"
   733     by auto
   734   then have "\<forall>i. \<exists>Q'. Q'' i = \<mu> Q' \<and> Q' \<in> ?Q" by auto
   735   from choice[OF this] obtain Q' where Q': "\<And>i. Q'' i = \<mu> (Q' i)" "\<And>i. Q' i \<in> ?Q"
   736     by auto
   737   then have a_Lim: "?a = (SUP i::nat. \<mu> (Q' i))" using a by simp
   738   let "?O n" = "\<Union>i\<le>n. Q' i"
   739   have Union: "(SUP i. \<mu> (?O i)) = \<mu> (\<Union>i. ?O i)"
   740   proof (rule continuity_from_below[of ?O])
   741     show "range ?O \<subseteq> sets M" using Q' by (auto intro!: finite_UN)
   742     show "\<And>i. ?O i \<subseteq> ?O (Suc i)" by fastsimp
   743   qed
   744 
   745   have Q'_sets: "\<And>i. Q' i \<in> sets M" using Q' by auto
   746 
   747   have O_sets: "\<And>i. ?O i \<in> sets M"
   748      using Q' by (auto intro!: finite_UN Un)
   749   then have O_in_G: "\<And>i. ?O i \<in> ?Q"
   750   proof (safe del: notI)
   751     fix i have "Q' ` {..i} \<subseteq> sets M"
   752       using Q' by (auto intro: finite_UN)
   753     with v.measure_finitely_subadditive[of "{.. i}" Q']
   754     have "\<nu> (?O i) \<le> (\<Sum>i\<le>i. \<nu> (Q' i))" by auto
   755     also have "\<dots> < \<omega>" unfolding setsum_\<omega> pinfreal_less_\<omega> using Q' by auto
   756     finally show "\<nu> (?O i) \<noteq> \<omega>" unfolding pinfreal_less_\<omega> by auto
   757   qed auto
   758   have O_mono: "\<And>n. ?O n \<subseteq> ?O (Suc n)" by fastsimp
   759 
   760   have a_eq: "?a = \<mu> (\<Union>i. ?O i)" unfolding Union[symmetric]
   761   proof (rule antisym)
   762     show "?a \<le> (SUP i. \<mu> (?O i))" unfolding a_Lim
   763       using Q' by (auto intro!: SUP_mono measure_mono finite_UN)
   764     show "(SUP i. \<mu> (?O i)) \<le> ?a" unfolding SUPR_def
   765     proof (safe intro!: Sup_mono, unfold bex_simps)
   766       fix i
   767       have *: "(\<Union>Q' ` {..i}) = ?O i" by auto
   768       then show "\<exists>x. (x \<in> sets M \<and> \<nu> x \<noteq> \<omega>) \<and>
   769         \<mu> (\<Union>Q' ` {..i}) \<le> \<mu> x"
   770         using O_in_G[of i] by (auto intro!: exI[of _ "?O i"])
   771     qed
   772   qed
   773 
   774   let "?O_0" = "(\<Union>i. ?O i)"
   775   have "?O_0 \<in> sets M" using Q' by auto
   776 
   777   { fix A assume *: "A \<in> ?Q" "A \<subseteq> space M - ?O_0"
   778     then have "\<mu> ?O_0 + \<mu> A = \<mu> (?O_0 \<union> A)"
   779       using Q' by (auto intro!: measure_additive countable_UN)
   780     also have "\<dots> = (SUP i. \<mu> (?O i \<union> A))"
   781     proof (rule continuity_from_below[of "\<lambda>i. ?O i \<union> A", symmetric, simplified])
   782       show "range (\<lambda>i. ?O i \<union> A) \<subseteq> sets M"
   783         using * O_sets by auto
   784     qed fastsimp
   785     also have "\<dots> \<le> ?a"
   786     proof (safe intro!: SUPR_bound)
   787       fix i have "?O i \<union> A \<in> ?Q"
   788       proof (safe del: notI)
   789         show "?O i \<union> A \<in> sets M" using O_sets * by auto
   790         from O_in_G[of i]
   791         moreover have "\<nu> (?O i \<union> A) \<le> \<nu> (?O i) + \<nu> A"
   792           using v.measure_subadditive[of "?O i" A] * O_sets by auto
   793         ultimately show "\<nu> (?O i \<union> A) \<noteq> \<omega>"
   794           using * by auto
   795       qed
   796       then show "\<mu> (?O i \<union> A) \<le> ?a" by (rule le_SUPI)
   797     qed
   798     finally have "\<mu> A = 0" unfolding a_eq using finite_measure[OF `?O_0 \<in> sets M`]
   799       by (cases "\<mu> A") (auto simp: pinfreal_noteq_omega_Ex) }
   800   note stetic = this
   801 
   802   def Q \<equiv> "\<lambda>i. case i of 0 \<Rightarrow> ?O 0 | Suc n \<Rightarrow> ?O (Suc n) - ?O n"
   803 
   804   { fix i have "Q i \<in> sets M" unfolding Q_def using Q'[of 0] by (cases i) (auto intro: O_sets) }
   805   note Q_sets = this
   806 
   807   { fix i have "\<nu> (Q i) \<noteq> \<omega>"
   808     proof (cases i)
   809       case 0 then show ?thesis
   810         unfolding Q_def using Q'[of 0] by simp
   811     next
   812       case (Suc n)
   813       then show ?thesis unfolding Q_def
   814         using `?O n \<in> ?Q` `?O (Suc n) \<in> ?Q` O_mono
   815         using v.measure_Diff[of "?O n" "?O (Suc n)"] by auto
   816     qed }
   817   note Q_omega = this
   818 
   819   { fix j have "(\<Union>i\<le>j. ?O i) = (\<Union>i\<le>j. Q i)"
   820     proof (induct j)
   821       case 0 then show ?case by (simp add: Q_def)
   822     next
   823       case (Suc j)
   824       have eq: "\<And>j. (\<Union>i\<le>j. ?O i) = (\<Union>i\<le>j. Q' i)" by fastsimp
   825       have "{..j} \<union> {..Suc j} = {..Suc j}" by auto
   826       then have "(\<Union>i\<le>Suc j. Q' i) = (\<Union>i\<le>j. Q' i) \<union> Q (Suc j)"
   827         by (simp add: UN_Un[symmetric] Q_def del: UN_Un)
   828       then show ?case using Suc by (auto simp add: eq atMost_Suc)
   829     qed }
   830   then have "(\<Union>j. (\<Union>i\<le>j. ?O i)) = (\<Union>j. (\<Union>i\<le>j. Q i))" by simp
   831   then have O_0_eq_Q: "?O_0 = (\<Union>j. Q j)" by fastsimp
   832 
   833   have "\<forall>i. \<exists>f. f\<in>borel_measurable M \<and> (\<forall>A\<in>sets M.
   834     \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f x * indicator (Q i \<inter> A) x))"
   835   proof
   836     fix i
   837     have indicator_eq: "\<And>f x A. (f x :: pinfreal) * indicator (Q i \<inter> A) x * indicator (Q i) x
   838       = (f x * indicator (Q i) x) * indicator A x"
   839       unfolding indicator_def by auto
   840 
   841     have fm: "finite_measure (M\<lparr>space := Q i, sets := op \<inter> (Q i) ` sets M\<rparr>) \<mu>"
   842       (is "finite_measure ?R \<mu>") by (rule restricted_finite_measure[OF Q_sets[of i]])
   843     then interpret R: finite_measure ?R .
   844     have fmv: "finite_measure ?R \<nu>"
   845       unfolding finite_measure_def finite_measure_axioms_def
   846     proof
   847       show "measure_space ?R \<nu>"
   848         using v.restricted_measure_space Q_sets[of i] by auto
   849       show "\<nu>  (space ?R) \<noteq> \<omega>"
   850         using Q_omega by simp
   851     qed
   852     have "R.absolutely_continuous \<nu>"
   853       using `absolutely_continuous \<nu>` `Q i \<in> sets M`
   854       by (auto simp: R.absolutely_continuous_def absolutely_continuous_def)
   855     from finite_measure.Radon_Nikodym_finite_measure[OF fm fmv this]
   856     obtain f where f: "(\<lambda>x. f x * indicator (Q i) x) \<in> borel_measurable M"
   857       and f_int: "\<And>A. A\<in>sets M \<Longrightarrow> \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. (f x * indicator (Q i) x) * indicator A x)"
   858       unfolding Bex_def borel_measurable_restricted[OF `Q i \<in> sets M`]
   859         positive_integral_restricted[OF `Q i \<in> sets M`] by (auto simp: indicator_eq)
   860     then show "\<exists>f. f\<in>borel_measurable M \<and> (\<forall>A\<in>sets M.
   861       \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f x * indicator (Q i \<inter> A) x))"
   862       by (fastsimp intro!: exI[of _ "\<lambda>x. f x * indicator (Q i) x"] positive_integral_cong
   863           simp: indicator_def)
   864   qed
   865   from choice[OF this] obtain f where borel: "\<And>i. f i \<in> borel_measurable M"
   866     and f: "\<And>A i. A \<in> sets M \<Longrightarrow>
   867       \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f i x * indicator (Q i \<inter> A) x)"
   868     by auto
   869   let "?f x" =
   870     "(\<Sum>\<^isub>\<infinity> i. f i x * indicator (Q i) x) + \<omega> * indicator (space M - ?O_0) x"
   871   show ?thesis
   872   proof (safe intro!: bexI[of _ ?f])
   873     show "?f \<in> borel_measurable M"
   874       by (safe intro!: borel_measurable_psuminf borel_measurable_pinfreal_times
   875         borel_measurable_pinfreal_add borel_measurable_indicator
   876         borel_measurable_const borel Q_sets O_sets Diff countable_UN)
   877     fix A assume "A \<in> sets M"
   878     let ?C = "(space M - (\<Union>i. Q i)) \<inter> A"
   879     have *: 
   880       "\<And>x i. indicator A x * (f i x * indicator (Q i) x) =
   881         f i x * indicator (Q i \<inter> A) x"
   882       "\<And>x i. (indicator A x * indicator (space M - (\<Union>i. UNION {..i} Q')) x :: pinfreal) =
   883         indicator ?C x" unfolding O_0_eq_Q by (auto simp: indicator_def)
   884     have "positive_integral (\<lambda>x. ?f x * indicator A x) =
   885       (\<Sum>\<^isub>\<infinity> i. \<nu> (Q i \<inter> A)) + \<omega> * \<mu> ?C"
   886       unfolding f[OF `A \<in> sets M`]
   887       apply (simp del: pinfreal_times(2) add: field_simps)
   888       apply (subst positive_integral_add)
   889       apply (safe intro!: borel_measurable_pinfreal_times Diff borel_measurable_const
   890         borel_measurable_psuminf borel_measurable_indicator `A \<in> sets M` Q_sets borel countable_UN Q'_sets)
   891       unfolding psuminf_cmult_right[symmetric]
   892       apply (subst positive_integral_psuminf)
   893       apply (safe intro!: borel_measurable_pinfreal_times Diff borel_measurable_const
   894         borel_measurable_psuminf borel_measurable_indicator `A \<in> sets M` Q_sets borel countable_UN Q'_sets)
   895       apply (subst positive_integral_cmult)
   896       apply (safe intro!: borel_measurable_pinfreal_times Diff borel_measurable_const
   897         borel_measurable_psuminf borel_measurable_indicator `A \<in> sets M` Q_sets borel countable_UN Q'_sets)
   898       unfolding *
   899       apply (subst positive_integral_indicator)
   900       apply (safe intro!: borel_measurable_pinfreal_times Diff borel_measurable_const Int
   901         borel_measurable_psuminf borel_measurable_indicator `A \<in> sets M` Q_sets borel countable_UN Q'_sets)
   902       by simp
   903     moreover have "(\<Sum>\<^isub>\<infinity>i. \<nu> (Q i \<inter> A)) = \<nu> ((\<Union>i. Q i) \<inter> A)"
   904     proof (rule v.measure_countably_additive[of "\<lambda>i. Q i \<inter> A", unfolded comp_def, simplified])
   905       show "range (\<lambda>i. Q i \<inter> A) \<subseteq> sets M"
   906         using Q_sets `A \<in> sets M` by auto
   907       show "disjoint_family (\<lambda>i. Q i \<inter> A)"
   908         by (fastsimp simp: disjoint_family_on_def Q_def
   909           split: nat.split_asm)
   910     qed
   911     moreover have "\<omega> * \<mu> ?C = \<nu> ?C"
   912     proof cases
   913       assume null: "\<mu> ?C = 0"
   914       hence "?C \<in> null_sets" using Q_sets `A \<in> sets M` by auto
   915       with `absolutely_continuous \<nu>` and null
   916       show ?thesis by (simp add: absolutely_continuous_def)
   917     next
   918       assume not_null: "\<mu> ?C \<noteq> 0"
   919       have "\<nu> ?C = \<omega>"
   920       proof (rule ccontr)
   921         assume "\<nu> ?C \<noteq> \<omega>"
   922         then have "?C \<in> ?Q"
   923           using Q_sets `A \<in> sets M` by auto
   924         from stetic[OF this] not_null
   925         show False unfolding O_0_eq_Q by auto
   926       qed
   927       then show ?thesis using not_null by simp
   928     qed
   929     moreover have "?C \<in> sets M" "((\<Union>i. Q i) \<inter> A) \<in> sets M"
   930       using Q_sets `A \<in> sets M` by (auto intro!: countable_UN)
   931     moreover have "((\<Union>i. Q i) \<inter> A) \<union> ?C = A" "((\<Union>i. Q i) \<inter> A) \<inter> ?C = {}"
   932       using `A \<in> sets M` sets_into_space by auto
   933     ultimately show "\<nu> A = positive_integral (\<lambda>x. ?f x * indicator A x)"
   934       using v.measure_additive[simplified, of "(\<Union>i. Q i) \<inter> A" ?C] by auto
   935   qed
   936 qed
   937 
   938 lemma (in measure_space) positive_integral_translated_density:
   939   assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   940   shows "measure_space.positive_integral M (\<lambda>A. positive_integral (\<lambda>x. f x * indicator A x)) g =
   941     positive_integral (\<lambda>x. f x * g x)" (is "measure_space.positive_integral M ?T _ = _")
   942 proof -
   943   from measure_space_density[OF assms(1)]
   944   interpret T: measure_space M ?T .
   945 
   946   from borel_measurable_implies_simple_function_sequence[OF assms(2)]
   947   obtain G where G: "\<And>i. simple_function (G i)" "G \<up> g" by blast
   948   note G_borel = borel_measurable_simple_function[OF this(1)]
   949 
   950   from T.positive_integral_isoton[OF `G \<up> g` G_borel]
   951   have *: "(\<lambda>i. T.positive_integral (G i)) \<up> T.positive_integral g" .
   952 
   953   { fix i
   954     have [simp]: "finite (G i ` space M)"
   955       using G(1) unfolding simple_function_def by auto
   956     have "T.positive_integral (G i) = T.simple_integral (G i)"
   957       using G T.positive_integral_eq_simple_integral by simp
   958     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))"
   959       apply (simp add: T.simple_integral_def)
   960       apply (subst positive_integral_cmult[symmetric])
   961       using G_borel assms(1) apply (fastsimp intro: borel_measurable_indicator borel_measurable_vimage)
   962       apply (subst positive_integral_setsum[symmetric])
   963       using G_borel assms(1) apply (fastsimp intro: borel_measurable_indicator borel_measurable_vimage)
   964       by (simp add: setsum_right_distrib field_simps)
   965     also have "\<dots> = positive_integral (\<lambda>x. f x * G i x)"
   966       by (auto intro!: positive_integral_cong
   967                simp: indicator_def if_distrib setsum_cases)
   968     finally have "T.positive_integral (G i) = positive_integral (\<lambda>x. f x * G i x)" . }
   969   with * have eq_Tg: "(\<lambda>i. positive_integral (\<lambda>x. f x * G i x)) \<up> T.positive_integral g" by simp
   970 
   971   from G(2) have "(\<lambda>i x. f x * G i x) \<up> (\<lambda>x. f x * g x)"
   972     unfolding isoton_fun_expand by (auto intro!: isoton_cmult_right)
   973   then have "(\<lambda>i. positive_integral (\<lambda>x. f x * G i x)) \<up> positive_integral (\<lambda>x. f x * g x)"
   974     using assms(1) G_borel by (auto intro!: positive_integral_isoton borel_measurable_pinfreal_times)
   975   with eq_Tg show "T.positive_integral g = positive_integral (\<lambda>x. f x * g x)"
   976     unfolding isoton_def by simp
   977 qed
   978 
   979 lemma (in sigma_finite_measure) Radon_Nikodym:
   980   assumes "measure_space M \<nu>"
   981   assumes "absolutely_continuous \<nu>"
   982   shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
   983 proof -
   984   from Ex_finite_integrable_function
   985   obtain h where finite: "positive_integral h \<noteq> \<omega>" and
   986     borel: "h \<in> borel_measurable M" and
   987     pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x" and
   988     "\<And>x. x \<in> space M \<Longrightarrow> h x < \<omega>" by auto
   989   let "?T A" = "positive_integral (\<lambda>x. h x * indicator A x)"
   990   from measure_space_density[OF borel] finite
   991   interpret T: finite_measure M ?T
   992     unfolding finite_measure_def finite_measure_axioms_def
   993     by (simp cong: positive_integral_cong)
   994   have "\<And>N. N \<in> sets M \<Longrightarrow> {x \<in> space M. h x \<noteq> 0 \<and> indicator N x \<noteq> (0::pinfreal)} = N"
   995     using sets_into_space pos by (force simp: indicator_def)
   996   then have "T.absolutely_continuous \<nu>" using assms(2) borel
   997     unfolding T.absolutely_continuous_def absolutely_continuous_def
   998     by (fastsimp simp: borel_measurable_indicator positive_integral_0_iff)
   999   from T.Radon_Nikodym_finite_measure_infinite[simplified, OF assms(1) this]
  1000   obtain f where f_borel: "f \<in> borel_measurable M" and
  1001     fT: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = T.positive_integral (\<lambda>x. f x * indicator A x)" by auto
  1002   show ?thesis
  1003   proof (safe intro!: bexI[of _ "\<lambda>x. h x * f x"])
  1004     show "(\<lambda>x. h x * f x) \<in> borel_measurable M"
  1005       using borel f_borel by (auto intro: borel_measurable_pinfreal_times)
  1006     fix A assume "A \<in> sets M"
  1007     then have "(\<lambda>x. f x * indicator A x) \<in> borel_measurable M"
  1008       using f_borel by (auto intro: borel_measurable_pinfreal_times borel_measurable_indicator)
  1009     from positive_integral_translated_density[OF borel this]
  1010     show "\<nu> A = positive_integral (\<lambda>x. h x * f x * indicator A x)"
  1011       unfolding fT[OF `A \<in> sets M`] by (simp add: field_simps)
  1012   qed
  1013 qed
  1014 
  1015 section "Radon Nikodym derivative"
  1016 
  1017 definition (in sigma_finite_measure)
  1018   "RN_deriv \<nu> \<equiv> SOME f. f \<in> borel_measurable M \<and>
  1019     (\<forall>A \<in> sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x))"
  1020 
  1021 lemma (in sigma_finite_measure) RN_deriv:
  1022   assumes "measure_space M \<nu>"
  1023   assumes "absolutely_continuous \<nu>"
  1024   shows "RN_deriv \<nu> \<in> borel_measurable M" (is ?borel)
  1025   and "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)"
  1026     (is "\<And>A. _ \<Longrightarrow> ?int A")
  1027 proof -
  1028   note Ex = Radon_Nikodym[OF assms, unfolded Bex_def]
  1029   thus ?borel unfolding RN_deriv_def by (rule someI2_ex) auto
  1030   fix A assume "A \<in> sets M"
  1031   from Ex show "?int A" unfolding RN_deriv_def
  1032     by (rule someI2_ex) (simp add: `A \<in> sets M`)
  1033 qed
  1034 
  1035 lemma (in sigma_finite_measure) RN_deriv_singleton:
  1036   assumes "measure_space M \<nu>"
  1037   and ac: "absolutely_continuous \<nu>"
  1038   and "{x} \<in> sets M"
  1039   shows "\<nu> {x} = RN_deriv \<nu> x * \<mu> {x}"
  1040 proof -
  1041   note deriv = RN_deriv[OF assms(1, 2)]
  1042   from deriv(2)[OF `{x} \<in> sets M`]
  1043   have "\<nu> {x} = positive_integral (\<lambda>w. RN_deriv \<nu> x * indicator {x} w)"
  1044     by (auto simp: indicator_def intro!: positive_integral_cong)
  1045   thus ?thesis using positive_integral_cmult_indicator[OF `{x} \<in> sets M`]
  1046     by auto
  1047 qed
  1048 
  1049 theorem (in finite_measure_space) RN_deriv_finite_measure:
  1050   assumes "measure_space M \<nu>"
  1051   and ac: "absolutely_continuous \<nu>"
  1052   and "x \<in> space M"
  1053   shows "\<nu> {x} = RN_deriv \<nu> x * \<mu> {x}"
  1054 proof -
  1055   have "{x} \<in> sets M" using sets_eq_Pow `x \<in> space M` by auto
  1056   from RN_deriv_singleton[OF assms(1,2) this] show ?thesis .
  1057 qed
  1058 
  1059 end