author hoelzl Wed Dec 01 19:20:30 2010 +0100 (2010-12-01) changeset 40859 de0b30e6c2d2 parent 39097 943c7b348524 child 40871 688f6ff859e1 permissions -rw-r--r--
Support product spaces on sigma finite measures.
Introduce the almost everywhere quantifier.
Introduce 'morphism' theorems for most constants.
Prove uniqueness of measures on cut stable generators.
Prove uniqueness of the Radon-Nikodym derivative.
Removed misleading suffix from borel_space and lebesgue_space.
Use product spaces to introduce Fubini on the Lebesgue integral.
Combine Euclidean_Lebesgue and Lebesgue_Measure.
Generalize theorems about mutual information and entropy to arbitrary probability spaces.
Remove simproc mult_log as it does not work with interpretations.
Introduce completion of measure spaces.
Change type of sigma.
Introduce dynkin systems.
2 imports Lebesgue_Integration
3 begin
5 lemma less_\<omega>_Ex_of_nat: "x < \<omega> \<longleftrightarrow> (\<exists>n. x < of_nat n)"
6 proof safe
7   assume "x < \<omega>"
8   then obtain r where "0 \<le> r" "x = Real r" by (cases x) auto
9   moreover obtain n where "r < of_nat n" using ex_less_of_nat by auto
10   ultimately show "\<exists>n. x < of_nat n" by (auto simp: real_eq_of_nat)
11 qed auto
13 lemma (in sigma_finite_measure) Ex_finite_integrable_function:
14   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>)"
15 proof -
16   obtain A :: "nat \<Rightarrow> 'a set" where
17     range: "range A \<subseteq> sets M" and
18     space: "(\<Union>i. A i) = space M" and
19     measure: "\<And>i. \<mu> (A i) \<noteq> \<omega>" and
20     disjoint: "disjoint_family A"
21     using disjoint_sigma_finite by auto
22   let "?B i" = "2^Suc i * \<mu> (A i)"
23   have "\<forall>i. \<exists>x. 0 < x \<and> x < inverse (?B i)"
24   proof
25     fix i show "\<exists>x. 0 < x \<and> x < inverse (?B i)"
26     proof cases
27       assume "\<mu> (A i) = 0"
28       then show ?thesis by (auto intro!: exI[of _ 1])
29     next
30       assume not_0: "\<mu> (A i) \<noteq> 0"
31       then have "?B i \<noteq> \<omega>" using measure[of i] by auto
32       then have "inverse (?B i) \<noteq> 0" unfolding pinfreal_inverse_eq_0 by simp
33       then show ?thesis using measure[of i] not_0
34         by (auto intro!: exI[of _ "inverse (?B i) / 2"]
35                  simp: pinfreal_noteq_omega_Ex zero_le_mult_iff zero_less_mult_iff mult_le_0_iff power_le_zero_eq)
36     qed
37   qed
38   from choice[OF this] obtain n where n: "\<And>i. 0 < n i"
39     "\<And>i. n i < inverse (2^Suc i * \<mu> (A i))" by auto
40   let "?h x" = "\<Sum>\<^isub>\<infinity> i. n i * indicator (A i) x"
41   show ?thesis
42   proof (safe intro!: bexI[of _ ?h] del: notI)
43     have "\<And>i. A i \<in> sets M"
44       using range by fastsimp+
45     then have "positive_integral ?h = (\<Sum>\<^isub>\<infinity> i. n i * \<mu> (A i))"
46       by (simp add: positive_integral_psuminf positive_integral_cmult_indicator)
47     also have "\<dots> \<le> (\<Sum>\<^isub>\<infinity> i. Real ((1 / 2)^Suc i))"
48     proof (rule psuminf_le)
49       fix N show "n N * \<mu> (A N) \<le> Real ((1 / 2) ^ Suc N)"
50         using measure[of N] n[of N]
51         by (cases "n N")
52            (auto simp: pinfreal_noteq_omega_Ex field_simps zero_le_mult_iff
53                        mult_le_0_iff mult_less_0_iff power_less_zero_eq
54                        power_le_zero_eq inverse_eq_divide less_divide_eq
55                        power_divide split: split_if_asm)
56     qed
57     also have "\<dots> = Real 1"
58       by (rule suminf_imp_psuminf, rule power_half_series, auto)
59     finally show "positive_integral ?h \<noteq> \<omega>" by auto
60   next
61     fix x assume "x \<in> space M"
62     then obtain i where "x \<in> A i" using space[symmetric] by auto
63     from psuminf_cmult_indicator[OF disjoint, OF this]
64     have "?h x = n i" by simp
65     then show "0 < ?h x" and "?h x < \<omega>" using n[of i] by auto
66   next
67     show "?h \<in> borel_measurable M" using range
68       by (auto intro!: borel_measurable_psuminf borel_measurable_pinfreal_times)
69   qed
70 qed
72 definition (in measure_space)
73   "absolutely_continuous \<nu> = (\<forall>N\<in>null_sets. \<nu> N = (0 :: pinfreal))"
75 lemma (in sigma_finite_measure) absolutely_continuous_AE:
76   assumes "measure_space M \<nu>" "absolutely_continuous \<nu>" "AE x. P x"
77   shows "measure_space.almost_everywhere M \<nu> P"
78 proof -
79   interpret \<nu>: measure_space M \<nu> by fact
80   from `AE x. P x` obtain N where N: "N \<in> null_sets" and "{x\<in>space M. \<not> P x} \<subseteq> N"
81     unfolding almost_everywhere_def by auto
82   show "\<nu>.almost_everywhere P"
83   proof (rule \<nu>.AE_I')
84     show "{x\<in>space M. \<not> P x} \<subseteq> N" by fact
85     from `absolutely_continuous \<nu>` show "N \<in> \<nu>.null_sets"
86       using N unfolding absolutely_continuous_def by auto
87   qed
88 qed
90 lemma (in finite_measure_space) absolutely_continuousI:
91   assumes "finite_measure_space M \<nu>"
92   assumes v: "\<And>x. \<lbrakk> x \<in> space M ; \<mu> {x} = 0 \<rbrakk> \<Longrightarrow> \<nu> {x} = 0"
93   shows "absolutely_continuous \<nu>"
94 proof (unfold absolutely_continuous_def sets_eq_Pow, safe)
95   fix N assume "\<mu> N = 0" "N \<subseteq> space M"
96   interpret v: finite_measure_space M \<nu> by fact
97   have "\<nu> N = \<nu> (\<Union>x\<in>N. {x})" by simp
98   also have "\<dots> = (\<Sum>x\<in>N. \<nu> {x})"
99   proof (rule v.measure_finitely_additive''[symmetric])
100     show "finite N" using `N \<subseteq> space M` finite_space by (auto intro: finite_subset)
101     show "disjoint_family_on (\<lambda>i. {i}) N" unfolding disjoint_family_on_def by auto
102     fix x assume "x \<in> N" thus "{x} \<in> sets M" using `N \<subseteq> space M` sets_eq_Pow by auto
103   qed
104   also have "\<dots> = 0"
105   proof (safe intro!: setsum_0')
106     fix x assume "x \<in> N"
107     hence "\<mu> {x} \<le> \<mu> N" using sets_eq_Pow `N \<subseteq> space M` by (auto intro!: measure_mono)
108     hence "\<mu> {x} = 0" using `\<mu> N = 0` by simp
109     thus "\<nu> {x} = 0" using v[of x] `x \<in> N` `N \<subseteq> space M` by auto
110   qed
111   finally show "\<nu> N = 0" .
112 qed
114 lemma (in finite_measure) Radon_Nikodym_aux_epsilon:
115   fixes e :: real assumes "0 < e"
116   assumes "finite_measure M s"
117   shows "\<exists>A\<in>sets M. real (\<mu> (space M)) - real (s (space M)) \<le>
118                     real (\<mu> A) - real (s A) \<and>
119                     (\<forall>B\<in>sets M. B \<subseteq> A \<longrightarrow> - e < real (\<mu> B) - real (s B))"
120 proof -
121   let "?d A" = "real (\<mu> A) - real (s A)"
122   interpret M': finite_measure M s by fact
124   let "?A A" = "if (\<forall>B\<in>sets M. B \<subseteq> space M - A \<longrightarrow> -e < ?d B)
125     then {}
126     else (SOME B. B \<in> sets M \<and> B \<subseteq> space M - A \<and> ?d B \<le> -e)"
127   def A \<equiv> "\<lambda>n. ((\<lambda>B. B \<union> ?A B) ^^ n) {}"
129   have A_simps[simp]:
130     "A 0 = {}"
131     "\<And>n. A (Suc n) = (A n \<union> ?A (A n))" unfolding A_def by simp_all
133   { fix A assume "A \<in> sets M"
134     have "?A A \<in> sets M"
135       by (auto intro!: someI2[of _ _ "\<lambda>A. A \<in> sets M"] simp: not_less) }
136   note A'_in_sets = this
138   { fix n have "A n \<in> sets M"
139     proof (induct n)
140       case (Suc n) thus "A (Suc n) \<in> sets M"
141         using A'_in_sets[of "A n"] by (auto split: split_if_asm)
142     qed (simp add: A_def) }
143   note A_in_sets = this
144   hence "range A \<subseteq> sets M" by auto
146   { fix n B
147     assume Ex: "\<exists>B. B \<in> sets M \<and> B \<subseteq> space M - A n \<and> ?d B \<le> -e"
148     hence False: "\<not> (\<forall>B\<in>sets M. B \<subseteq> space M - A n \<longrightarrow> -e < ?d B)" by (auto simp: not_less)
149     have "?d (A (Suc n)) \<le> ?d (A n) - e" unfolding A_simps if_not_P[OF False]
150     proof (rule someI2_ex[OF Ex])
151       fix B assume "B \<in> sets M \<and> B \<subseteq> space M - A n \<and> ?d B \<le> - e"
152       hence "A n \<inter> B = {}" "B \<in> sets M" and dB: "?d B \<le> -e" by auto
153       hence "?d (A n \<union> B) = ?d (A n) + ?d B"
154         using `A n \<in> sets M` real_finite_measure_Union M'.real_finite_measure_Union by simp
155       also have "\<dots> \<le> ?d (A n) - e" using dB by simp
156       finally show "?d (A n \<union> B) \<le> ?d (A n) - e" .
157     qed }
158   note dA_epsilon = this
160   { fix n have "?d (A (Suc n)) \<le> ?d (A n)"
161     proof (cases "\<exists>B. B\<in>sets M \<and> B \<subseteq> space M - A n \<and> ?d B \<le> - e")
162       case True from dA_epsilon[OF this] show ?thesis using `0 < e` by simp
163     next
164       case False
165       hence "\<forall>B\<in>sets M. B \<subseteq> space M - A n \<longrightarrow> -e < ?d B" by (auto simp: not_le)
166       thus ?thesis by simp
167     qed }
168   note dA_mono = this
170   show ?thesis
171   proof (cases "\<exists>n. \<forall>B\<in>sets M. B \<subseteq> space M - A n \<longrightarrow> -e < ?d B")
172     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
173     show ?thesis
174     proof (safe intro!: bexI[of _ "space M - A n"])
175       fix B assume "B \<in> sets M" "B \<subseteq> space M - A n"
176       from B[OF this] show "-e < ?d B" .
177     next
178       show "space M - A n \<in> sets M" by (rule compl_sets) fact
179     next
180       show "?d (space M) \<le> ?d (space M - A n)"
181       proof (induct n)
182         fix n assume "?d (space M) \<le> ?d (space M - A n)"
183         also have "\<dots> \<le> ?d (space M - A (Suc n))"
184           using A_in_sets sets_into_space dA_mono[of n]
185             real_finite_measure_Diff[of "space M"]
186             real_finite_measure_Diff[of "space M"]
187             M'.real_finite_measure_Diff[of "space M"]
188             M'.real_finite_measure_Diff[of "space M"]
189           by (simp del: A_simps)
190         finally show "?d (space M) \<le> ?d (space M - A (Suc n))" .
191       qed simp
192     qed
193   next
194     case False hence B: "\<And>n. \<exists>B. B\<in>sets M \<and> B \<subseteq> space M - A n \<and> ?d B \<le> - e"
195       by (auto simp add: not_less)
196     { fix n have "?d (A n) \<le> - real n * e"
197       proof (induct n)
198         case (Suc n) with dA_epsilon[of n, OF B] show ?case by (simp del: A_simps add: real_of_nat_Suc field_simps)
199       qed simp } note dA_less = this
200     have decseq: "decseq (\<lambda>n. ?d (A n))" unfolding decseq_eq_incseq
201     proof (rule incseq_SucI)
202       fix n show "- ?d (A n) \<le> - ?d (A (Suc n))" using dA_mono[of n] by auto
203     qed
204     from real_finite_continuity_from_below[of A] `range A \<subseteq> sets M`
205       M'.real_finite_continuity_from_below[of A]
206     have convergent: "(\<lambda>i. ?d (A i)) ----> ?d (\<Union>i. A i)"
207       by (auto intro!: LIMSEQ_diff)
208     obtain n :: nat where "- ?d (\<Union>i. A i) / e < real n" using reals_Archimedean2 by auto
209     moreover from order_trans[OF decseq_le[OF decseq convergent] dA_less]
210     have "real n \<le> - ?d (\<Union>i. A i) / e" using `0<e` by (simp add: field_simps)
211     ultimately show ?thesis by auto
212   qed
213 qed
215 lemma (in finite_measure) Radon_Nikodym_aux:
216   assumes "finite_measure M s"
217   shows "\<exists>A\<in>sets M. real (\<mu> (space M)) - real (s (space M)) \<le>
218                     real (\<mu> A) - real (s A) \<and>
219                     (\<forall>B\<in>sets M. B \<subseteq> A \<longrightarrow> 0 \<le> real (\<mu> B) - real (s B))"
220 proof -
221   let "?d A" = "real (\<mu> A) - real (s A)"
222   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)"
224   interpret M': finite_measure M s by fact
226   let "?r S" = "restricted_space S"
228   { fix S n
229     assume S: "S \<in> sets M"
230     hence **: "\<And>X. X \<in> op \<inter> S ` sets M \<longleftrightarrow> X \<in> sets M \<and> X \<subseteq> S" by auto
231     from M'.restricted_finite_measure[of S] restricted_finite_measure[of S] S
232     have "finite_measure (?r S) \<mu>" "0 < 1 / real (Suc n)"
233       "finite_measure (?r S) s" by auto
234     from finite_measure.Radon_Nikodym_aux_epsilon[OF this] guess X ..
235     hence "?P X S n"
236     proof (simp add: **, safe)
237       fix C assume C: "C \<in> sets M" "C \<subseteq> X" "X \<subseteq> S" and
238         *: "\<forall>B\<in>sets M. S \<inter> B \<subseteq> X \<longrightarrow> - (1 / real (Suc n)) < ?d (S \<inter> B)"
239       hence "C \<subseteq> S" "C \<subseteq> X" "S \<inter> C = C" by auto
240       with *[THEN bspec, OF `C \<in> sets M`]
241       show "- (1 / real (Suc n)) < ?d C" by auto
242     qed
243     hence "\<exists>A. ?P A S n" by auto }
244   note Ex_P = this
246   def A \<equiv> "nat_rec (space M) (\<lambda>n A. SOME B. ?P B A n)"
247   have A_Suc: "\<And>n. A (Suc n) = (SOME B. ?P B (A n) n)" by (simp add: A_def)
248   have A_0[simp]: "A 0 = space M" unfolding A_def by simp
250   { fix i have "A i \<in> sets M" unfolding A_def
251     proof (induct i)
252       case (Suc i)
253       from Ex_P[OF this, of i] show ?case unfolding nat_rec_Suc
254         by (rule someI2_ex) simp
255     qed simp }
256   note A_in_sets = this
258   { fix n have "?P (A (Suc n)) (A n) n"
259       using Ex_P[OF A_in_sets] unfolding A_Suc
260       by (rule someI2_ex) simp }
261   note P_A = this
263   have "range A \<subseteq> sets M" using A_in_sets by auto
265   have A_mono: "\<And>i. A (Suc i) \<subseteq> A i" using P_A by simp
266   have mono_dA: "mono (\<lambda>i. ?d (A i))" using P_A by (simp add: mono_iff_le_Suc)
267   have epsilon: "\<And>C i. \<lbrakk> C \<in> sets M; C \<subseteq> A (Suc i) \<rbrakk> \<Longrightarrow> - 1 / real (Suc i) < ?d C"
268       using P_A by auto
270   show ?thesis
271   proof (safe intro!: bexI[of _ "\<Inter>i. A i"])
272     show "(\<Inter>i. A i) \<in> sets M" using A_in_sets by auto
273     from `range A \<subseteq> sets M` A_mono
274       real_finite_continuity_from_above[of A]
275       M'.real_finite_continuity_from_above[of A]
276     have "(\<lambda>i. ?d (A i)) ----> ?d (\<Inter>i. A i)" by (auto intro!: LIMSEQ_diff)
277     thus "?d (space M) \<le> ?d (\<Inter>i. A i)" using mono_dA[THEN monoD, of 0 _]
278       by (rule_tac LIMSEQ_le_const) (auto intro!: exI)
279   next
280     fix B assume B: "B \<in> sets M" "B \<subseteq> (\<Inter>i. A i)"
281     show "0 \<le> ?d B"
282     proof (rule ccontr)
283       assume "\<not> 0 \<le> ?d B"
284       hence "0 < - ?d B" by auto
285       from ex_inverse_of_nat_Suc_less[OF this]
286       obtain n where *: "?d B < - 1 / real (Suc n)"
287         by (auto simp: real_eq_of_nat inverse_eq_divide field_simps)
288       have "B \<subseteq> A (Suc n)" using B by (auto simp del: nat_rec_Suc)
289       from epsilon[OF B(1) this] *
290       show False by auto
291     qed
292   qed
293 qed
295 lemma (in finite_measure) Radon_Nikodym_finite_measure:
296   assumes "finite_measure M \<nu>"
297   assumes "absolutely_continuous \<nu>"
298   shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
299 proof -
300   interpret M': finite_measure M \<nu> using assms(1) .
302   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}"
303   have "(\<lambda>x. 0) \<in> G" unfolding G_def by auto
304   hence "G \<noteq> {}" by auto
306   { fix f g assume f: "f \<in> G" and g: "g \<in> G"
307     have "(\<lambda>x. max (g x) (f x)) \<in> G" (is "?max \<in> G") unfolding G_def
308     proof safe
309       show "?max \<in> borel_measurable M" using f g unfolding G_def by auto
311       let ?A = "{x \<in> space M. f x \<le> g x}"
312       have "?A \<in> sets M" using f g unfolding G_def by auto
314       fix A assume "A \<in> sets M"
315       hence sets: "?A \<inter> A \<in> sets M" "(space M - ?A) \<inter> A \<in> sets M" using `?A \<in> sets M` by auto
316       have union: "((?A \<inter> A) \<union> ((space M - ?A) \<inter> A)) = A"
317         using sets_into_space[OF `A \<in> sets M`] by auto
319       have "\<And>x. x \<in> space M \<Longrightarrow> max (g x) (f x) * indicator A x =
320         g x * indicator (?A \<inter> A) x + f x * indicator ((space M - ?A) \<inter> A) x"
321         by (auto simp: indicator_def max_def)
322       hence "positive_integral (\<lambda>x. max (g x) (f x) * indicator A x) =
323         positive_integral (\<lambda>x. g x * indicator (?A \<inter> A) x) +
324         positive_integral (\<lambda>x. f x * indicator ((space M - ?A) \<inter> A) x)"
325         using f g sets unfolding G_def
326         by (auto cong: positive_integral_cong intro!: positive_integral_add borel_measurable_indicator)
327       also have "\<dots> \<le> \<nu> (?A \<inter> A) + \<nu> ((space M - ?A) \<inter> A)"
328         using f g sets unfolding G_def by (auto intro!: add_mono)
329       also have "\<dots> = \<nu> A"
330         using M'.measure_additive[OF sets] union by auto
331       finally show "positive_integral (\<lambda>x. max (g x) (f x) * indicator A x) \<le> \<nu> A" .
332     qed }
333   note max_in_G = this
335   { fix f g assume  "f \<up> g" and f: "\<And>i. f i \<in> G"
336     have "g \<in> G" unfolding G_def
337     proof safe
338       from `f \<up> g` have [simp]: "g = (SUP i. f i)" unfolding isoton_def by simp
339       have f_borel: "\<And>i. f i \<in> borel_measurable M" using f unfolding G_def by simp
340       thus "g \<in> borel_measurable M" by (auto intro!: borel_measurable_SUP)
342       fix A assume "A \<in> sets M"
343       hence "\<And>i. (\<lambda>x. f i x * indicator A x) \<in> borel_measurable M"
344         using f_borel by (auto intro!: borel_measurable_indicator)
345       from positive_integral_isoton[OF isoton_indicator[OF `f \<up> g`] this]
346       have SUP: "positive_integral (\<lambda>x. g x * indicator A x) =
347           (SUP i. positive_integral (\<lambda>x. f i x * indicator A x))"
348         unfolding isoton_def by simp
349       show "positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A" unfolding SUP
350         using f `A \<in> sets M` unfolding G_def by (auto intro!: SUP_leI)
351     qed }
352   note SUP_in_G = this
354   let ?y = "SUP g : G. positive_integral g"
355   have "?y \<le> \<nu> (space M)" unfolding G_def
356   proof (safe intro!: SUP_leI)
357     fix g assume "\<forall>A\<in>sets M. positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A"
358     from this[THEN bspec, OF top] show "positive_integral g \<le> \<nu> (space M)"
359       by (simp cong: positive_integral_cong)
360   qed
361   hence "?y \<noteq> \<omega>" using M'.finite_measure_of_space by auto
362   from SUPR_countable_SUPR[OF this `G \<noteq> {}`] guess ys .. note ys = this
363   hence "\<forall>n. \<exists>g. g\<in>G \<and> positive_integral g = ys n"
364   proof safe
365     fix n assume "range ys \<subseteq> positive_integral ` G"
366     hence "ys n \<in> positive_integral ` G" by auto
367     thus "\<exists>g. g\<in>G \<and> positive_integral g = ys n" by auto
368   qed
369   from choice[OF this] obtain gs where "\<And>i. gs i \<in> G" "\<And>n. positive_integral (gs n) = ys n" by auto
370   hence y_eq: "?y = (SUP i. positive_integral (gs i))" using ys by auto
371   let "?g i x" = "Max ((\<lambda>n. gs n x) ` {..i})"
372   def f \<equiv> "SUP i. ?g i"
373   have gs_not_empty: "\<And>i. (\<lambda>n. gs n x) ` {..i} \<noteq> {}" by auto
374   { fix i have "?g i \<in> G"
375     proof (induct i)
376       case 0 thus ?case by simp fact
377     next
378       case (Suc i)
379       with Suc gs_not_empty `gs (Suc i) \<in> G` show ?case
380         by (auto simp add: atMost_Suc intro!: max_in_G)
381     qed }
382   note g_in_G = this
383   have "\<And>x. \<forall>i. ?g i x \<le> ?g (Suc i) x"
384     using gs_not_empty by (simp add: atMost_Suc)
385   hence isoton_g: "?g \<up> f" by (simp add: isoton_def le_fun_def f_def)
386   from SUP_in_G[OF this g_in_G] have "f \<in> G" .
387   hence [simp, intro]: "f \<in> borel_measurable M" unfolding G_def by auto
389   have "(\<lambda>i. positive_integral (?g i)) \<up> positive_integral f"
390     using isoton_g g_in_G by (auto intro!: positive_integral_isoton simp: G_def f_def)
391   hence "positive_integral f = (SUP i. positive_integral (?g i))"
392     unfolding isoton_def by simp
393   also have "\<dots> = ?y"
394   proof (rule antisym)
395     show "(SUP i. positive_integral (?g i)) \<le> ?y"
396       using g_in_G by (auto intro!: exI Sup_mono simp: SUPR_def)
397     show "?y \<le> (SUP i. positive_integral (?g i))" unfolding y_eq
398       by (auto intro!: SUP_mono positive_integral_mono Max_ge)
399   qed
400   finally have int_f_eq_y: "positive_integral f = ?y" .
402   let "?t A" = "\<nu> A - positive_integral (\<lambda>x. f x * indicator A x)"
404   have "finite_measure M ?t"
405   proof
406     show "?t {} = 0" by simp
407     show "?t (space M) \<noteq> \<omega>" using M'.finite_measure by simp
408     show "countably_additive M ?t" unfolding countably_additive_def
409     proof safe
410       fix A :: "nat \<Rightarrow> 'a set"  assume A: "range A \<subseteq> sets M" "disjoint_family A"
411       have "(\<Sum>\<^isub>\<infinity> n. positive_integral (\<lambda>x. f x * indicator (A n) x))
412         = positive_integral (\<lambda>x. (\<Sum>\<^isub>\<infinity>n. f x * indicator (A n) x))"
413         using `range A \<subseteq> sets M`
414         by (rule_tac positive_integral_psuminf[symmetric]) (auto intro!: borel_measurable_indicator)
415       also have "\<dots> = positive_integral (\<lambda>x. f x * indicator (\<Union>n. A n) x)"
416         apply (rule positive_integral_cong)
417         apply (subst psuminf_cmult_right)
418         unfolding psuminf_indicator[OF `disjoint_family A`] ..
419       finally have "(\<Sum>\<^isub>\<infinity> n. positive_integral (\<lambda>x. f x * indicator (A n) x))
420         = positive_integral (\<lambda>x. f x * indicator (\<Union>n. A n) x)" .
421       moreover have "(\<Sum>\<^isub>\<infinity>n. \<nu> (A n)) = \<nu> (\<Union>n. A n)"
422         using M'.measure_countably_additive A by (simp add: comp_def)
423       moreover have "\<And>i. positive_integral (\<lambda>x. f x * indicator (A i) x) \<le> \<nu> (A i)"
424           using A `f \<in> G` unfolding G_def by auto
425       moreover have v_fin: "\<nu> (\<Union>i. A i) \<noteq> \<omega>" using M'.finite_measure A by (simp add: countable_UN)
426       moreover {
427         have "positive_integral (\<lambda>x. f x * indicator (\<Union>i. A i) x) \<le> \<nu> (\<Union>i. A i)"
428           using A `f \<in> G` unfolding G_def by (auto simp: countable_UN)
429         also have "\<nu> (\<Union>i. A i) < \<omega>" using v_fin by (simp add: pinfreal_less_\<omega>)
430         finally have "positive_integral (\<lambda>x. f x * indicator (\<Union>i. A i) x) \<noteq> \<omega>"
431           by (simp add: pinfreal_less_\<omega>) }
432       ultimately
433       show "(\<Sum>\<^isub>\<infinity> n. ?t (A n)) = ?t (\<Union>i. A i)"
434         apply (subst psuminf_minus) by simp_all
435     qed
436   qed
437   then interpret M: finite_measure M ?t .
439   have ac: "absolutely_continuous ?t" using `absolutely_continuous \<nu>` unfolding absolutely_continuous_def by auto
441   have upper_bound: "\<forall>A\<in>sets M. ?t A \<le> 0"
442   proof (rule ccontr)
443     assume "\<not> ?thesis"
444     then obtain A where A: "A \<in> sets M" and pos: "0 < ?t A"
445       by (auto simp: not_le)
446     note pos
447     also have "?t A \<le> ?t (space M)"
448       using M.measure_mono[of A "space M"] A sets_into_space by simp
449     finally have pos_t: "0 < ?t (space M)" by simp
450     moreover
451     hence pos_M: "0 < \<mu> (space M)"
452       using ac top unfolding absolutely_continuous_def by auto
453     moreover
454     have "positive_integral (\<lambda>x. f x * indicator (space M) x) \<le> \<nu> (space M)"
455       using `f \<in> G` unfolding G_def by auto
456     hence "positive_integral (\<lambda>x. f x * indicator (space M) x) \<noteq> \<omega>"
457       using M'.finite_measure_of_space by auto
458     moreover
459     def b \<equiv> "?t (space M) / \<mu> (space M) / 2"
460     ultimately have b: "b \<noteq> 0" "b \<noteq> \<omega>"
461       using M'.finite_measure_of_space
462       by (auto simp: pinfreal_inverse_eq_0 finite_measure_of_space)
464     have "finite_measure M (\<lambda>A. b * \<mu> A)" (is "finite_measure M ?b")
465     proof
466       show "?b {} = 0" by simp
467       show "?b (space M) \<noteq> \<omega>" using finite_measure_of_space b by auto
468       show "countably_additive M ?b"
469         unfolding countably_additive_def psuminf_cmult_right
470         using measure_countably_additive by auto
471     qed
473     from M.Radon_Nikodym_aux[OF this]
474     obtain A0 where "A0 \<in> sets M" and
475       space_less_A0: "real (?t (space M)) - real (b * \<mu> (space M)) \<le> real (?t A0) - real (b * \<mu> A0)" and
476       *: "\<And>B. \<lbrakk> B \<in> sets M ; B \<subseteq> A0 \<rbrakk> \<Longrightarrow> 0 \<le> real (?t B) - real (b * \<mu> B)" by auto
477     { fix B assume "B \<in> sets M" "B \<subseteq> A0"
478       with *[OF this] have "b * \<mu> B \<le> ?t B"
479         using M'.finite_measure b finite_measure
480         by (cases "b * \<mu> B", cases "?t B") (auto simp: field_simps) }
481     note bM_le_t = this
483     let "?f0 x" = "f x + b * indicator A0 x"
485     { fix A assume A: "A \<in> sets M"
486       hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
487       have "positive_integral (\<lambda>x. ?f0 x  * indicator A x) =
488         positive_integral (\<lambda>x. f x * indicator A x + b * indicator (A \<inter> A0) x)"
489         by (auto intro!: positive_integral_cong simp: field_simps indicator_inter_arith)
490       hence "positive_integral (\<lambda>x. ?f0 x * indicator A x) =
491           positive_integral (\<lambda>x. f x * indicator A x) + b * \<mu> (A \<inter> A0)"
492         using `A0 \<in> sets M` `A \<inter> A0 \<in> sets M` A
493         by (simp add: borel_measurable_indicator positive_integral_add positive_integral_cmult_indicator) }
494     note f0_eq = this
496     { fix A assume A: "A \<in> sets M"
497       hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
498       have f_le_v: "positive_integral (\<lambda>x. f x * indicator A x) \<le> \<nu> A"
499         using `f \<in> G` A unfolding G_def by auto
500       note f0_eq[OF A]
501       also have "positive_integral (\<lambda>x. f x * indicator A x) + b * \<mu> (A \<inter> A0) \<le>
502           positive_integral (\<lambda>x. f x * indicator A x) + ?t (A \<inter> A0)"
503         using bM_le_t[OF `A \<inter> A0 \<in> sets M`] `A \<in> sets M` `A0 \<in> sets M`
504         by (auto intro!: add_left_mono)
505       also have "\<dots> \<le> positive_integral (\<lambda>x. f x * indicator A x) + ?t A"
506         using M.measure_mono[simplified, OF _ `A \<inter> A0 \<in> sets M` `A \<in> sets M`]
507         by (auto intro!: add_left_mono)
508       also have "\<dots> \<le> \<nu> A"
509         using f_le_v M'.finite_measure[simplified, OF `A \<in> sets M`]
510         by (cases "positive_integral (\<lambda>x. f x * indicator A x)", cases "\<nu> A", auto)
511       finally have "positive_integral (\<lambda>x. ?f0 x * indicator A x) \<le> \<nu> A" . }
512     hence "?f0 \<in> G" using `A0 \<in> sets M` unfolding G_def
513       by (auto intro!: borel_measurable_indicator borel_measurable_pinfreal_add borel_measurable_pinfreal_times)
515     have real: "?t (space M) \<noteq> \<omega>" "?t A0 \<noteq> \<omega>"
516       "b * \<mu> (space M) \<noteq> \<omega>" "b * \<mu> A0 \<noteq> \<omega>"
517       using `A0 \<in> sets M` b
518         finite_measure[of A0] M.finite_measure[of A0]
519         finite_measure_of_space M.finite_measure_of_space
520       by auto
522     have int_f_finite: "positive_integral f \<noteq> \<omega>"
523       using M'.finite_measure_of_space pos_t unfolding pinfreal_zero_less_diff_iff
524       by (auto cong: positive_integral_cong)
526     have "?t (space M) > b * \<mu> (space M)" unfolding b_def
527       apply (simp add: field_simps)
528       apply (subst mult_assoc[symmetric])
529       apply (subst pinfreal_mult_inverse)
530       using finite_measure_of_space M'.finite_measure_of_space pos_t pos_M
531       using pinfreal_mult_strict_right_mono[of "Real (1/2)" 1 "?t (space M)"]
532       by simp_all
533     hence  "0 < ?t (space M) - b * \<mu> (space M)"
534       by (simp add: pinfreal_zero_less_diff_iff)
535     also have "\<dots> \<le> ?t A0 - b * \<mu> A0"
536       using space_less_A0 pos_M pos_t b real[unfolded pinfreal_noteq_omega_Ex] by auto
537     finally have "b * \<mu> A0 < ?t A0" unfolding pinfreal_zero_less_diff_iff .
538     hence "0 < ?t A0" by auto
539     hence "0 < \<mu> A0" using ac unfolding absolutely_continuous_def
540       using `A0 \<in> sets M` by auto
541     hence "0 < b * \<mu> A0" using b by auto
543     from int_f_finite this
544     have "?y + 0 < positive_integral f + b * \<mu> A0" unfolding int_f_eq_y
545       by (rule pinfreal_less_add)
546     also have "\<dots> = positive_integral ?f0" using f0_eq[OF top] `A0 \<in> sets M` sets_into_space
547       by (simp cong: positive_integral_cong)
548     finally have "?y < positive_integral ?f0" by simp
550     moreover from `?f0 \<in> G` have "positive_integral ?f0 \<le> ?y" by (auto intro!: le_SUPI)
551     ultimately show False by auto
552   qed
554   show ?thesis
555   proof (safe intro!: bexI[of _ f])
556     fix A assume "A\<in>sets M"
557     show "\<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
558     proof (rule antisym)
559       show "positive_integral (\<lambda>x. f x * indicator A x) \<le> \<nu> A"
560         using `f \<in> G` `A \<in> sets M` unfolding G_def by auto
561       show "\<nu> A \<le> positive_integral (\<lambda>x. f x * indicator A x)"
562         using upper_bound[THEN bspec, OF `A \<in> sets M`]
563          by (simp add: pinfreal_zero_le_diff)
564     qed
565   qed simp
566 qed
568 lemma (in finite_measure) split_space_into_finite_sets_and_rest:
569   assumes "measure_space M \<nu>"
570   assumes ac: "absolutely_continuous \<nu>"
571   shows "\<exists>\<Omega>0\<in>sets M. \<exists>\<Omega>::nat\<Rightarrow>'a set. disjoint_family \<Omega> \<and> range \<Omega> \<subseteq> sets M \<and> \<Omega>0 = space M - (\<Union>i. \<Omega> i) \<and>
572     (\<forall>A\<in>sets M. A \<subseteq> \<Omega>0 \<longrightarrow> (\<mu> A = 0 \<and> \<nu> A = 0) \<or> (\<mu> A > 0 \<and> \<nu> A = \<omega>)) \<and>
573     (\<forall>i. \<nu> (\<Omega> i) \<noteq> \<omega>)"
574 proof -
575   interpret v: measure_space M \<nu> by fact
576   let ?Q = "{Q\<in>sets M. \<nu> Q \<noteq> \<omega>}"
577   let ?a = "SUP Q:?Q. \<mu> Q"
579   have "{} \<in> ?Q" using v.empty_measure by auto
580   then have Q_not_empty: "?Q \<noteq> {}" by blast
582   have "?a \<le> \<mu> (space M)" using sets_into_space
583     by (auto intro!: SUP_leI measure_mono top)
584   then have "?a \<noteq> \<omega>" using finite_measure_of_space
585     by auto
586   from SUPR_countable_SUPR[OF this Q_not_empty]
587   obtain Q'' where "range Q'' \<subseteq> \<mu> ` ?Q" and a: "?a = (SUP i::nat. Q'' i)"
588     by auto
589   then have "\<forall>i. \<exists>Q'. Q'' i = \<mu> Q' \<and> Q' \<in> ?Q" by auto
590   from choice[OF this] obtain Q' where Q': "\<And>i. Q'' i = \<mu> (Q' i)" "\<And>i. Q' i \<in> ?Q"
591     by auto
592   then have a_Lim: "?a = (SUP i::nat. \<mu> (Q' i))" using a by simp
593   let "?O n" = "\<Union>i\<le>n. Q' i"
594   have Union: "(SUP i. \<mu> (?O i)) = \<mu> (\<Union>i. ?O i)"
595   proof (rule continuity_from_below[of ?O])
596     show "range ?O \<subseteq> sets M" using Q' by (auto intro!: finite_UN)
597     show "\<And>i. ?O i \<subseteq> ?O (Suc i)" by fastsimp
598   qed
600   have Q'_sets: "\<And>i. Q' i \<in> sets M" using Q' by auto
602   have O_sets: "\<And>i. ?O i \<in> sets M"
603      using Q' by (auto intro!: finite_UN Un)
604   then have O_in_G: "\<And>i. ?O i \<in> ?Q"
605   proof (safe del: notI)
606     fix i have "Q' ` {..i} \<subseteq> sets M"
607       using Q' by (auto intro: finite_UN)
608     with v.measure_finitely_subadditive[of "{.. i}" Q']
609     have "\<nu> (?O i) \<le> (\<Sum>i\<le>i. \<nu> (Q' i))" by auto
610     also have "\<dots> < \<omega>" unfolding setsum_\<omega> pinfreal_less_\<omega> using Q' by auto
611     finally show "\<nu> (?O i) \<noteq> \<omega>" unfolding pinfreal_less_\<omega> by auto
612   qed auto
613   have O_mono: "\<And>n. ?O n \<subseteq> ?O (Suc n)" by fastsimp
615   have a_eq: "?a = \<mu> (\<Union>i. ?O i)" unfolding Union[symmetric]
616   proof (rule antisym)
617     show "?a \<le> (SUP i. \<mu> (?O i))" unfolding a_Lim
618       using Q' by (auto intro!: SUP_mono measure_mono finite_UN)
619     show "(SUP i. \<mu> (?O i)) \<le> ?a" unfolding SUPR_def
620     proof (safe intro!: Sup_mono, unfold bex_simps)
621       fix i
622       have *: "(\<Union>Q' ` {..i}) = ?O i" by auto
623       then show "\<exists>x. (x \<in> sets M \<and> \<nu> x \<noteq> \<omega>) \<and>
624         \<mu> (\<Union>Q' ` {..i}) \<le> \<mu> x"
625         using O_in_G[of i] by (auto intro!: exI[of _ "?O i"])
626     qed
627   qed
629   let "?O_0" = "(\<Union>i. ?O i)"
630   have "?O_0 \<in> sets M" using Q' by auto
632   def Q \<equiv> "\<lambda>i. case i of 0 \<Rightarrow> Q' 0 | Suc n \<Rightarrow> ?O (Suc n) - ?O n"
633   { fix i have "Q i \<in> sets M" unfolding Q_def using Q'[of 0] by (cases i) (auto intro: O_sets) }
634   note Q_sets = this
636   show ?thesis
637   proof (intro bexI exI conjI ballI impI allI)
638     show "disjoint_family Q"
639       by (fastsimp simp: disjoint_family_on_def Q_def
640         split: nat.split_asm)
641     show "range Q \<subseteq> sets M"
642       using Q_sets by auto
644     { fix A assume A: "A \<in> sets M" "A \<subseteq> space M - ?O_0"
645       show "\<mu> A = 0 \<and> \<nu> A = 0 \<or> 0 < \<mu> A \<and> \<nu> A = \<omega>"
646       proof (rule disjCI, simp)
647         assume *: "0 < \<mu> A \<longrightarrow> \<nu> A \<noteq> \<omega>"
648         show "\<mu> A = 0 \<and> \<nu> A = 0"
649         proof cases
650           assume "\<mu> A = 0" moreover with ac A have "\<nu> A = 0"
651             unfolding absolutely_continuous_def by auto
652           ultimately show ?thesis by simp
653         next
654           assume "\<mu> A \<noteq> 0" with * have "\<nu> A \<noteq> \<omega>" by auto
655           with A have "\<mu> ?O_0 + \<mu> A = \<mu> (?O_0 \<union> A)"
656             using Q' by (auto intro!: measure_additive countable_UN)
657           also have "\<dots> = (SUP i. \<mu> (?O i \<union> A))"
658           proof (rule continuity_from_below[of "\<lambda>i. ?O i \<union> A", symmetric, simplified])
659             show "range (\<lambda>i. ?O i \<union> A) \<subseteq> sets M"
660               using `\<nu> A \<noteq> \<omega>` O_sets A by auto
661           qed fastsimp
662           also have "\<dots> \<le> ?a"
663           proof (safe intro!: SUPR_bound)
664             fix i have "?O i \<union> A \<in> ?Q"
665             proof (safe del: notI)
666               show "?O i \<union> A \<in> sets M" using O_sets A by auto
667               from O_in_G[of i]
668               moreover have "\<nu> (?O i \<union> A) \<le> \<nu> (?O i) + \<nu> A"
669                 using v.measure_subadditive[of "?O i" A] A O_sets by auto
670               ultimately show "\<nu> (?O i \<union> A) \<noteq> \<omega>"
671                 using `\<nu> A \<noteq> \<omega>` by auto
672             qed
673             then show "\<mu> (?O i \<union> A) \<le> ?a" by (rule le_SUPI)
674           qed
675           finally have "\<mu> A = 0" unfolding a_eq using finite_measure[OF `?O_0 \<in> sets M`]
676             by (cases "\<mu> A") (auto simp: pinfreal_noteq_omega_Ex)
677           with `\<mu> A \<noteq> 0` show ?thesis by auto
678         qed
679       qed }
681     { fix i show "\<nu> (Q i) \<noteq> \<omega>"
682       proof (cases i)
683         case 0 then show ?thesis
684           unfolding Q_def using Q'[of 0] by simp
685       next
686         case (Suc n)
687         then show ?thesis unfolding Q_def
688           using `?O n \<in> ?Q` `?O (Suc n) \<in> ?Q` O_mono
689           using v.measure_Diff[of "?O n" "?O (Suc n)"] by auto
690       qed }
692     show "space M - ?O_0 \<in> sets M" using Q'_sets by auto
694     { fix j have "(\<Union>i\<le>j. ?O i) = (\<Union>i\<le>j. Q i)"
695       proof (induct j)
696         case 0 then show ?case by (simp add: Q_def)
697       next
698         case (Suc j)
699         have eq: "\<And>j. (\<Union>i\<le>j. ?O i) = (\<Union>i\<le>j. Q' i)" by fastsimp
700         have "{..j} \<union> {..Suc j} = {..Suc j}" by auto
701         then have "(\<Union>i\<le>Suc j. Q' i) = (\<Union>i\<le>j. Q' i) \<union> Q (Suc j)"
702           by (simp add: UN_Un[symmetric] Q_def del: UN_Un)
703         then show ?case using Suc by (auto simp add: eq atMost_Suc)
704       qed }
705     then have "(\<Union>j. (\<Union>i\<le>j. ?O i)) = (\<Union>j. (\<Union>i\<le>j. Q i))" by simp
706     then show "space M - ?O_0 = space M - (\<Union>i. Q i)" by fastsimp
707   qed
708 qed
710 lemma (in finite_measure) Radon_Nikodym_finite_measure_infinite:
711   assumes "measure_space M \<nu>"
712   assumes "absolutely_continuous \<nu>"
713   shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
714 proof -
715   interpret v: measure_space M \<nu> by fact
717   from split_space_into_finite_sets_and_rest[OF assms]
718   obtain Q0 and Q :: "nat \<Rightarrow> 'a set"
719     where Q: "disjoint_family Q" "range Q \<subseteq> sets M"
720     and Q0: "Q0 \<in> sets M" "Q0 = space M - (\<Union>i. Q i)"
721     and in_Q0: "\<And>A. A \<in> sets M \<Longrightarrow> A \<subseteq> Q0 \<Longrightarrow> \<mu> A = 0 \<and> \<nu> A = 0 \<or> 0 < \<mu> A \<and> \<nu> A = \<omega>"
722     and Q_fin: "\<And>i. \<nu> (Q i) \<noteq> \<omega>" by force
723   from Q have Q_sets: "\<And>i. Q i \<in> sets M" by auto
725   have "\<forall>i. \<exists>f. f\<in>borel_measurable M \<and> (\<forall>A\<in>sets M.
726     \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f x * indicator (Q i \<inter> A) x))"
727   proof
728     fix i
729     have indicator_eq: "\<And>f x A. (f x :: pinfreal) * indicator (Q i \<inter> A) x * indicator (Q i) x
730       = (f x * indicator (Q i) x) * indicator A x"
731       unfolding indicator_def by auto
733     have fm: "finite_measure (restricted_space (Q i)) \<mu>"
734       (is "finite_measure ?R \<mu>") by (rule restricted_finite_measure[OF Q_sets[of i]])
735     then interpret R: finite_measure ?R .
736     have fmv: "finite_measure ?R \<nu>"
737       unfolding finite_measure_def finite_measure_axioms_def
738     proof
739       show "measure_space ?R \<nu>"
740         using v.restricted_measure_space Q_sets[of i] by auto
741       show "\<nu>  (space ?R) \<noteq> \<omega>"
742         using Q_fin by simp
743     qed
744     have "R.absolutely_continuous \<nu>"
745       using `absolutely_continuous \<nu>` `Q i \<in> sets M`
746       by (auto simp: R.absolutely_continuous_def absolutely_continuous_def)
747     from finite_measure.Radon_Nikodym_finite_measure[OF fm fmv this]
748     obtain f where f: "(\<lambda>x. f x * indicator (Q i) x) \<in> borel_measurable M"
749       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)"
750       unfolding Bex_def borel_measurable_restricted[OF `Q i \<in> sets M`]
751         positive_integral_restricted[OF `Q i \<in> sets M`] by (auto simp: indicator_eq)
752     then show "\<exists>f. f\<in>borel_measurable M \<and> (\<forall>A\<in>sets M.
753       \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f x * indicator (Q i \<inter> A) x))"
754       by (fastsimp intro!: exI[of _ "\<lambda>x. f x * indicator (Q i) x"] positive_integral_cong
755           simp: indicator_def)
756   qed
757   from choice[OF this] obtain f where borel: "\<And>i. f i \<in> borel_measurable M"
758     and f: "\<And>A i. A \<in> sets M \<Longrightarrow>
759       \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f i x * indicator (Q i \<inter> A) x)"
760     by auto
761   let "?f x" =
762     "(\<Sum>\<^isub>\<infinity> i. f i x * indicator (Q i) x) + \<omega> * indicator Q0 x"
763   show ?thesis
764   proof (safe intro!: bexI[of _ ?f])
765     show "?f \<in> borel_measurable M"
766       by (safe intro!: borel_measurable_psuminf borel_measurable_pinfreal_times
768         borel_measurable_const borel Q_sets Q0 Diff countable_UN)
769     fix A assume "A \<in> sets M"
770     have *:
771       "\<And>x i. indicator A x * (f i x * indicator (Q i) x) =
772         f i x * indicator (Q i \<inter> A) x"
773       "\<And>x i. (indicator A x * indicator Q0 x :: pinfreal) =
774         indicator (Q0 \<inter> A) x" by (auto simp: indicator_def)
775     have "positive_integral (\<lambda>x. ?f x * indicator A x) =
776       (\<Sum>\<^isub>\<infinity> i. \<nu> (Q i \<inter> A)) + \<omega> * \<mu> (Q0 \<inter> A)"
777       unfolding f[OF `A \<in> sets M`]
778       apply (simp del: pinfreal_times(2) add: field_simps *)
779       apply (subst positive_integral_add)
780       apply (fastsimp intro: Q0 `A \<in> sets M`)
781       apply (fastsimp intro: Q_sets `A \<in> sets M` borel_measurable_psuminf borel)
782       apply (subst positive_integral_cmult_indicator)
783       apply (fastsimp intro: Q0 `A \<in> sets M`)
784       unfolding psuminf_cmult_right[symmetric]
785       apply (subst positive_integral_psuminf)
786       apply (fastsimp intro: `A \<in> sets M` Q_sets borel)
787       apply (simp add: *)
788       done
789     moreover have "(\<Sum>\<^isub>\<infinity>i. \<nu> (Q i \<inter> A)) = \<nu> ((\<Union>i. Q i) \<inter> A)"
790       using Q Q_sets `A \<in> sets M`
791       by (intro v.measure_countably_additive[of "\<lambda>i. Q i \<inter> A", unfolded comp_def, simplified])
792          (auto simp: disjoint_family_on_def)
793     moreover have "\<omega> * \<mu> (Q0 \<inter> A) = \<nu> (Q0 \<inter> A)"
794     proof -
795       have "Q0 \<inter> A \<in> sets M" using Q0(1) `A \<in> sets M` by blast
796       from in_Q0[OF this] show ?thesis by auto
797     qed
798     moreover have "Q0 \<inter> A \<in> sets M" "((\<Union>i. Q i) \<inter> A) \<in> sets M"
799       using Q_sets `A \<in> sets M` Q0(1) by (auto intro!: countable_UN)
800     moreover have "((\<Union>i. Q i) \<inter> A) \<union> (Q0 \<inter> A) = A" "((\<Union>i. Q i) \<inter> A) \<inter> (Q0 \<inter> A) = {}"
801       using `A \<in> sets M` sets_into_space Q0 by auto
802     ultimately show "\<nu> A = positive_integral (\<lambda>x. ?f x * indicator A x)"
803       using v.measure_additive[simplified, of "(\<Union>i. Q i) \<inter> A" "Q0 \<inter> A"]
804       by simp
805   qed
806 qed
808 lemma (in sigma_finite_measure) Radon_Nikodym:
809   assumes "measure_space M \<nu>"
810   assumes "absolutely_continuous \<nu>"
811   shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
812 proof -
813   from Ex_finite_integrable_function
814   obtain h where finite: "positive_integral h \<noteq> \<omega>" and
815     borel: "h \<in> borel_measurable M" and
816     pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x" and
817     "\<And>x. x \<in> space M \<Longrightarrow> h x < \<omega>" by auto
818   let "?T A" = "positive_integral (\<lambda>x. h x * indicator A x)"
819   from measure_space_density[OF borel] finite
820   interpret T: finite_measure M ?T
821     unfolding finite_measure_def finite_measure_axioms_def
822     by (simp cong: positive_integral_cong)
823   have "\<And>N. N \<in> sets M \<Longrightarrow> {x \<in> space M. h x \<noteq> 0 \<and> indicator N x \<noteq> (0::pinfreal)} = N"
824     using sets_into_space pos by (force simp: indicator_def)
825   then have "T.absolutely_continuous \<nu>" using assms(2) borel
826     unfolding T.absolutely_continuous_def absolutely_continuous_def
827     by (fastsimp simp: borel_measurable_indicator positive_integral_0_iff)
828   from T.Radon_Nikodym_finite_measure_infinite[simplified, OF assms(1) this]
829   obtain f where f_borel: "f \<in> borel_measurable M" and
830     fT: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = T.positive_integral (\<lambda>x. f x * indicator A x)" by auto
831   show ?thesis
832   proof (safe intro!: bexI[of _ "\<lambda>x. h x * f x"])
833     show "(\<lambda>x. h x * f x) \<in> borel_measurable M"
834       using borel f_borel by (auto intro: borel_measurable_pinfreal_times)
835     fix A assume "A \<in> sets M"
836     then have "(\<lambda>x. f x * indicator A x) \<in> borel_measurable M"
837       using f_borel by (auto intro: borel_measurable_pinfreal_times borel_measurable_indicator)
838     from positive_integral_translated_density[OF borel this]
839     show "\<nu> A = positive_integral (\<lambda>x. h x * f x * indicator A x)"
840       unfolding fT[OF `A \<in> sets M`] by (simp add: field_simps)
841   qed
842 qed
844 section "Uniqueness of densities"
846 lemma (in measure_space) density_is_absolutely_continuous:
847   assumes "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
848   shows "absolutely_continuous \<nu>"
849   using assms unfolding absolutely_continuous_def
850   by (simp add: positive_integral_null_set)
852 lemma (in measure_space) finite_density_unique:
853   assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
854   and fin: "positive_integral f < \<omega>"
855   shows "(\<forall>A\<in>sets M. positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. g x * indicator A x))
856     \<longleftrightarrow> (AE x. f x = g x)"
857     (is "(\<forall>A\<in>sets M. ?P f A = ?P g A) \<longleftrightarrow> _")
858 proof (intro iffI ballI)
859   fix A assume eq: "AE x. f x = g x"
860   show "?P f A = ?P g A"
861     by (rule positive_integral_cong_AE[OF AE_mp[OF eq]]) simp
862 next
863   assume eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
864   from this[THEN bspec, OF top] fin
865   have g_fin: "positive_integral g < \<omega>" by (simp cong: positive_integral_cong)
866   { fix f g assume borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
867       and g_fin: "positive_integral g < \<omega>" and eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
868     let ?N = "{x\<in>space M. g x < f x}"
869     have N: "?N \<in> sets M" using borel by simp
870     have "?P (\<lambda>x. (f x - g x)) ?N = positive_integral (\<lambda>x. f x * indicator ?N x - g x * indicator ?N x)"
871       by (auto intro!: positive_integral_cong simp: indicator_def)
872     also have "\<dots> = ?P f ?N - ?P g ?N"
873     proof (rule positive_integral_diff)
874       show "(\<lambda>x. f x * indicator ?N x) \<in> borel_measurable M" "(\<lambda>x. g x * indicator ?N x) \<in> borel_measurable M"
875         using borel N by auto
876       have "?P g ?N \<le> positive_integral g"
877         by (auto intro!: positive_integral_mono simp: indicator_def)
878       then show "?P g ?N \<noteq> \<omega>" using g_fin by auto
879       fix x assume "x \<in> space M"
880       show "g x * indicator ?N x \<le> f x * indicator ?N x"
881         by (auto simp: indicator_def)
882     qed
883     also have "\<dots> = 0"
884       using eq[THEN bspec, OF N] by simp
885     finally have "\<mu> {x\<in>space M. (f x - g x) * indicator ?N x \<noteq> 0} = 0"
886       using borel N by (subst (asm) positive_integral_0_iff) auto
887     moreover have "{x\<in>space M. (f x - g x) * indicator ?N x \<noteq> 0} = ?N"
888       by (auto simp: pinfreal_zero_le_diff)
889     ultimately have "?N \<in> null_sets" using N by simp }
890   from this[OF borel g_fin eq] this[OF borel(2,1) fin]
891   have "{x\<in>space M. g x < f x} \<union> {x\<in>space M. f x < g x} \<in> null_sets"
892     using eq by (intro null_sets_Un) auto
893   also have "{x\<in>space M. g x < f x} \<union> {x\<in>space M. f x < g x} = {x\<in>space M. f x \<noteq> g x}"
894     by auto
895   finally show "AE x. f x = g x"
896     unfolding almost_everywhere_def by auto
897 qed
899 lemma (in finite_measure) density_unique_finite_measure:
900   assumes borel: "f \<in> borel_measurable M" "f' \<in> borel_measurable M"
901   assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. f' x * indicator A x)"
902     (is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A")
903   shows "AE x. f x = f' x"
904 proof -
905   let "?\<nu> A" = "?P f A" and "?\<nu>' A" = "?P f' A"
906   let "?f A x" = "f x * indicator A x" and "?f' A x" = "f' x * indicator A x"
907   interpret M: measure_space M ?\<nu>
908     using borel(1) by (rule measure_space_density)
909   have ac: "absolutely_continuous ?\<nu>"
910     using f by (rule density_is_absolutely_continuous)
911   from split_space_into_finite_sets_and_rest[OF `measure_space M ?\<nu>` ac]
912   obtain Q0 and Q :: "nat \<Rightarrow> 'a set"
913     where Q: "disjoint_family Q" "range Q \<subseteq> sets M"
914     and Q0: "Q0 \<in> sets M" "Q0 = space M - (\<Union>i. Q i)"
915     and in_Q0: "\<And>A. A \<in> sets M \<Longrightarrow> A \<subseteq> Q0 \<Longrightarrow> \<mu> A = 0 \<and> ?\<nu> A = 0 \<or> 0 < \<mu> A \<and> ?\<nu> A = \<omega>"
916     and Q_fin: "\<And>i. ?\<nu> (Q i) \<noteq> \<omega>" by force
917   from Q have Q_sets: "\<And>i. Q i \<in> sets M" by auto
918   let ?N = "{x\<in>space M. f x \<noteq> f' x}"
919   have "?N \<in> sets M" using borel by auto
920   have *: "\<And>i x A. \<And>y::pinfreal. y * indicator (Q i) x * indicator A x = y * indicator (Q i \<inter> A) x"
921     unfolding indicator_def by auto
922   have 1: "\<forall>i. AE x. ?f (Q i) x = ?f' (Q i) x"
923     using borel Q_fin Q
924     by (intro finite_density_unique[THEN iffD1] allI)
925        (auto intro!: borel_measurable_pinfreal_times f Int simp: *)
926   have 2: "AE x. ?f Q0 x = ?f' Q0 x"
927   proof (rule AE_I')
928     { fix f :: "'a \<Rightarrow> pinfreal" assume borel: "f \<in> borel_measurable M"
929         and eq: "\<And>A. A \<in> sets M \<Longrightarrow> ?\<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
930       let "?A i" = "Q0 \<inter> {x \<in> space M. f x < of_nat i}"
931       have "(\<Union>i. ?A i) \<in> null_sets"
932       proof (rule null_sets_UN)
933         fix i have "?A i \<in> sets M"
934           using borel Q0(1) by auto
935         have "?\<nu> (?A i) \<le> positive_integral (\<lambda>x. of_nat i * indicator (?A i) x)"
936           unfolding eq[OF `?A i \<in> sets M`]
937           by (auto intro!: positive_integral_mono simp: indicator_def)
938         also have "\<dots> = of_nat i * \<mu> (?A i)"
939           using `?A i \<in> sets M` by (auto intro!: positive_integral_cmult_indicator)
940         also have "\<dots> < \<omega>"
941           using `?A i \<in> sets M`[THEN finite_measure] by auto
942         finally have "?\<nu> (?A i) \<noteq> \<omega>" by simp
943         then show "?A i \<in> null_sets" using in_Q0[OF `?A i \<in> sets M`] `?A i \<in> sets M` by auto
944       qed
945       also have "(\<Union>i. ?A i) = Q0 \<inter> {x\<in>space M. f x < \<omega>}"
946         by (auto simp: less_\<omega>_Ex_of_nat)
947       finally have "Q0 \<inter> {x\<in>space M. f x \<noteq> \<omega>} \<in> null_sets" by (simp add: pinfreal_less_\<omega>) }
948     from this[OF borel(1) refl] this[OF borel(2) f]
949     have "Q0 \<inter> {x\<in>space M. f x \<noteq> \<omega>} \<in> null_sets" "Q0 \<inter> {x\<in>space M. f' x \<noteq> \<omega>} \<in> null_sets" by simp_all
950     then show "(Q0 \<inter> {x\<in>space M. f x \<noteq> \<omega>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<omega>}) \<in> null_sets" by (rule null_sets_Un)
951     show "{x \<in> space M. ?f Q0 x \<noteq> ?f' Q0 x} \<subseteq>
952       (Q0 \<inter> {x\<in>space M. f x \<noteq> \<omega>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<omega>})" by (auto simp: indicator_def)
953   qed
954   have **: "\<And>x. (?f Q0 x = ?f' Q0 x) \<longrightarrow> (\<forall>i. ?f (Q i) x = ?f' (Q i) x) \<longrightarrow>
955     ?f (space M) x = ?f' (space M) x"
956     by (auto simp: indicator_def Q0)
957   have 3: "AE x. ?f (space M) x = ?f' (space M) x"
958     by (rule AE_mp[OF 1[unfolded all_AE_countable] AE_mp[OF 2]]) (simp add: **)
959   then show "AE x. f x = f' x"
960     by (rule AE_mp) (auto intro!: AE_cong simp: indicator_def)
961 qed
963 lemma (in sigma_finite_measure) density_unique:
964   assumes borel: "f \<in> borel_measurable M" "f' \<in> borel_measurable M"
965   assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. f' x * indicator A x)"
966     (is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A")
967   shows "AE x. f x = f' x"
968 proof -
969   obtain h where h_borel: "h \<in> borel_measurable M"
970     and fin: "positive_integral h \<noteq> \<omega>" and pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<omega>"
971     using Ex_finite_integrable_function by auto
972   interpret h: measure_space M "\<lambda>A. positive_integral (\<lambda>x. h x * indicator A x)"
973     using h_borel by (rule measure_space_density)
974   interpret h: finite_measure M "\<lambda>A. positive_integral (\<lambda>x. h x * indicator A x)"
975     by default (simp cong: positive_integral_cong add: fin)
977   interpret f: measure_space M "\<lambda>A. positive_integral (\<lambda>x. f x * indicator A x)"
978     using borel(1) by (rule measure_space_density)
979   interpret f': measure_space M "\<lambda>A. positive_integral (\<lambda>x. f' x * indicator A x)"
980     using borel(2) by (rule measure_space_density)
982   { fix A assume "A \<in> sets M"
983     then have " {x \<in> space M. h x \<noteq> 0 \<and> indicator A x \<noteq> (0::pinfreal)} = A"
984       using pos sets_into_space by (force simp: indicator_def)
985     then have "positive_integral (\<lambda>xa. h xa * indicator A xa) = 0 \<longleftrightarrow> A \<in> null_sets"
986       using h_borel `A \<in> sets M` by (simp add: positive_integral_0_iff) }
987   note h_null_sets = this
989   { fix A assume "A \<in> sets M"
990     have "positive_integral (\<lambda>x. h x * (f x * indicator A x)) =
991       f.positive_integral (\<lambda>x. h x * indicator A x)"
992       using `A \<in> sets M` h_borel borel
993       by (simp add: positive_integral_translated_density ac_simps cong: positive_integral_cong)
994     also have "\<dots> = f'.positive_integral (\<lambda>x. h x * indicator A x)"
995       by (rule f'.positive_integral_cong_measure) (rule f)
996     also have "\<dots> = positive_integral (\<lambda>x. h x * (f' x * indicator A x))"
997       using `A \<in> sets M` h_borel borel
998       by (simp add: positive_integral_translated_density ac_simps cong: positive_integral_cong)
999     finally have "positive_integral (\<lambda>x. h x * (f x * indicator A x)) = positive_integral (\<lambda>x. h x * (f' x * indicator A x))" . }
1000   then have "h.almost_everywhere (\<lambda>x. f x = f' x)"
1001     using h_borel borel
1002     by (intro h.density_unique_finite_measure[OF borel])
1003        (simp add: positive_integral_translated_density)
1004   then show "AE x. f x = f' x"
1005     unfolding h.almost_everywhere_def almost_everywhere_def
1006     by (auto simp add: h_null_sets)
1007 qed
1009 lemma (in sigma_finite_measure) sigma_finite_iff_density_finite:
1010   assumes \<nu>: "measure_space M \<nu>" and f: "f \<in> borel_measurable M"
1011     and eq: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
1012   shows "sigma_finite_measure M \<nu> \<longleftrightarrow> (AE x. f x \<noteq> \<omega>)"
1013 proof
1014   assume "sigma_finite_measure M \<nu>"
1015   then interpret \<nu>: sigma_finite_measure M \<nu> .
1016   from \<nu>.Ex_finite_integrable_function obtain h where
1017     h: "h \<in> borel_measurable M" "\<nu>.positive_integral h \<noteq> \<omega>"
1018     and fin: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<omega>" by auto
1019   have "AE x. f x * h x \<noteq> \<omega>"
1020   proof (rule AE_I')
1021     have "\<nu>.positive_integral h = positive_integral (\<lambda>x. f x * h x)"
1022       by (simp add: \<nu>.positive_integral_cong_measure[symmetric, OF eq[symmetric]])
1023          (intro positive_integral_translated_density f h)
1024     then have "positive_integral (\<lambda>x. f x * h x) \<noteq> \<omega>"
1025       using h(2) by simp
1026     then show "(\<lambda>x. f x * h x) -` {\<omega>} \<inter> space M \<in> null_sets"
1027       using f h(1) by (auto intro!: positive_integral_omega borel_measurable_vimage)
1028   qed auto
1029   then show "AE x. f x \<noteq> \<omega>"
1030   proof (rule AE_mp, intro AE_cong)
1031     fix x assume "x \<in> space M" from this[THEN fin]
1032     show "f x * h x \<noteq> \<omega> \<longrightarrow> f x \<noteq> \<omega>" by auto
1033   qed
1034 next
1035   assume AE: "AE x. f x \<noteq> \<omega>"
1036   from sigma_finite guess Q .. note Q = this
1037   interpret \<nu>: measure_space M \<nu> by fact
1038   def A \<equiv> "\<lambda>i. f -` (case i of 0 \<Rightarrow> {\<omega>} | Suc n \<Rightarrow> {.. of_nat (Suc n)}) \<inter> space M"
1039   { fix i j have "A i \<inter> Q j \<in> sets M"
1040     unfolding A_def using f Q
1041     apply (rule_tac Int)
1042     by (cases i) (auto intro: measurable_sets[OF f]) }
1043   note A_in_sets = this
1044   let "?A n" = "case prod_decode n of (i,j) \<Rightarrow> A i \<inter> Q j"
1045   show "sigma_finite_measure M \<nu>"
1046   proof (default, intro exI conjI subsetI allI)
1047     fix x assume "x \<in> range ?A"
1048     then obtain n where n: "x = ?A n" by auto
1049     then show "x \<in> sets M" using A_in_sets by (cases "prod_decode n") auto
1050   next
1051     have "(\<Union>i. ?A i) = (\<Union>i j. A i \<inter> Q j)"
1052     proof safe
1053       fix x i j assume "x \<in> A i" "x \<in> Q j"
1054       then show "x \<in> (\<Union>i. case prod_decode i of (i, j) \<Rightarrow> A i \<inter> Q j)"
1055         by (intro UN_I[of "prod_encode (i,j)"]) auto
1056     qed auto
1057     also have "\<dots> = (\<Union>i. A i) \<inter> space M" using Q by auto
1058     also have "(\<Union>i. A i) = space M"
1059     proof safe
1060       fix x assume x: "x \<in> space M"
1061       show "x \<in> (\<Union>i. A i)"
1062       proof (cases "f x")
1063         case infinite then show ?thesis using x unfolding A_def by (auto intro: exI[of _ 0])
1064       next
1065         case (preal r)
1066         with less_\<omega>_Ex_of_nat[of "f x"] obtain n where "f x < of_nat n" by auto
1067         then show ?thesis using x preal unfolding A_def by (auto intro!: exI[of _ "Suc n"])
1068       qed
1069     qed (auto simp: A_def)
1070     finally show "(\<Union>i. ?A i) = space M" by simp
1071   next
1072     fix n obtain i j where
1073       [simp]: "prod_decode n = (i, j)" by (cases "prod_decode n") auto
1074     have "positive_integral (\<lambda>x. f x * indicator (A i \<inter> Q j) x) \<noteq> \<omega>"
1075     proof (cases i)
1076       case 0
1077       have "AE x. f x * indicator (A i \<inter> Q j) x = 0"
1078         using AE by (rule AE_mp) (auto intro!: AE_cong simp: A_def `i = 0`)
1079       then have "positive_integral (\<lambda>x. f x * indicator (A i \<inter> Q j) x) = 0"
1080         using A_in_sets f
1081         apply (subst positive_integral_0_iff)
1082         apply fast
1083         apply (subst (asm) AE_iff_null_set)
1084         apply (intro borel_measurable_pinfreal_neq_const)
1085         apply fast
1086         by simp
1087       then show ?thesis by simp
1088     next
1089       case (Suc n)
1090       then have "positive_integral (\<lambda>x. f x * indicator (A i \<inter> Q j) x) \<le>
1091         positive_integral (\<lambda>x. of_nat (Suc n) * indicator (Q j) x)"
1092         by (auto intro!: positive_integral_mono simp: indicator_def A_def)
1093       also have "\<dots> = of_nat (Suc n) * \<mu> (Q j)"
1094         using Q by (auto intro!: positive_integral_cmult_indicator)
1095       also have "\<dots> < \<omega>"
1096         using Q by auto
1097       finally show ?thesis by simp
1098     qed
1099     then show "\<nu> (?A n) \<noteq> \<omega>"
1100       using A_in_sets Q eq by auto
1101   qed
1102 qed
1104 section "Radon Nikodym derivative"
1106 definition (in sigma_finite_measure)
1107   "RN_deriv \<nu> \<equiv> SOME f. f \<in> borel_measurable M \<and>
1108     (\<forall>A \<in> sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x))"
1110 lemma (in sigma_finite_measure) RN_deriv_cong:
1111   assumes cong: "\<And>A. A \<in> sets M \<Longrightarrow> \<mu>' A = \<mu> A" "\<And>A. A \<in> sets M \<Longrightarrow> \<nu>' A = \<nu> A"
1112   shows "sigma_finite_measure.RN_deriv M \<mu>' \<nu>' x = RN_deriv \<nu> x"
1113 proof -
1114   interpret \<mu>': sigma_finite_measure M \<mu>'
1115     using cong(1) by (rule sigma_finite_measure_cong)
1116   show ?thesis
1117     unfolding RN_deriv_def \<mu>'.RN_deriv_def
1118     by (simp add: cong positive_integral_cong_measure[OF cong(1)])
1119 qed
1121 lemma (in sigma_finite_measure) RN_deriv:
1122   assumes "measure_space M \<nu>"
1123   assumes "absolutely_continuous \<nu>"
1124   shows "RN_deriv \<nu> \<in> borel_measurable M" (is ?borel)
1125   and "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)"
1126     (is "\<And>A. _ \<Longrightarrow> ?int A")
1127 proof -
1128   note Ex = Radon_Nikodym[OF assms, unfolded Bex_def]
1129   thus ?borel unfolding RN_deriv_def by (rule someI2_ex) auto
1130   fix A assume "A \<in> sets M"
1131   from Ex show "?int A" unfolding RN_deriv_def
1132     by (rule someI2_ex) (simp add: `A \<in> sets M`)
1133 qed
1135 lemma (in sigma_finite_measure) RN_deriv_positive_integral:
1136   assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
1137     and f: "f \<in> borel_measurable M"
1138   shows "measure_space.positive_integral M \<nu> f = positive_integral (\<lambda>x. RN_deriv \<nu> x * f x)"
1139 proof -
1140   interpret \<nu>: measure_space M \<nu> by fact
1141   have "\<nu>.positive_integral f =
1142     measure_space.positive_integral M (\<lambda>A. positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)) f"
1143     by (intro \<nu>.positive_integral_cong_measure[symmetric] RN_deriv(2)[OF \<nu>, symmetric])
1144   also have "\<dots> = positive_integral (\<lambda>x. RN_deriv \<nu> x * f x)"
1145     by (intro positive_integral_translated_density RN_deriv[OF \<nu>] f)
1146   finally show ?thesis .
1147 qed
1149 lemma (in sigma_finite_measure) RN_deriv_unique:
1150   assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
1151   and f: "f \<in> borel_measurable M"
1152   and eq: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
1153   shows "AE x. f x = RN_deriv \<nu> x"
1154 proof (rule density_unique[OF f RN_deriv(1)[OF \<nu>]])
1155   fix A assume A: "A \<in> sets M"
1156   show "positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)"
1157     unfolding eq[OF A, symmetric] RN_deriv(2)[OF \<nu> A, symmetric] ..
1158 qed
1160 lemma the_inv_into_in:
1161   assumes "inj_on f A" and x: "x \<in> f`A"
1162   shows "the_inv_into A f x \<in> A"
1163   using assms by (auto simp: the_inv_into_f_f)
1165 lemma (in sigma_finite_measure) RN_deriv_vimage:
1166   fixes f :: "'b \<Rightarrow> 'a"
1167   assumes f: "bij_betw f S (space M)"
1168   assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
1169   shows "AE x.
1170     sigma_finite_measure.RN_deriv (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>A. \<nu> (f ` A)) (the_inv_into S f x) = RN_deriv \<nu> x"
1171 proof (rule RN_deriv_unique[OF \<nu>])
1172   interpret sf: sigma_finite_measure "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
1173     using f by (rule sigma_finite_measure_isomorphic)
1174   interpret \<nu>: measure_space M \<nu> using \<nu>(1) .
1175   have \<nu>': "measure_space (vimage_algebra S f) (\<lambda>A. \<nu> (f ` A))"
1176     using f by (rule \<nu>.measure_space_isomorphic)
1177   { fix A assume "A \<in> sets M" then have "f ` (f -` A \<inter> S) = A"
1178       using sets_into_space f[unfolded bij_betw_def]
1179       by (intro image_vimage_inter_eq[where T="space M"]) auto }
1180   note A_f = this
1181   then have ac: "sf.absolutely_continuous (\<lambda>A. \<nu> (f ` A))"
1182     using \<nu>(2) by (auto simp: sf.absolutely_continuous_def absolutely_continuous_def)
1183   show "(\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (the_inv_into S f x)) \<in> borel_measurable M"
1184     using sf.RN_deriv(1)[OF \<nu>' ac]
1185     unfolding measurable_vimage_iff_inv[OF f] comp_def .
1186   fix A assume "A \<in> sets M"
1187   then have *: "\<And>x. x \<in> space M \<Longrightarrow> indicator (f -` A \<inter> S) (the_inv_into S f x) = (indicator A x :: pinfreal)"
1188     using f[unfolded bij_betw_def]
1189     unfolding indicator_def by (auto simp: f_the_inv_into_f the_inv_into_in)
1190   have "\<nu> (f ` (f -` A \<inter> S)) = sf.positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) x * indicator (f -` A \<inter> S) x)"
1191     using `A \<in> sets M` by (force intro!: sf.RN_deriv(2)[OF \<nu>' ac])
1192   also have "\<dots> = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (the_inv_into S f x) * indicator A x)"
1193     unfolding positive_integral_vimage_inv[OF f]
1194     by (simp add: * cong: positive_integral_cong)
1195   finally show "\<nu> A = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (the_inv_into S f x) * indicator A x)"
1196     unfolding A_f[OF `A \<in> sets M`] .
1197 qed
1199 lemma (in sigma_finite_measure) RN_deriv_finite:
1200   assumes sfm: "sigma_finite_measure M \<nu>" and ac: "absolutely_continuous \<nu>"
1201   shows "AE x. RN_deriv \<nu> x \<noteq> \<omega>"
1202 proof -
1203   interpret \<nu>: sigma_finite_measure M \<nu> by fact
1204   have \<nu>: "measure_space M \<nu>" by default
1205   from sfm show ?thesis
1206     using sigma_finite_iff_density_finite[OF \<nu> RN_deriv[OF \<nu> ac]] by simp
1207 qed
1209 lemma (in sigma_finite_measure)
1210   assumes \<nu>: "sigma_finite_measure M \<nu>" "absolutely_continuous \<nu>"
1211     and f: "f \<in> borel_measurable M"
1212   shows RN_deriv_integral: "measure_space.integral M \<nu> f = integral (\<lambda>x. real (RN_deriv \<nu> x) * f x)" (is ?integral)
1213     and RN_deriv_integrable: "measure_space.integrable M \<nu> f \<longleftrightarrow> integrable (\<lambda>x. real (RN_deriv \<nu> x) * f x)" (is ?integrable)
1214 proof -
1215   interpret \<nu>: sigma_finite_measure M \<nu> by fact
1216   have ms: "measure_space M \<nu>" by default
1217   have minus_cong: "\<And>A B A' B'::pinfreal. A = A' \<Longrightarrow> B = B' \<Longrightarrow> real A - real B = real A' - real B'" by simp
1218   have f': "(\<lambda>x. - f x) \<in> borel_measurable M" using f by auto
1219   { fix f :: "'a \<Rightarrow> real" assume "f \<in> borel_measurable M"
1220     { fix x assume *: "RN_deriv \<nu> x \<noteq> \<omega>"
1221       have "Real (real (RN_deriv \<nu> x)) * Real (f x) = Real (real (RN_deriv \<nu> x) * f x)"
1222         by (simp add: mult_le_0_iff)
1223       then have "RN_deriv \<nu> x * Real (f x) = Real (real (RN_deriv \<nu> x) * f x)"
1224         using * by (simp add: Real_real) }
1225     note * = this
1226     have "positive_integral (\<lambda>x. RN_deriv \<nu> x * Real (f x)) = positive_integral (\<lambda>x. Real (real (RN_deriv \<nu> x) * f x))"
1227       apply (rule positive_integral_cong_AE)
1228       apply (rule AE_mp[OF RN_deriv_finite[OF \<nu>]])
1229       by (auto intro!: AE_cong simp: *) }
1230   with this[OF f] this[OF f'] f f'
1231   show ?integral ?integrable
1232     unfolding \<nu>.integral_def integral_def \<nu>.integrable_def integrable_def
1233     by (auto intro!: RN_deriv(1)[OF ms \<nu>(2)] minus_cong simp: RN_deriv_positive_integral[OF ms \<nu>(2)])
1234 qed
1236 lemma (in sigma_finite_measure) RN_deriv_singleton:
1237   assumes "measure_space M \<nu>"
1238   and ac: "absolutely_continuous \<nu>"
1239   and "{x} \<in> sets M"
1240   shows "\<nu> {x} = RN_deriv \<nu> x * \<mu> {x}"
1241 proof -
1242   note deriv = RN_deriv[OF assms(1, 2)]
1243   from deriv(2)[OF `{x} \<in> sets M`]
1244   have "\<nu> {x} = positive_integral (\<lambda>w. RN_deriv \<nu> x * indicator {x} w)"
1245     by (auto simp: indicator_def intro!: positive_integral_cong)
1246   thus ?thesis using positive_integral_cmult_indicator[OF `{x} \<in> sets M`]
1247     by auto
1248 qed
1250 theorem (in finite_measure_space) RN_deriv_finite_measure:
1251   assumes "measure_space M \<nu>"
1252   and ac: "absolutely_continuous \<nu>"
1253   and "x \<in> space M"
1254   shows "\<nu> {x} = RN_deriv \<nu> x * \<mu> {x}"
1255 proof -
1256   have "{x} \<in> sets M" using sets_eq_Pow `x \<in> space M` by auto
1257   from RN_deriv_singleton[OF assms(1,2) this] show ?thesis .
1258 qed
1260 end