hoelzl@42067 ` 1` ```(* Title: HOL/Probability/Radon_Nikodym.thy ``` hoelzl@42067 ` 2` ``` Author: Johannes Hölzl, TU München ``` hoelzl@42067 ` 3` ```*) ``` hoelzl@42067 ` 4` hoelzl@42067 ` 5` ```header {*Radon-Nikod{\'y}m derivative*} ``` hoelzl@42067 ` 6` hoelzl@38656 ` 7` ```theory Radon_Nikodym ``` hoelzl@38656 ` 8` ```imports Lebesgue_Integration ``` hoelzl@38656 ` 9` ```begin ``` hoelzl@38656 ` 10` hoelzl@47694 ` 11` ```definition "diff_measure M N = ``` hoelzl@47694 ` 12` ``` measure_of (space M) (sets M) (\A. emeasure M A - emeasure N A)" ``` hoelzl@47694 ` 13` hoelzl@47694 ` 14` ```lemma ``` hoelzl@47694 ` 15` ``` shows space_diff_measure[simp]: "space (diff_measure M N) = space M" ``` hoelzl@47694 ` 16` ``` and sets_diff_measure[simp]: "sets (diff_measure M N) = sets M" ``` hoelzl@47694 ` 17` ``` by (auto simp: diff_measure_def) ``` hoelzl@47694 ` 18` hoelzl@47694 ` 19` ```lemma emeasure_diff_measure: ``` hoelzl@47694 ` 20` ``` assumes fin: "finite_measure M" "finite_measure N" and sets_eq: "sets M = sets N" ``` hoelzl@47694 ` 21` ``` assumes pos: "\A. A \ sets M \ emeasure N A \ emeasure M A" and A: "A \ sets M" ``` hoelzl@47694 ` 22` ``` shows "emeasure (diff_measure M N) A = emeasure M A - emeasure N A" (is "_ = ?\ A") ``` hoelzl@47694 ` 23` ``` unfolding diff_measure_def ``` hoelzl@47694 ` 24` ```proof (rule emeasure_measure_of_sigma) ``` hoelzl@47694 ` 25` ``` show "sigma_algebra (space M) (sets M)" .. ``` hoelzl@47694 ` 26` ``` show "positive (sets M) ?\" ``` hoelzl@47694 ` 27` ``` using pos by (simp add: positive_def ereal_diff_positive) ``` hoelzl@47694 ` 28` ``` show "countably_additive (sets M) ?\" ``` hoelzl@47694 ` 29` ``` proof (rule countably_additiveI) ``` hoelzl@47694 ` 30` ``` fix A :: "nat \ _" assume A: "range A \ sets M" and "disjoint_family A" ``` hoelzl@47694 ` 31` ``` then have suminf: ``` hoelzl@47694 ` 32` ``` "(\i. emeasure M (A i)) = emeasure M (\i. A i)" ``` hoelzl@47694 ` 33` ``` "(\i. emeasure N (A i)) = emeasure N (\i. A i)" ``` hoelzl@47694 ` 34` ``` by (simp_all add: suminf_emeasure sets_eq) ``` hoelzl@47694 ` 35` ``` with A have "(\i. emeasure M (A i) - emeasure N (A i)) = ``` hoelzl@47694 ` 36` ``` (\i. emeasure M (A i)) - (\i. emeasure N (A i))" ``` hoelzl@47694 ` 37` ``` using fin ``` hoelzl@47694 ` 38` ``` by (intro suminf_ereal_minus pos emeasure_nonneg) ``` hoelzl@47694 ` 39` ``` (auto simp: sets_eq finite_measure.emeasure_eq_measure suminf_emeasure) ``` hoelzl@47694 ` 40` ``` then show "(\i. emeasure M (A i) - emeasure N (A i)) = ``` hoelzl@47694 ` 41` ``` emeasure M (\i. A i) - emeasure N (\i. A i) " ``` hoelzl@47694 ` 42` ``` by (simp add: suminf) ``` hoelzl@47694 ` 43` ``` qed ``` hoelzl@47694 ` 44` ```qed fact ``` hoelzl@47694 ` 45` hoelzl@38656 ` 46` ```lemma (in sigma_finite_measure) Ex_finite_integrable_function: ``` wenzelm@53015 ` 47` ``` shows "\h\borel_measurable M. integral\<^sup>P M h \ \ \ (\x\space M. 0 < h x \ h x < \) \ (\x. 0 \ h x)" ``` hoelzl@38656 ` 48` ```proof - ``` hoelzl@38656 ` 49` ``` obtain A :: "nat \ 'a set" where ``` hoelzl@50003 ` 50` ``` range[measurable]: "range A \ sets M" and ``` hoelzl@38656 ` 51` ``` space: "(\i. A i) = space M" and ``` hoelzl@47694 ` 52` ``` measure: "\i. emeasure M (A i) \ \" and ``` hoelzl@38656 ` 53` ``` disjoint: "disjoint_family A" ``` hoelzl@47694 ` 54` ``` using sigma_finite_disjoint by auto ``` hoelzl@47694 ` 55` ``` let ?B = "\i. 2^Suc i * emeasure M (A i)" ``` hoelzl@38656 ` 56` ``` have "\i. \x. 0 < x \ x < inverse (?B i)" ``` hoelzl@38656 ` 57` ``` proof ``` hoelzl@47694 ` 58` ``` fix i show "\x. 0 < x \ x < inverse (?B i)" ``` hoelzl@47694 ` 59` ``` using measure[of i] emeasure_nonneg[of M "A i"] ``` hoelzl@51329 ` 60` ``` by (auto intro!: dense simp: ereal_0_gt_inverse ereal_zero_le_0_iff) ``` hoelzl@38656 ` 61` ``` qed ``` hoelzl@38656 ` 62` ``` from choice[OF this] obtain n where n: "\i. 0 < n i" ``` hoelzl@47694 ` 63` ``` "\i. n i < inverse (2^Suc i * emeasure M (A i))" by auto ``` hoelzl@41981 ` 64` ``` { fix i have "0 \ n i" using n(1)[of i] by auto } note pos = this ``` wenzelm@46731 ` 65` ``` let ?h = "\x. \i. n i * indicator (A i) x" ``` hoelzl@38656 ` 66` ``` show ?thesis ``` hoelzl@38656 ` 67` ``` proof (safe intro!: bexI[of _ ?h] del: notI) ``` hoelzl@39092 ` 68` ``` have "\i. A i \ sets M" ``` nipkow@44890 ` 69` ``` using range by fastforce+ ``` wenzelm@53015 ` 70` ``` then have "integral\<^sup>P M ?h = (\i. n i * emeasure M (A i))" using pos ``` hoelzl@41981 ` 71` ``` by (simp add: positive_integral_suminf positive_integral_cmult_indicator) ``` hoelzl@41981 ` 72` ``` also have "\ \ (\i. (1 / 2)^Suc i)" ``` hoelzl@41981 ` 73` ``` proof (rule suminf_le_pos) ``` hoelzl@41981 ` 74` ``` fix N ``` hoelzl@47694 ` 75` ``` have "n N * emeasure M (A N) \ inverse (2^Suc N * emeasure M (A N)) * emeasure M (A N)" ``` hoelzl@47694 ` 76` ``` using n[of N] ``` hoelzl@43920 ` 77` ``` by (intro ereal_mult_right_mono) auto ``` hoelzl@41981 ` 78` ``` also have "\ \ (1 / 2) ^ Suc N" ``` hoelzl@38656 ` 79` ``` using measure[of N] n[of N] ``` hoelzl@47694 ` 80` ``` by (cases rule: ereal2_cases[of "n N" "emeasure M (A N)"]) ``` hoelzl@43920 ` 81` ``` (simp_all add: inverse_eq_divide power_divide one_ereal_def ereal_power_divide) ``` hoelzl@47694 ` 82` ``` finally show "n N * emeasure M (A N) \ (1 / 2) ^ Suc N" . ``` hoelzl@47694 ` 83` ``` show "0 \ n N * emeasure M (A N)" using n[of N] `A N \ sets M` by (simp add: emeasure_nonneg) ``` hoelzl@38656 ` 84` ``` qed ``` wenzelm@53015 ` 85` ``` finally show "integral\<^sup>P M ?h \ \" unfolding suminf_half_series_ereal by auto ``` hoelzl@38656 ` 86` ``` next ``` hoelzl@41981 ` 87` ``` { fix x assume "x \ space M" ``` hoelzl@41981 ` 88` ``` then obtain i where "x \ A i" using space[symmetric] by auto ``` hoelzl@41981 ` 89` ``` with disjoint n have "?h x = n i" ``` hoelzl@41981 ` 90` ``` by (auto intro!: suminf_cmult_indicator intro: less_imp_le) ``` hoelzl@41981 ` 91` ``` then show "0 < ?h x" and "?h x < \" using n[of i] by auto } ``` hoelzl@41981 ` 92` ``` note pos = this ``` hoelzl@41981 ` 93` ``` fix x show "0 \ ?h x" ``` hoelzl@41981 ` 94` ``` proof cases ``` hoelzl@41981 ` 95` ``` assume "x \ space M" then show "0 \ ?h x" using pos by (auto intro: less_imp_le) ``` hoelzl@41981 ` 96` ``` next ``` hoelzl@41981 ` 97` ``` assume "x \ space M" then have "\i. x \ A i" using space by auto ``` hoelzl@41981 ` 98` ``` then show "0 \ ?h x" by auto ``` hoelzl@41981 ` 99` ``` qed ``` hoelzl@50003 ` 100` ``` qed measurable ``` hoelzl@38656 ` 101` ```qed ``` hoelzl@38656 ` 102` hoelzl@40871 ` 103` ```subsection "Absolutely continuous" ``` hoelzl@40871 ` 104` hoelzl@47694 ` 105` ```definition absolutely_continuous :: "'a measure \ 'a measure \ bool" where ``` hoelzl@47694 ` 106` ``` "absolutely_continuous M N \ null_sets M \ null_sets N" ``` hoelzl@47694 ` 107` hoelzl@47694 ` 108` ```lemma absolutely_continuousI_count_space: "absolutely_continuous (count_space A) M" ``` hoelzl@47694 ` 109` ``` unfolding absolutely_continuous_def by (auto simp: null_sets_count_space) ``` hoelzl@38656 ` 110` hoelzl@47694 ` 111` ```lemma absolutely_continuousI_density: ``` hoelzl@47694 ` 112` ``` "f \ borel_measurable M \ absolutely_continuous M (density M f)" ``` hoelzl@47694 ` 113` ``` by (force simp add: absolutely_continuous_def null_sets_density_iff dest: AE_not_in) ``` hoelzl@47694 ` 114` hoelzl@47694 ` 115` ```lemma absolutely_continuousI_point_measure_finite: ``` hoelzl@47694 ` 116` ``` "(\x. \ x \ A ; f x \ 0 \ \ g x \ 0) \ absolutely_continuous (point_measure A f) (point_measure A g)" ``` hoelzl@47694 ` 117` ``` unfolding absolutely_continuous_def by (force simp: null_sets_point_measure_iff) ``` hoelzl@47694 ` 118` hoelzl@47694 ` 119` ```lemma absolutely_continuous_AE: ``` hoelzl@47694 ` 120` ``` assumes sets_eq: "sets M' = sets M" ``` hoelzl@47694 ` 121` ``` and "absolutely_continuous M M'" "AE x in M. P x" ``` hoelzl@41981 ` 122` ``` shows "AE x in M'. P x" ``` hoelzl@40859 ` 123` ```proof - ``` hoelzl@47694 ` 124` ``` from `AE x in M. P x` obtain N where N: "N \ null_sets M" "{x\space M. \ P x} \ N" ``` hoelzl@47694 ` 125` ``` unfolding eventually_ae_filter by auto ``` hoelzl@41981 ` 126` ``` show "AE x in M'. P x" ``` hoelzl@47694 ` 127` ``` proof (rule AE_I') ``` hoelzl@47694 ` 128` ``` show "{x\space M'. \ P x} \ N" using sets_eq_imp_space_eq[OF sets_eq] N(2) by simp ``` hoelzl@47694 ` 129` ``` from `absolutely_continuous M M'` show "N \ null_sets M'" ``` hoelzl@47694 ` 130` ``` using N unfolding absolutely_continuous_def sets_eq null_sets_def by auto ``` hoelzl@40859 ` 131` ``` qed ``` hoelzl@40859 ` 132` ```qed ``` hoelzl@40859 ` 133` hoelzl@40871 ` 134` ```subsection "Existence of the Radon-Nikodym derivative" ``` hoelzl@40871 ` 135` hoelzl@38656 ` 136` ```lemma (in finite_measure) Radon_Nikodym_aux_epsilon: ``` hoelzl@38656 ` 137` ``` fixes e :: real assumes "0 < e" ``` hoelzl@47694 ` 138` ``` assumes "finite_measure N" and sets_eq: "sets N = sets M" ``` hoelzl@47694 ` 139` ``` shows "\A\sets M. measure M (space M) - measure N (space M) \ measure M A - measure N A \ ``` hoelzl@47694 ` 140` ``` (\B\sets M. B \ A \ - e < measure M B - measure N B)" ``` hoelzl@38656 ` 141` ```proof - ``` hoelzl@47694 ` 142` ``` interpret M': finite_measure N by fact ``` hoelzl@47694 ` 143` ``` let ?d = "\A. measure M A - measure N A" ``` wenzelm@46731 ` 144` ``` let ?A = "\A. if (\B\sets M. B \ space M - A \ -e < ?d B) ``` hoelzl@38656 ` 145` ``` then {} ``` hoelzl@38656 ` 146` ``` else (SOME B. B \ sets M \ B \ space M - A \ ?d B \ -e)" ``` hoelzl@38656 ` 147` ``` def A \ "\n. ((\B. B \ ?A B) ^^ n) {}" ``` hoelzl@38656 ` 148` ``` have A_simps[simp]: ``` hoelzl@38656 ` 149` ``` "A 0 = {}" ``` hoelzl@38656 ` 150` ``` "\n. A (Suc n) = (A n \ ?A (A n))" unfolding A_def by simp_all ``` hoelzl@38656 ` 151` ``` { fix A assume "A \ sets M" ``` hoelzl@38656 ` 152` ``` have "?A A \ sets M" ``` hoelzl@38656 ` 153` ``` by (auto intro!: someI2[of _ _ "\A. A \ sets M"] simp: not_less) } ``` hoelzl@38656 ` 154` ``` note A'_in_sets = this ``` hoelzl@38656 ` 155` ``` { fix n have "A n \ sets M" ``` hoelzl@38656 ` 156` ``` proof (induct n) ``` hoelzl@38656 ` 157` ``` case (Suc n) thus "A (Suc n) \ sets M" ``` hoelzl@38656 ` 158` ``` using A'_in_sets[of "A n"] by (auto split: split_if_asm) ``` hoelzl@38656 ` 159` ``` qed (simp add: A_def) } ``` hoelzl@38656 ` 160` ``` note A_in_sets = this ``` hoelzl@38656 ` 161` ``` hence "range A \ sets M" by auto ``` hoelzl@38656 ` 162` ``` { fix n B ``` hoelzl@38656 ` 163` ``` assume Ex: "\B. B \ sets M \ B \ space M - A n \ ?d B \ -e" ``` hoelzl@38656 ` 164` ``` hence False: "\ (\B\sets M. B \ space M - A n \ -e < ?d B)" by (auto simp: not_less) ``` hoelzl@38656 ` 165` ``` have "?d (A (Suc n)) \ ?d (A n) - e" unfolding A_simps if_not_P[OF False] ``` hoelzl@38656 ` 166` ``` proof (rule someI2_ex[OF Ex]) ``` hoelzl@38656 ` 167` ``` fix B assume "B \ sets M \ B \ space M - A n \ ?d B \ - e" ``` hoelzl@38656 ` 168` ``` hence "A n \ B = {}" "B \ sets M" and dB: "?d B \ -e" by auto ``` hoelzl@38656 ` 169` ``` hence "?d (A n \ B) = ?d (A n) + ?d B" ``` hoelzl@47694 ` 170` ``` using `A n \ sets M` finite_measure_Union M'.finite_measure_Union by (simp add: sets_eq) ``` hoelzl@38656 ` 171` ``` also have "\ \ ?d (A n) - e" using dB by simp ``` hoelzl@38656 ` 172` ``` finally show "?d (A n \ B) \ ?d (A n) - e" . ``` hoelzl@38656 ` 173` ``` qed } ``` hoelzl@38656 ` 174` ``` note dA_epsilon = this ``` hoelzl@38656 ` 175` ``` { fix n have "?d (A (Suc n)) \ ?d (A n)" ``` hoelzl@38656 ` 176` ``` proof (cases "\B. B\sets M \ B \ space M - A n \ ?d B \ - e") ``` hoelzl@38656 ` 177` ``` case True from dA_epsilon[OF this] show ?thesis using `0 < e` by simp ``` hoelzl@38656 ` 178` ``` next ``` hoelzl@38656 ` 179` ``` case False ``` hoelzl@38656 ` 180` ``` hence "\B\sets M. B \ space M - A n \ -e < ?d B" by (auto simp: not_le) ``` hoelzl@38656 ` 181` ``` thus ?thesis by simp ``` hoelzl@38656 ` 182` ``` qed } ``` hoelzl@38656 ` 183` ``` note dA_mono = this ``` hoelzl@38656 ` 184` ``` show ?thesis ``` hoelzl@38656 ` 185` ``` proof (cases "\n. \B\sets M. B \ space M - A n \ -e < ?d B") ``` hoelzl@38656 ` 186` ``` case True then obtain n where B: "\B. \ B \ sets M; B \ space M - A n\ \ -e < ?d B" by blast ``` hoelzl@38656 ` 187` ``` show ?thesis ``` hoelzl@38656 ` 188` ``` proof (safe intro!: bexI[of _ "space M - A n"]) ``` hoelzl@38656 ` 189` ``` fix B assume "B \ sets M" "B \ space M - A n" ``` hoelzl@38656 ` 190` ``` from B[OF this] show "-e < ?d B" . ``` hoelzl@38656 ` 191` ``` next ``` immler@50244 ` 192` ``` show "space M - A n \ sets M" by (rule sets.compl_sets) fact ``` hoelzl@38656 ` 193` ``` next ``` hoelzl@38656 ` 194` ``` show "?d (space M) \ ?d (space M - A n)" ``` hoelzl@38656 ` 195` ``` proof (induct n) ``` hoelzl@38656 ` 196` ``` fix n assume "?d (space M) \ ?d (space M - A n)" ``` hoelzl@38656 ` 197` ``` also have "\ \ ?d (space M - A (Suc n))" ``` immler@50244 ` 198` ``` using A_in_sets sets.sets_into_space dA_mono[of n] finite_measure_compl M'.finite_measure_compl ``` hoelzl@47694 ` 199` ``` by (simp del: A_simps add: sets_eq sets_eq_imp_space_eq[OF sets_eq]) ``` hoelzl@38656 ` 200` ``` finally show "?d (space M) \ ?d (space M - A (Suc n))" . ``` hoelzl@38656 ` 201` ``` qed simp ``` hoelzl@38656 ` 202` ``` qed ``` hoelzl@38656 ` 203` ``` next ``` hoelzl@38656 ` 204` ``` case False hence B: "\n. \B. B\sets M \ B \ space M - A n \ ?d B \ - e" ``` hoelzl@38656 ` 205` ``` by (auto simp add: not_less) ``` hoelzl@38656 ` 206` ``` { fix n have "?d (A n) \ - real n * e" ``` hoelzl@38656 ` 207` ``` proof (induct n) ``` hoelzl@38656 ` 208` ``` case (Suc n) with dA_epsilon[of n, OF B] show ?case by (simp del: A_simps add: real_of_nat_Suc field_simps) ``` hoelzl@41981 ` 209` ``` next ``` hoelzl@47694 ` 210` ``` case 0 with measure_empty show ?case by (simp add: zero_ereal_def) ``` hoelzl@41981 ` 211` ``` qed } note dA_less = this ``` hoelzl@38656 ` 212` ``` have decseq: "decseq (\n. ?d (A n))" unfolding decseq_eq_incseq ``` hoelzl@38656 ` 213` ``` proof (rule incseq_SucI) ``` hoelzl@38656 ` 214` ``` fix n show "- ?d (A n) \ - ?d (A (Suc n))" using dA_mono[of n] by auto ``` hoelzl@38656 ` 215` ``` qed ``` hoelzl@41981 ` 216` ``` have A: "incseq A" by (auto intro!: incseq_SucI) ``` hoelzl@47694 ` 217` ``` from finite_Lim_measure_incseq[OF _ A] `range A \ sets M` ``` hoelzl@47694 ` 218` ``` M'.finite_Lim_measure_incseq[OF _ A] ``` hoelzl@38656 ` 219` ``` have convergent: "(\i. ?d (A i)) ----> ?d (\i. A i)" ``` hoelzl@47694 ` 220` ``` by (auto intro!: tendsto_diff simp: sets_eq) ``` hoelzl@38656 ` 221` ``` obtain n :: nat where "- ?d (\i. A i) / e < real n" using reals_Archimedean2 by auto ``` hoelzl@38656 ` 222` ``` moreover from order_trans[OF decseq_le[OF decseq convergent] dA_less] ``` hoelzl@38656 ` 223` ``` have "real n \ - ?d (\i. A i) / e" using `0A\sets M. measure M (space M) - measure N (space M) \ ``` hoelzl@47694 ` 231` ``` measure M A - measure N A \ ``` hoelzl@47694 ` 232` ``` (\B\sets M. B \ A \ 0 \ measure M B - measure N B)" ``` hoelzl@41981 ` 233` ```proof - ``` hoelzl@47694 ` 234` ``` interpret N: finite_measure N by fact ``` hoelzl@47694 ` 235` ``` let ?d = "\A. measure M A - measure N A" ``` wenzelm@46731 ` 236` ``` let ?P = "\A B n. A \ sets M \ A \ B \ ?d B \ ?d A \ (\C\sets M. C \ A \ - 1 / real (Suc n) < ?d C)" ``` wenzelm@46731 ` 237` ``` let ?r = "\S. restricted_space S" ``` hoelzl@41981 ` 238` ``` { fix S n assume S: "S \ sets M" ``` hoelzl@47694 ` 239` ``` then have "finite_measure (density M (indicator S))" "0 < 1 / real (Suc n)" ``` hoelzl@47694 ` 240` ``` "finite_measure (density N (indicator S))" "sets (density N (indicator S)) = sets (density M (indicator S))" ``` hoelzl@47694 ` 241` ``` by (auto simp: finite_measure_restricted N.finite_measure_restricted sets_eq) ``` hoelzl@41981 ` 242` ``` from finite_measure.Radon_Nikodym_aux_epsilon[OF this] guess X .. note X = this ``` hoelzl@47694 ` 243` ``` with S have "?P (S \ X) S n" ``` immler@50244 ` 244` ``` by (simp add: measure_restricted sets_eq sets.Int) (metis inf_absorb2) ``` hoelzl@47694 ` 245` ``` hence "\A. ?P A S n" .. } ``` hoelzl@38656 ` 246` ``` note Ex_P = this ``` blanchet@55415 ` 247` ``` def A \ "rec_nat (space M) (\n A. SOME B. ?P B A n)" ``` hoelzl@38656 ` 248` ``` have A_Suc: "\n. A (Suc n) = (SOME B. ?P B (A n) n)" by (simp add: A_def) ``` hoelzl@38656 ` 249` ``` have A_0[simp]: "A 0 = space M" unfolding A_def by simp ``` hoelzl@38656 ` 250` ``` { fix i have "A i \ sets M" unfolding A_def ``` hoelzl@38656 ` 251` ``` proof (induct i) ``` hoelzl@38656 ` 252` ``` case (Suc i) ``` blanchet@55642 ` 253` ``` from Ex_P[OF this, of i] show ?case unfolding nat.rec(2) ``` hoelzl@38656 ` 254` ``` by (rule someI2_ex) simp ``` hoelzl@38656 ` 255` ``` qed simp } ``` hoelzl@38656 ` 256` ``` note A_in_sets = this ``` hoelzl@38656 ` 257` ``` { fix n have "?P (A (Suc n)) (A n) n" ``` hoelzl@38656 ` 258` ``` using Ex_P[OF A_in_sets] unfolding A_Suc ``` hoelzl@38656 ` 259` ``` by (rule someI2_ex) simp } ``` hoelzl@38656 ` 260` ``` note P_A = this ``` hoelzl@38656 ` 261` ``` have "range A \ sets M" using A_in_sets by auto ``` hoelzl@38656 ` 262` ``` have A_mono: "\i. A (Suc i) \ A i" using P_A by simp ``` hoelzl@38656 ` 263` ``` have mono_dA: "mono (\i. ?d (A i))" using P_A by (simp add: mono_iff_le_Suc) ``` hoelzl@38656 ` 264` ``` have epsilon: "\C i. \ C \ sets M; C \ A (Suc i) \ \ - 1 / real (Suc i) < ?d C" ``` hoelzl@38656 ` 265` ``` using P_A by auto ``` hoelzl@38656 ` 266` ``` show ?thesis ``` hoelzl@38656 ` 267` ``` proof (safe intro!: bexI[of _ "\i. A i"]) ``` hoelzl@38656 ` 268` ``` show "(\i. A i) \ sets M" using A_in_sets by auto ``` hoelzl@41981 ` 269` ``` have A: "decseq A" using A_mono by (auto intro!: decseq_SucI) ``` hoelzl@47694 ` 270` ``` from `range A \ sets M` ``` hoelzl@47694 ` 271` ``` finite_Lim_measure_decseq[OF _ A] N.finite_Lim_measure_decseq[OF _ A] ``` hoelzl@47694 ` 272` ``` have "(\i. ?d (A i)) ----> ?d (\i. A i)" by (auto intro!: tendsto_diff simp: sets_eq) ``` hoelzl@38656 ` 273` ``` thus "?d (space M) \ ?d (\i. A i)" using mono_dA[THEN monoD, of 0 _] ``` hoelzl@47694 ` 274` ``` by (rule_tac LIMSEQ_le_const) auto ``` hoelzl@38656 ` 275` ``` next ``` hoelzl@38656 ` 276` ``` fix B assume B: "B \ sets M" "B \ (\i. A i)" ``` hoelzl@38656 ` 277` ``` show "0 \ ?d B" ``` hoelzl@38656 ` 278` ``` proof (rule ccontr) ``` hoelzl@38656 ` 279` ``` assume "\ 0 \ ?d B" ``` hoelzl@38656 ` 280` ``` hence "0 < - ?d B" by auto ``` hoelzl@38656 ` 281` ``` from ex_inverse_of_nat_Suc_less[OF this] ``` hoelzl@38656 ` 282` ``` obtain n where *: "?d B < - 1 / real (Suc n)" ``` hoelzl@38656 ` 283` ``` by (auto simp: real_eq_of_nat inverse_eq_divide field_simps) ``` blanchet@55642 ` 284` ``` have "B \ A (Suc n)" using B by (auto simp del: nat.rec(2)) ``` hoelzl@38656 ` 285` ``` from epsilon[OF B(1) this] * ``` hoelzl@38656 ` 286` ``` show False by auto ``` hoelzl@38656 ` 287` ``` qed ``` hoelzl@38656 ` 288` ``` qed ``` hoelzl@38656 ` 289` ```qed ``` hoelzl@38656 ` 290` hoelzl@38656 ` 291` ```lemma (in finite_measure) Radon_Nikodym_finite_measure: ``` hoelzl@47694 ` 292` ``` assumes "finite_measure N" and sets_eq: "sets N = sets M" ``` hoelzl@47694 ` 293` ``` assumes "absolutely_continuous M N" ``` hoelzl@47694 ` 294` ``` shows "\f \ borel_measurable M. (\x. 0 \ f x) \ density M f = N" ``` hoelzl@38656 ` 295` ```proof - ``` hoelzl@47694 ` 296` ``` interpret N: finite_measure N by fact ``` wenzelm@53015 ` 297` ``` def G \ "{g \ borel_measurable M. (\x. 0 \ g x) \ (\A\sets M. (\\<^sup>+x. g x * indicator A x \M) \ N A)}" ``` hoelzl@50003 ` 298` ``` { fix f have "f \ G \ f \ borel_measurable M" by (auto simp: G_def) } ``` hoelzl@50003 ` 299` ``` note this[measurable_dest] ``` hoelzl@38656 ` 300` ``` have "(\x. 0) \ G" unfolding G_def by auto ``` hoelzl@38656 ` 301` ``` hence "G \ {}" by auto ``` hoelzl@38656 ` 302` ``` { fix f g assume f: "f \ G" and g: "g \ G" ``` hoelzl@38656 ` 303` ``` have "(\x. max (g x) (f x)) \ G" (is "?max \ G") unfolding G_def ``` hoelzl@38656 ` 304` ``` proof safe ``` hoelzl@38656 ` 305` ``` show "?max \ borel_measurable M" using f g unfolding G_def by auto ``` hoelzl@38656 ` 306` ``` let ?A = "{x \ space M. f x \ g x}" ``` hoelzl@38656 ` 307` ``` have "?A \ sets M" using f g unfolding G_def by auto ``` hoelzl@38656 ` 308` ``` fix A assume "A \ sets M" ``` hoelzl@38656 ` 309` ``` hence sets: "?A \ A \ sets M" "(space M - ?A) \ A \ sets M" using `?A \ sets M` by auto ``` hoelzl@47694 ` 310` ``` hence sets': "?A \ A \ sets N" "(space M - ?A) \ A \ sets N" by (auto simp: sets_eq) ``` hoelzl@38656 ` 311` ``` have union: "((?A \ A) \ ((space M - ?A) \ A)) = A" ``` immler@50244 ` 312` ``` using sets.sets_into_space[OF `A \ sets M`] by auto ``` hoelzl@38656 ` 313` ``` have "\x. x \ space M \ max (g x) (f x) * indicator A x = ``` hoelzl@38656 ` 314` ``` g x * indicator (?A \ A) x + f x * indicator ((space M - ?A) \ A) x" ``` hoelzl@38656 ` 315` ``` by (auto simp: indicator_def max_def) ``` wenzelm@53015 ` 316` ``` hence "(\\<^sup>+x. max (g x) (f x) * indicator A x \M) = ``` wenzelm@53015 ` 317` ``` (\\<^sup>+x. g x * indicator (?A \ A) x \M) + ``` wenzelm@53015 ` 318` ``` (\\<^sup>+x. f x * indicator ((space M - ?A) \ A) x \M)" ``` hoelzl@38656 ` 319` ``` using f g sets unfolding G_def ``` wenzelm@46731 ` 320` ``` by (auto cong: positive_integral_cong intro!: positive_integral_add) ``` hoelzl@47694 ` 321` ``` also have "\ \ N (?A \ A) + N ((space M - ?A) \ A)" ``` hoelzl@38656 ` 322` ``` using f g sets unfolding G_def by (auto intro!: add_mono) ``` hoelzl@47694 ` 323` ``` also have "\ = N A" ``` hoelzl@47694 ` 324` ``` using plus_emeasure[OF sets'] union by auto ``` wenzelm@53015 ` 325` ``` finally show "(\\<^sup>+x. max (g x) (f x) * indicator A x \M) \ N A" . ``` hoelzl@41981 ` 326` ``` next ``` hoelzl@41981 ` 327` ``` fix x show "0 \ max (g x) (f x)" using f g by (auto simp: G_def split: split_max) ``` hoelzl@38656 ` 328` ``` qed } ``` hoelzl@38656 ` 329` ``` note max_in_G = this ``` hoelzl@41981 ` 330` ``` { fix f assume "incseq f" and f: "\i. f i \ G" ``` hoelzl@50003 ` 331` ``` then have [measurable]: "\i. f i \ borel_measurable M" by (auto simp: G_def) ``` hoelzl@41981 ` 332` ``` have "(\x. SUP i. f i x) \ G" unfolding G_def ``` hoelzl@38656 ` 333` ``` proof safe ``` hoelzl@50003 ` 334` ``` show "(\x. SUP i. f i x) \ borel_measurable M" by measurable ``` hoelzl@41981 ` 335` ``` { fix x show "0 \ (SUP i. f i x)" ``` hoelzl@44928 ` 336` ``` using f by (auto simp: G_def intro: SUP_upper2) } ``` hoelzl@41981 ` 337` ``` next ``` hoelzl@38656 ` 338` ``` fix A assume "A \ sets M" ``` wenzelm@53015 ` 339` ``` have "(\\<^sup>+x. (SUP i. f i x) * indicator A x \M) = ``` wenzelm@53015 ` 340` ``` (\\<^sup>+x. (SUP i. f i x * indicator A x) \M)" ``` hoelzl@41981 ` 341` ``` by (intro positive_integral_cong) (simp split: split_indicator) ``` wenzelm@53015 ` 342` ``` also have "\ = (SUP i. (\\<^sup>+x. f i x * indicator A x \M))" ``` hoelzl@41981 ` 343` ``` using `incseq f` f `A \ sets M` ``` hoelzl@41981 ` 344` ``` by (intro positive_integral_monotone_convergence_SUP) ``` hoelzl@41981 ` 345` ``` (auto simp: G_def incseq_Suc_iff le_fun_def split: split_indicator) ``` wenzelm@53015 ` 346` ``` finally show "(\\<^sup>+x. (SUP i. f i x) * indicator A x \M) \ N A" ``` hoelzl@44928 ` 347` ``` using f `A \ sets M` by (auto intro!: SUP_least simp: G_def) ``` hoelzl@38656 ` 348` ``` qed } ``` hoelzl@38656 ` 349` ``` note SUP_in_G = this ``` wenzelm@53015 ` 350` ``` let ?y = "SUP g : G. integral\<^sup>P M g" ``` hoelzl@47694 ` 351` ``` have y_le: "?y \ N (space M)" unfolding G_def ``` hoelzl@44928 ` 352` ``` proof (safe intro!: SUP_least) ``` wenzelm@53015 ` 353` ``` fix g assume "\A\sets M. (\\<^sup>+x. g x * indicator A x \M) \ N A" ``` wenzelm@53015 ` 354` ``` from this[THEN bspec, OF sets.top] show "integral\<^sup>P M g \ N (space M)" ``` hoelzl@38656 ` 355` ``` by (simp cong: positive_integral_cong) ``` hoelzl@38656 ` 356` ``` qed ``` haftmann@56212 ` 357` ``` from SUP_countable_SUP [OF `G \ {}`, of "integral\<^sup>P M"] guess ys .. note ys = this ``` wenzelm@53015 ` 358` ``` then have "\n. \g. g\G \ integral\<^sup>P M g = ys n" ``` hoelzl@38656 ` 359` ``` proof safe ``` wenzelm@53015 ` 360` ``` fix n assume "range ys \ integral\<^sup>P M ` G" ``` wenzelm@53015 ` 361` ``` hence "ys n \ integral\<^sup>P M ` G" by auto ``` wenzelm@53015 ` 362` ``` thus "\g. g\G \ integral\<^sup>P M g = ys n" by auto ``` hoelzl@38656 ` 363` ``` qed ``` wenzelm@53015 ` 364` ``` from choice[OF this] obtain gs where "\i. gs i \ G" "\n. integral\<^sup>P M (gs n) = ys n" by auto ``` wenzelm@53015 ` 365` ``` hence y_eq: "?y = (SUP i. integral\<^sup>P M (gs i))" using ys by auto ``` wenzelm@46731 ` 366` ``` let ?g = "\i x. Max ((\n. gs n x) ` {..i})" ``` hoelzl@41981 ` 367` ``` def f \ "\x. SUP i. ?g i x" ``` wenzelm@46731 ` 368` ``` let ?F = "\A x. f x * indicator A x" ``` hoelzl@41981 ` 369` ``` have gs_not_empty: "\i x. (\n. gs n x) ` {..i} \ {}" by auto ``` hoelzl@38656 ` 370` ``` { fix i have "?g i \ G" ``` hoelzl@38656 ` 371` ``` proof (induct i) ``` hoelzl@38656 ` 372` ``` case 0 thus ?case by simp fact ``` hoelzl@38656 ` 373` ``` next ``` hoelzl@38656 ` 374` ``` case (Suc i) ``` hoelzl@38656 ` 375` ``` with Suc gs_not_empty `gs (Suc i) \ G` show ?case ``` hoelzl@38656 ` 376` ``` by (auto simp add: atMost_Suc intro!: max_in_G) ``` hoelzl@38656 ` 377` ``` qed } ``` hoelzl@38656 ` 378` ``` note g_in_G = this ``` hoelzl@41981 ` 379` ``` have "incseq ?g" using gs_not_empty ``` hoelzl@41981 ` 380` ``` by (auto intro!: incseq_SucI le_funI simp add: atMost_Suc) ``` hoelzl@50003 ` 381` ``` from SUP_in_G[OF this g_in_G] have [measurable]: "f \ G" unfolding f_def . ``` hoelzl@41981 ` 382` ``` then have [simp, intro]: "f \ borel_measurable M" unfolding G_def by auto ``` wenzelm@53015 ` 383` ``` have "integral\<^sup>P M f = (SUP i. integral\<^sup>P M (?g i))" unfolding f_def ``` hoelzl@41981 ` 384` ``` using g_in_G `incseq ?g` ``` hoelzl@41981 ` 385` ``` by (auto intro!: positive_integral_monotone_convergence_SUP simp: G_def) ``` hoelzl@38656 ` 386` ``` also have "\ = ?y" ``` hoelzl@38656 ` 387` ``` proof (rule antisym) ``` wenzelm@53015 ` 388` ``` show "(SUP i. integral\<^sup>P M (?g i)) \ ?y" ``` haftmann@56166 ` 389` ``` using g_in_G by (auto intro: SUP_mono) ``` wenzelm@53015 ` 390` ``` show "?y \ (SUP i. integral\<^sup>P M (?g i))" unfolding y_eq ``` hoelzl@38656 ` 391` ``` by (auto intro!: SUP_mono positive_integral_mono Max_ge) ``` hoelzl@38656 ` 392` ``` qed ``` wenzelm@53015 ` 393` ``` finally have int_f_eq_y: "integral\<^sup>P M f = ?y" . ``` hoelzl@41981 ` 394` ``` have "\x. 0 \ f x" ``` hoelzl@41981 ` 395` ``` unfolding f_def using `\i. gs i \ G` ``` hoelzl@44928 ` 396` ``` by (auto intro!: SUP_upper2 Max_ge_iff[THEN iffD2] simp: G_def) ``` wenzelm@53015 ` 397` ``` let ?t = "\A. N A - (\\<^sup>+x. ?F A x \M)" ``` hoelzl@47694 ` 398` ``` let ?M = "diff_measure N (density M f)" ``` wenzelm@53015 ` 399` ``` have f_le_N: "\A. A \ sets M \ (\\<^sup>+x. ?F A x \M) \ N A" ``` hoelzl@41981 ` 400` ``` using `f \ G` unfolding G_def by auto ``` hoelzl@47694 ` 401` ``` have emeasure_M: "\A. A \ sets M \ emeasure ?M A = ?t A" ``` hoelzl@47694 ` 402` ``` proof (subst emeasure_diff_measure) ``` hoelzl@47694 ` 403` ``` from f_le_N[of "space M"] show "finite_measure N" "finite_measure (density M f)" ``` hoelzl@47694 ` 404` ``` by (auto intro!: finite_measureI simp: emeasure_density cong: positive_integral_cong) ``` hoelzl@47694 ` 405` ``` next ``` hoelzl@47694 ` 406` ``` fix B assume "B \ sets N" with f_le_N[of B] show "emeasure (density M f) B \ emeasure N B" ``` hoelzl@47694 ` 407` ``` by (auto simp: sets_eq emeasure_density cong: positive_integral_cong) ``` hoelzl@47694 ` 408` ``` qed (auto simp: sets_eq emeasure_density) ``` hoelzl@47694 ` 409` ``` from emeasure_M[of "space M"] N.finite_emeasure_space positive_integral_positive[of M "?F (space M)"] ``` hoelzl@47694 ` 410` ``` interpret M': finite_measure ?M ``` hoelzl@47694 ` 411` ``` by (auto intro!: finite_measureI simp: sets_eq_imp_space_eq[OF sets_eq] N.emeasure_eq_measure ereal_minus_eq_PInfty_iff) ``` hoelzl@47694 ` 412` hoelzl@47694 ` 413` ``` have ac: "absolutely_continuous M ?M" unfolding absolutely_continuous_def ``` hoelzl@45777 ` 414` ``` proof ``` wenzelm@53374 ` 415` ``` fix A assume A_M: "A \ null_sets M" ``` wenzelm@53374 ` 416` ``` with `absolutely_continuous M N` have A_N: "A \ null_sets N" ``` hoelzl@47694 ` 417` ``` unfolding absolutely_continuous_def by auto ``` wenzelm@53374 ` 418` ``` moreover from A_M A_N have "(\\<^sup>+ x. ?F A x \M) \ N A" using `f \ G` by (auto simp: G_def) ``` wenzelm@53015 ` 419` ``` ultimately have "N A - (\\<^sup>+ x. ?F A x \M) = 0" ``` hoelzl@47694 ` 420` ``` using positive_integral_positive[of M] by (auto intro!: antisym) ``` hoelzl@47694 ` 421` ``` then show "A \ null_sets ?M" ``` wenzelm@53374 ` 422` ``` using A_M by (simp add: emeasure_M null_sets_def sets_eq) ``` hoelzl@38656 ` 423` ``` qed ``` hoelzl@47694 ` 424` ``` have upper_bound: "\A\sets M. ?M A \ 0" ``` hoelzl@38656 ` 425` ``` proof (rule ccontr) ``` hoelzl@38656 ` 426` ``` assume "\ ?thesis" ``` hoelzl@47694 ` 427` ``` then obtain A where A: "A \ sets M" and pos: "0 < ?M A" ``` hoelzl@38656 ` 428` ``` by (auto simp: not_le) ``` hoelzl@38656 ` 429` ``` note pos ``` hoelzl@47694 ` 430` ``` also have "?M A \ ?M (space M)" ``` hoelzl@47694 ` 431` ``` using emeasure_space[of ?M A] by (simp add: sets_eq[THEN sets_eq_imp_space_eq]) ``` hoelzl@47694 ` 432` ``` finally have pos_t: "0 < ?M (space M)" by simp ``` hoelzl@38656 ` 433` ``` moreover ``` wenzelm@53374 ` 434` ``` from pos_t have "emeasure M (space M) \ 0" ``` hoelzl@47694 ` 435` ``` using ac unfolding absolutely_continuous_def by (auto simp: null_sets_def) ``` hoelzl@47694 ` 436` ``` then have pos_M: "0 < emeasure M (space M)" ``` hoelzl@47694 ` 437` ``` using emeasure_nonneg[of M "space M"] by (simp add: le_less) ``` hoelzl@38656 ` 438` ``` moreover ``` wenzelm@53015 ` 439` ``` have "(\\<^sup>+x. f x * indicator (space M) x \M) \ N (space M)" ``` hoelzl@38656 ` 440` ``` using `f \ G` unfolding G_def by auto ``` wenzelm@53015 ` 441` ``` hence "(\\<^sup>+x. f x * indicator (space M) x \M) \ \" ``` hoelzl@47694 ` 442` ``` using M'.finite_emeasure_space by auto ``` hoelzl@38656 ` 443` ``` moreover ``` hoelzl@47694 ` 444` ``` def b \ "?M (space M) / emeasure M (space M) / 2" ``` hoelzl@41981 ` 445` ``` ultimately have b: "b \ 0 \ 0 \ b \ b \ \" ``` hoelzl@47694 ` 446` ``` by (auto simp: ereal_divide_eq) ``` hoelzl@41981 ` 447` ``` then have b: "b \ 0" "0 \ b" "0 < b" "b \ \" by auto ``` hoelzl@47694 ` 448` ``` let ?Mb = "density M (\_. b)" ``` hoelzl@47694 ` 449` ``` have Mb: "finite_measure ?Mb" "sets ?Mb = sets ?M" ``` hoelzl@47694 ` 450` ``` using b by (auto simp: emeasure_density_const sets_eq intro!: finite_measureI) ``` hoelzl@47694 ` 451` ``` from M'.Radon_Nikodym_aux[OF this] guess A0 .. ``` hoelzl@47694 ` 452` ``` then have "A0 \ sets M" ``` hoelzl@47694 ` 453` ``` and space_less_A0: "measure ?M (space M) - real b * measure M (space M) \ measure ?M A0 - real b * measure M A0" ``` hoelzl@47694 ` 454` ``` and *: "\B. B \ sets M \ B \ A0 \ 0 \ measure ?M B - real b * measure M B" ``` hoelzl@47694 ` 455` ``` using b by (simp_all add: measure_density_const sets_eq_imp_space_eq[OF sets_eq] sets_eq) ``` hoelzl@41981 ` 456` ``` { fix B assume B: "B \ sets M" "B \ A0" ``` hoelzl@47694 ` 457` ``` with *[OF this] have "b * emeasure M B \ ?M B" ``` hoelzl@47694 ` 458` ``` using b unfolding M'.emeasure_eq_measure emeasure_eq_measure by (cases b) auto } ``` hoelzl@38656 ` 459` ``` note bM_le_t = this ``` wenzelm@46731 ` 460` ``` let ?f0 = "\x. f x + b * indicator A0 x" ``` hoelzl@38656 ` 461` ``` { fix A assume A: "A \ sets M" ``` hoelzl@38656 ` 462` ``` hence "A \ A0 \ sets M" using `A0 \ sets M` by auto ``` wenzelm@53015 ` 463` ``` have "(\\<^sup>+x. ?f0 x * indicator A x \M) = ``` wenzelm@53015 ` 464` ``` (\\<^sup>+x. f x * indicator A x + b * indicator (A \ A0) x \M)" ``` hoelzl@41981 ` 465` ``` by (auto intro!: positive_integral_cong split: split_indicator) ``` wenzelm@53015 ` 466` ``` hence "(\\<^sup>+x. ?f0 x * indicator A x \M) = ``` wenzelm@53015 ` 467` ``` (\\<^sup>+x. f x * indicator A x \M) + b * emeasure M (A \ A0)" ``` hoelzl@41981 ` 468` ``` using `A0 \ sets M` `A \ A0 \ sets M` A b `f \ G` ``` hoelzl@50003 ` 469` ``` by (simp add: positive_integral_add positive_integral_cmult_indicator G_def) } ``` hoelzl@38656 ` 470` ``` note f0_eq = this ``` hoelzl@38656 ` 471` ``` { fix A assume A: "A \ sets M" ``` hoelzl@38656 ` 472` ``` hence "A \ A0 \ sets M" using `A0 \ sets M` by auto ``` wenzelm@53015 ` 473` ``` have f_le_v: "(\\<^sup>+x. ?F A x \M) \ N A" using `f \ G` A unfolding G_def by auto ``` hoelzl@38656 ` 474` ``` note f0_eq[OF A] ``` wenzelm@53015 ` 475` ``` also have "(\\<^sup>+x. ?F A x \M) + b * emeasure M (A \ A0) \ (\\<^sup>+x. ?F A x \M) + ?M (A \ A0)" ``` hoelzl@38656 ` 476` ``` using bM_le_t[OF `A \ A0 \ sets M`] `A \ sets M` `A0 \ sets M` ``` hoelzl@38656 ` 477` ``` by (auto intro!: add_left_mono) ``` wenzelm@53015 ` 478` ``` also have "\ \ (\\<^sup>+x. f x * indicator A x \M) + ?M A" ``` hoelzl@47694 ` 479` ``` using emeasure_mono[of "A \ A0" A ?M] `A \ sets M` `A0 \ sets M` ``` hoelzl@47694 ` 480` ``` by (auto intro!: add_left_mono simp: sets_eq) ``` hoelzl@47694 ` 481` ``` also have "\ \ N A" ``` hoelzl@47694 ` 482` ``` unfolding emeasure_M[OF `A \ sets M`] ``` hoelzl@47694 ` 483` ``` using f_le_v N.emeasure_eq_measure[of A] positive_integral_positive[of M "?F A"] ``` wenzelm@53015 ` 484` ``` by (cases "\\<^sup>+x. ?F A x \M", cases "N A") auto ``` wenzelm@53015 ` 485` ``` finally have "(\\<^sup>+x. ?f0 x * indicator A x \M) \ N A" . } ``` hoelzl@50003 ` 486` ``` hence "?f0 \ G" using `A0 \ sets M` b `f \ G` ``` hoelzl@50003 ` 487` ``` by (auto intro!: ereal_add_nonneg_nonneg simp: G_def) ``` wenzelm@53015 ` 488` ``` have int_f_finite: "integral\<^sup>P M f \ \" ``` hoelzl@47694 ` 489` ``` by (metis N.emeasure_finite ereal_infty_less_eq2(1) int_f_eq_y y_le) ``` hoelzl@47694 ` 490` ``` have "0 < ?M (space M) - emeasure ?Mb (space M)" ``` hoelzl@47694 ` 491` ``` using pos_t ``` hoelzl@47694 ` 492` ``` by (simp add: b emeasure_density_const) ``` hoelzl@47694 ` 493` ``` (simp add: M'.emeasure_eq_measure emeasure_eq_measure pos_M b_def) ``` hoelzl@47694 ` 494` ``` also have "\ \ ?M A0 - b * emeasure M A0" ``` hoelzl@47694 ` 495` ``` using space_less_A0 `A0 \ sets M` b ``` hoelzl@47694 ` 496` ``` by (cases b) (auto simp add: b emeasure_density_const sets_eq M'.emeasure_eq_measure emeasure_eq_measure) ``` hoelzl@47694 ` 497` ``` finally have 1: "b * emeasure M A0 < ?M A0" ``` hoelzl@47694 ` 498` ``` by (metis M'.emeasure_real `A0 \ sets M` bM_le_t diff_self ereal_less(1) ereal_minus(1) ``` hoelzl@47694 ` 499` ``` less_eq_ereal_def mult_zero_left not_square_less_zero subset_refl zero_ereal_def) ``` hoelzl@47694 ` 500` ``` with b have "0 < ?M A0" ``` hoelzl@47694 ` 501` ``` by (metis M'.emeasure_real MInfty_neq_PInfty(1) emeasure_real ereal_less_eq(5) ereal_zero_times ``` hoelzl@47694 ` 502` ``` ereal_mult_eq_MInfty ereal_mult_eq_PInfty ereal_zero_less_0_iff less_eq_ereal_def) ``` hoelzl@47694 ` 503` ``` then have "emeasure M A0 \ 0" using ac `A0 \ sets M` ``` hoelzl@47694 ` 504` ``` by (auto simp: absolutely_continuous_def null_sets_def) ``` hoelzl@47694 ` 505` ``` then have "0 < emeasure M A0" using emeasure_nonneg[of M A0] by auto ``` hoelzl@47694 ` 506` ``` hence "0 < b * emeasure M A0" using b by (auto simp: ereal_zero_less_0_iff) ``` wenzelm@53015 ` 507` ``` with int_f_finite have "?y + 0 < integral\<^sup>P M f + b * emeasure M A0" unfolding int_f_eq_y ``` hoelzl@41981 ` 508` ``` using `f \ G` ``` hoelzl@44928 ` 509` ``` by (intro ereal_add_strict_mono) (auto intro!: SUP_upper2 positive_integral_positive) ``` wenzelm@53015 ` 510` ``` also have "\ = integral\<^sup>P M ?f0" using f0_eq[OF sets.top] `A0 \ sets M` sets.sets_into_space ``` hoelzl@38656 ` 511` ``` by (simp cong: positive_integral_cong) ``` wenzelm@53015 ` 512` ``` finally have "?y < integral\<^sup>P M ?f0" by simp ``` wenzelm@53015 ` 513` ``` moreover from `?f0 \ G` have "integral\<^sup>P M ?f0 \ ?y" by (auto intro!: SUP_upper) ``` hoelzl@38656 ` 514` ``` ultimately show False by auto ``` hoelzl@38656 ` 515` ``` qed ``` hoelzl@47694 ` 516` ``` let ?f = "\x. max 0 (f x)" ``` hoelzl@38656 ` 517` ``` show ?thesis ``` hoelzl@47694 ` 518` ``` proof (intro bexI[of _ ?f] measure_eqI conjI) ``` hoelzl@47694 ` 519` ``` show "sets (density M ?f) = sets N" ``` hoelzl@47694 ` 520` ``` by (simp add: sets_eq) ``` hoelzl@47694 ` 521` ``` fix A assume A: "A\sets (density M ?f)" ``` hoelzl@47694 ` 522` ``` then show "emeasure (density M ?f) A = emeasure N A" ``` hoelzl@47694 ` 523` ``` using `f \ G` A upper_bound[THEN bspec, of A] N.emeasure_eq_measure[of A] ``` wenzelm@53015 ` 524` ``` by (cases "integral\<^sup>P M (?F A)") ``` hoelzl@47694 ` 525` ``` (auto intro!: antisym simp add: emeasure_density G_def emeasure_M density_max_0[symmetric]) ``` hoelzl@47694 ` 526` ``` qed auto ``` hoelzl@38656 ` 527` ```qed ``` hoelzl@38656 ` 528` hoelzl@40859 ` 529` ```lemma (in finite_measure) split_space_into_finite_sets_and_rest: ``` hoelzl@47694 ` 530` ``` assumes ac: "absolutely_continuous M N" and sets_eq: "sets N = sets M" ``` hoelzl@41981 ` 531` ``` shows "\A0\sets M. \B::nat\'a set. disjoint_family B \ range B \ sets M \ A0 = space M - (\i. B i) \ ``` hoelzl@47694 ` 532` ``` (\A\sets M. A \ A0 \ (emeasure M A = 0 \ N A = 0) \ (emeasure M A > 0 \ N A = \)) \ ``` hoelzl@47694 ` 533` ``` (\i. N (B i) \ \)" ``` hoelzl@38656 ` 534` ```proof - ``` hoelzl@47694 ` 535` ``` let ?Q = "{Q\sets M. N Q \ \}" ``` hoelzl@47694 ` 536` ``` let ?a = "SUP Q:?Q. emeasure M Q" ``` hoelzl@47694 ` 537` ``` have "{} \ ?Q" by auto ``` hoelzl@38656 ` 538` ``` then have Q_not_empty: "?Q \ {}" by blast ``` immler@50244 ` 539` ``` have "?a \ emeasure M (space M)" using sets.sets_into_space ``` hoelzl@47694 ` 540` ``` by (auto intro!: SUP_least emeasure_mono) ``` hoelzl@47694 ` 541` ``` then have "?a \ \" using finite_emeasure_space ``` hoelzl@38656 ` 542` ``` by auto ``` haftmann@56212 ` 543` ``` from SUP_countable_SUP [OF Q_not_empty, of "emeasure M"] ``` hoelzl@47694 ` 544` ``` obtain Q'' where "range Q'' \ emeasure M ` ?Q" and a: "?a = (SUP i::nat. Q'' i)" ``` hoelzl@38656 ` 545` ``` by auto ``` hoelzl@47694 ` 546` ``` then have "\i. \Q'. Q'' i = emeasure M Q' \ Q' \ ?Q" by auto ``` hoelzl@47694 ` 547` ``` from choice[OF this] obtain Q' where Q': "\i. Q'' i = emeasure M (Q' i)" "\i. Q' i \ ?Q" ``` hoelzl@38656 ` 548` ``` by auto ``` hoelzl@47694 ` 549` ``` then have a_Lim: "?a = (SUP i::nat. emeasure M (Q' i))" using a by simp ``` wenzelm@46731 ` 550` ``` let ?O = "\n. \i\n. Q' i" ``` hoelzl@47694 ` 551` ``` have Union: "(SUP i. emeasure M (?O i)) = emeasure M (\i. ?O i)" ``` hoelzl@47694 ` 552` ``` proof (rule SUP_emeasure_incseq[of ?O]) ``` hoelzl@47694 ` 553` ``` show "range ?O \ sets M" using Q' by auto ``` nipkow@44890 ` 554` ``` show "incseq ?O" by (fastforce intro!: incseq_SucI) ``` hoelzl@38656 ` 555` ``` qed ``` hoelzl@38656 ` 556` ``` have Q'_sets: "\i. Q' i \ sets M" using Q' by auto ``` hoelzl@47694 ` 557` ``` have O_sets: "\i. ?O i \ sets M" using Q' by auto ``` hoelzl@38656 ` 558` ``` then have O_in_G: "\i. ?O i \ ?Q" ``` hoelzl@38656 ` 559` ``` proof (safe del: notI) ``` hoelzl@47694 ` 560` ``` fix i have "Q' ` {..i} \ sets M" using Q' by auto ``` hoelzl@47694 ` 561` ``` then have "N (?O i) \ (\i\i. N (Q' i))" ``` hoelzl@47694 ` 562` ``` by (simp add: sets_eq emeasure_subadditive_finite) ``` hoelzl@41981 ` 563` ``` also have "\ < \" using Q' by (simp add: setsum_Pinfty) ``` hoelzl@47694 ` 564` ``` finally show "N (?O i) \ \" by simp ``` hoelzl@38656 ` 565` ``` qed auto ``` nipkow@44890 ` 566` ``` have O_mono: "\n. ?O n \ ?O (Suc n)" by fastforce ``` hoelzl@47694 ` 567` ``` have a_eq: "?a = emeasure M (\i. ?O i)" unfolding Union[symmetric] ``` hoelzl@38656 ` 568` ``` proof (rule antisym) ``` hoelzl@47694 ` 569` ``` show "?a \ (SUP i. emeasure M (?O i))" unfolding a_Lim ``` hoelzl@47694 ` 570` ``` using Q' by (auto intro!: SUP_mono emeasure_mono) ``` hoelzl@47694 ` 571` ``` show "(SUP i. emeasure M (?O i)) \ ?a" unfolding SUP_def ``` hoelzl@38656 ` 572` ``` proof (safe intro!: Sup_mono, unfold bex_simps) ``` hoelzl@38656 ` 573` ``` fix i ``` haftmann@52141 ` 574` ``` have *: "(\(Q' ` {..i})) = ?O i" by auto ``` hoelzl@47694 ` 575` ``` then show "\x. (x \ sets M \ N x \ \) \ ``` haftmann@52141 ` 576` ``` emeasure M (\(Q' ` {..i})) \ emeasure M x" ``` hoelzl@38656 ` 577` ``` using O_in_G[of i] by (auto intro!: exI[of _ "?O i"]) ``` hoelzl@38656 ` 578` ``` qed ``` hoelzl@38656 ` 579` ``` qed ``` wenzelm@46731 ` 580` ``` let ?O_0 = "(\i. ?O i)" ``` hoelzl@38656 ` 581` ``` have "?O_0 \ sets M" using Q' by auto ``` hoelzl@40859 ` 582` ``` def Q \ "\i. case i of 0 \ Q' 0 | Suc n \ ?O (Suc n) - ?O n" ``` hoelzl@38656 ` 583` ``` { fix i have "Q i \ sets M" unfolding Q_def using Q'[of 0] by (cases i) (auto intro: O_sets) } ``` hoelzl@38656 ` 584` ``` note Q_sets = this ``` hoelzl@40859 ` 585` ``` show ?thesis ``` hoelzl@40859 ` 586` ``` proof (intro bexI exI conjI ballI impI allI) ``` hoelzl@40859 ` 587` ``` show "disjoint_family Q" ``` nipkow@44890 ` 588` ``` by (fastforce simp: disjoint_family_on_def Q_def ``` hoelzl@40859 ` 589` ``` split: nat.split_asm) ``` hoelzl@40859 ` 590` ``` show "range Q \ sets M" ``` hoelzl@40859 ` 591` ``` using Q_sets by auto ``` hoelzl@40859 ` 592` ``` { fix A assume A: "A \ sets M" "A \ space M - ?O_0" ``` hoelzl@47694 ` 593` ``` show "emeasure M A = 0 \ N A = 0 \ 0 < emeasure M A \ N A = \" ``` hoelzl@40859 ` 594` ``` proof (rule disjCI, simp) ``` hoelzl@47694 ` 595` ``` assume *: "0 < emeasure M A \ N A \ \" ``` hoelzl@47694 ` 596` ``` show "emeasure M A = 0 \ N A = 0" ``` wenzelm@53374 ` 597` ``` proof (cases "emeasure M A = 0") ``` wenzelm@53374 ` 598` ``` case True ``` wenzelm@53374 ` 599` ``` with ac A have "N A = 0" ``` hoelzl@40859 ` 600` ``` unfolding absolutely_continuous_def by auto ``` wenzelm@53374 ` 601` ``` with True show ?thesis by simp ``` hoelzl@40859 ` 602` ``` next ``` wenzelm@53374 ` 603` ``` case False ``` wenzelm@53374 ` 604` ``` with * have "N A \ \" using emeasure_nonneg[of M A] by auto ``` hoelzl@47694 ` 605` ``` with A have "emeasure M ?O_0 + emeasure M A = emeasure M (?O_0 \ A)" ``` immler@50244 ` 606` ``` using Q' by (auto intro!: plus_emeasure sets.countable_UN) ``` hoelzl@47694 ` 607` ``` also have "\ = (SUP i. emeasure M (?O i \ A))" ``` hoelzl@47694 ` 608` ``` proof (rule SUP_emeasure_incseq[of "\i. ?O i \ A", symmetric, simplified]) ``` hoelzl@40859 ` 609` ``` show "range (\i. ?O i \ A) \ sets M" ``` hoelzl@47694 ` 610` ``` using `N A \ \` O_sets A by auto ``` nipkow@44890 ` 611` ``` qed (fastforce intro!: incseq_SucI) ``` hoelzl@40859 ` 612` ``` also have "\ \ ?a" ``` hoelzl@44928 ` 613` ``` proof (safe intro!: SUP_least) ``` hoelzl@40859 ` 614` ``` fix i have "?O i \ A \ ?Q" ``` hoelzl@40859 ` 615` ``` proof (safe del: notI) ``` hoelzl@40859 ` 616` ``` show "?O i \ A \ sets M" using O_sets A by auto ``` hoelzl@47694 ` 617` ``` from O_in_G[of i] have "N (?O i \ A) \ N (?O i) + N A" ``` hoelzl@47694 ` 618` ``` using emeasure_subadditive[of "?O i" N A] A O_sets by (auto simp: sets_eq) ``` hoelzl@47694 ` 619` ``` with O_in_G[of i] show "N (?O i \ A) \ \" ``` hoelzl@47694 ` 620` ``` using `N A \ \` by auto ``` hoelzl@40859 ` 621` ``` qed ``` hoelzl@47694 ` 622` ``` then show "emeasure M (?O i \ A) \ ?a" by (rule SUP_upper) ``` hoelzl@40859 ` 623` ``` qed ``` hoelzl@47694 ` 624` ``` finally have "emeasure M A = 0" ``` hoelzl@47694 ` 625` ``` unfolding a_eq using measure_nonneg[of M A] by (simp add: emeasure_eq_measure) ``` hoelzl@47694 ` 626` ``` with `emeasure M A \ 0` show ?thesis by auto ``` hoelzl@40859 ` 627` ``` qed ``` hoelzl@40859 ` 628` ``` qed } ``` hoelzl@47694 ` 629` ``` { fix i show "N (Q i) \ \" ``` hoelzl@40859 ` 630` ``` proof (cases i) ``` hoelzl@40859 ` 631` ``` case 0 then show ?thesis ``` hoelzl@40859 ` 632` ``` unfolding Q_def using Q'[of 0] by simp ``` hoelzl@40859 ` 633` ``` next ``` hoelzl@40859 ` 634` ``` case (Suc n) ``` hoelzl@47694 ` 635` ``` with `?O n \ ?Q` `?O (Suc n) \ ?Q` ``` hoelzl@47694 ` 636` ``` emeasure_Diff[OF _ _ _ O_mono, of N n] emeasure_nonneg[of N "(\ x\n. Q' x)"] ``` hoelzl@47694 ` 637` ``` show ?thesis ``` hoelzl@47694 ` 638` ``` by (auto simp: sets_eq ereal_minus_eq_PInfty_iff Q_def) ``` hoelzl@40859 ` 639` ``` qed } ``` hoelzl@40859 ` 640` ``` show "space M - ?O_0 \ sets M" using Q'_sets by auto ``` hoelzl@40859 ` 641` ``` { fix j have "(\i\j. ?O i) = (\i\j. Q i)" ``` hoelzl@40859 ` 642` ``` proof (induct j) ``` hoelzl@40859 ` 643` ``` case 0 then show ?case by (simp add: Q_def) ``` hoelzl@40859 ` 644` ``` next ``` hoelzl@40859 ` 645` ``` case (Suc j) ``` nipkow@44890 ` 646` ``` have eq: "\j. (\i\j. ?O i) = (\i\j. Q' i)" by fastforce ``` hoelzl@40859 ` 647` ``` have "{..j} \ {..Suc j} = {..Suc j}" by auto ``` hoelzl@40859 ` 648` ``` then have "(\i\Suc j. Q' i) = (\i\j. Q' i) \ Q (Suc j)" ``` hoelzl@40859 ` 649` ``` by (simp add: UN_Un[symmetric] Q_def del: UN_Un) ``` hoelzl@40859 ` 650` ``` then show ?case using Suc by (auto simp add: eq atMost_Suc) ``` hoelzl@40859 ` 651` ``` qed } ``` hoelzl@40859 ` 652` ``` then have "(\j. (\i\j. ?O i)) = (\j. (\i\j. Q i))" by simp ``` nipkow@44890 ` 653` ``` then show "space M - ?O_0 = space M - (\i. Q i)" by fastforce ``` hoelzl@40859 ` 654` ``` qed ``` hoelzl@40859 ` 655` ```qed ``` hoelzl@40859 ` 656` hoelzl@40859 ` 657` ```lemma (in finite_measure) Radon_Nikodym_finite_measure_infinite: ``` hoelzl@47694 ` 658` ``` assumes "absolutely_continuous M N" and sets_eq: "sets N = sets M" ``` hoelzl@47694 ` 659` ``` shows "\f\borel_measurable M. (\x. 0 \ f x) \ density M f = N" ``` hoelzl@40859 ` 660` ```proof - ``` hoelzl@40859 ` 661` ``` from split_space_into_finite_sets_and_rest[OF assms] ``` hoelzl@40859 ` 662` ``` obtain Q0 and Q :: "nat \ 'a set" ``` hoelzl@40859 ` 663` ``` where Q: "disjoint_family Q" "range Q \ sets M" ``` hoelzl@40859 ` 664` ``` and Q0: "Q0 \ sets M" "Q0 = space M - (\i. Q i)" ``` hoelzl@47694 ` 665` ``` and in_Q0: "\A. A \ sets M \ A \ Q0 \ emeasure M A = 0 \ N A = 0 \ 0 < emeasure M A \ N A = \" ``` hoelzl@47694 ` 666` ``` and Q_fin: "\i. N (Q i) \ \" by force ``` hoelzl@40859 ` 667` ``` from Q have Q_sets: "\i. Q i \ sets M" by auto ``` hoelzl@47694 ` 668` ``` let ?N = "\i. density N (indicator (Q i))" and ?M = "\i. density M (indicator (Q i))" ``` hoelzl@47694 ` 669` ``` have "\i. \f\borel_measurable (?M i). (\x. 0 \ f x) \ density (?M i) f = ?N i" ``` hoelzl@47694 ` 670` ``` proof (intro allI finite_measure.Radon_Nikodym_finite_measure) ``` hoelzl@38656 ` 671` ``` fix i ``` hoelzl@47694 ` 672` ``` from Q show "finite_measure (?M i)" ``` hoelzl@47694 ` 673` ``` by (auto intro!: finite_measureI cong: positive_integral_cong ``` hoelzl@47694 ` 674` ``` simp add: emeasure_density subset_eq sets_eq) ``` hoelzl@47694 ` 675` ``` from Q have "emeasure (?N i) (space N) = emeasure N (Q i)" ``` hoelzl@47694 ` 676` ``` by (simp add: sets_eq[symmetric] emeasure_density subset_eq cong: positive_integral_cong) ``` hoelzl@47694 ` 677` ``` with Q_fin show "finite_measure (?N i)" ``` hoelzl@47694 ` 678` ``` by (auto intro!: finite_measureI) ``` hoelzl@47694 ` 679` ``` show "sets (?N i) = sets (?M i)" by (simp add: sets_eq) ``` hoelzl@50003 ` 680` ``` have [measurable]: "\A. A \ sets M \ A \ sets N" by (simp add: sets_eq) ``` hoelzl@47694 ` 681` ``` show "absolutely_continuous (?M i) (?N i)" ``` hoelzl@47694 ` 682` ``` using `absolutely_continuous M N` `Q i \ sets M` ``` hoelzl@47694 ` 683` ``` by (auto simp: absolutely_continuous_def null_sets_density_iff sets_eq ``` hoelzl@47694 ` 684` ``` intro!: absolutely_continuous_AE[OF sets_eq]) ``` hoelzl@38656 ` 685` ``` qed ``` hoelzl@47694 ` 686` ``` from choice[OF this[unfolded Bex_def]] ``` hoelzl@47694 ` 687` ``` obtain f where borel: "\i. f i \ borel_measurable M" "\i x. 0 \ f i x" ``` hoelzl@47694 ` 688` ``` and f_density: "\i. density (?M i) (f i) = ?N i" ``` immler@54776 ` 689` ``` by force ``` hoelzl@47694 ` 690` ``` { fix A i assume A: "A \ sets M" ``` wenzelm@53015 ` 691` ``` with Q borel have "(\\<^sup>+x. f i x * indicator (Q i \ A) x \M) = emeasure (density (?M i) (f i)) A" ``` hoelzl@47694 ` 692` ``` by (auto simp add: emeasure_density positive_integral_density subset_eq ``` hoelzl@47694 ` 693` ``` intro!: positive_integral_cong split: split_indicator) ``` hoelzl@47694 ` 694` ``` also have "\ = emeasure N (Q i \ A)" ``` hoelzl@47694 ` 695` ``` using A Q by (simp add: f_density emeasure_restricted subset_eq sets_eq) ``` wenzelm@53015 ` 696` ``` finally have "emeasure N (Q i \ A) = (\\<^sup>+x. f i x * indicator (Q i \ A) x \M)" .. } ``` hoelzl@47694 ` 697` ``` note integral_eq = this ``` wenzelm@46731 ` 698` ``` let ?f = "\x. (\i. f i x * indicator (Q i) x) + \ * indicator Q0 x" ``` hoelzl@38656 ` 699` ``` show ?thesis ``` hoelzl@38656 ` 700` ``` proof (safe intro!: bexI[of _ ?f]) ``` hoelzl@41981 ` 701` ``` show "?f \ borel_measurable M" using Q0 borel Q_sets ``` hoelzl@41981 ` 702` ``` by (auto intro!: measurable_If) ``` hoelzl@41981 ` 703` ``` show "\x. 0 \ ?f x" using borel by (auto intro!: suminf_0_le simp: indicator_def) ``` hoelzl@47694 ` 704` ``` show "density M ?f = N" ``` hoelzl@47694 ` 705` ``` proof (rule measure_eqI) ``` hoelzl@47694 ` 706` ``` fix A assume "A \ sets (density M ?f)" ``` hoelzl@47694 ` 707` ``` then have "A \ sets M" by simp ``` hoelzl@47694 ` 708` ``` have Qi: "\i. Q i \ sets M" using Q by auto ``` hoelzl@47694 ` 709` ``` have [intro,simp]: "\i. (\x. f i x * indicator (Q i \ A) x) \ borel_measurable M" ``` hoelzl@47694 ` 710` ``` "\i. AE x in M. 0 \ f i x * indicator (Q i \ A) x" ``` hoelzl@47694 ` 711` ``` using borel Qi Q0(1) `A \ sets M` by (auto intro!: borel_measurable_ereal_times) ``` wenzelm@53015 ` 712` ``` have "(\\<^sup>+x. ?f x * indicator A x \M) = (\\<^sup>+x. (\i. f i x * indicator (Q i \ A) x) + \ * indicator (Q0 \ A) x \M)" ``` hoelzl@47694 ` 713` ``` using borel by (intro positive_integral_cong) (auto simp: indicator_def) ``` wenzelm@53015 ` 714` ``` also have "\ = (\\<^sup>+x. (\i. f i x * indicator (Q i \ A) x) \M) + \ * emeasure M (Q0 \ A)" ``` hoelzl@47694 ` 715` ``` using borel Qi Q0(1) `A \ sets M` ``` hoelzl@47694 ` 716` ``` by (subst positive_integral_add) (auto simp del: ereal_infty_mult ``` immler@50244 ` 717` ``` simp add: positive_integral_cmult_indicator sets.Int intro!: suminf_0_le) ``` hoelzl@47694 ` 718` ``` also have "\ = (\i. N (Q i \ A)) + \ * emeasure M (Q0 \ A)" ``` hoelzl@47694 ` 719` ``` by (subst integral_eq[OF `A \ sets M`], subst positive_integral_suminf) auto ``` wenzelm@53015 ` 720` ``` finally have "(\\<^sup>+x. ?f x * indicator A x \M) = (\i. N (Q i \ A)) + \ * emeasure M (Q0 \ A)" . ``` hoelzl@47694 ` 721` ``` moreover have "(\i. N (Q i \ A)) = N ((\i. Q i) \ A)" ``` hoelzl@47694 ` 722` ``` using Q Q_sets `A \ sets M` ``` hoelzl@47694 ` 723` ``` by (subst suminf_emeasure) (auto simp: disjoint_family_on_def sets_eq) ``` hoelzl@47694 ` 724` ``` moreover have "\ * emeasure M (Q0 \ A) = N (Q0 \ A)" ``` hoelzl@47694 ` 725` ``` proof - ``` hoelzl@47694 ` 726` ``` have "Q0 \ A \ sets M" using Q0(1) `A \ sets M` by blast ``` hoelzl@47694 ` 727` ``` from in_Q0[OF this] show ?thesis by auto ``` hoelzl@47694 ` 728` ``` qed ``` hoelzl@47694 ` 729` ``` moreover have "Q0 \ A \ sets M" "((\i. Q i) \ A) \ sets M" ``` hoelzl@47694 ` 730` ``` using Q_sets `A \ sets M` Q0(1) by auto ``` hoelzl@47694 ` 731` ``` moreover have "((\i. Q i) \ A) \ (Q0 \ A) = A" "((\i. Q i) \ A) \ (Q0 \ A) = {}" ``` immler@50244 ` 732` ``` using `A \ sets M` sets.sets_into_space Q0 by auto ``` wenzelm@53015 ` 733` ``` ultimately have "N A = (\\<^sup>+x. ?f x * indicator A x \M)" ``` hoelzl@47694 ` 734` ``` using plus_emeasure[of "(\i. Q i) \ A" N "Q0 \ A"] by (simp add: sets_eq) ``` hoelzl@47694 ` 735` ``` with `A \ sets M` borel Q Q0(1) show "emeasure (density M ?f) A = N A" ``` hoelzl@50003 ` 736` ``` by (auto simp: subset_eq emeasure_density) ``` hoelzl@47694 ` 737` ``` qed (simp add: sets_eq) ``` hoelzl@38656 ` 738` ``` qed ``` hoelzl@38656 ` 739` ```qed ``` hoelzl@38656 ` 740` hoelzl@38656 ` 741` ```lemma (in sigma_finite_measure) Radon_Nikodym: ``` hoelzl@47694 ` 742` ``` assumes ac: "absolutely_continuous M N" assumes sets_eq: "sets N = sets M" ``` hoelzl@47694 ` 743` ``` shows "\f \ borel_measurable M. (\x. 0 \ f x) \ density M f = N" ``` hoelzl@38656 ` 744` ```proof - ``` hoelzl@38656 ` 745` ``` from Ex_finite_integrable_function ``` wenzelm@53015 ` 746` ``` obtain h where finite: "integral\<^sup>P M h \ \" and ``` hoelzl@38656 ` 747` ``` borel: "h \ borel_measurable M" and ``` hoelzl@41981 ` 748` ``` nn: "\x. 0 \ h x" and ``` hoelzl@38656 ` 749` ``` pos: "\x. x \ space M \ 0 < h x" and ``` hoelzl@41981 ` 750` ``` "\x. x \ space M \ h x < \" by auto ``` wenzelm@53015 ` 751` ``` let ?T = "\A. (\\<^sup>+x. h x * indicator A x \M)" ``` hoelzl@47694 ` 752` ``` let ?MT = "density M h" ``` hoelzl@47694 ` 753` ``` from borel finite nn interpret T: finite_measure ?MT ``` hoelzl@47694 ` 754` ``` by (auto intro!: finite_measureI cong: positive_integral_cong simp: emeasure_density) ``` hoelzl@47694 ` 755` ``` have "absolutely_continuous ?MT N" "sets N = sets ?MT" ``` hoelzl@47694 ` 756` ``` proof (unfold absolutely_continuous_def, safe) ``` hoelzl@47694 ` 757` ``` fix A assume "A \ null_sets ?MT" ``` hoelzl@47694 ` 758` ``` with borel have "A \ sets M" "AE x in M. x \ A \ h x \ 0" ``` hoelzl@47694 ` 759` ``` by (auto simp add: null_sets_density_iff) ``` immler@50244 ` 760` ``` with pos sets.sets_into_space have "AE x in M. x \ A" ``` hoelzl@47694 ` 761` ``` by (elim eventually_elim1) (auto simp: not_le[symmetric]) ``` hoelzl@47694 ` 762` ``` then have "A \ null_sets M" ``` hoelzl@47694 ` 763` ``` using `A \ sets M` by (simp add: AE_iff_null_sets) ``` hoelzl@47694 ` 764` ``` with ac show "A \ null_sets N" ``` hoelzl@47694 ` 765` ``` by (auto simp: absolutely_continuous_def) ``` hoelzl@47694 ` 766` ``` qed (auto simp add: sets_eq) ``` hoelzl@47694 ` 767` ``` from T.Radon_Nikodym_finite_measure_infinite[OF this] ``` hoelzl@47694 ` 768` ``` obtain f where f_borel: "f \ borel_measurable M" "\x. 0 \ f x" "density ?MT f = N" by auto ``` hoelzl@47694 ` 769` ``` with nn borel show ?thesis ``` hoelzl@47694 ` 770` ``` by (auto intro!: bexI[of _ "\x. h x * f x"] simp: density_density_eq) ``` hoelzl@38656 ` 771` ```qed ``` hoelzl@38656 ` 772` hoelzl@40859 ` 773` ```section "Uniqueness of densities" ``` hoelzl@40859 ` 774` hoelzl@47694 ` 775` ```lemma finite_density_unique: ``` hoelzl@40859 ` 776` ``` assumes borel: "f \ borel_measurable M" "g \ borel_measurable M" ``` hoelzl@47694 ` 777` ``` assumes pos: "AE x in M. 0 \ f x" "AE x in M. 0 \ g x" ``` wenzelm@53015 ` 778` ``` and fin: "integral\<^sup>P M f \ \" ``` hoelzl@49785 ` 779` ``` shows "density M f = density M g \ (AE x in M. f x = g x)" ``` hoelzl@40859 ` 780` ```proof (intro iffI ballI) ``` hoelzl@47694 ` 781` ``` fix A assume eq: "AE x in M. f x = g x" ``` hoelzl@49785 ` 782` ``` with borel show "density M f = density M g" ``` hoelzl@49785 ` 783` ``` by (auto intro: density_cong) ``` hoelzl@40859 ` 784` ```next ``` wenzelm@53015 ` 785` ``` let ?P = "\f A. \\<^sup>+ x. f x * indicator A x \M" ``` hoelzl@49785 ` 786` ``` assume "density M f = density M g" ``` hoelzl@49785 ` 787` ``` with borel have eq: "\A\sets M. ?P f A = ?P g A" ``` hoelzl@49785 ` 788` ``` by (simp add: emeasure_density[symmetric]) ``` immler@50244 ` 789` ``` from this[THEN bspec, OF sets.top] fin ``` wenzelm@53015 ` 790` ``` have g_fin: "integral\<^sup>P M g \ \" by (simp cong: positive_integral_cong) ``` hoelzl@40859 ` 791` ``` { fix f g assume borel: "f \ borel_measurable M" "g \ borel_measurable M" ``` hoelzl@47694 ` 792` ``` and pos: "AE x in M. 0 \ f x" "AE x in M. 0 \ g x" ``` wenzelm@53015 ` 793` ``` and g_fin: "integral\<^sup>P M g \ \" and eq: "\A\sets M. ?P f A = ?P g A" ``` hoelzl@40859 ` 794` ``` let ?N = "{x\space M. g x < f x}" ``` hoelzl@40859 ` 795` ``` have N: "?N \ sets M" using borel by simp ``` wenzelm@53015 ` 796` ``` have "?P g ?N \ integral\<^sup>P M g" using pos ``` hoelzl@41981 ` 797` ``` by (intro positive_integral_mono_AE) (auto split: split_indicator) ``` hoelzl@41981 ` 798` ``` then have Pg_fin: "?P g ?N \ \" using g_fin by auto ``` wenzelm@53015 ` 799` ``` have "?P (\x. (f x - g x)) ?N = (\\<^sup>+x. f x * indicator ?N x - g x * indicator ?N x \M)" ``` hoelzl@40859 ` 800` ``` by (auto intro!: positive_integral_cong simp: indicator_def) ``` hoelzl@40859 ` 801` ``` also have "\ = ?P f ?N - ?P g ?N" ``` hoelzl@40859 ` 802` ``` proof (rule positive_integral_diff) ``` hoelzl@40859 ` 803` ``` show "(\x. f x * indicator ?N x) \ borel_measurable M" "(\x. g x * indicator ?N x) \ borel_measurable M" ``` hoelzl@40859 ` 804` ``` using borel N by auto ``` hoelzl@47694 ` 805` ``` show "AE x in M. g x * indicator ?N x \ f x * indicator ?N x" ``` hoelzl@47694 ` 806` ``` "AE x in M. 0 \ g x * indicator ?N x" ``` hoelzl@41981 ` 807` ``` using pos by (auto split: split_indicator) ``` hoelzl@41981 ` 808` ``` qed fact ``` hoelzl@40859 ` 809` ``` also have "\ = 0" ``` hoelzl@47694 ` 810` ``` unfolding eq[THEN bspec, OF N] using positive_integral_positive[of M] Pg_fin by auto ``` hoelzl@47694 ` 811` ``` finally have "AE x in M. f x \ g x" ``` hoelzl@41981 ` 812` ``` using pos borel positive_integral_PInf_AE[OF borel(2) g_fin] ``` hoelzl@41981 ` 813` ``` by (subst (asm) positive_integral_0_iff_AE) ``` hoelzl@43920 ` 814` ``` (auto split: split_indicator simp: not_less ereal_minus_le_iff) } ``` hoelzl@41981 ` 815` ``` from this[OF borel pos g_fin eq] this[OF borel(2,1) pos(2,1) fin] eq ``` hoelzl@47694 ` 816` ``` show "AE x in M. f x = g x" by auto ``` hoelzl@40859 ` 817` ```qed ``` hoelzl@40859 ` 818` hoelzl@40859 ` 819` ```lemma (in finite_measure) density_unique_finite_measure: ``` hoelzl@40859 ` 820` ``` assumes borel: "f \ borel_measurable M" "f' \ borel_measurable M" ``` hoelzl@47694 ` 821` ``` assumes pos: "AE x in M. 0 \ f x" "AE x in M. 0 \ f' x" ``` wenzelm@53015 ` 822` ``` assumes f: "\A. A \ sets M \ (\\<^sup>+x. f x * indicator A x \M) = (\\<^sup>+x. f' x * indicator A x \M)" ``` hoelzl@40859 ` 823` ``` (is "\A. A \ sets M \ ?P f A = ?P f' A") ``` hoelzl@47694 ` 824` ``` shows "AE x in M. f x = f' x" ``` hoelzl@40859 ` 825` ```proof - ``` hoelzl@47694 ` 826` ``` let ?D = "\f. density M f" ``` hoelzl@47694 ` 827` ``` let ?N = "\A. ?P f A" and ?N' = "\A. ?P f' A" ``` wenzelm@46731 ` 828` ``` let ?f = "\A x. f x * indicator A x" and ?f' = "\A x. f' x * indicator A x" ``` hoelzl@47694 ` 829` hoelzl@47694 ` 830` ``` have ac: "absolutely_continuous M (density M f)" "sets (density M f) = sets M" ``` hoelzl@47694 ` 831` ``` using borel by (auto intro!: absolutely_continuousI_density) ``` hoelzl@47694 ` 832` ``` from split_space_into_finite_sets_and_rest[OF this] ``` hoelzl@40859 ` 833` ``` obtain Q0 and Q :: "nat \ 'a set" ``` hoelzl@40859 ` 834` ``` where Q: "disjoint_family Q" "range Q \ sets M" ``` hoelzl@40859 ` 835` ``` and Q0: "Q0 \ sets M" "Q0 = space M - (\i. Q i)" ``` hoelzl@47694 ` 836` ``` and in_Q0: "\A. A \ sets M \ A \ Q0 \ emeasure M A = 0 \ ?D f A = 0 \ 0 < emeasure M A \ ?D f A = \" ``` hoelzl@47694 ` 837` ``` and Q_fin: "\i. ?D f (Q i) \ \" by force ``` hoelzl@47694 ` 838` ``` with borel pos have in_Q0: "\A. A \ sets M \ A \ Q0 \ emeasure M A = 0 \ ?N A = 0 \ 0 < emeasure M A \ ?N A = \" ``` hoelzl@47694 ` 839` ``` and Q_fin: "\i. ?N (Q i) \ \" by (auto simp: emeasure_density subset_eq) ``` hoelzl@47694 ` 840` hoelzl@40859 ` 841` ``` from Q have Q_sets: "\i. Q i \ sets M" by auto ``` hoelzl@47694 ` 842` ``` let ?D = "{x\space M. f x \ f' x}" ``` hoelzl@47694 ` 843` ``` have "?D \ sets M" using borel by auto ``` hoelzl@43920 ` 844` ``` have *: "\i x A. \y::ereal. y * indicator (Q i) x * indicator A x = y * indicator (Q i \ A) x" ``` hoelzl@40859 ` 845` ``` unfolding indicator_def by auto ``` hoelzl@47694 ` 846` ``` have "\i. AE x in M. ?f (Q i) x = ?f' (Q i) x" using borel Q_fin Q pos ``` hoelzl@40859 ` 847` ``` by (intro finite_density_unique[THEN iffD1] allI) ``` hoelzl@50003 ` 848` ``` (auto intro!: f measure_eqI simp: emeasure_density * subset_eq) ``` hoelzl@47694 ` 849` ``` moreover have "AE x in M. ?f Q0 x = ?f' Q0 x" ``` hoelzl@40859 ` 850` ``` proof (rule AE_I') ``` hoelzl@43920 ` 851` ``` { fix f :: "'a \ ereal" assume borel: "f \ borel_measurable M" ``` wenzelm@53015 ` 852` ``` and eq: "\A. A \ sets M \ ?N A = (\\<^sup>+x. f x * indicator A x \M)" ``` wenzelm@46731 ` 853` ``` let ?A = "\i. Q0 \ {x \ space M. f x < (i::nat)}" ``` hoelzl@47694 ` 854` ``` have "(\i. ?A i) \ null_sets M" ``` hoelzl@40859 ` 855` ``` proof (rule null_sets_UN) ``` hoelzl@43923 ` 856` ``` fix i ::nat have "?A i \ sets M" ``` hoelzl@40859 ` 857` ``` using borel Q0(1) by auto ``` wenzelm@53015 ` 858` ``` have "?N (?A i) \ (\\<^sup>+x. (i::ereal) * indicator (?A i) x \M)" ``` hoelzl@40859 ` 859` ``` unfolding eq[OF `?A i \ sets M`] ``` hoelzl@40859 ` 860` ``` by (auto intro!: positive_integral_mono simp: indicator_def) ``` hoelzl@47694 ` 861` ``` also have "\ = i * emeasure M (?A i)" ``` hoelzl@40859 ` 862` ``` using `?A i \ sets M` by (auto intro!: positive_integral_cmult_indicator) ``` hoelzl@47694 ` 863` ``` also have "\ < \" using emeasure_real[of "?A i"] by simp ``` hoelzl@47694 ` 864` ``` finally have "?N (?A i) \ \" by simp ``` hoelzl@47694 ` 865` ``` then show "?A i \ null_sets M" using in_Q0[OF `?A i \ sets M`] `?A i \ sets M` by auto ``` hoelzl@40859 ` 866` ``` qed ``` hoelzl@41981 ` 867` ``` also have "(\i. ?A i) = Q0 \ {x\space M. f x \ \}" ``` hoelzl@41981 ` 868` ``` by (auto simp: less_PInf_Ex_of_nat real_eq_of_nat) ``` hoelzl@47694 ` 869` ``` finally have "Q0 \ {x\space M. f x \ \} \ null_sets M" by simp } ``` hoelzl@40859 ` 870` ``` from this[OF borel(1) refl] this[OF borel(2) f] ``` hoelzl@47694 ` 871` ``` have "Q0 \ {x\space M. f x \ \} \ null_sets M" "Q0 \ {x\space M. f' x \ \} \ null_sets M" by simp_all ``` hoelzl@47694 ` 872` ``` then show "(Q0 \ {x\space M. f x \ \}) \ (Q0 \ {x\space M. f' x \ \}) \ null_sets M" by (rule null_sets.Un) ``` hoelzl@40859 ` 873` ``` show "{x \ space M. ?f Q0 x \ ?f' Q0 x} \ ``` hoelzl@41981 ` 874` ``` (Q0 \ {x\space M. f x \ \}) \ (Q0 \ {x\space M. f' x \ \})" by (auto simp: indicator_def) ``` hoelzl@40859 ` 875` ``` qed ``` hoelzl@47694 ` 876` ``` moreover have "AE x in M. (?f Q0 x = ?f' Q0 x) \ (\i. ?f (Q i) x = ?f' (Q i) x) \ ``` hoelzl@40859 ` 877` ``` ?f (space M) x = ?f' (space M) x" ``` hoelzl@40859 ` 878` ``` by (auto simp: indicator_def Q0) ``` hoelzl@47694 ` 879` ``` ultimately have "AE x in M. ?f (space M) x = ?f' (space M) x" ``` hoelzl@47694 ` 880` ``` unfolding AE_all_countable[symmetric] ``` hoelzl@47694 ` 881` ``` by eventually_elim (auto intro!: AE_I2 split: split_if_asm simp: indicator_def) ``` hoelzl@47694 ` 882` ``` then show "AE x in M. f x = f' x" by auto ``` hoelzl@40859 ` 883` ```qed ``` hoelzl@40859 ` 884` hoelzl@40859 ` 885` ```lemma (in sigma_finite_measure) density_unique: ``` hoelzl@47694 ` 886` ``` assumes f: "f \ borel_measurable M" "AE x in M. 0 \ f x" ``` hoelzl@47694 ` 887` ``` assumes f': "f' \ borel_measurable M" "AE x in M. 0 \ f' x" ``` hoelzl@47694 ` 888` ``` assumes density_eq: "density M f = density M f'" ``` hoelzl@47694 ` 889` ``` shows "AE x in M. f x = f' x" ``` hoelzl@40859 ` 890` ```proof - ``` hoelzl@40859 ` 891` ``` obtain h where h_borel: "h \ borel_measurable M" ``` wenzelm@53015 ` 892` ``` and fin: "integral\<^sup>P M h \ \" and pos: "\x. x \ space M \ 0 < h x \ h x < \" "\x. 0 \ h x" ``` hoelzl@40859 ` 893` ``` using Ex_finite_integrable_function by auto ``` hoelzl@47694 ` 894` ``` then have h_nn: "AE x in M. 0 \ h x" by auto ``` hoelzl@47694 ` 895` ``` let ?H = "density M h" ``` hoelzl@47694 ` 896` ``` interpret h: finite_measure ?H ``` hoelzl@47694 ` 897` ``` using fin h_borel pos ``` hoelzl@47694 ` 898` ``` by (intro finite_measureI) (simp cong: positive_integral_cong emeasure_density add: fin) ``` hoelzl@47694 ` 899` ``` let ?fM = "density M f" ``` hoelzl@47694 ` 900` ``` let ?f'M = "density M f'" ``` hoelzl@40859 ` 901` ``` { fix A assume "A \ sets M" ``` hoelzl@41981 ` 902` ``` then have "{x \ space M. h x * indicator A x \ 0} = A" ``` immler@50244 ` 903` ``` using pos(1) sets.sets_into_space by (force simp: indicator_def) ``` wenzelm@53015 ` 904` ``` then have "(\\<^sup>+x. h x * indicator A x \M) = 0 \ A \ null_sets M" ``` hoelzl@41981 ` 905` ``` using h_borel `A \ sets M` h_nn by (subst positive_integral_0_iff) auto } ``` hoelzl@40859 ` 906` ``` note h_null_sets = this ``` hoelzl@40859 ` 907` ``` { fix A assume "A \ sets M" ``` wenzelm@53015 ` 908` ``` have "(\\<^sup>+x. f x * (h x * indicator A x) \M) = (\\<^sup>+x. h x * indicator A x \?fM)" ``` hoelzl@41981 ` 909` ``` using `A \ sets M` h_borel h_nn f f' ``` hoelzl@47694 ` 910` ``` by (intro positive_integral_density[symmetric]) auto ``` wenzelm@53015 ` 911` ``` also have "\ = (\\<^sup>+x. h x * indicator A x \?f'M)" ``` hoelzl@47694 ` 912` ``` by (simp_all add: density_eq) ``` wenzelm@53015 ` 913` ``` also have "\ = (\\<^sup>+x. f' x * (h x * indicator A x) \M)" ``` hoelzl@41981 ` 914` ``` using `A \ sets M` h_borel h_nn f f' ``` hoelzl@47694 ` 915` ``` by (intro positive_integral_density) auto ``` wenzelm@53015 ` 916` ``` finally have "(\\<^sup>+x. h x * (f x * indicator A x) \M) = (\\<^sup>+x. h x * (f' x * indicator A x) \M)" ``` hoelzl@41981 ` 917` ``` by (simp add: ac_simps) ``` wenzelm@53015 ` 918` ``` then have "(\\<^sup>+x. (f x * indicator A x) \?H) = (\\<^sup>+x. (f' x * indicator A x) \?H)" ``` hoelzl@41981 ` 919` ``` using `A \ sets M` h_borel h_nn f f' ``` hoelzl@47694 ` 920` ``` by (subst (asm) (1 2) positive_integral_density[symmetric]) auto } ``` hoelzl@41981 ` 921` ``` then have "AE x in ?H. f x = f' x" using h_borel h_nn f f' ``` hoelzl@47694 ` 922` ``` by (intro h.density_unique_finite_measure absolutely_continuous_AE[of M]) ``` hoelzl@47694 ` 923` ``` (auto simp add: AE_density) ``` hoelzl@47694 ` 924` ``` then show "AE x in M. f x = f' x" ``` hoelzl@47694 ` 925` ``` unfolding eventually_ae_filter using h_borel pos ``` hoelzl@47694 ` 926` ``` by (auto simp add: h_null_sets null_sets_density_iff not_less[symmetric] ``` hoelzl@50021 ` 927` ``` AE_iff_null_sets[symmetric]) blast ``` hoelzl@40859 ` 928` ```qed ``` hoelzl@40859 ` 929` hoelzl@47694 ` 930` ```lemma (in sigma_finite_measure) density_unique_iff: ``` hoelzl@47694 ` 931` ``` assumes f: "f \ borel_measurable M" and "AE x in M. 0 \ f x" ``` hoelzl@47694 ` 932` ``` assumes f': "f' \ borel_measurable M" and "AE x in M. 0 \ f' x" ``` hoelzl@47694 ` 933` ``` shows "density M f = density M f' \ (AE x in M. f x = f' x)" ``` hoelzl@47694 ` 934` ``` using density_unique[OF assms] density_cong[OF f f'] by auto ``` hoelzl@47694 ` 935` hoelzl@49785 ` 936` ```lemma sigma_finite_density_unique: ``` hoelzl@49785 ` 937` ``` assumes borel: "f \ borel_measurable M" "g \ borel_measurable M" ``` hoelzl@49785 ` 938` ``` assumes pos: "AE x in M. 0 \ f x" "AE x in M. 0 \ g x" ``` hoelzl@49785 ` 939` ``` and fin: "sigma_finite_measure (density M f)" ``` hoelzl@49785 ` 940` ``` shows "density M f = density M g \ (AE x in M. f x = g x)" ``` hoelzl@49785 ` 941` ```proof ``` hoelzl@49785 ` 942` ``` assume "AE x in M. f x = g x" with borel show "density M f = density M g" ``` hoelzl@49785 ` 943` ``` by (auto intro: density_cong) ``` hoelzl@49785 ` 944` ```next ``` hoelzl@49785 ` 945` ``` assume eq: "density M f = density M g" ``` hoelzl@49785 ` 946` ``` interpret f!: sigma_finite_measure "density M f" by fact ``` hoelzl@49785 ` 947` ``` from f.sigma_finite_incseq guess A . note cover = this ``` hoelzl@49785 ` 948` hoelzl@49785 ` 949` ``` have "AE x in M. \i. x \ A i \ f x = g x" ``` hoelzl@49785 ` 950` ``` unfolding AE_all_countable ``` hoelzl@49785 ` 951` ``` proof ``` hoelzl@49785 ` 952` ``` fix i ``` hoelzl@49785 ` 953` ``` have "density (density M f) (indicator (A i)) = density (density M g) (indicator (A i))" ``` hoelzl@49785 ` 954` ``` unfolding eq .. ``` wenzelm@53015 ` 955` ``` moreover have "(\\<^sup>+x. f x * indicator (A i) x \M) \ \" ``` hoelzl@49785 ` 956` ``` using cover(1) cover(3)[of i] borel by (auto simp: emeasure_density subset_eq) ``` hoelzl@49785 ` 957` ``` ultimately have "AE x in M. f x * indicator (A i) x = g x * indicator (A i) x" ``` hoelzl@49785 ` 958` ``` using borel pos cover(1) pos ``` hoelzl@49785 ` 959` ``` by (intro finite_density_unique[THEN iffD1]) ``` hoelzl@49785 ` 960` ``` (auto simp: density_density_eq subset_eq) ``` hoelzl@49785 ` 961` ``` then show "AE x in M. x \ A i \ f x = g x" ``` hoelzl@49785 ` 962` ``` by auto ``` hoelzl@49785 ` 963` ``` qed ``` hoelzl@49785 ` 964` ``` with AE_space show "AE x in M. f x = g x" ``` hoelzl@49785 ` 965` ``` apply eventually_elim ``` hoelzl@49785 ` 966` ``` using cover(2)[symmetric] ``` hoelzl@49785 ` 967` ``` apply auto ``` hoelzl@49785 ` 968` ``` done ``` hoelzl@49785 ` 969` ```qed ``` hoelzl@49785 ` 970` hoelzl@49778 ` 971` ```lemma (in sigma_finite_measure) sigma_finite_iff_density_finite': ``` hoelzl@47694 ` 972` ``` assumes f: "f \ borel_measurable M" "AE x in M. 0 \ f x" ``` hoelzl@47694 ` 973` ``` shows "sigma_finite_measure (density M f) \ (AE x in M. f x \ \)" ``` hoelzl@47694 ` 974` ``` (is "sigma_finite_measure ?N \ _") ``` hoelzl@40859 ` 975` ```proof ``` hoelzl@41689 ` 976` ``` assume "sigma_finite_measure ?N" ``` hoelzl@47694 ` 977` ``` then interpret N: sigma_finite_measure ?N . ``` hoelzl@47694 ` 978` ``` from N.Ex_finite_integrable_function obtain h where ``` wenzelm@53015 ` 979` ``` h: "h \ borel_measurable M" "integral\<^sup>P ?N h \ \" and ``` hoelzl@41981 ` 980` ``` h_nn: "\x. 0 \ h x" and ``` hoelzl@41981 ` 981` ``` fin: "\x\space M. 0 < h x \ h x < \" by auto ``` hoelzl@47694 ` 982` ``` have "AE x in M. f x * h x \ \" ``` hoelzl@40859 ` 983` ``` proof (rule AE_I') ``` wenzelm@53015 ` 984` ``` have "integral\<^sup>P ?N h = (\\<^sup>+x. f x * h x \M)" using f h h_nn ``` hoelzl@47694 ` 985` ``` by (auto intro!: positive_integral_density) ``` wenzelm@53015 ` 986` ``` then have "(\\<^sup>+x. f x * h x \M) \ \" ``` hoelzl@40859 ` 987` ``` using h(2) by simp ``` hoelzl@47694 ` 988` ``` then show "(\x. f x * h x) -` {\} \ space M \ null_sets M" ``` hoelzl@41981 ` 989` ``` using f h(1) by (auto intro!: positive_integral_PInf borel_measurable_vimage) ``` hoelzl@40859 ` 990` ``` qed auto ``` hoelzl@47694 ` 991` ``` then show "AE x in M. f x \ \" ``` hoelzl@41705 ` 992` ``` using fin by (auto elim!: AE_Ball_mp) ``` hoelzl@40859 ` 993` ```next ``` hoelzl@47694 ` 994` ``` assume AE: "AE x in M. f x \ \" ``` hoelzl@40859 ` 995` ``` from sigma_finite guess Q .. note Q = this ``` hoelzl@43923 ` 996` ``` def A \ "\i. f -` (case i of 0 \ {\} | Suc n \ {.. ereal(of_nat (Suc n))}) \ space M" ``` hoelzl@40859 ` 997` ``` { fix i j have "A i \ Q j \ sets M" ``` hoelzl@40859 ` 998` ``` unfolding A_def using f Q ``` immler@50244 ` 999` ``` apply (rule_tac sets.Int) ``` hoelzl@41981 ` 1000` ``` by (cases i) (auto intro: measurable_sets[OF f(1)]) } ``` hoelzl@40859 ` 1001` ``` note A_in_sets = this ``` wenzelm@46731 ` 1002` ``` let ?A = "\n. case prod_decode n of (i,j) \ A i \ Q j" ``` hoelzl@41689 ` 1003` ``` show "sigma_finite_measure ?N" ``` hoelzl@40859 ` 1004` ``` proof (default, intro exI conjI subsetI allI) ``` hoelzl@40859 ` 1005` ``` fix x assume "x \ range ?A" ``` hoelzl@40859 ` 1006` ``` then obtain n where n: "x = ?A n" by auto ``` hoelzl@41689 ` 1007` ``` then show "x \ sets ?N" using A_in_sets by (cases "prod_decode n") auto ``` hoelzl@40859 ` 1008` ``` next ``` hoelzl@40859 ` 1009` ``` have "(\i. ?A i) = (\i j. A i \ Q j)" ``` hoelzl@40859 ` 1010` ``` proof safe ``` hoelzl@40859 ` 1011` ``` fix x i j assume "x \ A i" "x \ Q j" ``` hoelzl@40859 ` 1012` ``` then show "x \ (\i. case prod_decode i of (i, j) \ A i \ Q j)" ``` hoelzl@40859 ` 1013` ``` by (intro UN_I[of "prod_encode (i,j)"]) auto ``` hoelzl@40859 ` 1014` ``` qed auto ``` hoelzl@40859 ` 1015` ``` also have "\ = (\i. A i) \ space M" using Q by auto ``` hoelzl@40859 ` 1016` ``` also have "(\i. A i) = space M" ``` hoelzl@40859 ` 1017` ``` proof safe ``` hoelzl@40859 ` 1018` ``` fix x assume x: "x \ space M" ``` hoelzl@40859 ` 1019` ``` show "x \ (\i. A i)" ``` hoelzl@40859 ` 1020` ``` proof (cases "f x") ``` hoelzl@41981 ` 1021` ``` case PInf with x show ?thesis unfolding A_def by (auto intro: exI[of _ 0]) ``` hoelzl@40859 ` 1022` ``` next ``` hoelzl@41981 ` 1023` ``` case (real r) ``` hoelzl@43923 ` 1024` ``` with less_PInf_Ex_of_nat[of "f x"] obtain n :: nat where "f x < n" by (auto simp: real_eq_of_nat) ``` hoelzl@45769 ` 1025` ``` then show ?thesis using x real unfolding A_def by (auto intro!: exI[of _ "Suc n"] simp: real_eq_of_nat) ``` hoelzl@41981 ` 1026` ``` next ``` hoelzl@41981 ` 1027` ``` case MInf with x show ?thesis ``` hoelzl@41981 ` 1028` ``` unfolding A_def by (auto intro!: exI[of _ "Suc 0"]) ``` hoelzl@40859 ` 1029` ``` qed ``` hoelzl@40859 ` 1030` ``` qed (auto simp: A_def) ``` hoelzl@41689 ` 1031` ``` finally show "(\i. ?A i) = space ?N" by simp ``` hoelzl@40859 ` 1032` ``` next ``` hoelzl@40859 ` 1033` ``` fix n obtain i j where ``` hoelzl@40859 ` 1034` ``` [simp]: "prod_decode n = (i, j)" by (cases "prod_decode n") auto ``` wenzelm@53015 ` 1035` ``` have "(\\<^sup>+x. f x * indicator (A i \ Q j) x \M) \ \" ``` hoelzl@40859 ` 1036` ``` proof (cases i) ``` hoelzl@40859 ` 1037` ``` case 0 ``` hoelzl@47694 ` 1038` ``` have "AE x in M. f x * indicator (A i \ Q j) x = 0" ``` hoelzl@41705 ` 1039` ``` using AE by (auto simp: A_def `i = 0`) ``` hoelzl@41705 ` 1040` ``` from positive_integral_cong_AE[OF this] show ?thesis by simp ``` hoelzl@40859 ` 1041` ``` next ``` hoelzl@40859 ` 1042` ``` case (Suc n) ``` wenzelm@53015 ` 1043` ``` then have "(\\<^sup>+x. f x * indicator (A i \ Q j) x \M) \ ``` wenzelm@53015 ` 1044` ``` (\\<^sup>+x. (Suc n :: ereal) * indicator (Q j) x \M)" ``` hoelzl@45769 ` 1045` ``` by (auto intro!: positive_integral_mono simp: indicator_def A_def real_eq_of_nat) ``` hoelzl@47694 ` 1046` ``` also have "\ = Suc n * emeasure M (Q j)" ``` hoelzl@40859 ` 1047` ``` using Q by (auto intro!: positive_integral_cmult_indicator) ``` hoelzl@41981 ` 1048` ``` also have "\ < \" ``` hoelzl@41981 ` 1049` ``` using Q by (auto simp: real_eq_of_nat[symmetric]) ``` hoelzl@40859 ` 1050` ``` finally show ?thesis by simp ``` hoelzl@40859 ` 1051` ``` qed ``` hoelzl@47694 ` 1052` ``` then show "emeasure ?N (?A n) \ \" ``` hoelzl@47694 ` 1053` ``` using A_in_sets Q f by (auto simp: emeasure_density) ``` hoelzl@40859 ` 1054` ``` qed ``` hoelzl@40859 ` 1055` ```qed ``` hoelzl@40859 ` 1056` hoelzl@49778 ` 1057` ```lemma (in sigma_finite_measure) sigma_finite_iff_density_finite: ``` hoelzl@49778 ` 1058` ``` "f \ borel_measurable M \ sigma_finite_measure (density M f) \ (AE x in M. f x \ \)" ``` hoelzl@49778 ` 1059` ``` apply (subst density_max_0) ``` hoelzl@49778 ` 1060` ``` apply (subst sigma_finite_iff_density_finite') ``` hoelzl@49778 ` 1061` ``` apply (auto simp: max_def intro!: measurable_If) ``` hoelzl@49778 ` 1062` ``` done ``` hoelzl@49778 ` 1063` hoelzl@40871 ` 1064` ```section "Radon-Nikodym derivative" ``` hoelzl@38656 ` 1065` hoelzl@41689 ` 1066` ```definition ``` hoelzl@47694 ` 1067` ``` "RN_deriv M N \ SOME f. f \ borel_measurable M \ (\x. 0 \ f x) \ density M f = N" ``` hoelzl@38656 ` 1068` hoelzl@47694 ` 1069` ```lemma ``` hoelzl@47694 ` 1070` ``` assumes f: "f \ borel_measurable M" "AE x in M. 0 \ f x" ``` hoelzl@47694 ` 1071` ``` shows borel_measurable_RN_deriv_density: "RN_deriv M (density M f) \ borel_measurable M" (is ?borel) ``` hoelzl@47694 ` 1072` ``` and density_RN_deriv_density: "density M (RN_deriv M (density M f)) = density M f" (is ?density) ``` hoelzl@47694 ` 1073` ``` and RN_deriv_density_nonneg: "0 \ RN_deriv M (density M f) x" (is ?pos) ``` hoelzl@40859 ` 1074` ```proof - ``` hoelzl@47694 ` 1075` ``` let ?f = "\x. max 0 (f x)" ``` hoelzl@47694 ` 1076` ``` let ?P = "\g. g \ borel_measurable M \ (\x. 0 \ g x) \ density M g = density M f" ``` hoelzl@47694 ` 1077` ``` from f have "?P ?f" using f by (auto intro!: density_cong simp: split: split_max) ``` hoelzl@47694 ` 1078` ``` then have "?P (RN_deriv M (density M f))" ``` hoelzl@47694 ` 1079` ``` unfolding RN_deriv_def by (rule someI[where P="?P"]) ``` hoelzl@47694 ` 1080` ``` then show ?borel ?density ?pos by auto ``` hoelzl@40859 ` 1081` ```qed ``` hoelzl@40859 ` 1082` hoelzl@38656 ` 1083` ```lemma (in sigma_finite_measure) RN_deriv: ``` hoelzl@47694 ` 1084` ``` assumes "absolutely_continuous M N" "sets N = sets M" ``` hoelzl@50003 ` 1085` ``` shows borel_measurable_RN_deriv[measurable]: "RN_deriv M N \ borel_measurable M" (is ?borel) ``` hoelzl@47694 ` 1086` ``` and density_RN_deriv: "density M (RN_deriv M N) = N" (is ?density) ``` hoelzl@47694 ` 1087` ``` and RN_deriv_nonneg: "0 \ RN_deriv M N x" (is ?pos) ``` hoelzl@38656 ` 1088` ```proof - ``` hoelzl@38656 ` 1089` ``` note Ex = Radon_Nikodym[OF assms, unfolded Bex_def] ``` hoelzl@47694 ` 1090` ``` from Ex show ?borel unfolding RN_deriv_def by (rule someI2_ex) simp ``` hoelzl@47694 ` 1091` ``` from Ex show ?density unfolding RN_deriv_def by (rule someI2_ex) simp ``` hoelzl@47694 ` 1092` ``` from Ex show ?pos unfolding RN_deriv_def by (rule someI2_ex) simp ``` hoelzl@38656 ` 1093` ```qed ``` hoelzl@38656 ` 1094` hoelzl@40859 ` 1095` ```lemma (in sigma_finite_measure) RN_deriv_positive_integral: ``` hoelzl@47694 ` 1096` ``` assumes N: "absolutely_continuous M N" "sets N = sets M" ``` hoelzl@40859 ` 1097` ``` and f: "f \ borel_measurable M" ``` wenzelm@53015 ` 1098` ``` shows "integral\<^sup>P N f = (\\<^sup>+x. RN_deriv M N x * f x \M)" ``` hoelzl@40859 ` 1099` ```proof - ``` wenzelm@53015 ` 1100` ``` have "integral\<^sup>P N f = integral\<^sup>P (density M (RN_deriv M N)) f" ``` hoelzl@47694 ` 1101` ``` using N by (simp add: density_RN_deriv) ``` wenzelm@53015 ` 1102` ``` also have "\ = (\\<^sup>+x. RN_deriv M N x * f x \M)" ``` hoelzl@47694 ` 1103` ``` using RN_deriv(1,3)[OF N] f by (simp add: positive_integral_density) ``` hoelzl@47694 ` 1104` ``` finally show ?thesis by simp ``` hoelzl@40859 ` 1105` ```qed ``` hoelzl@40859 ` 1106` hoelzl@47694 ` 1107` ```lemma null_setsD_AE: "N \ null_sets M \ AE x in M. x \ N" ``` hoelzl@47694 ` 1108` ``` using AE_iff_null_sets[of N M] by auto ``` hoelzl@47694 ` 1109` hoelzl@47694 ` 1110` ```lemma (in sigma_finite_measure) RN_deriv_unique: ``` hoelzl@47694 ` 1111` ``` assumes f: "f \ borel_measurable M" "AE x in M. 0 \ f x" ``` hoelzl@47694 ` 1112` ``` and eq: "density M f = N" ``` hoelzl@47694 ` 1113` ``` shows "AE x in M. f x = RN_deriv M N x" ``` hoelzl@49785 ` 1114` ``` unfolding eq[symmetric] ``` hoelzl@49785 ` 1115` ``` by (intro density_unique_iff[THEN iffD1] f borel_measurable_RN_deriv_density ``` hoelzl@49785 ` 1116` ``` RN_deriv_density_nonneg[THEN AE_I2] density_RN_deriv_density[symmetric]) ``` hoelzl@49785 ` 1117` hoelzl@49785 ` 1118` ```lemma RN_deriv_unique_sigma_finite: ``` hoelzl@49785 ` 1119` ``` assumes f: "f \ borel_measurable M" "AE x in M. 0 \ f x" ``` hoelzl@49785 ` 1120` ``` and eq: "density M f = N" and fin: "sigma_finite_measure N" ``` hoelzl@49785 ` 1121` ``` shows "AE x in M. f x = RN_deriv M N x" ``` hoelzl@49785 ` 1122` ``` using fin unfolding eq[symmetric] ``` hoelzl@49785 ` 1123` ``` by (intro sigma_finite_density_unique[THEN iffD1] f borel_measurable_RN_deriv_density ``` hoelzl@49785 ` 1124` ``` RN_deriv_density_nonneg[THEN AE_I2] density_RN_deriv_density[symmetric]) ``` hoelzl@47694 ` 1125` hoelzl@47694 ` 1126` ```lemma (in sigma_finite_measure) RN_deriv_distr: ``` hoelzl@47694 ` 1127` ``` fixes T :: "'a \ 'b" ``` hoelzl@47694 ` 1128` ``` assumes T: "T \ measurable M M'" and T': "T' \ measurable M' M" ``` hoelzl@47694 ` 1129` ``` and inv: "\x\space M. T' (T x) = x" ``` hoelzl@50021 ` 1130` ``` and ac[simp]: "absolutely_continuous (distr M M' T) (distr N M' T)" ``` hoelzl@47694 ` 1131` ``` and N: "sets N = sets M" ``` hoelzl@47694 ` 1132` ``` shows "AE x in M. RN_deriv (distr M M' T) (distr N M' T) (T x) = RN_deriv M N x" ``` hoelzl@41832 ` 1133` ```proof (rule RN_deriv_unique) ``` hoelzl@47694 ` 1134` ``` have [simp]: "sets N = sets M" by fact ``` hoelzl@47694 ` 1135` ``` note sets_eq_imp_space_eq[OF N, simp] ``` hoelzl@47694 ` 1136` ``` have measurable_N[simp]: "\M'. measurable N M' = measurable M M'" by (auto simp: measurable_def) ``` hoelzl@47694 ` 1137` ``` { fix A assume "A \ sets M" ``` immler@50244 ` 1138` ``` with inv T T' sets.sets_into_space[OF this] ``` hoelzl@47694 ` 1139` ``` have "T -` T' -` A \ T -` space M' \ space M = A" ``` hoelzl@47694 ` 1140` ``` by (auto simp: measurable_def) } ``` hoelzl@47694 ` 1141` ``` note eq = this[simp] ``` hoelzl@47694 ` 1142` ``` { fix A assume "A \ sets M" ``` immler@50244 ` 1143` ``` with inv T T' sets.sets_into_space[OF this] ``` hoelzl@47694 ` 1144` ``` have "(T' \ T) -` A \ space M = A" ``` hoelzl@47694 ` 1145` ``` by (auto simp: measurable_def) } ``` hoelzl@47694 ` 1146` ``` note eq2 = this[simp] ``` hoelzl@47694 ` 1147` ``` let ?M' = "distr M M' T" and ?N' = "distr N M' T" ``` hoelzl@47694 ` 1148` ``` interpret M': sigma_finite_measure ?M' ``` hoelzl@41832 ` 1149` ``` proof ``` hoelzl@41832 ` 1150` ``` from sigma_finite guess F .. note F = this ``` hoelzl@47694 ` 1151` ``` show "\A::nat \ 'b set. range A \ sets ?M' \ (\i. A i) = space ?M' \ (\i. emeasure ?M' (A i) \ \)" ``` hoelzl@41832 ` 1152` ``` proof (intro exI conjI allI) ``` hoelzl@47694 ` 1153` ``` show *: "range (\i. T' -` F i \ space ?M') \ sets ?M'" ``` hoelzl@47694 ` 1154` ``` using F T' by (auto simp: measurable_def) ``` hoelzl@47694 ` 1155` ``` show "(\i. T' -` F i \ space ?M') = space ?M'" ``` hoelzl@47694 ` 1156` ``` using F T' by (force simp: measurable_def) ``` hoelzl@41832 ` 1157` ``` fix i ``` hoelzl@41832 ` 1158` ``` have "T' -` F i \ space M' \ sets M'" using * by auto ``` hoelzl@41832 ` 1159` ``` moreover ``` hoelzl@41832 ` 1160` ``` have Fi: "F i \ sets M" using F by auto ``` hoelzl@47694 ` 1161` ``` ultimately show "emeasure ?M' (T' -` F i \ space ?M') \ \" ``` hoelzl@47694 ` 1162` ``` using F T T' by (simp add: emeasure_distr) ``` hoelzl@41832 ` 1163` ``` qed ``` hoelzl@41832 ` 1164` ``` qed ``` hoelzl@47694 ` 1165` ``` have "(RN_deriv ?M' ?N') \ T \ borel_measurable M" ``` hoelzl@50021 ` 1166` ``` using T ac by measurable ``` hoelzl@47694 ` 1167` ``` then show "(\x. RN_deriv ?M' ?N' (T x)) \ borel_measurable M" ``` hoelzl@41832 ` 1168` ``` by (simp add: comp_def) ``` hoelzl@47694 ` 1169` ``` show "AE x in M. 0 \ RN_deriv ?M' ?N' (T x)" using M'.RN_deriv_nonneg[OF ac] by auto ``` hoelzl@47694 ` 1170` hoelzl@47694 ` 1171` ``` have "N = distr N M (T' \ T)" ``` hoelzl@47694 ` 1172` ``` by (subst measure_of_of_measure[of N, symmetric]) ``` immler@50244 ` 1173` ``` (auto simp add: distr_def sets.sigma_sets_eq intro!: measure_of_eq sets.space_closed) ``` hoelzl@47694 ` 1174` ``` also have "\ = distr (distr N M' T) M T'" ``` hoelzl@47694 ` 1175` ``` using T T' by (simp add: distr_distr) ``` hoelzl@47694 ` 1176` ``` also have "\ = distr (density (distr M M' T) (RN_deriv (distr M M' T) (distr N M' T))) M T'" ``` hoelzl@47694 ` 1177` ``` using ac by (simp add: M'.density_RN_deriv) ``` hoelzl@47694 ` 1178` ``` also have "\ = density M (RN_deriv (distr M M' T) (distr N M' T) \ T)" ``` hoelzl@47694 ` 1179` ``` using M'.borel_measurable_RN_deriv[OF ac] by (simp add: distr_density_distr[OF T T', OF inv]) ``` hoelzl@47694 ` 1180` ``` finally show "density M (\x. RN_deriv (distr M M' T) (distr N M' T) (T x)) = N" ``` hoelzl@47694 ` 1181` ``` by (simp add: comp_def) ``` hoelzl@41832 ` 1182` ```qed ``` hoelzl@41832 ` 1183` hoelzl@40859 ` 1184` ```lemma (in sigma_finite_measure) RN_deriv_finite: ``` hoelzl@47694 ` 1185` ``` assumes N: "sigma_finite_measure N" and ac: "absolutely_continuous M N" "sets N = sets M" ``` hoelzl@47694 ` 1186` ``` shows "AE x in M. RN_deriv M N x \ \" ``` hoelzl@40859 ` 1187` ```proof - ``` hoelzl@47694 ` 1188` ``` interpret N: sigma_finite_measure N by fact ``` hoelzl@47694 ` 1189` ``` from N show ?thesis ``` hoelzl@47694 ` 1190` ``` using sigma_finite_iff_density_finite[OF RN_deriv(1)[OF ac]] RN_deriv(2,3)[OF ac] by simp ``` hoelzl@40859 ` 1191` ```qed ``` hoelzl@40859 ` 1192` hoelzl@40859 ` 1193` ```lemma (in sigma_finite_measure) ``` hoelzl@47694 ` 1194` ``` assumes N: "sigma_finite_measure N" and ac: "absolutely_continuous M N" "sets N = sets M" ``` hoelzl@40859 ` 1195` ``` and f: "f \ borel_measurable M" ``` hoelzl@47694 ` 1196` ``` shows RN_deriv_integrable: "integrable N f \ ``` hoelzl@47694 ` 1197` ``` integrable M (\x. real (RN_deriv M N x) * f x)" (is ?integrable) ``` wenzelm@53015 ` 1198` ``` and RN_deriv_integral: "integral\<^sup>L N f = ``` hoelzl@47694 ` 1199` ``` (\x. real (RN_deriv M N x) * f x \M)" (is ?integral) ``` hoelzl@40859 ` 1200` ```proof - ``` hoelzl@47694 ` 1201` ``` note ac(2)[simp] and sets_eq_imp_space_eq[OF ac(2), simp] ``` hoelzl@47694 ` 1202` ``` interpret N: sigma_finite_measure N by fact ``` hoelzl@43920 ` 1203` ``` have minus_cong: "\A B A' B'::ereal. A = A' \ B = B' \ real A - real B = real A' - real B'" by simp ``` hoelzl@40859 ` 1204` ``` have f': "(\x. - f x) \ borel_measurable M" using f by auto ``` hoelzl@47694 ` 1205` ``` have Nf: "f \ borel_measurable N" using f by (simp add: measurable_def) ``` hoelzl@41689 ` 1206` ``` { fix f :: "'a \ real" ``` hoelzl@47694 ` 1207` ``` { fix x assume *: "RN_deriv M N x \ \" ``` hoelzl@47694 ` 1208` ``` have "ereal (real (RN_deriv M N x)) * ereal (f x) = ereal (real (RN_deriv M N x) * f x)" ``` hoelzl@40859 ` 1209` ``` by (simp add: mult_le_0_iff) ``` hoelzl@47694 ` 1210` ``` then have "RN_deriv M N x * ereal (f x) = ereal (real (RN_deriv M N x) * f x)" ``` hoelzl@47694 ` 1211` ``` using RN_deriv(3)[OF ac] * by (auto simp add: ereal_real split: split_if_asm) } ``` wenzelm@53015 ` 1212` ``` then have "(\\<^sup>+x. ereal (real (RN_deriv M N x) * f x) \M) = (\\<^sup>+x. RN_deriv M N x * ereal (f x) \M)" ``` wenzelm@53015 ` 1213` ``` "(\\<^sup>+x. ereal (- (real (RN_deriv M N x) * f x)) \M) = (\\<^sup>+x. RN_deriv M N x * ereal (- f x) \M)" ``` hoelzl@47694 ` 1214` ``` using RN_deriv_finite[OF N ac] unfolding ereal_mult_minus_right uminus_ereal.simps(1)[symmetric] ``` hoelzl@41981 ` 1215` ``` by (auto intro!: positive_integral_cong_AE) } ``` hoelzl@41981 ` 1216` ``` note * = this ``` hoelzl@40859 ` 1217` ``` show ?integral ?integrable ``` hoelzl@41981 ` 1218` ``` unfolding lebesgue_integral_def integrable_def * ``` hoelzl@47694 ` 1219` ``` using Nf f RN_deriv(1)[OF ac] ``` hoelzl@47694 ` 1220` ``` by (auto simp: RN_deriv_positive_integral[OF ac]) ``` hoelzl@40859 ` 1221` ```qed ``` hoelzl@40859 ` 1222` hoelzl@43340 ` 1223` ```lemma (in sigma_finite_measure) real_RN_deriv: ``` hoelzl@47694 ` 1224` ``` assumes "finite_measure N" ``` hoelzl@47694 ` 1225` ``` assumes ac: "absolutely_continuous M N" "sets N = sets M" ``` hoelzl@43340 ` 1226` ``` obtains D where "D \ borel_measurable M" ``` hoelzl@47694 ` 1227` ``` and "AE x in M. RN_deriv M N x = ereal (D x)" ``` hoelzl@47694 ` 1228` ``` and "AE x in N. 0 < D x" ``` hoelzl@43340 ` 1229` ``` and "\x. 0 \ D x" ``` hoelzl@43340 ` 1230` ```proof ``` hoelzl@47694 ` 1231` ``` interpret N: finite_measure N by fact ``` hoelzl@47694 ` 1232` ``` ``` hoelzl@47694 ` 1233` ``` note RN = RN_deriv[OF ac] ``` hoelzl@43340 ` 1234` hoelzl@47694 ` 1235` ``` let ?RN = "\t. {x \ space M. RN_deriv M N x = t}" ``` hoelzl@43340 ` 1236` hoelzl@47694 ` 1237` ``` show "(\x. real (RN_deriv M N x)) \ borel_measurable M" ``` hoelzl@43340 ` 1238` ``` using RN by auto ``` hoelzl@43340 ` 1239` wenzelm@53015 ` 1240` ``` have "N (?RN \) = (\\<^sup>+ x. RN_deriv M N x * indicator (?RN \) x \M)" ``` hoelzl@47694 ` 1241` ``` using RN(1,3) by (subst RN(2)[symmetric]) (auto simp: emeasure_density) ``` wenzelm@53015 ` 1242` ``` also have "\ = (\\<^sup>+ x. \ * indicator (?RN \) x \M)" ``` hoelzl@43340 ` 1243` ``` by (intro positive_integral_cong) (auto simp: indicator_def) ``` hoelzl@47694 ` 1244` ``` also have "\ = \ * emeasure M (?RN \)" ``` hoelzl@43340 ` 1245` ``` using RN by (intro positive_integral_cmult_indicator) auto ``` hoelzl@47694 ` 1246` ``` finally have eq: "N (?RN \) = \ * emeasure M (?RN \)" . ``` hoelzl@43340 ` 1247` ``` moreover ``` hoelzl@47694 ` 1248` ``` have "emeasure M (?RN \) = 0" ``` hoelzl@43340 ` 1249` ``` proof (rule ccontr) ``` hoelzl@47694 ` 1250` ``` assume "emeasure M {x \ space M. RN_deriv M N x = \} \ 0" ``` hoelzl@47694 ` 1251` ``` moreover from RN have "0 \ emeasure M {x \ space M. RN_deriv M N x = \}" by auto ``` hoelzl@47694 ` 1252` ``` ultimately have "0 < emeasure M {x \ space M. RN_deriv M N x = \}" by auto ``` hoelzl@47694 ` 1253` ``` with eq have "N (?RN \) = \" by simp ``` hoelzl@47694 ` 1254` ``` with N.emeasure_finite[of "?RN \"] RN show False by auto ``` hoelzl@43340 ` 1255` ``` qed ``` hoelzl@47694 ` 1256` ``` ultimately have "AE x in M. RN_deriv M N x < \" ``` hoelzl@43340 ` 1257` ``` using RN by (intro AE_iff_measurable[THEN iffD2]) auto ``` hoelzl@47694 ` 1258` ``` then show "AE x in M. RN_deriv M N x = ereal (real (RN_deriv M N x))" ``` hoelzl@43920 ` 1259` ``` using RN(3) by (auto simp: ereal_real) ``` hoelzl@47694 ` 1260` ``` then have eq: "AE x in N. RN_deriv M N x = ereal (real (RN_deriv M N x))" ``` hoelzl@47694 ` 1261` ``` using ac absolutely_continuous_AE by auto ``` hoelzl@43340 ` 1262` hoelzl@47694 ` 1263` ``` show "\x. 0 \ real (RN_deriv M N x)" ``` hoelzl@43920 ` 1264` ``` using RN by (auto intro: real_of_ereal_pos) ``` hoelzl@43340 ` 1265` wenzelm@53015 ` 1266` ``` have "N (?RN 0) = (\\<^sup>+ x. RN_deriv M N x * indicator (?RN 0) x \M)" ``` hoelzl@47694 ` 1267` ``` using RN(1,3) by (subst RN(2)[symmetric]) (auto simp: emeasure_density) ``` wenzelm@53015 ` 1268` ``` also have "\ = (\\<^sup>+ x. 0 \M)" ``` hoelzl@43340 ` 1269` ``` by (intro positive_integral_cong) (auto simp: indicator_def) ``` hoelzl@47694 ` 1270` ``` finally have "AE x in N. RN_deriv M N x \ 0" ``` hoelzl@47694 ` 1271` ``` using RN by (subst AE_iff_measurable[OF _ refl]) (auto simp: ac cong: sets_eq_imp_space_eq) ``` hoelzl@47694 ` 1272` ``` with RN(3) eq show "AE x in N. 0 < real (RN_deriv M N x)" ``` hoelzl@43920 ` 1273` ``` by (auto simp: zero_less_real_of_ereal le_less) ``` hoelzl@43340 ` 1274` ```qed ``` hoelzl@43340 ` 1275` hoelzl@38656 ` 1276` ```lemma (in sigma_finite_measure) RN_deriv_singleton: ``` hoelzl@47694 ` 1277` ``` assumes ac: "absolutely_continuous M N" "sets N = sets M" ``` hoelzl@47694 ` 1278` ``` and x: "{x} \ sets M" ``` hoelzl@47694 ` 1279` ``` shows "N {x} = RN_deriv M N x * emeasure M {x}" ``` hoelzl@38656 ` 1280` ```proof - ``` hoelzl@47694 ` 1281` ``` note deriv = RN_deriv[OF ac] ``` hoelzl@47694 ` 1282` ``` from deriv(1,3) `{x} \ sets M` ``` wenzelm@53015 ` 1283` ``` have "density M (RN_deriv M N) {x} = (\\<^sup>+w. RN_deriv M N x * indicator {x} w \M)" ``` hoelzl@47694 ` 1284` ``` by (auto simp: indicator_def emeasure_density intro!: positive_integral_cong) ``` hoelzl@47694 ` 1285` ``` with x deriv show ?thesis ``` hoelzl@47694 ` 1286` ``` by (auto simp: positive_integral_cmult_indicator) ``` hoelzl@38656 ` 1287` ```qed ``` hoelzl@38656 ` 1288` hoelzl@38656 ` 1289` ```end ```