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.
2 imports Lebesgue_Integration
3 begin
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
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
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)
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
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
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
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])
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
189   note range' = range_disjointed_sets[OF range] range
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
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
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
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
258 definition (in measure_space)
259   "absolutely_continuous \<nu> = (\<forall>N\<in>null_sets. \<nu> N = (0 :: pinfreal))"
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
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) {}"
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
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
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
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
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
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
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)"
371   interpret M': finite_measure M s by fact
373   let "?r S" = "M\<lparr> space := S, sets := (\<lambda>C. S \<inter> C)`sets M\<rparr>"
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
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
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
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
410   have "range A \<subseteq> sets M" using A_in_sets by auto
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
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
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) .
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
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
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
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
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
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)
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
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
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" .
549   let "?t A" = "\<nu> A - positive_integral (\<lambda>x. f x * indicator A x)"
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 .
586   have ac: "absolutely_continuous ?t" using `absolutely_continuous \<nu>` unfolding absolutely_continuous_def by auto
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)
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
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
630     let "?f0 x" = "f x + b * indicator A0 x"
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
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)
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
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)
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
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
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
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
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"
724   have "{} \<in> ?Q" using v.empty_measure by auto
725   then have Q_not_empty: "?Q \<noteq> {}" by blast
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
745   have Q'_sets: "\<And>i. Q' i \<in> sets M" using Q' by auto
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
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
774   let "?O_0" = "(\<Union>i. ?O i)"
775   have "?O_0 \<in> sets M" using Q' by auto
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
802   def Q \<equiv> "\<lambda>i. case i of 0 \<Rightarrow> ?O 0 | Suc n \<Rightarrow> ?O (Suc n) - ?O n"
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
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
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
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
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
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
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 .
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)]
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" .
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
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
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
1015 section "Radon Nikodym derivative"
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))"
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
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
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
1059 end