hoelzl@38656 ` 1` ```theory Radon_Nikodym ``` hoelzl@38656 ` 2` ```imports Lebesgue_Integration ``` hoelzl@38656 ` 3` ```begin ``` hoelzl@38656 ` 4` hoelzl@38656 ` 5` ```lemma (in sigma_finite_measure) Ex_finite_integrable_function: ``` hoelzl@38656 ` 6` ``` shows "\h\borel_measurable M. positive_integral h \ \ \ (\x\space M. 0 < h x \ h x < \)" ``` hoelzl@38656 ` 7` ```proof - ``` hoelzl@38656 ` 8` ``` obtain A :: "nat \ 'a set" where ``` hoelzl@38656 ` 9` ``` range: "range A \ sets M" and ``` hoelzl@38656 ` 10` ``` space: "(\i. A i) = space M" and ``` hoelzl@38656 ` 11` ``` measure: "\i. \ (A i) \ \" and ``` hoelzl@38656 ` 12` ``` disjoint: "disjoint_family A" ``` hoelzl@38656 ` 13` ``` using disjoint_sigma_finite by auto ``` hoelzl@38656 ` 14` ``` let "?B i" = "2^Suc i * \ (A i)" ``` hoelzl@38656 ` 15` ``` have "\i. \x. 0 < x \ x < inverse (?B i)" ``` hoelzl@38656 ` 16` ``` proof ``` hoelzl@38656 ` 17` ``` fix i show "\x. 0 < x \ x < inverse (?B i)" ``` hoelzl@38656 ` 18` ``` proof cases ``` hoelzl@38656 ` 19` ``` assume "\ (A i) = 0" ``` hoelzl@38656 ` 20` ``` then show ?thesis by (auto intro!: exI[of _ 1]) ``` hoelzl@38656 ` 21` ``` next ``` hoelzl@38656 ` 22` ``` assume not_0: "\ (A i) \ 0" ``` hoelzl@38656 ` 23` ``` then have "?B i \ \" using measure[of i] by auto ``` hoelzl@38656 ` 24` ``` then have "inverse (?B i) \ 0" unfolding pinfreal_inverse_eq_0 by simp ``` hoelzl@38656 ` 25` ``` then show ?thesis using measure[of i] not_0 ``` hoelzl@38656 ` 26` ``` by (auto intro!: exI[of _ "inverse (?B i) / 2"] ``` hoelzl@38656 ` 27` ``` simp: pinfreal_noteq_omega_Ex zero_le_mult_iff zero_less_mult_iff mult_le_0_iff power_le_zero_eq) ``` hoelzl@38656 ` 28` ``` qed ``` hoelzl@38656 ` 29` ``` qed ``` hoelzl@38656 ` 30` ``` from choice[OF this] obtain n where n: "\i. 0 < n i" ``` hoelzl@38656 ` 31` ``` "\i. n i < inverse (2^Suc i * \ (A i))" by auto ``` hoelzl@38656 ` 32` ``` let "?h x" = "\\<^isub>\ i. n i * indicator (A i) x" ``` hoelzl@38656 ` 33` ``` show ?thesis ``` hoelzl@38656 ` 34` ``` proof (safe intro!: bexI[of _ ?h] del: notI) ``` hoelzl@39092 ` 35` ``` have "\i. A i \ sets M" ``` hoelzl@39092 ` 36` ``` using range by fastsimp+ ``` hoelzl@39092 ` 37` ``` then have "positive_integral ?h = (\\<^isub>\ i. n i * \ (A i))" ``` hoelzl@39092 ` 38` ``` by (simp add: positive_integral_psuminf positive_integral_cmult_indicator) ``` hoelzl@38656 ` 39` ``` also have "\ \ (\\<^isub>\ i. Real ((1 / 2)^Suc i))" ``` hoelzl@38656 ` 40` ``` proof (rule psuminf_le) ``` hoelzl@38656 ` 41` ``` fix N show "n N * \ (A N) \ Real ((1 / 2) ^ Suc N)" ``` hoelzl@38656 ` 42` ``` using measure[of N] n[of N] ``` hoelzl@39092 ` 43` ``` by (cases "n N") ``` hoelzl@39092 ` 44` ``` (auto simp: pinfreal_noteq_omega_Ex field_simps zero_le_mult_iff ``` hoelzl@39092 ` 45` ``` mult_le_0_iff mult_less_0_iff power_less_zero_eq ``` hoelzl@39092 ` 46` ``` power_le_zero_eq inverse_eq_divide less_divide_eq ``` hoelzl@39092 ` 47` ``` power_divide split: split_if_asm) ``` hoelzl@38656 ` 48` ``` qed ``` hoelzl@38656 ` 49` ``` also have "\ = Real 1" ``` hoelzl@38656 ` 50` ``` by (rule suminf_imp_psuminf, rule power_half_series, auto) ``` hoelzl@38656 ` 51` ``` finally show "positive_integral ?h \ \" by auto ``` hoelzl@38656 ` 52` ``` next ``` hoelzl@38656 ` 53` ``` fix x assume "x \ space M" ``` hoelzl@38656 ` 54` ``` then obtain i where "x \ A i" using space[symmetric] by auto ``` hoelzl@38656 ` 55` ``` from psuminf_cmult_indicator[OF disjoint, OF this] ``` hoelzl@38656 ` 56` ``` have "?h x = n i" by simp ``` hoelzl@38656 ` 57` ``` then show "0 < ?h x" and "?h x < \" using n[of i] by auto ``` hoelzl@38656 ` 58` ``` next ``` hoelzl@38656 ` 59` ``` show "?h \ borel_measurable M" using range ``` hoelzl@39092 ` 60` ``` by (auto intro!: borel_measurable_psuminf borel_measurable_pinfreal_times) ``` hoelzl@38656 ` 61` ``` qed ``` hoelzl@38656 ` 62` ```qed ``` hoelzl@38656 ` 63` hoelzl@38656 ` 64` ```definition (in measure_space) ``` hoelzl@38656 ` 65` ``` "absolutely_continuous \ = (\N\null_sets. \ N = (0 :: pinfreal))" ``` hoelzl@38656 ` 66` hoelzl@39097 ` 67` ```lemma (in finite_measure_space) absolutely_continuousI: ``` hoelzl@39097 ` 68` ``` assumes "finite_measure_space M \" ``` hoelzl@39097 ` 69` ``` assumes v: "\x. \ x \ space M ; \ {x} = 0 \ \ \ {x} = 0" ``` hoelzl@39097 ` 70` ``` shows "absolutely_continuous \" ``` hoelzl@39097 ` 71` ```proof (unfold absolutely_continuous_def sets_eq_Pow, safe) ``` hoelzl@39097 ` 72` ``` fix N assume "\ N = 0" "N \ space M" ``` hoelzl@39097 ` 73` ``` interpret v: finite_measure_space M \ by fact ``` hoelzl@39097 ` 74` ``` have "\ N = \ (\x\N. {x})" by simp ``` hoelzl@39097 ` 75` ``` also have "\ = (\x\N. \ {x})" ``` hoelzl@39097 ` 76` ``` proof (rule v.measure_finitely_additive''[symmetric]) ``` hoelzl@39097 ` 77` ``` show "finite N" using `N \ space M` finite_space by (auto intro: finite_subset) ``` hoelzl@39097 ` 78` ``` show "disjoint_family_on (\i. {i}) N" unfolding disjoint_family_on_def by auto ``` hoelzl@39097 ` 79` ``` fix x assume "x \ N" thus "{x} \ sets M" using `N \ space M` sets_eq_Pow by auto ``` hoelzl@39097 ` 80` ``` qed ``` hoelzl@39097 ` 81` ``` also have "\ = 0" ``` hoelzl@39097 ` 82` ``` proof (safe intro!: setsum_0') ``` hoelzl@39097 ` 83` ``` fix x assume "x \ N" ``` hoelzl@39097 ` 84` ``` hence "\ {x} \ \ N" using sets_eq_Pow `N \ space M` by (auto intro!: measure_mono) ``` hoelzl@39097 ` 85` ``` hence "\ {x} = 0" using `\ N = 0` by simp ``` hoelzl@39097 ` 86` ``` thus "\ {x} = 0" using v[of x] `x \ N` `N \ space M` by auto ``` hoelzl@39097 ` 87` ``` qed ``` hoelzl@39097 ` 88` ``` finally show "\ N = 0" . ``` hoelzl@39097 ` 89` ```qed ``` hoelzl@39097 ` 90` hoelzl@38656 ` 91` ```lemma (in finite_measure) Radon_Nikodym_aux_epsilon: ``` hoelzl@38656 ` 92` ``` fixes e :: real assumes "0 < e" ``` hoelzl@38656 ` 93` ``` assumes "finite_measure M s" ``` hoelzl@38656 ` 94` ``` shows "\A\sets M. real (\ (space M)) - real (s (space M)) \ ``` hoelzl@38656 ` 95` ``` real (\ A) - real (s A) \ ``` hoelzl@38656 ` 96` ``` (\B\sets M. B \ A \ - e < real (\ B) - real (s B))" ``` hoelzl@38656 ` 97` ```proof - ``` hoelzl@38656 ` 98` ``` let "?d A" = "real (\ A) - real (s A)" ``` hoelzl@38656 ` 99` ``` interpret M': finite_measure M s by fact ``` hoelzl@38656 ` 100` hoelzl@38656 ` 101` ``` let "?A A" = "if (\B\sets M. B \ space M - A \ -e < ?d B) ``` hoelzl@38656 ` 102` ``` then {} ``` hoelzl@38656 ` 103` ``` else (SOME B. B \ sets M \ B \ space M - A \ ?d B \ -e)" ``` hoelzl@38656 ` 104` ``` def A \ "\n. ((\B. B \ ?A B) ^^ n) {}" ``` hoelzl@38656 ` 105` hoelzl@38656 ` 106` ``` have A_simps[simp]: ``` hoelzl@38656 ` 107` ``` "A 0 = {}" ``` hoelzl@38656 ` 108` ``` "\n. A (Suc n) = (A n \ ?A (A n))" unfolding A_def by simp_all ``` hoelzl@38656 ` 109` hoelzl@38656 ` 110` ``` { fix A assume "A \ sets M" ``` hoelzl@38656 ` 111` ``` have "?A A \ sets M" ``` hoelzl@38656 ` 112` ``` by (auto intro!: someI2[of _ _ "\A. A \ sets M"] simp: not_less) } ``` hoelzl@38656 ` 113` ``` note A'_in_sets = this ``` hoelzl@38656 ` 114` hoelzl@38656 ` 115` ``` { fix n have "A n \ sets M" ``` hoelzl@38656 ` 116` ``` proof (induct n) ``` hoelzl@38656 ` 117` ``` case (Suc n) thus "A (Suc n) \ sets M" ``` hoelzl@38656 ` 118` ``` using A'_in_sets[of "A n"] by (auto split: split_if_asm) ``` hoelzl@38656 ` 119` ``` qed (simp add: A_def) } ``` hoelzl@38656 ` 120` ``` note A_in_sets = this ``` hoelzl@38656 ` 121` ``` hence "range A \ sets M" by auto ``` hoelzl@38656 ` 122` hoelzl@38656 ` 123` ``` { fix n B ``` hoelzl@38656 ` 124` ``` assume Ex: "\B. B \ sets M \ B \ space M - A n \ ?d B \ -e" ``` hoelzl@38656 ` 125` ``` hence False: "\ (\B\sets M. B \ space M - A n \ -e < ?d B)" by (auto simp: not_less) ``` hoelzl@38656 ` 126` ``` have "?d (A (Suc n)) \ ?d (A n) - e" unfolding A_simps if_not_P[OF False] ``` hoelzl@38656 ` 127` ``` proof (rule someI2_ex[OF Ex]) ``` hoelzl@38656 ` 128` ``` fix B assume "B \ sets M \ B \ space M - A n \ ?d B \ - e" ``` hoelzl@38656 ` 129` ``` hence "A n \ B = {}" "B \ sets M" and dB: "?d B \ -e" by auto ``` hoelzl@38656 ` 130` ``` hence "?d (A n \ B) = ?d (A n) + ?d B" ``` hoelzl@38656 ` 131` ``` using `A n \ sets M` real_finite_measure_Union M'.real_finite_measure_Union by simp ``` hoelzl@38656 ` 132` ``` also have "\ \ ?d (A n) - e" using dB by simp ``` hoelzl@38656 ` 133` ``` finally show "?d (A n \ B) \ ?d (A n) - e" . ``` hoelzl@38656 ` 134` ``` qed } ``` hoelzl@38656 ` 135` ``` note dA_epsilon = this ``` hoelzl@38656 ` 136` hoelzl@38656 ` 137` ``` { fix n have "?d (A (Suc n)) \ ?d (A n)" ``` hoelzl@38656 ` 138` ``` proof (cases "\B. B\sets M \ B \ space M - A n \ ?d B \ - e") ``` hoelzl@38656 ` 139` ``` case True from dA_epsilon[OF this] show ?thesis using `0 < e` by simp ``` hoelzl@38656 ` 140` ``` next ``` hoelzl@38656 ` 141` ``` case False ``` hoelzl@38656 ` 142` ``` hence "\B\sets M. B \ space M - A n \ -e < ?d B" by (auto simp: not_le) ``` hoelzl@38656 ` 143` ``` thus ?thesis by simp ``` hoelzl@38656 ` 144` ``` qed } ``` hoelzl@38656 ` 145` ``` note dA_mono = this ``` hoelzl@38656 ` 146` hoelzl@38656 ` 147` ``` show ?thesis ``` hoelzl@38656 ` 148` ``` proof (cases "\n. \B\sets M. B \ space M - A n \ -e < ?d B") ``` hoelzl@38656 ` 149` ``` case True then obtain n where B: "\B. \ B \ sets M; B \ space M - A n\ \ -e < ?d B" by blast ``` hoelzl@38656 ` 150` ``` show ?thesis ``` hoelzl@38656 ` 151` ``` proof (safe intro!: bexI[of _ "space M - A n"]) ``` hoelzl@38656 ` 152` ``` fix B assume "B \ sets M" "B \ space M - A n" ``` hoelzl@38656 ` 153` ``` from B[OF this] show "-e < ?d B" . ``` hoelzl@38656 ` 154` ``` next ``` hoelzl@38656 ` 155` ``` show "space M - A n \ sets M" by (rule compl_sets) fact ``` hoelzl@38656 ` 156` ``` next ``` hoelzl@38656 ` 157` ``` show "?d (space M) \ ?d (space M - A n)" ``` hoelzl@38656 ` 158` ``` proof (induct n) ``` hoelzl@38656 ` 159` ``` fix n assume "?d (space M) \ ?d (space M - A n)" ``` hoelzl@38656 ` 160` ``` also have "\ \ ?d (space M - A (Suc n))" ``` hoelzl@38656 ` 161` ``` using A_in_sets sets_into_space dA_mono[of n] ``` hoelzl@38656 ` 162` ``` real_finite_measure_Diff[of "space M"] ``` hoelzl@38656 ` 163` ``` real_finite_measure_Diff[of "space M"] ``` hoelzl@38656 ` 164` ``` M'.real_finite_measure_Diff[of "space M"] ``` hoelzl@38656 ` 165` ``` M'.real_finite_measure_Diff[of "space M"] ``` hoelzl@38656 ` 166` ``` by (simp del: A_simps) ``` hoelzl@38656 ` 167` ``` finally show "?d (space M) \ ?d (space M - A (Suc n))" . ``` hoelzl@38656 ` 168` ``` qed simp ``` hoelzl@38656 ` 169` ``` qed ``` hoelzl@38656 ` 170` ``` next ``` hoelzl@38656 ` 171` ``` case False hence B: "\n. \B. B\sets M \ B \ space M - A n \ ?d B \ - e" ``` hoelzl@38656 ` 172` ``` by (auto simp add: not_less) ``` hoelzl@38656 ` 173` ``` { fix n have "?d (A n) \ - real n * e" ``` hoelzl@38656 ` 174` ``` proof (induct n) ``` hoelzl@38656 ` 175` ``` 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@38656 ` 176` ``` qed simp } note dA_less = this ``` hoelzl@38656 ` 177` ``` have decseq: "decseq (\n. ?d (A n))" unfolding decseq_eq_incseq ``` hoelzl@38656 ` 178` ``` proof (rule incseq_SucI) ``` hoelzl@38656 ` 179` ``` fix n show "- ?d (A n) \ - ?d (A (Suc n))" using dA_mono[of n] by auto ``` hoelzl@38656 ` 180` ``` qed ``` hoelzl@38656 ` 181` ``` from real_finite_continuity_from_below[of A] `range A \ sets M` ``` hoelzl@38656 ` 182` ``` M'.real_finite_continuity_from_below[of A] ``` hoelzl@38656 ` 183` ``` have convergent: "(\i. ?d (A i)) ----> ?d (\i. A i)" ``` hoelzl@38656 ` 184` ``` by (auto intro!: LIMSEQ_diff) ``` hoelzl@38656 ` 185` ``` obtain n :: nat where "- ?d (\i. A i) / e < real n" using reals_Archimedean2 by auto ``` hoelzl@38656 ` 186` ``` moreover from order_trans[OF decseq_le[OF decseq convergent] dA_less] ``` hoelzl@38656 ` 187` ``` have "real n \ - ?d (\i. A i) / e" using `0A\sets M. real (\ (space M)) - real (s (space M)) \ ``` hoelzl@38656 ` 195` ``` real (\ A) - real (s A) \ ``` hoelzl@38656 ` 196` ``` (\B\sets M. B \ A \ 0 \ real (\ B) - real (s B))" ``` hoelzl@38656 ` 197` ```proof - ``` hoelzl@38656 ` 198` ``` let "?d A" = "real (\ A) - real (s A)" ``` hoelzl@38656 ` 199` ``` 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)" ``` hoelzl@38656 ` 200` hoelzl@38656 ` 201` ``` interpret M': finite_measure M s by fact ``` hoelzl@38656 ` 202` hoelzl@39092 ` 203` ``` let "?r S" = "restricted_space S" ``` hoelzl@38656 ` 204` hoelzl@38656 ` 205` ``` { fix S n ``` hoelzl@38656 ` 206` ``` assume S: "S \ sets M" ``` hoelzl@38656 ` 207` ``` hence **: "\X. X \ op \ S ` sets M \ X \ sets M \ X \ S" by auto ``` hoelzl@38656 ` 208` ``` from M'.restricted_finite_measure[of S] restricted_finite_measure[of S] S ``` hoelzl@38656 ` 209` ``` have "finite_measure (?r S) \" "0 < 1 / real (Suc n)" ``` hoelzl@38656 ` 210` ``` "finite_measure (?r S) s" by auto ``` hoelzl@38656 ` 211` ``` from finite_measure.Radon_Nikodym_aux_epsilon[OF this] guess X .. ``` hoelzl@38656 ` 212` ``` hence "?P X S n" ``` hoelzl@38656 ` 213` ``` proof (simp add: **, safe) ``` hoelzl@38656 ` 214` ``` fix C assume C: "C \ sets M" "C \ X" "X \ S" and ``` hoelzl@38656 ` 215` ``` *: "\B\sets M. S \ B \ X \ - (1 / real (Suc n)) < ?d (S \ B)" ``` hoelzl@38656 ` 216` ``` hence "C \ S" "C \ X" "S \ C = C" by auto ``` hoelzl@38656 ` 217` ``` with *[THEN bspec, OF `C \ sets M`] ``` hoelzl@38656 ` 218` ``` show "- (1 / real (Suc n)) < ?d C" by auto ``` hoelzl@38656 ` 219` ``` qed ``` hoelzl@38656 ` 220` ``` hence "\A. ?P A S n" by auto } ``` hoelzl@38656 ` 221` ``` note Ex_P = this ``` hoelzl@38656 ` 222` hoelzl@38656 ` 223` ``` def A \ "nat_rec (space M) (\n A. SOME B. ?P B A n)" ``` hoelzl@38656 ` 224` ``` have A_Suc: "\n. A (Suc n) = (SOME B. ?P B (A n) n)" by (simp add: A_def) ``` hoelzl@38656 ` 225` ``` have A_0[simp]: "A 0 = space M" unfolding A_def by simp ``` hoelzl@38656 ` 226` hoelzl@38656 ` 227` ``` { fix i have "A i \ sets M" unfolding A_def ``` hoelzl@38656 ` 228` ``` proof (induct i) ``` hoelzl@38656 ` 229` ``` case (Suc i) ``` hoelzl@38656 ` 230` ``` from Ex_P[OF this, of i] show ?case unfolding nat_rec_Suc ``` hoelzl@38656 ` 231` ``` by (rule someI2_ex) simp ``` hoelzl@38656 ` 232` ``` qed simp } ``` hoelzl@38656 ` 233` ``` note A_in_sets = this ``` hoelzl@38656 ` 234` hoelzl@38656 ` 235` ``` { fix n have "?P (A (Suc n)) (A n) n" ``` hoelzl@38656 ` 236` ``` using Ex_P[OF A_in_sets] unfolding A_Suc ``` hoelzl@38656 ` 237` ``` by (rule someI2_ex) simp } ``` hoelzl@38656 ` 238` ``` note P_A = this ``` hoelzl@38656 ` 239` hoelzl@38656 ` 240` ``` have "range A \ sets M" using A_in_sets by auto ``` hoelzl@38656 ` 241` hoelzl@38656 ` 242` ``` have A_mono: "\i. A (Suc i) \ A i" using P_A by simp ``` hoelzl@38656 ` 243` ``` have mono_dA: "mono (\i. ?d (A i))" using P_A by (simp add: mono_iff_le_Suc) ``` hoelzl@38656 ` 244` ``` have epsilon: "\C i. \ C \ sets M; C \ A (Suc i) \ \ - 1 / real (Suc i) < ?d C" ``` hoelzl@38656 ` 245` ``` using P_A by auto ``` hoelzl@38656 ` 246` hoelzl@38656 ` 247` ``` show ?thesis ``` hoelzl@38656 ` 248` ``` proof (safe intro!: bexI[of _ "\i. A i"]) ``` hoelzl@38656 ` 249` ``` show "(\i. A i) \ sets M" using A_in_sets by auto ``` hoelzl@38656 ` 250` ``` from `range A \ sets M` A_mono ``` hoelzl@38656 ` 251` ``` real_finite_continuity_from_above[of A] ``` hoelzl@38656 ` 252` ``` M'.real_finite_continuity_from_above[of A] ``` hoelzl@38656 ` 253` ``` have "(\i. ?d (A i)) ----> ?d (\i. A i)" by (auto intro!: LIMSEQ_diff) ``` hoelzl@38656 ` 254` ``` thus "?d (space M) \ ?d (\i. A i)" using mono_dA[THEN monoD, of 0 _] ``` hoelzl@38656 ` 255` ``` by (rule_tac LIMSEQ_le_const) (auto intro!: exI) ``` hoelzl@38656 ` 256` ``` next ``` hoelzl@38656 ` 257` ``` fix B assume B: "B \ sets M" "B \ (\i. A i)" ``` hoelzl@38656 ` 258` ``` show "0 \ ?d B" ``` hoelzl@38656 ` 259` ``` proof (rule ccontr) ``` hoelzl@38656 ` 260` ``` assume "\ 0 \ ?d B" ``` hoelzl@38656 ` 261` ``` hence "0 < - ?d B" by auto ``` hoelzl@38656 ` 262` ``` from ex_inverse_of_nat_Suc_less[OF this] ``` hoelzl@38656 ` 263` ``` obtain n where *: "?d B < - 1 / real (Suc n)" ``` hoelzl@38656 ` 264` ``` by (auto simp: real_eq_of_nat inverse_eq_divide field_simps) ``` hoelzl@38656 ` 265` ``` have "B \ A (Suc n)" using B by (auto simp del: nat_rec_Suc) ``` hoelzl@38656 ` 266` ``` from epsilon[OF B(1) this] * ``` hoelzl@38656 ` 267` ``` show False by auto ``` hoelzl@38656 ` 268` ``` qed ``` hoelzl@38656 ` 269` ``` qed ``` hoelzl@38656 ` 270` ```qed ``` hoelzl@38656 ` 271` hoelzl@38656 ` 272` ```lemma (in finite_measure) Radon_Nikodym_finite_measure: ``` hoelzl@38656 ` 273` ``` assumes "finite_measure M \" ``` hoelzl@38656 ` 274` ``` assumes "absolutely_continuous \" ``` hoelzl@38656 ` 275` ``` shows "\f \ borel_measurable M. \A\sets M. \ A = positive_integral (\x. f x * indicator A x)" ``` hoelzl@38656 ` 276` ```proof - ``` hoelzl@38656 ` 277` ``` interpret M': finite_measure M \ using assms(1) . ``` hoelzl@38656 ` 278` hoelzl@38656 ` 279` ``` def G \ "{g \ borel_measurable M. \A\sets M. positive_integral (\x. g x * indicator A x) \ \ A}" ``` hoelzl@38656 ` 280` ``` have "(\x. 0) \ G" unfolding G_def by auto ``` hoelzl@38656 ` 281` ``` hence "G \ {}" by auto ``` hoelzl@38656 ` 282` hoelzl@38656 ` 283` ``` { fix f g assume f: "f \ G" and g: "g \ G" ``` hoelzl@38656 ` 284` ``` have "(\x. max (g x) (f x)) \ G" (is "?max \ G") unfolding G_def ``` hoelzl@38656 ` 285` ``` proof safe ``` hoelzl@38656 ` 286` ``` show "?max \ borel_measurable M" using f g unfolding G_def by auto ``` hoelzl@38656 ` 287` hoelzl@38656 ` 288` ``` let ?A = "{x \ space M. f x \ g x}" ``` hoelzl@38656 ` 289` ``` have "?A \ sets M" using f g unfolding G_def by auto ``` hoelzl@38656 ` 290` hoelzl@38656 ` 291` ``` fix A assume "A \ sets M" ``` hoelzl@38656 ` 292` ``` hence sets: "?A \ A \ sets M" "(space M - ?A) \ A \ sets M" using `?A \ sets M` by auto ``` hoelzl@38656 ` 293` ``` have union: "((?A \ A) \ ((space M - ?A) \ A)) = A" ``` hoelzl@38656 ` 294` ``` using sets_into_space[OF `A \ sets M`] by auto ``` hoelzl@38656 ` 295` hoelzl@38656 ` 296` ``` have "\x. x \ space M \ max (g x) (f x) * indicator A x = ``` hoelzl@38656 ` 297` ``` g x * indicator (?A \ A) x + f x * indicator ((space M - ?A) \ A) x" ``` hoelzl@38656 ` 298` ``` by (auto simp: indicator_def max_def) ``` hoelzl@38656 ` 299` ``` hence "positive_integral (\x. max (g x) (f x) * indicator A x) = ``` hoelzl@38656 ` 300` ``` positive_integral (\x. g x * indicator (?A \ A) x) + ``` hoelzl@38656 ` 301` ``` positive_integral (\x. f x * indicator ((space M - ?A) \ A) x)" ``` hoelzl@38656 ` 302` ``` using f g sets unfolding G_def ``` hoelzl@38656 ` 303` ``` by (auto cong: positive_integral_cong intro!: positive_integral_add borel_measurable_indicator) ``` hoelzl@38656 ` 304` ``` also have "\ \ \ (?A \ A) + \ ((space M - ?A) \ A)" ``` hoelzl@38656 ` 305` ``` using f g sets unfolding G_def by (auto intro!: add_mono) ``` hoelzl@38656 ` 306` ``` also have "\ = \ A" ``` hoelzl@38656 ` 307` ``` using M'.measure_additive[OF sets] union by auto ``` hoelzl@38656 ` 308` ``` finally show "positive_integral (\x. max (g x) (f x) * indicator A x) \ \ A" . ``` hoelzl@38656 ` 309` ``` qed } ``` hoelzl@38656 ` 310` ``` note max_in_G = this ``` hoelzl@38656 ` 311` hoelzl@38656 ` 312` ``` { fix f g assume "f \ g" and f: "\i. f i \ G" ``` hoelzl@38656 ` 313` ``` have "g \ G" unfolding G_def ``` hoelzl@38656 ` 314` ``` proof safe ``` hoelzl@38656 ` 315` ``` from `f \ g` have [simp]: "g = (SUP i. f i)" unfolding isoton_def by simp ``` hoelzl@38656 ` 316` ``` have f_borel: "\i. f i \ borel_measurable M" using f unfolding G_def by simp ``` hoelzl@38656 ` 317` ``` thus "g \ borel_measurable M" by (auto intro!: borel_measurable_SUP) ``` hoelzl@38656 ` 318` hoelzl@38656 ` 319` ``` fix A assume "A \ sets M" ``` hoelzl@38656 ` 320` ``` hence "\i. (\x. f i x * indicator A x) \ borel_measurable M" ``` hoelzl@38656 ` 321` ``` using f_borel by (auto intro!: borel_measurable_indicator) ``` hoelzl@38656 ` 322` ``` from positive_integral_isoton[OF isoton_indicator[OF `f \ g`] this] ``` hoelzl@38656 ` 323` ``` have SUP: "positive_integral (\x. g x * indicator A x) = ``` hoelzl@38656 ` 324` ``` (SUP i. positive_integral (\x. f i x * indicator A x))" ``` hoelzl@38656 ` 325` ``` unfolding isoton_def by simp ``` hoelzl@38656 ` 326` ``` show "positive_integral (\x. g x * indicator A x) \ \ A" unfolding SUP ``` hoelzl@38656 ` 327` ``` using f `A \ sets M` unfolding G_def by (auto intro!: SUP_leI) ``` hoelzl@38656 ` 328` ``` qed } ``` hoelzl@38656 ` 329` ``` note SUP_in_G = this ``` hoelzl@38656 ` 330` hoelzl@38656 ` 331` ``` let ?y = "SUP g : G. positive_integral g" ``` hoelzl@38656 ` 332` ``` have "?y \ \ (space M)" unfolding G_def ``` hoelzl@38656 ` 333` ``` proof (safe intro!: SUP_leI) ``` hoelzl@38656 ` 334` ``` fix g assume "\A\sets M. positive_integral (\x. g x * indicator A x) \ \ A" ``` hoelzl@38656 ` 335` ``` from this[THEN bspec, OF top] show "positive_integral g \ \ (space M)" ``` hoelzl@38656 ` 336` ``` by (simp cong: positive_integral_cong) ``` hoelzl@38656 ` 337` ``` qed ``` hoelzl@38656 ` 338` ``` hence "?y \ \" using M'.finite_measure_of_space by auto ``` hoelzl@38656 ` 339` ``` from SUPR_countable_SUPR[OF this `G \ {}`] guess ys .. note ys = this ``` hoelzl@38656 ` 340` ``` hence "\n. \g. g\G \ positive_integral g = ys n" ``` hoelzl@38656 ` 341` ``` proof safe ``` hoelzl@38656 ` 342` ``` fix n assume "range ys \ positive_integral ` G" ``` hoelzl@38656 ` 343` ``` hence "ys n \ positive_integral ` G" by auto ``` hoelzl@38656 ` 344` ``` thus "\g. g\G \ positive_integral g = ys n" by auto ``` hoelzl@38656 ` 345` ``` qed ``` hoelzl@38656 ` 346` ``` from choice[OF this] obtain gs where "\i. gs i \ G" "\n. positive_integral (gs n) = ys n" by auto ``` hoelzl@38656 ` 347` ``` hence y_eq: "?y = (SUP i. positive_integral (gs i))" using ys by auto ``` hoelzl@38656 ` 348` ``` let "?g i x" = "Max ((\n. gs n x) ` {..i})" ``` hoelzl@38656 ` 349` ``` def f \ "SUP i. ?g i" ``` hoelzl@38656 ` 350` ``` have gs_not_empty: "\i. (\n. gs n x) ` {..i} \ {}" by auto ``` hoelzl@38656 ` 351` ``` { fix i have "?g i \ G" ``` hoelzl@38656 ` 352` ``` proof (induct i) ``` hoelzl@38656 ` 353` ``` case 0 thus ?case by simp fact ``` hoelzl@38656 ` 354` ``` next ``` hoelzl@38656 ` 355` ``` case (Suc i) ``` hoelzl@38656 ` 356` ``` with Suc gs_not_empty `gs (Suc i) \ G` show ?case ``` hoelzl@38656 ` 357` ``` by (auto simp add: atMost_Suc intro!: max_in_G) ``` hoelzl@38656 ` 358` ``` qed } ``` hoelzl@38656 ` 359` ``` note g_in_G = this ``` hoelzl@38656 ` 360` ``` have "\x. \i. ?g i x \ ?g (Suc i) x" ``` hoelzl@38656 ` 361` ``` using gs_not_empty by (simp add: atMost_Suc) ``` hoelzl@38656 ` 362` ``` hence isoton_g: "?g \ f" by (simp add: isoton_def le_fun_def f_def) ``` hoelzl@38656 ` 363` ``` from SUP_in_G[OF this g_in_G] have "f \ G" . ``` hoelzl@38656 ` 364` ``` hence [simp, intro]: "f \ borel_measurable M" unfolding G_def by auto ``` hoelzl@38656 ` 365` hoelzl@38656 ` 366` ``` have "(\i. positive_integral (?g i)) \ positive_integral f" ``` hoelzl@38656 ` 367` ``` using isoton_g g_in_G by (auto intro!: positive_integral_isoton simp: G_def f_def) ``` hoelzl@38656 ` 368` ``` hence "positive_integral f = (SUP i. positive_integral (?g i))" ``` hoelzl@38656 ` 369` ``` unfolding isoton_def by simp ``` hoelzl@38656 ` 370` ``` also have "\ = ?y" ``` hoelzl@38656 ` 371` ``` proof (rule antisym) ``` hoelzl@38656 ` 372` ``` show "(SUP i. positive_integral (?g i)) \ ?y" ``` hoelzl@38656 ` 373` ``` using g_in_G by (auto intro!: exI Sup_mono simp: SUPR_def) ``` hoelzl@38656 ` 374` ``` show "?y \ (SUP i. positive_integral (?g i))" unfolding y_eq ``` hoelzl@38656 ` 375` ``` by (auto intro!: SUP_mono positive_integral_mono Max_ge) ``` hoelzl@38656 ` 376` ``` qed ``` hoelzl@38656 ` 377` ``` finally have int_f_eq_y: "positive_integral f = ?y" . ``` hoelzl@38656 ` 378` hoelzl@38656 ` 379` ``` let "?t A" = "\ A - positive_integral (\x. f x * indicator A x)" ``` hoelzl@38656 ` 380` hoelzl@38656 ` 381` ``` have "finite_measure M ?t" ``` hoelzl@38656 ` 382` ``` proof ``` hoelzl@38656 ` 383` ``` show "?t {} = 0" by simp ``` hoelzl@38656 ` 384` ``` show "?t (space M) \ \" using M'.finite_measure by simp ``` hoelzl@38656 ` 385` ``` show "countably_additive M ?t" unfolding countably_additive_def ``` hoelzl@38656 ` 386` ``` proof safe ``` hoelzl@38656 ` 387` ``` fix A :: "nat \ 'a set" assume A: "range A \ sets M" "disjoint_family A" ``` hoelzl@38656 ` 388` ``` have "(\\<^isub>\ n. positive_integral (\x. f x * indicator (A n) x)) ``` hoelzl@38656 ` 389` ``` = positive_integral (\x. (\\<^isub>\n. f x * indicator (A n) x))" ``` hoelzl@38656 ` 390` ``` using `range A \ sets M` ``` hoelzl@38656 ` 391` ``` by (rule_tac positive_integral_psuminf[symmetric]) (auto intro!: borel_measurable_indicator) ``` hoelzl@38656 ` 392` ``` also have "\ = positive_integral (\x. f x * indicator (\n. A n) x)" ``` hoelzl@38656 ` 393` ``` apply (rule positive_integral_cong) ``` hoelzl@38656 ` 394` ``` apply (subst psuminf_cmult_right) ``` hoelzl@38656 ` 395` ``` unfolding psuminf_indicator[OF `disjoint_family A`] .. ``` hoelzl@38656 ` 396` ``` finally have "(\\<^isub>\ n. positive_integral (\x. f x * indicator (A n) x)) ``` hoelzl@38656 ` 397` ``` = positive_integral (\x. f x * indicator (\n. A n) x)" . ``` hoelzl@38656 ` 398` ``` moreover have "(\\<^isub>\n. \ (A n)) = \ (\n. A n)" ``` hoelzl@38656 ` 399` ``` using M'.measure_countably_additive A by (simp add: comp_def) ``` hoelzl@38656 ` 400` ``` moreover have "\i. positive_integral (\x. f x * indicator (A i) x) \ \ (A i)" ``` hoelzl@38656 ` 401` ``` using A `f \ G` unfolding G_def by auto ``` hoelzl@38656 ` 402` ``` moreover have v_fin: "\ (\i. A i) \ \" using M'.finite_measure A by (simp add: countable_UN) ``` hoelzl@38656 ` 403` ``` moreover { ``` hoelzl@38656 ` 404` ``` have "positive_integral (\x. f x * indicator (\i. A i) x) \ \ (\i. A i)" ``` hoelzl@38656 ` 405` ``` using A `f \ G` unfolding G_def by (auto simp: countable_UN) ``` hoelzl@38656 ` 406` ``` also have "\ (\i. A i) < \" using v_fin by (simp add: pinfreal_less_\) ``` hoelzl@38656 ` 407` ``` finally have "positive_integral (\x. f x * indicator (\i. A i) x) \ \" ``` hoelzl@38656 ` 408` ``` by (simp add: pinfreal_less_\) } ``` hoelzl@38656 ` 409` ``` ultimately ``` hoelzl@38656 ` 410` ``` show "(\\<^isub>\ n. ?t (A n)) = ?t (\i. A i)" ``` hoelzl@38656 ` 411` ``` apply (subst psuminf_minus) by simp_all ``` hoelzl@38656 ` 412` ``` qed ``` hoelzl@38656 ` 413` ``` qed ``` hoelzl@38656 ` 414` ``` then interpret M: finite_measure M ?t . ``` hoelzl@38656 ` 415` hoelzl@38656 ` 416` ``` have ac: "absolutely_continuous ?t" using `absolutely_continuous \` unfolding absolutely_continuous_def by auto ``` hoelzl@38656 ` 417` hoelzl@38656 ` 418` ``` have upper_bound: "\A\sets M. ?t A \ 0" ``` hoelzl@38656 ` 419` ``` proof (rule ccontr) ``` hoelzl@38656 ` 420` ``` assume "\ ?thesis" ``` hoelzl@38656 ` 421` ``` then obtain A where A: "A \ sets M" and pos: "0 < ?t A" ``` hoelzl@38656 ` 422` ``` by (auto simp: not_le) ``` hoelzl@38656 ` 423` ``` note pos ``` hoelzl@38656 ` 424` ``` also have "?t A \ ?t (space M)" ``` hoelzl@38656 ` 425` ``` using M.measure_mono[of A "space M"] A sets_into_space by simp ``` hoelzl@38656 ` 426` ``` finally have pos_t: "0 < ?t (space M)" by simp ``` hoelzl@38656 ` 427` ``` moreover ``` hoelzl@38656 ` 428` ``` hence pos_M: "0 < \ (space M)" ``` hoelzl@38656 ` 429` ``` using ac top unfolding absolutely_continuous_def by auto ``` hoelzl@38656 ` 430` ``` moreover ``` hoelzl@38656 ` 431` ``` have "positive_integral (\x. f x * indicator (space M) x) \ \ (space M)" ``` hoelzl@38656 ` 432` ``` using `f \ G` unfolding G_def by auto ``` hoelzl@38656 ` 433` ``` hence "positive_integral (\x. f x * indicator (space M) x) \ \" ``` hoelzl@38656 ` 434` ``` using M'.finite_measure_of_space by auto ``` hoelzl@38656 ` 435` ``` moreover ``` hoelzl@38656 ` 436` ``` def b \ "?t (space M) / \ (space M) / 2" ``` hoelzl@38656 ` 437` ``` ultimately have b: "b \ 0" "b \ \" ``` hoelzl@38656 ` 438` ``` using M'.finite_measure_of_space ``` hoelzl@38656 ` 439` ``` by (auto simp: pinfreal_inverse_eq_0 finite_measure_of_space) ``` hoelzl@38656 ` 440` hoelzl@38656 ` 441` ``` have "finite_measure M (\A. b * \ A)" (is "finite_measure M ?b") ``` hoelzl@38656 ` 442` ``` proof ``` hoelzl@38656 ` 443` ``` show "?b {} = 0" by simp ``` hoelzl@38656 ` 444` ``` show "?b (space M) \ \" using finite_measure_of_space b by auto ``` hoelzl@38656 ` 445` ``` show "countably_additive M ?b" ``` hoelzl@38656 ` 446` ``` unfolding countably_additive_def psuminf_cmult_right ``` hoelzl@38656 ` 447` ``` using measure_countably_additive by auto ``` hoelzl@38656 ` 448` ``` qed ``` hoelzl@38656 ` 449` hoelzl@38656 ` 450` ``` from M.Radon_Nikodym_aux[OF this] ``` hoelzl@38656 ` 451` ``` obtain A0 where "A0 \ sets M" and ``` hoelzl@38656 ` 452` ``` space_less_A0: "real (?t (space M)) - real (b * \ (space M)) \ real (?t A0) - real (b * \ A0)" and ``` hoelzl@38656 ` 453` ``` *: "\B. \ B \ sets M ; B \ A0 \ \ 0 \ real (?t B) - real (b * \ B)" by auto ``` hoelzl@38656 ` 454` ``` { fix B assume "B \ sets M" "B \ A0" ``` hoelzl@38656 ` 455` ``` with *[OF this] have "b * \ B \ ?t B" ``` hoelzl@38656 ` 456` ``` using M'.finite_measure b finite_measure ``` hoelzl@38656 ` 457` ``` by (cases "b * \ B", cases "?t B") (auto simp: field_simps) } ``` hoelzl@38656 ` 458` ``` note bM_le_t = this ``` hoelzl@38656 ` 459` hoelzl@38656 ` 460` ``` let "?f0 x" = "f x + b * indicator A0 x" ``` hoelzl@38656 ` 461` hoelzl@38656 ` 462` ``` { fix A assume A: "A \ sets M" ``` hoelzl@38656 ` 463` ``` hence "A \ A0 \ sets M" using `A0 \ sets M` by auto ``` hoelzl@38656 ` 464` ``` have "positive_integral (\x. ?f0 x * indicator A x) = ``` hoelzl@38656 ` 465` ``` positive_integral (\x. f x * indicator A x + b * indicator (A \ A0) x)" ``` hoelzl@38656 ` 466` ``` by (auto intro!: positive_integral_cong simp: field_simps indicator_inter_arith) ``` hoelzl@38656 ` 467` ``` hence "positive_integral (\x. ?f0 x * indicator A x) = ``` hoelzl@38656 ` 468` ``` positive_integral (\x. f x * indicator A x) + b * \ (A \ A0)" ``` hoelzl@38656 ` 469` ``` using `A0 \ sets M` `A \ A0 \ sets M` A ``` hoelzl@38656 ` 470` ``` by (simp add: borel_measurable_indicator positive_integral_add positive_integral_cmult_indicator) } ``` hoelzl@38656 ` 471` ``` note f0_eq = this ``` hoelzl@38656 ` 472` hoelzl@38656 ` 473` ``` { fix A assume A: "A \ sets M" ``` hoelzl@38656 ` 474` ``` hence "A \ A0 \ sets M" using `A0 \ sets M` by auto ``` hoelzl@38656 ` 475` ``` have f_le_v: "positive_integral (\x. f x * indicator A x) \ \ A" ``` hoelzl@38656 ` 476` ``` using `f \ G` A unfolding G_def by auto ``` hoelzl@38656 ` 477` ``` note f0_eq[OF A] ``` hoelzl@38656 ` 478` ``` also have "positive_integral (\x. f x * indicator A x) + b * \ (A \ A0) \ ``` hoelzl@38656 ` 479` ``` positive_integral (\x. f x * indicator A x) + ?t (A \ A0)" ``` hoelzl@38656 ` 480` ``` using bM_le_t[OF `A \ A0 \ sets M`] `A \ sets M` `A0 \ sets M` ``` hoelzl@38656 ` 481` ``` by (auto intro!: add_left_mono) ``` hoelzl@38656 ` 482` ``` also have "\ \ positive_integral (\x. f x * indicator A x) + ?t A" ``` hoelzl@38656 ` 483` ``` using M.measure_mono[simplified, OF _ `A \ A0 \ sets M` `A \ sets M`] ``` hoelzl@38656 ` 484` ``` by (auto intro!: add_left_mono) ``` hoelzl@38656 ` 485` ``` also have "\ \ \ A" ``` hoelzl@38656 ` 486` ``` using f_le_v M'.finite_measure[simplified, OF `A \ sets M`] ``` hoelzl@38656 ` 487` ``` by (cases "positive_integral (\x. f x * indicator A x)", cases "\ A", auto) ``` hoelzl@38656 ` 488` ``` finally have "positive_integral (\x. ?f0 x * indicator A x) \ \ A" . } ``` hoelzl@38656 ` 489` ``` hence "?f0 \ G" using `A0 \ sets M` unfolding G_def ``` hoelzl@38656 ` 490` ``` by (auto intro!: borel_measurable_indicator borel_measurable_pinfreal_add borel_measurable_pinfreal_times) ``` hoelzl@38656 ` 491` hoelzl@38656 ` 492` ``` have real: "?t (space M) \ \" "?t A0 \ \" ``` hoelzl@38656 ` 493` ``` "b * \ (space M) \ \" "b * \ A0 \ \" ``` hoelzl@38656 ` 494` ``` using `A0 \ sets M` b ``` hoelzl@38656 ` 495` ``` finite_measure[of A0] M.finite_measure[of A0] ``` hoelzl@38656 ` 496` ``` finite_measure_of_space M.finite_measure_of_space ``` hoelzl@38656 ` 497` ``` by auto ``` hoelzl@38656 ` 498` hoelzl@38656 ` 499` ``` have int_f_finite: "positive_integral f \ \" ``` hoelzl@38656 ` 500` ``` using M'.finite_measure_of_space pos_t unfolding pinfreal_zero_less_diff_iff ``` hoelzl@38656 ` 501` ``` by (auto cong: positive_integral_cong) ``` hoelzl@38656 ` 502` hoelzl@38656 ` 503` ``` have "?t (space M) > b * \ (space M)" unfolding b_def ``` hoelzl@38656 ` 504` ``` apply (simp add: field_simps) ``` hoelzl@38656 ` 505` ``` apply (subst mult_assoc[symmetric]) ``` hoelzl@38656 ` 506` ``` apply (subst pinfreal_mult_inverse) ``` hoelzl@38656 ` 507` ``` using finite_measure_of_space M'.finite_measure_of_space pos_t pos_M ``` hoelzl@38656 ` 508` ``` using pinfreal_mult_strict_right_mono[of "Real (1/2)" 1 "?t (space M)"] ``` hoelzl@38656 ` 509` ``` by simp_all ``` hoelzl@38656 ` 510` ``` hence "0 < ?t (space M) - b * \ (space M)" ``` hoelzl@38656 ` 511` ``` by (simp add: pinfreal_zero_less_diff_iff) ``` hoelzl@38656 ` 512` ``` also have "\ \ ?t A0 - b * \ A0" ``` hoelzl@38656 ` 513` ``` using space_less_A0 pos_M pos_t b real[unfolded pinfreal_noteq_omega_Ex] by auto ``` hoelzl@38656 ` 514` ``` finally have "b * \ A0 < ?t A0" unfolding pinfreal_zero_less_diff_iff . ``` hoelzl@38656 ` 515` ``` hence "0 < ?t A0" by auto ``` hoelzl@38656 ` 516` ``` hence "0 < \ A0" using ac unfolding absolutely_continuous_def ``` hoelzl@38656 ` 517` ``` using `A0 \ sets M` by auto ``` hoelzl@38656 ` 518` ``` hence "0 < b * \ A0" using b by auto ``` hoelzl@38656 ` 519` hoelzl@38656 ` 520` ``` from int_f_finite this ``` hoelzl@38656 ` 521` ``` have "?y + 0 < positive_integral f + b * \ A0" unfolding int_f_eq_y ``` hoelzl@38656 ` 522` ``` by (rule pinfreal_less_add) ``` hoelzl@38656 ` 523` ``` also have "\ = positive_integral ?f0" using f0_eq[OF top] `A0 \ sets M` sets_into_space ``` hoelzl@38656 ` 524` ``` by (simp cong: positive_integral_cong) ``` hoelzl@38656 ` 525` ``` finally have "?y < positive_integral ?f0" by simp ``` hoelzl@38656 ` 526` hoelzl@38656 ` 527` ``` moreover from `?f0 \ G` have "positive_integral ?f0 \ ?y" by (auto intro!: le_SUPI) ``` hoelzl@38656 ` 528` ``` ultimately show False by auto ``` hoelzl@38656 ` 529` ``` qed ``` hoelzl@38656 ` 530` hoelzl@38656 ` 531` ``` show ?thesis ``` hoelzl@38656 ` 532` ``` proof (safe intro!: bexI[of _ f]) ``` hoelzl@38656 ` 533` ``` fix A assume "A\sets M" ``` hoelzl@38656 ` 534` ``` show "\ A = positive_integral (\x. f x * indicator A x)" ``` hoelzl@38656 ` 535` ``` proof (rule antisym) ``` hoelzl@38656 ` 536` ``` show "positive_integral (\x. f x * indicator A x) \ \ A" ``` hoelzl@38656 ` 537` ``` using `f \ G` `A \ sets M` unfolding G_def by auto ``` hoelzl@38656 ` 538` ``` show "\ A \ positive_integral (\x. f x * indicator A x)" ``` hoelzl@38656 ` 539` ``` using upper_bound[THEN bspec, OF `A \ sets M`] ``` hoelzl@38656 ` 540` ``` by (simp add: pinfreal_zero_le_diff) ``` hoelzl@38656 ` 541` ``` qed ``` hoelzl@38656 ` 542` ``` qed simp ``` hoelzl@38656 ` 543` ```qed ``` hoelzl@38656 ` 544` hoelzl@38656 ` 545` ```lemma (in finite_measure) Radon_Nikodym_finite_measure_infinite: ``` hoelzl@38656 ` 546` ``` assumes "measure_space M \" ``` hoelzl@38656 ` 547` ``` assumes "absolutely_continuous \" ``` hoelzl@38656 ` 548` ``` shows "\f \ borel_measurable M. \A\sets M. \ A = positive_integral (\x. f x * indicator A x)" ``` hoelzl@38656 ` 549` ```proof - ``` hoelzl@38656 ` 550` ``` interpret v: measure_space M \ by fact ``` hoelzl@38656 ` 551` ``` let ?Q = "{Q\sets M. \ Q \ \}" ``` hoelzl@38656 ` 552` ``` let ?a = "SUP Q:?Q. \ Q" ``` hoelzl@38656 ` 553` hoelzl@38656 ` 554` ``` have "{} \ ?Q" using v.empty_measure by auto ``` hoelzl@38656 ` 555` ``` then have Q_not_empty: "?Q \ {}" by blast ``` hoelzl@38656 ` 556` hoelzl@38656 ` 557` ``` have "?a \ \ (space M)" using sets_into_space ``` hoelzl@38656 ` 558` ``` by (auto intro!: SUP_leI measure_mono top) ``` hoelzl@38656 ` 559` ``` then have "?a \ \" using finite_measure_of_space ``` hoelzl@38656 ` 560` ``` by auto ``` hoelzl@38656 ` 561` ``` from SUPR_countable_SUPR[OF this Q_not_empty] ``` hoelzl@38656 ` 562` ``` obtain Q'' where "range Q'' \ \ ` ?Q" and a: "?a = (SUP i::nat. Q'' i)" ``` hoelzl@38656 ` 563` ``` by auto ``` hoelzl@38656 ` 564` ``` then have "\i. \Q'. Q'' i = \ Q' \ Q' \ ?Q" by auto ``` hoelzl@38656 ` 565` ``` from choice[OF this] obtain Q' where Q': "\i. Q'' i = \ (Q' i)" "\i. Q' i \ ?Q" ``` hoelzl@38656 ` 566` ``` by auto ``` hoelzl@38656 ` 567` ``` then have a_Lim: "?a = (SUP i::nat. \ (Q' i))" using a by simp ``` hoelzl@38656 ` 568` ``` let "?O n" = "\i\n. Q' i" ``` hoelzl@38656 ` 569` ``` have Union: "(SUP i. \ (?O i)) = \ (\i. ?O i)" ``` hoelzl@38656 ` 570` ``` proof (rule continuity_from_below[of ?O]) ``` hoelzl@38656 ` 571` ``` show "range ?O \ sets M" using Q' by (auto intro!: finite_UN) ``` hoelzl@38656 ` 572` ``` show "\i. ?O i \ ?O (Suc i)" by fastsimp ``` hoelzl@38656 ` 573` ``` qed ``` hoelzl@38656 ` 574` hoelzl@38656 ` 575` ``` have Q'_sets: "\i. Q' i \ sets M" using Q' by auto ``` hoelzl@38656 ` 576` hoelzl@38656 ` 577` ``` have O_sets: "\i. ?O i \ sets M" ``` hoelzl@38656 ` 578` ``` using Q' by (auto intro!: finite_UN Un) ``` hoelzl@38656 ` 579` ``` then have O_in_G: "\i. ?O i \ ?Q" ``` hoelzl@38656 ` 580` ``` proof (safe del: notI) ``` hoelzl@38656 ` 581` ``` fix i have "Q' ` {..i} \ sets M" ``` hoelzl@38656 ` 582` ``` using Q' by (auto intro: finite_UN) ``` hoelzl@38656 ` 583` ``` with v.measure_finitely_subadditive[of "{.. i}" Q'] ``` hoelzl@38656 ` 584` ``` have "\ (?O i) \ (\i\i. \ (Q' i))" by auto ``` hoelzl@38656 ` 585` ``` also have "\ < \" unfolding setsum_\ pinfreal_less_\ using Q' by auto ``` hoelzl@38656 ` 586` ``` finally show "\ (?O i) \ \" unfolding pinfreal_less_\ by auto ``` hoelzl@38656 ` 587` ``` qed auto ``` hoelzl@38656 ` 588` ``` have O_mono: "\n. ?O n \ ?O (Suc n)" by fastsimp ``` hoelzl@38656 ` 589` hoelzl@38656 ` 590` ``` have a_eq: "?a = \ (\i. ?O i)" unfolding Union[symmetric] ``` hoelzl@38656 ` 591` ``` proof (rule antisym) ``` hoelzl@38656 ` 592` ``` show "?a \ (SUP i. \ (?O i))" unfolding a_Lim ``` hoelzl@38656 ` 593` ``` using Q' by (auto intro!: SUP_mono measure_mono finite_UN) ``` hoelzl@38656 ` 594` ``` show "(SUP i. \ (?O i)) \ ?a" unfolding SUPR_def ``` hoelzl@38656 ` 595` ``` proof (safe intro!: Sup_mono, unfold bex_simps) ``` hoelzl@38656 ` 596` ``` fix i ``` hoelzl@38656 ` 597` ``` have *: "(\Q' ` {..i}) = ?O i" by auto ``` hoelzl@38656 ` 598` ``` then show "\x. (x \ sets M \ \ x \ \) \ ``` hoelzl@38656 ` 599` ``` \ (\Q' ` {..i}) \ \ x" ``` hoelzl@38656 ` 600` ``` using O_in_G[of i] by (auto intro!: exI[of _ "?O i"]) ``` hoelzl@38656 ` 601` ``` qed ``` hoelzl@38656 ` 602` ``` qed ``` hoelzl@38656 ` 603` hoelzl@38656 ` 604` ``` let "?O_0" = "(\i. ?O i)" ``` hoelzl@38656 ` 605` ``` have "?O_0 \ sets M" using Q' by auto ``` hoelzl@38656 ` 606` hoelzl@38656 ` 607` ``` { fix A assume *: "A \ ?Q" "A \ space M - ?O_0" ``` hoelzl@38656 ` 608` ``` then have "\ ?O_0 + \ A = \ (?O_0 \ A)" ``` hoelzl@38656 ` 609` ``` using Q' by (auto intro!: measure_additive countable_UN) ``` hoelzl@38656 ` 610` ``` also have "\ = (SUP i. \ (?O i \ A))" ``` hoelzl@38656 ` 611` ``` proof (rule continuity_from_below[of "\i. ?O i \ A", symmetric, simplified]) ``` hoelzl@38656 ` 612` ``` show "range (\i. ?O i \ A) \ sets M" ``` hoelzl@38656 ` 613` ``` using * O_sets by auto ``` hoelzl@38656 ` 614` ``` qed fastsimp ``` hoelzl@38656 ` 615` ``` also have "\ \ ?a" ``` hoelzl@38656 ` 616` ``` proof (safe intro!: SUPR_bound) ``` hoelzl@38656 ` 617` ``` fix i have "?O i \ A \ ?Q" ``` hoelzl@38656 ` 618` ``` proof (safe del: notI) ``` hoelzl@38656 ` 619` ``` show "?O i \ A \ sets M" using O_sets * by auto ``` hoelzl@38656 ` 620` ``` from O_in_G[of i] ``` hoelzl@38656 ` 621` ``` moreover have "\ (?O i \ A) \ \ (?O i) + \ A" ``` hoelzl@38656 ` 622` ``` using v.measure_subadditive[of "?O i" A] * O_sets by auto ``` hoelzl@38656 ` 623` ``` ultimately show "\ (?O i \ A) \ \" ``` hoelzl@38656 ` 624` ``` using * by auto ``` hoelzl@38656 ` 625` ``` qed ``` hoelzl@38656 ` 626` ``` then show "\ (?O i \ A) \ ?a" by (rule le_SUPI) ``` hoelzl@38656 ` 627` ``` qed ``` hoelzl@38656 ` 628` ``` finally have "\ A = 0" unfolding a_eq using finite_measure[OF `?O_0 \ sets M`] ``` hoelzl@38656 ` 629` ``` by (cases "\ A") (auto simp: pinfreal_noteq_omega_Ex) } ``` hoelzl@38656 ` 630` ``` note stetic = this ``` hoelzl@38656 ` 631` hoelzl@38656 ` 632` ``` def Q \ "\i. case i of 0 \ ?O 0 | Suc n \ ?O (Suc n) - ?O n" ``` hoelzl@38656 ` 633` hoelzl@38656 ` 634` ``` { fix i have "Q i \ sets M" unfolding Q_def using Q'[of 0] by (cases i) (auto intro: O_sets) } ``` hoelzl@38656 ` 635` ``` note Q_sets = this ``` hoelzl@38656 ` 636` hoelzl@38656 ` 637` ``` { fix i have "\ (Q i) \ \" ``` hoelzl@38656 ` 638` ``` proof (cases i) ``` hoelzl@38656 ` 639` ``` case 0 then show ?thesis ``` hoelzl@38656 ` 640` ``` unfolding Q_def using Q'[of 0] by simp ``` hoelzl@38656 ` 641` ``` next ``` hoelzl@38656 ` 642` ``` case (Suc n) ``` hoelzl@38656 ` 643` ``` then show ?thesis unfolding Q_def ``` hoelzl@38656 ` 644` ``` using `?O n \ ?Q` `?O (Suc n) \ ?Q` O_mono ``` hoelzl@38656 ` 645` ``` using v.measure_Diff[of "?O n" "?O (Suc n)"] by auto ``` hoelzl@38656 ` 646` ``` qed } ``` hoelzl@38656 ` 647` ``` note Q_omega = this ``` hoelzl@38656 ` 648` hoelzl@38656 ` 649` ``` { fix j have "(\i\j. ?O i) = (\i\j. Q i)" ``` hoelzl@38656 ` 650` ``` proof (induct j) ``` hoelzl@38656 ` 651` ``` case 0 then show ?case by (simp add: Q_def) ``` hoelzl@38656 ` 652` ``` next ``` hoelzl@38656 ` 653` ``` case (Suc j) ``` hoelzl@38656 ` 654` ``` have eq: "\j. (\i\j. ?O i) = (\i\j. Q' i)" by fastsimp ``` hoelzl@38656 ` 655` ``` have "{..j} \ {..Suc j} = {..Suc j}" by auto ``` hoelzl@38656 ` 656` ``` then have "(\i\Suc j. Q' i) = (\i\j. Q' i) \ Q (Suc j)" ``` hoelzl@38656 ` 657` ``` by (simp add: UN_Un[symmetric] Q_def del: UN_Un) ``` hoelzl@38656 ` 658` ``` then show ?case using Suc by (auto simp add: eq atMost_Suc) ``` hoelzl@38656 ` 659` ``` qed } ``` hoelzl@38656 ` 660` ``` then have "(\j. (\i\j. ?O i)) = (\j. (\i\j. Q i))" by simp ``` hoelzl@38656 ` 661` ``` then have O_0_eq_Q: "?O_0 = (\j. Q j)" by fastsimp ``` hoelzl@38656 ` 662` hoelzl@38656 ` 663` ``` have "\i. \f. f\borel_measurable M \ (\A\sets M. ``` hoelzl@38656 ` 664` ``` \ (Q i \ A) = positive_integral (\x. f x * indicator (Q i \ A) x))" ``` hoelzl@38656 ` 665` ``` proof ``` hoelzl@38656 ` 666` ``` fix i ``` hoelzl@38656 ` 667` ``` have indicator_eq: "\f x A. (f x :: pinfreal) * indicator (Q i \ A) x * indicator (Q i) x ``` hoelzl@38656 ` 668` ``` = (f x * indicator (Q i) x) * indicator A x" ``` hoelzl@38656 ` 669` ``` unfolding indicator_def by auto ``` hoelzl@38656 ` 670` hoelzl@39092 ` 671` ``` have fm: "finite_measure (restricted_space (Q i)) \" ``` hoelzl@38656 ` 672` ``` (is "finite_measure ?R \") by (rule restricted_finite_measure[OF Q_sets[of i]]) ``` hoelzl@38656 ` 673` ``` then interpret R: finite_measure ?R . ``` hoelzl@38656 ` 674` ``` have fmv: "finite_measure ?R \" ``` hoelzl@38656 ` 675` ``` unfolding finite_measure_def finite_measure_axioms_def ``` hoelzl@38656 ` 676` ``` proof ``` hoelzl@38656 ` 677` ``` show "measure_space ?R \" ``` hoelzl@38656 ` 678` ``` using v.restricted_measure_space Q_sets[of i] by auto ``` hoelzl@38656 ` 679` ``` show "\ (space ?R) \ \" ``` hoelzl@38656 ` 680` ``` using Q_omega by simp ``` hoelzl@38656 ` 681` ``` qed ``` hoelzl@38656 ` 682` ``` have "R.absolutely_continuous \" ``` hoelzl@38656 ` 683` ``` using `absolutely_continuous \` `Q i \ sets M` ``` hoelzl@38656 ` 684` ``` by (auto simp: R.absolutely_continuous_def absolutely_continuous_def) ``` hoelzl@38656 ` 685` ``` from finite_measure.Radon_Nikodym_finite_measure[OF fm fmv this] ``` hoelzl@38656 ` 686` ``` obtain f where f: "(\x. f x * indicator (Q i) x) \ borel_measurable M" ``` hoelzl@38656 ` 687` ``` and f_int: "\A. A\sets M \ \ (Q i \ A) = positive_integral (\x. (f x * indicator (Q i) x) * indicator A x)" ``` hoelzl@38656 ` 688` ``` unfolding Bex_def borel_measurable_restricted[OF `Q i \ sets M`] ``` hoelzl@38656 ` 689` ``` positive_integral_restricted[OF `Q i \ sets M`] by (auto simp: indicator_eq) ``` hoelzl@38656 ` 690` ``` then show "\f. f\borel_measurable M \ (\A\sets M. ``` hoelzl@38656 ` 691` ``` \ (Q i \ A) = positive_integral (\x. f x * indicator (Q i \ A) x))" ``` hoelzl@38656 ` 692` ``` by (fastsimp intro!: exI[of _ "\x. f x * indicator (Q i) x"] positive_integral_cong ``` hoelzl@38656 ` 693` ``` simp: indicator_def) ``` hoelzl@38656 ` 694` ``` qed ``` hoelzl@38656 ` 695` ``` from choice[OF this] obtain f where borel: "\i. f i \ borel_measurable M" ``` hoelzl@38656 ` 696` ``` and f: "\A i. A \ sets M \ ``` hoelzl@38656 ` 697` ``` \ (Q i \ A) = positive_integral (\x. f i x * indicator (Q i \ A) x)" ``` hoelzl@38656 ` 698` ``` by auto ``` hoelzl@38656 ` 699` ``` let "?f x" = ``` hoelzl@38656 ` 700` ``` "(\\<^isub>\ i. f i x * indicator (Q i) x) + \ * indicator (space M - ?O_0) x" ``` hoelzl@38656 ` 701` ``` show ?thesis ``` hoelzl@38656 ` 702` ``` proof (safe intro!: bexI[of _ ?f]) ``` hoelzl@38656 ` 703` ``` show "?f \ borel_measurable M" ``` hoelzl@38656 ` 704` ``` by (safe intro!: borel_measurable_psuminf borel_measurable_pinfreal_times ``` hoelzl@38656 ` 705` ``` borel_measurable_pinfreal_add borel_measurable_indicator ``` hoelzl@38656 ` 706` ``` borel_measurable_const borel Q_sets O_sets Diff countable_UN) ``` hoelzl@38656 ` 707` ``` fix A assume "A \ sets M" ``` hoelzl@38656 ` 708` ``` let ?C = "(space M - (\i. Q i)) \ A" ``` hoelzl@38656 ` 709` ``` have *: ``` hoelzl@38656 ` 710` ``` "\x i. indicator A x * (f i x * indicator (Q i) x) = ``` hoelzl@38656 ` 711` ``` f i x * indicator (Q i \ A) x" ``` hoelzl@38656 ` 712` ``` "\x i. (indicator A x * indicator (space M - (\i. UNION {..i} Q')) x :: pinfreal) = ``` hoelzl@38656 ` 713` ``` indicator ?C x" unfolding O_0_eq_Q by (auto simp: indicator_def) ``` hoelzl@38656 ` 714` ``` have "positive_integral (\x. ?f x * indicator A x) = ``` hoelzl@38656 ` 715` ``` (\\<^isub>\ i. \ (Q i \ A)) + \ * \ ?C" ``` hoelzl@38656 ` 716` ``` unfolding f[OF `A \ sets M`] ``` hoelzl@38656 ` 717` ``` apply (simp del: pinfreal_times(2) add: field_simps) ``` hoelzl@38656 ` 718` ``` apply (subst positive_integral_add) ``` hoelzl@38656 ` 719` ``` apply (safe intro!: borel_measurable_pinfreal_times Diff borel_measurable_const ``` hoelzl@38656 ` 720` ``` borel_measurable_psuminf borel_measurable_indicator `A \ sets M` Q_sets borel countable_UN Q'_sets) ``` hoelzl@38656 ` 721` ``` unfolding psuminf_cmult_right[symmetric] ``` hoelzl@38656 ` 722` ``` apply (subst positive_integral_psuminf) ``` hoelzl@38656 ` 723` ``` apply (safe intro!: borel_measurable_pinfreal_times Diff borel_measurable_const ``` hoelzl@38656 ` 724` ``` borel_measurable_psuminf borel_measurable_indicator `A \ sets M` Q_sets borel countable_UN Q'_sets) ``` hoelzl@38656 ` 725` ``` apply (subst positive_integral_cmult) ``` hoelzl@38656 ` 726` ``` apply (safe intro!: borel_measurable_pinfreal_times Diff borel_measurable_const ``` hoelzl@38656 ` 727` ``` borel_measurable_psuminf borel_measurable_indicator `A \ sets M` Q_sets borel countable_UN Q'_sets) ``` hoelzl@38656 ` 728` ``` unfolding * ``` hoelzl@38656 ` 729` ``` apply (subst positive_integral_indicator) ``` hoelzl@38656 ` 730` ``` apply (safe intro!: borel_measurable_pinfreal_times Diff borel_measurable_const Int ``` hoelzl@38656 ` 731` ``` borel_measurable_psuminf borel_measurable_indicator `A \ sets M` Q_sets borel countable_UN Q'_sets) ``` hoelzl@38656 ` 732` ``` by simp ``` hoelzl@38656 ` 733` ``` moreover have "(\\<^isub>\i. \ (Q i \ A)) = \ ((\i. Q i) \ A)" ``` hoelzl@38656 ` 734` ``` proof (rule v.measure_countably_additive[of "\i. Q i \ A", unfolded comp_def, simplified]) ``` hoelzl@38656 ` 735` ``` show "range (\i. Q i \ A) \ sets M" ``` hoelzl@38656 ` 736` ``` using Q_sets `A \ sets M` by auto ``` hoelzl@38656 ` 737` ``` show "disjoint_family (\i. Q i \ A)" ``` hoelzl@38656 ` 738` ``` by (fastsimp simp: disjoint_family_on_def Q_def ``` hoelzl@38656 ` 739` ``` split: nat.split_asm) ``` hoelzl@38656 ` 740` ``` qed ``` hoelzl@38656 ` 741` ``` moreover have "\ * \ ?C = \ ?C" ``` hoelzl@38656 ` 742` ``` proof cases ``` hoelzl@38656 ` 743` ``` assume null: "\ ?C = 0" ``` hoelzl@38656 ` 744` ``` hence "?C \ null_sets" using Q_sets `A \ sets M` by auto ``` hoelzl@38656 ` 745` ``` with `absolutely_continuous \` and null ``` hoelzl@38656 ` 746` ``` show ?thesis by (simp add: absolutely_continuous_def) ``` hoelzl@38656 ` 747` ``` next ``` hoelzl@38656 ` 748` ``` assume not_null: "\ ?C \ 0" ``` hoelzl@38656 ` 749` ``` have "\ ?C = \" ``` hoelzl@38656 ` 750` ``` proof (rule ccontr) ``` hoelzl@38656 ` 751` ``` assume "\ ?C \ \" ``` hoelzl@38656 ` 752` ``` then have "?C \ ?Q" ``` hoelzl@38656 ` 753` ``` using Q_sets `A \ sets M` by auto ``` hoelzl@38656 ` 754` ``` from stetic[OF this] not_null ``` hoelzl@38656 ` 755` ``` show False unfolding O_0_eq_Q by auto ``` hoelzl@38656 ` 756` ``` qed ``` hoelzl@38656 ` 757` ``` then show ?thesis using not_null by simp ``` hoelzl@38656 ` 758` ``` qed ``` hoelzl@38656 ` 759` ``` moreover have "?C \ sets M" "((\i. Q i) \ A) \ sets M" ``` hoelzl@38656 ` 760` ``` using Q_sets `A \ sets M` by (auto intro!: countable_UN) ``` hoelzl@38656 ` 761` ``` moreover have "((\i. Q i) \ A) \ ?C = A" "((\i. Q i) \ A) \ ?C = {}" ``` hoelzl@38656 ` 762` ``` using `A \ sets M` sets_into_space by auto ``` hoelzl@38656 ` 763` ``` ultimately show "\ A = positive_integral (\x. ?f x * indicator A x)" ``` hoelzl@38656 ` 764` ``` using v.measure_additive[simplified, of "(\i. Q i) \ A" ?C] by auto ``` hoelzl@38656 ` 765` ``` qed ``` hoelzl@38656 ` 766` ```qed ``` hoelzl@38656 ` 767` hoelzl@38656 ` 768` ```lemma (in sigma_finite_measure) Radon_Nikodym: ``` hoelzl@38656 ` 769` ``` assumes "measure_space M \" ``` hoelzl@38656 ` 770` ``` assumes "absolutely_continuous \" ``` hoelzl@38656 ` 771` ``` shows "\f \ borel_measurable M. \A\sets M. \ A = positive_integral (\x. f x * indicator A x)" ``` hoelzl@38656 ` 772` ```proof - ``` hoelzl@38656 ` 773` ``` from Ex_finite_integrable_function ``` hoelzl@38656 ` 774` ``` obtain h where finite: "positive_integral h \ \" and ``` hoelzl@38656 ` 775` ``` borel: "h \ borel_measurable M" and ``` hoelzl@38656 ` 776` ``` pos: "\x. x \ space M \ 0 < h x" and ``` hoelzl@38656 ` 777` ``` "\x. x \ space M \ h x < \" by auto ``` hoelzl@38656 ` 778` ``` let "?T A" = "positive_integral (\x. h x * indicator A x)" ``` hoelzl@38656 ` 779` ``` from measure_space_density[OF borel] finite ``` hoelzl@38656 ` 780` ``` interpret T: finite_measure M ?T ``` hoelzl@38656 ` 781` ``` unfolding finite_measure_def finite_measure_axioms_def ``` hoelzl@38656 ` 782` ``` by (simp cong: positive_integral_cong) ``` hoelzl@38656 ` 783` ``` have "\N. N \ sets M \ {x \ space M. h x \ 0 \ indicator N x \ (0::pinfreal)} = N" ``` hoelzl@38656 ` 784` ``` using sets_into_space pos by (force simp: indicator_def) ``` hoelzl@38656 ` 785` ``` then have "T.absolutely_continuous \" using assms(2) borel ``` hoelzl@38656 ` 786` ``` unfolding T.absolutely_continuous_def absolutely_continuous_def ``` hoelzl@38656 ` 787` ``` by (fastsimp simp: borel_measurable_indicator positive_integral_0_iff) ``` hoelzl@38656 ` 788` ``` from T.Radon_Nikodym_finite_measure_infinite[simplified, OF assms(1) this] ``` hoelzl@38656 ` 789` ``` obtain f where f_borel: "f \ borel_measurable M" and ``` hoelzl@38656 ` 790` ``` fT: "\A. A \ sets M \ \ A = T.positive_integral (\x. f x * indicator A x)" by auto ``` hoelzl@38656 ` 791` ``` show ?thesis ``` hoelzl@38656 ` 792` ``` proof (safe intro!: bexI[of _ "\x. h x * f x"]) ``` hoelzl@38656 ` 793` ``` show "(\x. h x * f x) \ borel_measurable M" ``` hoelzl@38656 ` 794` ``` using borel f_borel by (auto intro: borel_measurable_pinfreal_times) ``` hoelzl@38656 ` 795` ``` fix A assume "A \ sets M" ``` hoelzl@38656 ` 796` ``` then have "(\x. f x * indicator A x) \ borel_measurable M" ``` hoelzl@38656 ` 797` ``` using f_borel by (auto intro: borel_measurable_pinfreal_times borel_measurable_indicator) ``` hoelzl@38656 ` 798` ``` from positive_integral_translated_density[OF borel this] ``` hoelzl@38656 ` 799` ``` show "\ A = positive_integral (\x. h x * f x * indicator A x)" ``` hoelzl@38656 ` 800` ``` unfolding fT[OF `A \ sets M`] by (simp add: field_simps) ``` hoelzl@38656 ` 801` ``` qed ``` hoelzl@38656 ` 802` ```qed ``` hoelzl@38656 ` 803` hoelzl@38656 ` 804` ```section "Radon Nikodym derivative" ``` hoelzl@38656 ` 805` hoelzl@38656 ` 806` ```definition (in sigma_finite_measure) ``` hoelzl@38656 ` 807` ``` "RN_deriv \ \ SOME f. f \ borel_measurable M \ ``` hoelzl@38656 ` 808` ``` (\A \ sets M. \ A = positive_integral (\x. f x * indicator A x))" ``` hoelzl@38656 ` 809` hoelzl@38656 ` 810` ```lemma (in sigma_finite_measure) RN_deriv: ``` hoelzl@38656 ` 811` ``` assumes "measure_space M \" ``` hoelzl@38656 ` 812` ``` assumes "absolutely_continuous \" ``` hoelzl@38656 ` 813` ``` shows "RN_deriv \ \ borel_measurable M" (is ?borel) ``` hoelzl@38656 ` 814` ``` and "\A. A \ sets M \ \ A = positive_integral (\x. RN_deriv \ x * indicator A x)" ``` hoelzl@38656 ` 815` ``` (is "\A. _ \ ?int A") ``` hoelzl@38656 ` 816` ```proof - ``` hoelzl@38656 ` 817` ``` note Ex = Radon_Nikodym[OF assms, unfolded Bex_def] ``` hoelzl@38656 ` 818` ``` thus ?borel unfolding RN_deriv_def by (rule someI2_ex) auto ``` hoelzl@38656 ` 819` ``` fix A assume "A \ sets M" ``` hoelzl@38656 ` 820` ``` from Ex show "?int A" unfolding RN_deriv_def ``` hoelzl@38656 ` 821` ``` by (rule someI2_ex) (simp add: `A \ sets M`) ``` hoelzl@38656 ` 822` ```qed ``` hoelzl@38656 ` 823` hoelzl@38656 ` 824` ```lemma (in sigma_finite_measure) RN_deriv_singleton: ``` hoelzl@38656 ` 825` ``` assumes "measure_space M \" ``` hoelzl@38656 ` 826` ``` and ac: "absolutely_continuous \" ``` hoelzl@38656 ` 827` ``` and "{x} \ sets M" ``` hoelzl@38656 ` 828` ``` shows "\ {x} = RN_deriv \ x * \ {x}" ``` hoelzl@38656 ` 829` ```proof - ``` hoelzl@38656 ` 830` ``` note deriv = RN_deriv[OF assms(1, 2)] ``` hoelzl@38656 ` 831` ``` from deriv(2)[OF `{x} \ sets M`] ``` hoelzl@38656 ` 832` ``` have "\ {x} = positive_integral (\w. RN_deriv \ x * indicator {x} w)" ``` hoelzl@38656 ` 833` ``` by (auto simp: indicator_def intro!: positive_integral_cong) ``` hoelzl@38656 ` 834` ``` thus ?thesis using positive_integral_cmult_indicator[OF `{x} \ sets M`] ``` hoelzl@38656 ` 835` ``` by auto ``` hoelzl@38656 ` 836` ```qed ``` hoelzl@38656 ` 837` hoelzl@38656 ` 838` ```theorem (in finite_measure_space) RN_deriv_finite_measure: ``` hoelzl@38656 ` 839` ``` assumes "measure_space M \" ``` hoelzl@38656 ` 840` ``` and ac: "absolutely_continuous \" ``` hoelzl@38656 ` 841` ``` and "x \ space M" ``` hoelzl@38656 ` 842` ``` shows "\ {x} = RN_deriv \ x * \ {x}" ``` hoelzl@38656 ` 843` ```proof - ``` hoelzl@38656 ` 844` ``` have "{x} \ sets M" using sets_eq_Pow `x \ space M` by auto ``` hoelzl@38656 ` 845` ``` from RN_deriv_singleton[OF assms(1,2) this] show ?thesis . ``` hoelzl@38656 ` 846` ```qed ``` hoelzl@38656 ` 847` hoelzl@38656 ` 848` ```end ```