hoelzl@63627 ` 1` ```(* Title: HOL/Analysis/Radon_Nikodym.thy ``` hoelzl@42067 ` 2` ``` Author: Johannes Hölzl, TU München ``` hoelzl@42067 ` 3` ```*) ``` hoelzl@42067 ` 4` wenzelm@61808 ` 5` ```section \Radon-Nikod{\'y}m derivative\ ``` hoelzl@42067 ` 6` hoelzl@38656 ` 7` ```theory Radon_Nikodym ``` hoelzl@56993 ` 8` ```imports Bochner_Integration ``` hoelzl@38656 ` 9` ```begin ``` hoelzl@38656 ` 10` hoelzl@63329 ` 11` ```definition diff_measure :: "'a measure \ 'a measure \ 'a measure" ``` hoelzl@63329 ` 12` ```where ``` hoelzl@63329 ` 13` ``` "diff_measure M N = measure_of (space M) (sets M) (\A. emeasure M A - emeasure N A)" ``` hoelzl@47694 ` 14` lp15@61609 ` 15` ```lemma ``` hoelzl@47694 ` 16` ``` shows space_diff_measure[simp]: "space (diff_measure M N) = space M" ``` hoelzl@47694 ` 17` ``` and sets_diff_measure[simp]: "sets (diff_measure M N) = sets M" ``` hoelzl@47694 ` 18` ``` by (auto simp: diff_measure_def) ``` hoelzl@47694 ` 19` hoelzl@47694 ` 20` ```lemma emeasure_diff_measure: ``` hoelzl@47694 ` 21` ``` assumes fin: "finite_measure M" "finite_measure N" and sets_eq: "sets M = sets N" ``` hoelzl@47694 ` 22` ``` assumes pos: "\A. A \ sets M \ emeasure N A \ emeasure M A" and A: "A \ sets M" ``` hoelzl@47694 ` 23` ``` shows "emeasure (diff_measure M N) A = emeasure M A - emeasure N A" (is "_ = ?\ A") ``` hoelzl@47694 ` 24` ``` unfolding diff_measure_def ``` hoelzl@47694 ` 25` ```proof (rule emeasure_measure_of_sigma) ``` hoelzl@47694 ` 26` ``` show "sigma_algebra (space M) (sets M)" .. ``` hoelzl@47694 ` 27` ``` show "positive (sets M) ?\" ``` hoelzl@62975 ` 28` ``` using pos by (simp add: positive_def) ``` hoelzl@47694 ` 29` ``` show "countably_additive (sets M) ?\" ``` hoelzl@47694 ` 30` ``` proof (rule countably_additiveI) ``` hoelzl@47694 ` 31` ``` fix A :: "nat \ _" assume A: "range A \ sets M" and "disjoint_family A" ``` hoelzl@47694 ` 32` ``` then have suminf: ``` hoelzl@47694 ` 33` ``` "(\i. emeasure M (A i)) = emeasure M (\i. A i)" ``` hoelzl@47694 ` 34` ``` "(\i. emeasure N (A i)) = emeasure N (\i. A i)" ``` hoelzl@47694 ` 35` ``` by (simp_all add: suminf_emeasure sets_eq) ``` hoelzl@47694 ` 36` ``` with A have "(\i. emeasure M (A i) - emeasure N (A i)) = ``` hoelzl@47694 ` 37` ``` (\i. emeasure M (A i)) - (\i. emeasure N (A i))" ``` hoelzl@62975 ` 38` ``` using fin pos[of "A _"] ``` hoelzl@62975 ` 39` ``` by (intro ennreal_suminf_minus) ``` hoelzl@63329 ` 40` ``` (auto simp: sets_eq finite_measure.emeasure_eq_measure suminf_emeasure) ``` hoelzl@47694 ` 41` ``` then show "(\i. emeasure M (A i) - emeasure N (A i)) = ``` hoelzl@47694 ` 42` ``` emeasure M (\i. A i) - emeasure N (\i. A i) " ``` hoelzl@47694 ` 43` ``` by (simp add: suminf) ``` hoelzl@47694 ` 44` ``` qed ``` hoelzl@47694 ` 45` ```qed fact ``` hoelzl@47694 ` 46` wenzelm@64911 ` 47` ```text \An equivalent characterization of sigma-finite spaces is the existence of integrable ``` hoelzl@64283 ` 48` ```positive functions (or, still equivalently, the existence of a probability measure which is in ``` wenzelm@64911 ` 49` ```the same measure class as the original measure).\ ``` hoelzl@64283 ` 50` hoelzl@64283 ` 51` ```lemma (in sigma_finite_measure) obtain_positive_integrable_function: ``` hoelzl@64283 ` 52` ``` obtains f::"'a \ real" where ``` hoelzl@64283 ` 53` ``` "f \ borel_measurable M" ``` hoelzl@64283 ` 54` ``` "\x. f x > 0" ``` hoelzl@64283 ` 55` ``` "\x. f x \ 1" ``` hoelzl@64283 ` 56` ``` "integrable M f" ``` hoelzl@64283 ` 57` ```proof - ``` hoelzl@64283 ` 58` ``` obtain A :: "nat \ 'a set" where "range A \ sets M" "(\i. A i) = space M" "\i. emeasure M (A i) \ \" ``` hoelzl@64283 ` 59` ``` using sigma_finite by auto ``` hoelzl@64283 ` 60` ``` then have [measurable]:"A n \ sets M" for n by auto ``` hoelzl@64283 ` 61` ``` define g where "g = (\x. (\n. (1/2)^(Suc n) * indicator (A n) x / (1+ measure M (A n))))" ``` hoelzl@64283 ` 62` ``` have [measurable]: "g \ borel_measurable M" unfolding g_def by auto ``` hoelzl@64283 ` 63` ``` have *: "summable (\n. (1/2)^(Suc n) * indicator (A n) x / (1+ measure M (A n)))" for x ``` hoelzl@64283 ` 64` ``` apply (rule summable_comparison_test'[of "\n. (1/2)^(Suc n)" 0]) ``` hoelzl@64283 ` 65` ``` using power_half_series summable_def by (auto simp add: indicator_def divide_simps) ``` hoelzl@64283 ` 66` ``` have "g x \ (\n. (1/2)^(Suc n))" for x unfolding g_def ``` hoelzl@64283 ` 67` ``` apply (rule suminf_le) using * power_half_series summable_def by (auto simp add: indicator_def divide_simps) ``` hoelzl@64283 ` 68` ``` then have g_le_1: "g x \ 1" for x using power_half_series sums_unique by fastforce ``` hoelzl@64283 ` 69` hoelzl@64283 ` 70` ``` have g_pos: "g x > 0" if "x \ space M" for x ``` hoelzl@64283 ` 71` ``` unfolding g_def proof (subst suminf_pos_iff[OF *[of x]], auto) ``` wenzelm@64911 ` 72` ``` obtain i where "x \ A i" using \(\i. A i) = space M\ \x \ space M\ by auto ``` hoelzl@64283 ` 73` ``` then have "0 < (1 / 2) ^ Suc i * indicator (A i) x / (1 + Sigma_Algebra.measure M (A i))" ``` hoelzl@64283 ` 74` ``` unfolding indicator_def apply (auto simp add: divide_simps) using measure_nonneg[of M "A i"] ``` hoelzl@64283 ` 75` ``` by (auto, meson add_nonneg_nonneg linorder_not_le mult_nonneg_nonneg zero_le_numeral zero_le_one zero_le_power) ``` hoelzl@64283 ` 76` ``` then show "\i. 0 < (1 / 2) ^ i * indicator (A i) x / (2 + 2 * Sigma_Algebra.measure M (A i))" ``` hoelzl@64283 ` 77` ``` by auto ``` hoelzl@64283 ` 78` ``` qed ``` hoelzl@64283 ` 79` hoelzl@64283 ` 80` ``` have "integrable M g" ``` hoelzl@64283 ` 81` ``` unfolding g_def proof (rule integrable_suminf) ``` hoelzl@64283 ` 82` ``` fix n ``` hoelzl@64283 ` 83` ``` show "integrable M (\x. (1 / 2) ^ Suc n * indicator (A n) x / (1 + Sigma_Algebra.measure M (A n)))" ``` wenzelm@64911 ` 84` ``` using \emeasure M (A n) \ \\ ``` hoelzl@64283 ` 85` ``` by (auto intro!: integrable_mult_right integrable_divide_zero integrable_real_indicator simp add: top.not_eq_extremum) ``` hoelzl@64283 ` 86` ``` next ``` hoelzl@64283 ` 87` ``` show "AE x in M. summable (\n. norm ((1 / 2) ^ Suc n * indicator (A n) x / (1 + Sigma_Algebra.measure M (A n))))" ``` hoelzl@64283 ` 88` ``` using * by auto ``` hoelzl@64283 ` 89` ``` show "summable (\n. (\x. norm ((1 / 2) ^ Suc n * indicator (A n) x / (1 + Sigma_Algebra.measure M (A n))) \M))" ``` hoelzl@64283 ` 90` ``` apply (rule summable_comparison_test'[of "\n. (1/2)^(Suc n)" 0], auto) ``` hoelzl@64283 ` 91` ``` using power_half_series summable_def apply auto[1] ``` hoelzl@64283 ` 92` ``` apply (auto simp add: divide_simps) using measure_nonneg[of M] not_less by fastforce ``` hoelzl@64283 ` 93` ``` qed ``` hoelzl@64283 ` 94` hoelzl@64283 ` 95` ``` define f where "f = (\x. if x \ space M then g x else 1)" ``` hoelzl@64283 ` 96` ``` have "f x > 0" for x unfolding f_def using g_pos by auto ``` hoelzl@64283 ` 97` ``` moreover have "f x \ 1" for x unfolding f_def using g_le_1 by auto ``` hoelzl@64283 ` 98` ``` moreover have [measurable]: "f \ borel_measurable M" unfolding f_def by auto ``` hoelzl@64283 ` 99` ``` moreover have "integrable M f" ``` wenzelm@64911 ` 100` ``` apply (subst integrable_cong[of _ _ _ g]) unfolding f_def using \integrable M g\ by auto ``` hoelzl@64283 ` 101` ``` ultimately show "(\f. f \ borel_measurable M \ (\x. 0 < f x) \ (\x. f x \ 1) \ integrable M f \ thesis) \ thesis" ``` hoelzl@64283 ` 102` ``` by (meson that) ``` hoelzl@64283 ` 103` ```qed ``` hoelzl@64283 ` 104` hoelzl@38656 ` 105` ```lemma (in sigma_finite_measure) Ex_finite_integrable_function: ``` hoelzl@62975 ` 106` ``` "\h\borel_measurable M. integral\<^sup>N M h \ \ \ (\x\space M. 0 < h x \ h x < \)" ``` hoelzl@38656 ` 107` ```proof - ``` hoelzl@38656 ` 108` ``` obtain A :: "nat \ 'a set" where ``` hoelzl@50003 ` 109` ``` range[measurable]: "range A \ sets M" and ``` hoelzl@38656 ` 110` ``` space: "(\i. A i) = space M" and ``` hoelzl@47694 ` 111` ``` measure: "\i. emeasure M (A i) \ \" and ``` hoelzl@38656 ` 112` ``` disjoint: "disjoint_family A" ``` haftmann@62343 ` 113` ``` using sigma_finite_disjoint by blast ``` hoelzl@47694 ` 114` ``` let ?B = "\i. 2^Suc i * emeasure M (A i)" ``` hoelzl@63329 ` 115` ``` have [measurable]: "\i. A i \ sets M" ``` hoelzl@63329 ` 116` ``` using range by fastforce+ ``` hoelzl@38656 ` 117` ``` have "\i. \x. 0 < x \ x < inverse (?B i)" ``` hoelzl@38656 ` 118` ``` proof ``` hoelzl@47694 ` 119` ``` fix i show "\x. 0 < x \ x < inverse (?B i)" ``` hoelzl@62975 ` 120` ``` using measure[of i] ``` hoelzl@62975 ` 121` ``` by (auto intro!: dense simp: ennreal_inverse_positive ennreal_mult_eq_top_iff power_eq_top_ennreal) ``` hoelzl@38656 ` 122` ``` qed ``` hoelzl@38656 ` 123` ``` from choice[OF this] obtain n where n: "\i. 0 < n i" ``` hoelzl@47694 ` 124` ``` "\i. n i < inverse (2^Suc i * emeasure M (A i))" by auto ``` hoelzl@41981 ` 125` ``` { fix i have "0 \ n i" using n(1)[of i] by auto } note pos = this ``` wenzelm@46731 ` 126` ``` let ?h = "\x. \i. n i * indicator (A i) x" ``` hoelzl@38656 ` 127` ``` show ?thesis ``` hoelzl@38656 ` 128` ``` proof (safe intro!: bexI[of _ ?h] del: notI) ``` hoelzl@63329 ` 129` ``` have "integral\<^sup>N M ?h = (\i. n i * emeasure M (A i))" using pos ``` hoelzl@56996 ` 130` ``` by (simp add: nn_integral_suminf nn_integral_cmult_indicator) ``` hoelzl@62975 ` 131` ``` also have "\ \ (\i. ennreal ((1/2)^Suc i))" ``` hoelzl@62975 ` 132` ``` proof (intro suminf_le allI) ``` hoelzl@41981 ` 133` ``` fix N ``` hoelzl@47694 ` 134` ``` have "n N * emeasure M (A N) \ inverse (2^Suc N * emeasure M (A N)) * emeasure M (A N)" ``` hoelzl@62975 ` 135` ``` using n[of N] by (intro mult_right_mono) auto ``` hoelzl@62975 ` 136` ``` also have "\ = (1/2)^Suc N * (inverse (emeasure M (A N)) * emeasure M (A N))" ``` hoelzl@62975 ` 137` ``` using measure[of N] ``` hoelzl@62975 ` 138` ``` by (simp add: ennreal_inverse_power divide_ennreal_def ennreal_inverse_mult ``` hoelzl@62975 ` 139` ``` power_eq_top_ennreal less_top[symmetric] mult_ac ``` hoelzl@62975 ` 140` ``` del: power_Suc) ``` hoelzl@62975 ` 141` ``` also have "\ \ inverse (ennreal 2) ^ Suc N" ``` hoelzl@62975 ` 142` ``` using measure[of N] ``` hoelzl@63329 ` 143` ``` by (cases "emeasure M (A N)"; cases "emeasure M (A N) = 0") ``` hoelzl@63329 ` 144` ``` (auto simp: inverse_ennreal ennreal_mult[symmetric] divide_ennreal_def simp del: power_Suc) ``` hoelzl@62975 ` 145` ``` also have "\ = ennreal (inverse 2 ^ Suc N)" ``` hoelzl@62975 ` 146` ``` by (subst ennreal_power[symmetric], simp) (simp add: inverse_ennreal) ``` hoelzl@62975 ` 147` ``` finally show "n N * emeasure M (A N) \ ennreal ((1/2)^Suc N)" ``` hoelzl@62975 ` 148` ``` by simp ``` hoelzl@62975 ` 149` ``` qed auto ``` hoelzl@62975 ` 150` ``` also have "\ < top" ``` hoelzl@62975 ` 151` ``` unfolding less_top[symmetric] ``` hoelzl@63329 ` 152` ``` by (rule ennreal_suminf_neq_top) ``` hoelzl@63329 ` 153` ``` (auto simp: summable_geometric summable_Suc_iff simp del: power_Suc) ``` hoelzl@62975 ` 154` ``` finally show "integral\<^sup>N M ?h \ \" ``` hoelzl@62975 ` 155` ``` by (auto simp: top_unique) ``` hoelzl@38656 ` 156` ``` next ``` hoelzl@41981 ` 157` ``` { fix x assume "x \ space M" ``` hoelzl@41981 ` 158` ``` then obtain i where "x \ A i" using space[symmetric] by auto ``` hoelzl@41981 ` 159` ``` with disjoint n have "?h x = n i" ``` hoelzl@41981 ` 160` ``` by (auto intro!: suminf_cmult_indicator intro: less_imp_le) ``` hoelzl@62975 ` 161` ``` then show "0 < ?h x" and "?h x < \" using n[of i] by (auto simp: less_top[symmetric]) } ``` hoelzl@41981 ` 162` ``` note pos = this ``` hoelzl@50003 ` 163` ``` qed measurable ``` hoelzl@38656 ` 164` ```qed ``` hoelzl@38656 ` 165` hoelzl@40871 ` 166` ```subsection "Absolutely continuous" ``` hoelzl@40871 ` 167` hoelzl@47694 ` 168` ```definition absolutely_continuous :: "'a measure \ 'a measure \ bool" where ``` hoelzl@47694 ` 169` ``` "absolutely_continuous M N \ null_sets M \ null_sets N" ``` hoelzl@47694 ` 170` hoelzl@47694 ` 171` ```lemma absolutely_continuousI_count_space: "absolutely_continuous (count_space A) M" ``` hoelzl@47694 ` 172` ``` unfolding absolutely_continuous_def by (auto simp: null_sets_count_space) ``` hoelzl@38656 ` 173` hoelzl@47694 ` 174` ```lemma absolutely_continuousI_density: ``` hoelzl@47694 ` 175` ``` "f \ borel_measurable M \ absolutely_continuous M (density M f)" ``` hoelzl@47694 ` 176` ``` by (force simp add: absolutely_continuous_def null_sets_density_iff dest: AE_not_in) ``` hoelzl@47694 ` 177` hoelzl@47694 ` 178` ```lemma absolutely_continuousI_point_measure_finite: ``` hoelzl@47694 ` 179` ``` "(\x. \ x \ A ; f x \ 0 \ \ g x \ 0) \ absolutely_continuous (point_measure A f) (point_measure A g)" ``` hoelzl@47694 ` 180` ``` unfolding absolutely_continuous_def by (force simp: null_sets_point_measure_iff) ``` hoelzl@47694 ` 181` hoelzl@63330 ` 182` ```lemma absolutely_continuousD: ``` hoelzl@63330 ` 183` ``` "absolutely_continuous M N \ A \ sets M \ emeasure M A = 0 \ emeasure N A = 0" ``` hoelzl@63330 ` 184` ``` by (auto simp: absolutely_continuous_def null_sets_def) ``` hoelzl@63330 ` 185` hoelzl@47694 ` 186` ```lemma absolutely_continuous_AE: ``` hoelzl@47694 ` 187` ``` assumes sets_eq: "sets M' = sets M" ``` hoelzl@47694 ` 188` ``` and "absolutely_continuous M M'" "AE x in M. P x" ``` hoelzl@41981 ` 189` ``` shows "AE x in M'. P x" ``` hoelzl@40859 ` 190` ```proof - ``` wenzelm@61808 ` 191` ``` from \AE x in M. P x\ obtain N where N: "N \ null_sets M" "{x\space M. \ P x} \ N" ``` hoelzl@47694 ` 192` ``` unfolding eventually_ae_filter by auto ``` hoelzl@41981 ` 193` ``` show "AE x in M'. P x" ``` hoelzl@47694 ` 194` ``` proof (rule AE_I') ``` hoelzl@47694 ` 195` ``` show "{x\space M'. \ P x} \ N" using sets_eq_imp_space_eq[OF sets_eq] N(2) by simp ``` wenzelm@61808 ` 196` ``` from \absolutely_continuous M M'\ show "N \ null_sets M'" ``` hoelzl@47694 ` 197` ``` using N unfolding absolutely_continuous_def sets_eq null_sets_def by auto ``` hoelzl@40859 ` 198` ``` qed ``` hoelzl@40859 ` 199` ```qed ``` hoelzl@40859 ` 200` hoelzl@40871 ` 201` ```subsection "Existence of the Radon-Nikodym derivative" ``` hoelzl@40871 ` 202` hoelzl@38656 ` 203` ```lemma (in finite_measure) Radon_Nikodym_finite_measure: ``` hoelzl@63330 ` 204` ``` assumes "finite_measure N" and sets_eq[simp]: "sets N = sets M" ``` hoelzl@47694 ` 205` ``` assumes "absolutely_continuous M N" ``` hoelzl@63329 ` 206` ``` shows "\f \ borel_measurable M. density M f = N" ``` hoelzl@38656 ` 207` ```proof - ``` hoelzl@47694 ` 208` ``` interpret N: finite_measure N by fact ``` hoelzl@63329 ` 209` ``` define G where "G = {g \ borel_measurable M. \A\sets M. (\\<^sup>+x. g x * indicator A x \M) \ N A}" ``` hoelzl@63330 ` 210` ``` have [measurable_dest]: "f \ G \ f \ borel_measurable M" ``` hoelzl@63330 ` 211` ``` and G_D: "\A. f \ G \ A \ sets M \ (\\<^sup>+x. f x * indicator A x \M) \ N A" for f ``` hoelzl@63330 ` 212` ``` by (auto simp: G_def) ``` hoelzl@50003 ` 213` ``` note this[measurable_dest] ``` hoelzl@38656 ` 214` ``` have "(\x. 0) \ G" unfolding G_def by auto ``` hoelzl@38656 ` 215` ``` hence "G \ {}" by auto ``` hoelzl@63329 ` 216` ``` { fix f g assume f[measurable]: "f \ G" and g[measurable]: "g \ G" ``` hoelzl@38656 ` 217` ``` have "(\x. max (g x) (f x)) \ G" (is "?max \ G") unfolding G_def ``` hoelzl@38656 ` 218` ``` proof safe ``` hoelzl@38656 ` 219` ``` let ?A = "{x \ space M. f x \ g x}" ``` hoelzl@38656 ` 220` ``` have "?A \ sets M" using f g unfolding G_def by auto ``` hoelzl@63329 ` 221` ``` fix A assume [measurable]: "A \ sets M" ``` hoelzl@38656 ` 222` ``` have union: "((?A \ A) \ ((space M - ?A) \ A)) = A" ``` wenzelm@61808 ` 223` ``` using sets.sets_into_space[OF \A \ sets M\] by auto ``` hoelzl@38656 ` 224` ``` have "\x. x \ space M \ max (g x) (f x) * indicator A x = ``` hoelzl@38656 ` 225` ``` g x * indicator (?A \ A) x + f x * indicator ((space M - ?A) \ A) x" ``` hoelzl@38656 ` 226` ``` by (auto simp: indicator_def max_def) ``` wenzelm@53015 ` 227` ``` hence "(\\<^sup>+x. max (g x) (f x) * indicator A x \M) = ``` wenzelm@53015 ` 228` ``` (\\<^sup>+x. g x * indicator (?A \ A) x \M) + ``` wenzelm@53015 ` 229` ``` (\\<^sup>+x. f x * indicator ((space M - ?A) \ A) x \M)" ``` hoelzl@56996 ` 230` ``` by (auto cong: nn_integral_cong intro!: nn_integral_add) ``` hoelzl@47694 ` 231` ``` also have "\ \ N (?A \ A) + N ((space M - ?A) \ A)" ``` hoelzl@63329 ` 232` ``` using f g unfolding G_def by (auto intro!: add_mono) ``` hoelzl@47694 ` 233` ``` also have "\ = N A" ``` hoelzl@63330 ` 234` ``` using union by (subst plus_emeasure) auto ``` wenzelm@53015 ` 235` ``` finally show "(\\<^sup>+x. max (g x) (f x) * indicator A x \M) \ N A" . ``` hoelzl@63329 ` 236` ``` qed auto } ``` hoelzl@38656 ` 237` ``` note max_in_G = this ``` hoelzl@41981 ` 238` ``` { fix f assume "incseq f" and f: "\i. f i \ G" ``` hoelzl@50003 ` 239` ``` then have [measurable]: "\i. f i \ borel_measurable M" by (auto simp: G_def) ``` hoelzl@41981 ` 240` ``` have "(\x. SUP i. f i x) \ G" unfolding G_def ``` hoelzl@38656 ` 241` ``` proof safe ``` hoelzl@50003 ` 242` ``` show "(\x. SUP i. f i x) \ borel_measurable M" by measurable ``` hoelzl@41981 ` 243` ``` next ``` hoelzl@38656 ` 244` ``` fix A assume "A \ sets M" ``` wenzelm@53015 ` 245` ``` have "(\\<^sup>+x. (SUP i. f i x) * indicator A x \M) = ``` wenzelm@53015 ` 246` ``` (\\<^sup>+x. (SUP i. f i x * indicator A x) \M)" ``` hoelzl@56996 ` 247` ``` by (intro nn_integral_cong) (simp split: split_indicator) ``` wenzelm@53015 ` 248` ``` also have "\ = (SUP i. (\\<^sup>+x. f i x * indicator A x \M))" ``` wenzelm@61808 ` 249` ``` using \incseq f\ f \A \ sets M\ ``` hoelzl@56996 ` 250` ``` by (intro nn_integral_monotone_convergence_SUP) ``` hoelzl@41981 ` 251` ``` (auto simp: G_def incseq_Suc_iff le_fun_def split: split_indicator) ``` wenzelm@53015 ` 252` ``` finally show "(\\<^sup>+x. (SUP i. f i x) * indicator A x \M) \ N A" ``` hoelzl@63330 ` 253` ``` using f \A \ sets M\ by (auto intro!: SUP_least simp: G_D) ``` hoelzl@38656 ` 254` ``` qed } ``` hoelzl@38656 ` 255` ``` note SUP_in_G = this ``` hoelzl@56996 ` 256` ``` let ?y = "SUP g : G. integral\<^sup>N M g" ``` hoelzl@47694 ` 257` ``` have y_le: "?y \ N (space M)" unfolding G_def ``` hoelzl@44928 ` 258` ``` proof (safe intro!: SUP_least) ``` wenzelm@53015 ` 259` ``` fix g assume "\A\sets M. (\\<^sup>+x. g x * indicator A x \M) \ N A" ``` hoelzl@56996 ` 260` ``` from this[THEN bspec, OF sets.top] show "integral\<^sup>N M g \ N (space M)" ``` hoelzl@56996 ` 261` ``` by (simp cong: nn_integral_cong) ``` hoelzl@38656 ` 262` ``` qed ``` hoelzl@62975 ` 263` ``` from ennreal_SUP_countable_SUP [OF \G \ {}\, of "integral\<^sup>N M"] guess ys .. note ys = this ``` hoelzl@56996 ` 264` ``` then have "\n. \g. g\G \ integral\<^sup>N M g = ys n" ``` hoelzl@38656 ` 265` ``` proof safe ``` hoelzl@56996 ` 266` ``` fix n assume "range ys \ integral\<^sup>N M ` G" ``` hoelzl@56996 ` 267` ``` hence "ys n \ integral\<^sup>N M ` G" by auto ``` hoelzl@56996 ` 268` ``` thus "\g. g\G \ integral\<^sup>N M g = ys n" by auto ``` hoelzl@38656 ` 269` ``` qed ``` hoelzl@56996 ` 270` ``` from choice[OF this] obtain gs where "\i. gs i \ G" "\n. integral\<^sup>N M (gs n) = ys n" by auto ``` hoelzl@56996 ` 271` ``` hence y_eq: "?y = (SUP i. integral\<^sup>N M (gs i))" using ys by auto ``` wenzelm@46731 ` 272` ``` let ?g = "\i x. Max ((\n. gs n x) ` {..i})" ``` wenzelm@63040 ` 273` ``` define f where [abs_def]: "f x = (SUP i. ?g i x)" for x ``` wenzelm@46731 ` 274` ``` let ?F = "\A x. f x * indicator A x" ``` hoelzl@41981 ` 275` ``` have gs_not_empty: "\i x. (\n. gs n x) ` {..i} \ {}" by auto ``` hoelzl@38656 ` 276` ``` { fix i have "?g i \ G" ``` hoelzl@38656 ` 277` ``` proof (induct i) ``` hoelzl@38656 ` 278` ``` case 0 thus ?case by simp fact ``` hoelzl@38656 ` 279` ``` next ``` hoelzl@38656 ` 280` ``` case (Suc i) ``` wenzelm@61808 ` 281` ``` with Suc gs_not_empty \gs (Suc i) \ G\ show ?case ``` hoelzl@38656 ` 282` ``` by (auto simp add: atMost_Suc intro!: max_in_G) ``` hoelzl@38656 ` 283` ``` qed } ``` hoelzl@38656 ` 284` ``` note g_in_G = this ``` hoelzl@41981 ` 285` ``` have "incseq ?g" using gs_not_empty ``` hoelzl@41981 ` 286` ``` by (auto intro!: incseq_SucI le_funI simp add: atMost_Suc) ``` hoelzl@63330 ` 287` hoelzl@50003 ` 288` ``` from SUP_in_G[OF this g_in_G] have [measurable]: "f \ G" unfolding f_def . ``` hoelzl@63330 ` 289` ``` then have [measurable]: "f \ borel_measurable M" unfolding G_def by auto ``` hoelzl@63330 ` 290` hoelzl@56996 ` 291` ``` have "integral\<^sup>N M f = (SUP i. integral\<^sup>N M (?g i))" unfolding f_def ``` hoelzl@63330 ` 292` ``` using g_in_G \incseq ?g\ by (auto intro!: nn_integral_monotone_convergence_SUP simp: G_def) ``` hoelzl@38656 ` 293` ``` also have "\ = ?y" ``` hoelzl@38656 ` 294` ``` proof (rule antisym) ``` hoelzl@56996 ` 295` ``` show "(SUP i. integral\<^sup>N M (?g i)) \ ?y" ``` haftmann@56166 ` 296` ``` using g_in_G by (auto intro: SUP_mono) ``` hoelzl@56996 ` 297` ``` show "?y \ (SUP i. integral\<^sup>N M (?g i))" unfolding y_eq ``` hoelzl@56996 ` 298` ``` by (auto intro!: SUP_mono nn_integral_mono Max_ge) ``` hoelzl@38656 ` 299` ``` qed ``` hoelzl@56996 ` 300` ``` finally have int_f_eq_y: "integral\<^sup>N M f = ?y" . ``` hoelzl@47694 ` 301` hoelzl@63330 ` 302` ``` have upper_bound: "\A\sets M. N A \ density M f A" ``` hoelzl@38656 ` 303` ``` proof (rule ccontr) ``` hoelzl@38656 ` 304` ``` assume "\ ?thesis" ``` hoelzl@63330 ` 305` ``` then obtain A where A[measurable]: "A \ sets M" and f_less_N: "density M f A < N A" ``` hoelzl@63330 ` 306` ``` by (auto simp: not_le) ``` hoelzl@63330 ` 307` ``` then have pos_A: "0 < M A" ``` hoelzl@63330 ` 308` ``` using \absolutely_continuous M N\[THEN absolutely_continuousD, OF A] ``` hoelzl@62975 ` 309` ``` by (auto simp: zero_less_iff_neq_zero) ``` hoelzl@63330 ` 310` hoelzl@63330 ` 311` ``` define b where "b = (N A - density M f A) / M A / 2" ``` hoelzl@63330 ` 312` ``` with f_less_N pos_A have "0 < b" "b \ top" ``` hoelzl@63330 ` 313` ``` by (auto intro!: diff_gr0_ennreal simp: zero_less_iff_neq_zero diff_eq_0_iff_ennreal ennreal_divide_eq_top_iff) ``` hoelzl@63330 ` 314` hoelzl@63330 ` 315` ``` let ?f = "\x. f x + b" ``` hoelzl@63330 ` 316` ``` have "nn_integral M f \ top" ``` wenzelm@64911 ` 317` ``` using \f \ G\[THEN G_D, of "space M"] by (auto simp: top_unique cong: nn_integral_cong) ``` hoelzl@63330 ` 318` ``` with \b \ top\ interpret Mf: finite_measure "density M ?f" ``` hoelzl@63330 ` 319` ``` by (intro finite_measureI) ``` hoelzl@63330 ` 320` ``` (auto simp: field_simps mult_indicator_subset ennreal_mult_eq_top_iff ``` hoelzl@63330 ` 321` ``` emeasure_density nn_integral_cmult_indicator nn_integral_add ``` hoelzl@63330 ` 322` ``` cong: nn_integral_cong) ``` hoelzl@63330 ` 323` hoelzl@63330 ` 324` ``` from unsigned_Hahn_decomposition[of "density M ?f" N A] ``` hoelzl@63330 ` 325` ``` obtain Y where [measurable]: "Y \ sets M" and [simp]: "Y \ A" ``` hoelzl@63330 ` 326` ``` and Y1: "\C. C \ sets M \ C \ Y \ density M ?f C \ N C" ``` hoelzl@63330 ` 327` ``` and Y2: "\C. C \ sets M \ C \ A \ C \ Y = {} \ N C \ density M ?f C" ``` hoelzl@63330 ` 328` ``` by auto ``` hoelzl@63330 ` 329` hoelzl@63330 ` 330` ``` let ?f' = "\x. f x + b * indicator Y x" ``` hoelzl@63330 ` 331` ``` have "M Y \ 0" ``` hoelzl@63330 ` 332` ``` proof ``` hoelzl@63330 ` 333` ``` assume "M Y = 0" ``` hoelzl@63330 ` 334` ``` then have "N Y = 0" ``` hoelzl@63330 ` 335` ``` using \absolutely_continuous M N\[THEN absolutely_continuousD, of Y] by auto ``` hoelzl@63330 ` 336` ``` then have "N A = N (A - Y)" ``` hoelzl@63330 ` 337` ``` by (subst emeasure_Diff) auto ``` hoelzl@63330 ` 338` ``` also have "\ \ density M ?f (A - Y)" ``` hoelzl@63330 ` 339` ``` by (rule Y2) auto ``` hoelzl@63330 ` 340` ``` also have "\ \ density M ?f A - density M ?f Y" ``` hoelzl@63330 ` 341` ``` by (subst emeasure_Diff) auto ``` hoelzl@63330 ` 342` ``` also have "\ \ density M ?f A - 0" ``` hoelzl@63330 ` 343` ``` by (intro ennreal_minus_mono) auto ``` hoelzl@63330 ` 344` ``` also have "density M ?f A = b * M A + density M f A" ``` hoelzl@63330 ` 345` ``` by (simp add: emeasure_density field_simps mult_indicator_subset nn_integral_add nn_integral_cmult_indicator) ``` hoelzl@63330 ` 346` ``` also have "\ < N A" ``` hoelzl@63330 ` 347` ``` using f_less_N pos_A ``` hoelzl@63330 ` 348` ``` by (cases "density M f A"; cases "M A"; cases "N A") ``` hoelzl@63330 ` 349` ``` (auto simp: b_def ennreal_less_iff ennreal_minus divide_ennreal ennreal_numeral[symmetric] ``` hoelzl@63330 ` 350` ``` ennreal_plus[symmetric] ennreal_mult[symmetric] field_simps ``` hoelzl@63330 ` 351` ``` simp del: ennreal_numeral ennreal_plus) ``` hoelzl@63330 ` 352` ``` finally show False ``` hoelzl@63330 ` 353` ``` by simp ``` hoelzl@63330 ` 354` ``` qed ``` hoelzl@63330 ` 355` ``` then have "nn_integral M f < nn_integral M ?f'" ``` hoelzl@63330 ` 356` ``` using \0 < b\ \nn_integral M f \ top\ ``` hoelzl@63330 ` 357` ``` by (simp add: nn_integral_add nn_integral_cmult_indicator ennreal_zero_less_mult_iff zero_less_iff_neq_zero) ``` hoelzl@38656 ` 358` ``` moreover ``` hoelzl@63330 ` 359` ``` have "?f' \ G" ``` hoelzl@63330 ` 360` ``` unfolding G_def ``` hoelzl@63330 ` 361` ``` proof safe ``` hoelzl@63330 ` 362` ``` fix X assume [measurable]: "X \ sets M" ``` hoelzl@63330 ` 363` ``` have "(\\<^sup>+ x. ?f' x * indicator X x \M) = density M f (X - Y) + density M ?f (X \ Y)" ``` hoelzl@63330 ` 364` ``` by (auto simp add: emeasure_density nn_integral_add[symmetric] split: split_indicator intro!: nn_integral_cong) ``` hoelzl@63330 ` 365` ``` also have "\ \ N (X - Y) + N (X \ Y)" ``` hoelzl@63330 ` 366` ``` using G_D[OF \f \ G\] by (intro add_mono Y1) (auto simp: emeasure_density) ``` hoelzl@63330 ` 367` ``` also have "\ = N X" ``` hoelzl@63330 ` 368` ``` by (subst plus_emeasure) (auto intro!: arg_cong2[where f=emeasure]) ``` hoelzl@63330 ` 369` ``` finally show "(\\<^sup>+ x. ?f' x * indicator X x \M) \ N X" . ``` hoelzl@63330 ` 370` ``` qed simp ``` hoelzl@63330 ` 371` ``` then have "nn_integral M ?f' \ ?y" ``` hoelzl@63330 ` 372` ``` by (rule SUP_upper) ``` hoelzl@63330 ` 373` ``` ultimately show False ``` hoelzl@63330 ` 374` ``` by (simp add: int_f_eq_y) ``` hoelzl@38656 ` 375` ``` qed ``` hoelzl@38656 ` 376` ``` show ?thesis ``` hoelzl@63330 ` 377` ``` proof (intro bexI[of _ f] measure_eqI conjI antisym) ``` hoelzl@63330 ` 378` ``` fix A assume "A \ sets (density M f)" then show "emeasure (density M f) A \ emeasure N A" ``` hoelzl@63330 ` 379` ``` by (auto simp: emeasure_density intro!: G_D[OF \f \ G\]) ``` hoelzl@63330 ` 380` ``` next ``` hoelzl@63330 ` 381` ``` fix A assume A: "A \ sets (density M f)" then show "emeasure N A \ emeasure (density M f) A" ``` hoelzl@63330 ` 382` ``` using upper_bound by auto ``` hoelzl@47694 ` 383` ``` qed auto ``` hoelzl@38656 ` 384` ```qed ``` hoelzl@38656 ` 385` hoelzl@40859 ` 386` ```lemma (in finite_measure) split_space_into_finite_sets_and_rest: ``` hoelzl@63330 ` 387` ``` assumes ac: "absolutely_continuous M N" and sets_eq[simp]: "sets N = sets M" ``` hoelzl@63330 ` 388` ``` shows "\B::nat\'a set. disjoint_family B \ range B \ sets M \ (\i. N (B i) \ \) \ ``` hoelzl@63330 ` 389` ``` (\A\sets M. A \ (\i. B i) = {} \ (emeasure M A = 0 \ N A = 0) \ (emeasure M A > 0 \ N A = \))" ``` hoelzl@38656 ` 390` ```proof - ``` hoelzl@47694 ` 391` ``` let ?Q = "{Q\sets M. N Q \ \}" ``` hoelzl@47694 ` 392` ``` let ?a = "SUP Q:?Q. emeasure M Q" ``` hoelzl@47694 ` 393` ``` have "{} \ ?Q" by auto ``` hoelzl@38656 ` 394` ``` then have Q_not_empty: "?Q \ {}" by blast ``` immler@50244 ` 395` ``` have "?a \ emeasure M (space M)" using sets.sets_into_space ``` hoelzl@47694 ` 396` ``` by (auto intro!: SUP_least emeasure_mono) ``` hoelzl@62975 ` 397` ``` then have "?a \ \" ``` hoelzl@62975 ` 398` ``` using finite_emeasure_space ``` hoelzl@62975 ` 399` ``` by (auto simp: less_top[symmetric] top_unique simp del: SUP_eq_top_iff Sup_eq_top_iff) ``` hoelzl@62975 ` 400` ``` from ennreal_SUP_countable_SUP [OF Q_not_empty, of "emeasure M"] ``` hoelzl@47694 ` 401` ``` obtain Q'' where "range Q'' \ emeasure M ` ?Q" and a: "?a = (SUP i::nat. Q'' i)" ``` hoelzl@38656 ` 402` ``` by auto ``` hoelzl@47694 ` 403` ``` then have "\i. \Q'. Q'' i = emeasure M Q' \ Q' \ ?Q" by auto ``` hoelzl@47694 ` 404` ``` from choice[OF this] obtain Q' where Q': "\i. Q'' i = emeasure M (Q' i)" "\i. Q' i \ ?Q" ``` hoelzl@38656 ` 405` ``` by auto ``` hoelzl@47694 ` 406` ``` then have a_Lim: "?a = (SUP i::nat. emeasure M (Q' i))" using a by simp ``` wenzelm@46731 ` 407` ``` let ?O = "\n. \i\n. Q' i" ``` hoelzl@47694 ` 408` ``` have Union: "(SUP i. emeasure M (?O i)) = emeasure M (\i. ?O i)" ``` hoelzl@47694 ` 409` ``` proof (rule SUP_emeasure_incseq[of ?O]) ``` hoelzl@47694 ` 410` ``` show "range ?O \ sets M" using Q' by auto ``` nipkow@44890 ` 411` ``` show "incseq ?O" by (fastforce intro!: incseq_SucI) ``` hoelzl@38656 ` 412` ``` qed ``` hoelzl@63330 ` 413` ``` have Q'_sets[measurable]: "\i. Q' i \ sets M" using Q' by auto ``` hoelzl@47694 ` 414` ``` have O_sets: "\i. ?O i \ sets M" using Q' by auto ``` hoelzl@38656 ` 415` ``` then have O_in_G: "\i. ?O i \ ?Q" ``` hoelzl@38656 ` 416` ``` proof (safe del: notI) ``` hoelzl@47694 ` 417` ``` fix i have "Q' ` {..i} \ sets M" using Q' by auto ``` hoelzl@47694 ` 418` ``` then have "N (?O i) \ (\i\i. N (Q' i))" ``` hoelzl@63330 ` 419` ``` by (simp add: emeasure_subadditive_finite) ``` hoelzl@62975 ` 420` ``` also have "\ < \" using Q' by (simp add: less_top) ``` hoelzl@47694 ` 421` ``` finally show "N (?O i) \ \" by simp ``` hoelzl@38656 ` 422` ``` qed auto ``` nipkow@44890 ` 423` ``` have O_mono: "\n. ?O n \ ?O (Suc n)" by fastforce ``` hoelzl@47694 ` 424` ``` have a_eq: "?a = emeasure M (\i. ?O i)" unfolding Union[symmetric] ``` hoelzl@38656 ` 425` ``` proof (rule antisym) ``` hoelzl@47694 ` 426` ``` show "?a \ (SUP i. emeasure M (?O i))" unfolding a_Lim ``` hoelzl@47694 ` 427` ``` using Q' by (auto intro!: SUP_mono emeasure_mono) ``` haftmann@62343 ` 428` ``` show "(SUP i. emeasure M (?O i)) \ ?a" ``` hoelzl@38656 ` 429` ``` proof (safe intro!: Sup_mono, unfold bex_simps) ``` hoelzl@38656 ` 430` ``` fix i ``` haftmann@52141 ` 431` ``` have *: "(\(Q' ` {..i})) = ?O i" by auto ``` hoelzl@47694 ` 432` ``` then show "\x. (x \ sets M \ N x \ \) \ ``` haftmann@52141 ` 433` ``` emeasure M (\(Q' ` {..i})) \ emeasure M x" ``` hoelzl@38656 ` 434` ``` using O_in_G[of i] by (auto intro!: exI[of _ "?O i"]) ``` hoelzl@38656 ` 435` ``` qed ``` hoelzl@38656 ` 436` ``` qed ``` wenzelm@46731 ` 437` ``` let ?O_0 = "(\i. ?O i)" ``` hoelzl@38656 ` 438` ``` have "?O_0 \ sets M" using Q' by auto ``` hoelzl@63330 ` 439` ``` have "disjointed Q' i \ sets M" for i ``` hoelzl@63330 ` 440` ``` using sets.range_disjointed_sets[of Q' M] using Q'_sets by (auto simp: subset_eq) ``` hoelzl@38656 ` 441` ``` note Q_sets = this ``` hoelzl@40859 ` 442` ``` show ?thesis ``` hoelzl@40859 ` 443` ``` proof (intro bexI exI conjI ballI impI allI) ``` hoelzl@63330 ` 444` ``` show "disjoint_family (disjointed Q')" ``` hoelzl@63330 ` 445` ``` by (rule disjoint_family_disjointed) ``` hoelzl@63330 ` 446` ``` show "range (disjointed Q') \ sets M" ``` hoelzl@63330 ` 447` ``` using Q'_sets by (intro sets.range_disjointed_sets) auto ``` hoelzl@63330 ` 448` ``` { fix A assume A: "A \ sets M" "A \ (\i. disjointed Q' i) = {}" ``` hoelzl@63330 ` 449` ``` then have A1: "A \ (\i. Q' i) = {}" ``` hoelzl@63330 ` 450` ``` unfolding UN_disjointed_eq by auto ``` hoelzl@47694 ` 451` ``` show "emeasure M A = 0 \ N A = 0 \ 0 < emeasure M A \ N A = \" ``` hoelzl@40859 ` 452` ``` proof (rule disjCI, simp) ``` hoelzl@62975 ` 453` ``` assume *: "emeasure M A = 0 \ N A \ top" ``` hoelzl@47694 ` 454` ``` show "emeasure M A = 0 \ N A = 0" ``` wenzelm@53374 ` 455` ``` proof (cases "emeasure M A = 0") ``` wenzelm@53374 ` 456` ``` case True ``` wenzelm@53374 ` 457` ``` with ac A have "N A = 0" ``` hoelzl@40859 ` 458` ``` unfolding absolutely_continuous_def by auto ``` wenzelm@53374 ` 459` ``` with True show ?thesis by simp ``` hoelzl@40859 ` 460` ``` next ``` wenzelm@53374 ` 461` ``` case False ``` hoelzl@62975 ` 462` ``` with * have "N A \ \" by auto ``` hoelzl@47694 ` 463` ``` with A have "emeasure M ?O_0 + emeasure M A = emeasure M (?O_0 \ A)" ``` hoelzl@63330 ` 464` ``` using Q' A1 by (auto intro!: plus_emeasure simp: set_eq_iff) ``` hoelzl@47694 ` 465` ``` also have "\ = (SUP i. emeasure M (?O i \ A))" ``` hoelzl@47694 ` 466` ``` proof (rule SUP_emeasure_incseq[of "\i. ?O i \ A", symmetric, simplified]) ``` hoelzl@40859 ` 467` ``` show "range (\i. ?O i \ A) \ sets M" ``` wenzelm@61808 ` 468` ``` using \N A \ \\ O_sets A by auto ``` nipkow@44890 ` 469` ``` qed (fastforce intro!: incseq_SucI) ``` hoelzl@40859 ` 470` ``` also have "\ \ ?a" ``` hoelzl@44928 ` 471` ``` proof (safe intro!: SUP_least) ``` hoelzl@40859 ` 472` ``` fix i have "?O i \ A \ ?Q" ``` hoelzl@40859 ` 473` ``` proof (safe del: notI) ``` hoelzl@40859 ` 474` ``` show "?O i \ A \ sets M" using O_sets A by auto ``` hoelzl@47694 ` 475` ``` from O_in_G[of i] have "N (?O i \ A) \ N (?O i) + N A" ``` hoelzl@63330 ` 476` ``` using emeasure_subadditive[of "?O i" N A] A O_sets by auto ``` hoelzl@47694 ` 477` ``` with O_in_G[of i] show "N (?O i \ A) \ \" ``` hoelzl@62975 ` 478` ``` using \N A \ \\ by (auto simp: top_unique) ``` hoelzl@40859 ` 479` ``` qed ``` hoelzl@47694 ` 480` ``` then show "emeasure M (?O i \ A) \ ?a" by (rule SUP_upper) ``` hoelzl@40859 ` 481` ``` qed ``` hoelzl@47694 ` 482` ``` finally have "emeasure M A = 0" ``` hoelzl@47694 ` 483` ``` unfolding a_eq using measure_nonneg[of M A] by (simp add: emeasure_eq_measure) ``` wenzelm@61808 ` 484` ``` with \emeasure M A \ 0\ show ?thesis by auto ``` hoelzl@40859 ` 485` ``` qed ``` hoelzl@40859 ` 486` ``` qed } ``` hoelzl@63330 ` 487` ``` { fix i ``` hoelzl@63330 ` 488` ``` have "N (disjointed Q' i) \ N (Q' i)" ``` hoelzl@63330 ` 489` ``` by (auto intro!: emeasure_mono simp: disjointed_def) ``` hoelzl@63330 ` 490` ``` then show "N (disjointed Q' i) \ \" ``` hoelzl@63330 ` 491` ``` using Q'(2)[of i] by (auto simp: top_unique) } ``` hoelzl@40859 ` 492` ``` qed ``` hoelzl@40859 ` 493` ```qed ``` hoelzl@40859 ` 494` hoelzl@40859 ` 495` ```lemma (in finite_measure) Radon_Nikodym_finite_measure_infinite: ``` hoelzl@47694 ` 496` ``` assumes "absolutely_continuous M N" and sets_eq: "sets N = sets M" ``` hoelzl@63329 ` 497` ``` shows "\f\borel_measurable M. density M f = N" ``` hoelzl@40859 ` 498` ```proof - ``` hoelzl@40859 ` 499` ``` from split_space_into_finite_sets_and_rest[OF assms] ``` hoelzl@63330 ` 500` ``` obtain Q :: "nat \ 'a set" ``` hoelzl@40859 ` 501` ``` where Q: "disjoint_family Q" "range Q \ sets M" ``` hoelzl@63330 ` 502` ``` and in_Q0: "\A. A \ sets M \ A \ (\i. Q i) = {} \ emeasure M A = 0 \ N A = 0 \ 0 < emeasure M A \ N A = \" ``` hoelzl@47694 ` 503` ``` and Q_fin: "\i. N (Q i) \ \" by force ``` hoelzl@40859 ` 504` ``` from Q have Q_sets: "\i. Q i \ sets M" by auto ``` hoelzl@47694 ` 505` ``` let ?N = "\i. density N (indicator (Q i))" and ?M = "\i. density M (indicator (Q i))" ``` hoelzl@63329 ` 506` ``` have "\i. \f\borel_measurable (?M i). density (?M i) f = ?N i" ``` hoelzl@47694 ` 507` ``` proof (intro allI finite_measure.Radon_Nikodym_finite_measure) ``` hoelzl@38656 ` 508` ``` fix i ``` hoelzl@47694 ` 509` ``` from Q show "finite_measure (?M i)" ``` hoelzl@56996 ` 510` ``` by (auto intro!: finite_measureI cong: nn_integral_cong ``` hoelzl@47694 ` 511` ``` simp add: emeasure_density subset_eq sets_eq) ``` hoelzl@47694 ` 512` ``` from Q have "emeasure (?N i) (space N) = emeasure N (Q i)" ``` hoelzl@56996 ` 513` ``` by (simp add: sets_eq[symmetric] emeasure_density subset_eq cong: nn_integral_cong) ``` hoelzl@47694 ` 514` ``` with Q_fin show "finite_measure (?N i)" ``` hoelzl@47694 ` 515` ``` by (auto intro!: finite_measureI) ``` hoelzl@47694 ` 516` ``` show "sets (?N i) = sets (?M i)" by (simp add: sets_eq) ``` hoelzl@50003 ` 517` ``` have [measurable]: "\A. A \ sets M \ A \ sets N" by (simp add: sets_eq) ``` hoelzl@47694 ` 518` ``` show "absolutely_continuous (?M i) (?N i)" ``` wenzelm@61808 ` 519` ``` using \absolutely_continuous M N\ \Q i \ sets M\ ``` hoelzl@47694 ` 520` ``` by (auto simp: absolutely_continuous_def null_sets_density_iff sets_eq ``` hoelzl@47694 ` 521` ``` intro!: absolutely_continuous_AE[OF sets_eq]) ``` hoelzl@38656 ` 522` ``` qed ``` hoelzl@47694 ` 523` ``` from choice[OF this[unfolded Bex_def]] ``` hoelzl@47694 ` 524` ``` obtain f where borel: "\i. f i \ borel_measurable M" "\i x. 0 \ f i x" ``` hoelzl@47694 ` 525` ``` and f_density: "\i. density (?M i) (f i) = ?N i" ``` immler@54776 ` 526` ``` by force ``` hoelzl@47694 ` 527` ``` { fix A i assume A: "A \ sets M" ``` wenzelm@53015 ` 528` ``` with Q borel have "(\\<^sup>+x. f i x * indicator (Q i \ A) x \M) = emeasure (density (?M i) (f i)) A" ``` hoelzl@56996 ` 529` ``` by (auto simp add: emeasure_density nn_integral_density subset_eq ``` hoelzl@56996 ` 530` ``` intro!: nn_integral_cong split: split_indicator) ``` hoelzl@47694 ` 531` ``` also have "\ = emeasure N (Q i \ A)" ``` hoelzl@47694 ` 532` ``` using A Q by (simp add: f_density emeasure_restricted subset_eq sets_eq) ``` wenzelm@53015 ` 533` ``` finally have "emeasure N (Q i \ A) = (\\<^sup>+x. f i x * indicator (Q i \ A) x \M)" .. } ``` hoelzl@47694 ` 534` ``` note integral_eq = this ``` hoelzl@63330 ` 535` ``` let ?f = "\x. (\i. f i x * indicator (Q i) x) + \ * indicator (space M - (\i. Q i)) x" ``` hoelzl@38656 ` 536` ``` show ?thesis ``` hoelzl@38656 ` 537` ``` proof (safe intro!: bexI[of _ ?f]) ``` hoelzl@63330 ` 538` ``` show "?f \ borel_measurable M" using borel Q_sets ``` hoelzl@41981 ` 539` ``` by (auto intro!: measurable_If) ``` hoelzl@47694 ` 540` ``` show "density M ?f = N" ``` hoelzl@47694 ` 541` ``` proof (rule measure_eqI) ``` hoelzl@47694 ` 542` ``` fix A assume "A \ sets (density M ?f)" ``` hoelzl@47694 ` 543` ``` then have "A \ sets M" by simp ``` hoelzl@47694 ` 544` ``` have Qi: "\i. Q i \ sets M" using Q by auto ``` hoelzl@47694 ` 545` ``` have [intro,simp]: "\i. (\x. f i x * indicator (Q i \ A) x) \ borel_measurable M" ``` hoelzl@47694 ` 546` ``` "\i. AE x in M. 0 \ f i x * indicator (Q i \ A) x" ``` hoelzl@63330 ` 547` ``` using borel Qi \A \ sets M\ by auto ``` hoelzl@63330 ` 548` ``` have "(\\<^sup>+x. ?f x * indicator A x \M) = (\\<^sup>+x. (\i. f i x * indicator (Q i \ A) x) + \ * indicator ((space M - (\i. Q i)) \ A) x \M)" ``` hoelzl@56996 ` 549` ``` using borel by (intro nn_integral_cong) (auto simp: indicator_def) ``` hoelzl@63330 ` 550` ``` also have "\ = (\\<^sup>+x. (\i. f i x * indicator (Q i \ A) x) \M) + \ * emeasure M ((space M - (\i. Q i)) \ A)" ``` hoelzl@63330 ` 551` ``` using borel Qi \A \ sets M\ ``` hoelzl@62975 ` 552` ``` by (subst nn_integral_add) ``` hoelzl@62975 ` 553` ``` (auto simp add: nn_integral_cmult_indicator sets.Int intro!: suminf_0_le) ``` hoelzl@63330 ` 554` ``` also have "\ = (\i. N (Q i \ A)) + \ * emeasure M ((space M - (\i. Q i)) \ A)" ``` wenzelm@61808 ` 555` ``` by (subst integral_eq[OF \A \ sets M\], subst nn_integral_suminf) auto ``` hoelzl@63330 ` 556` ``` finally have "(\\<^sup>+x. ?f x * indicator A x \M) = (\i. N (Q i \ A)) + \ * emeasure M ((space M - (\i. Q i)) \ A)" . ``` hoelzl@47694 ` 557` ``` moreover have "(\i. N (Q i \ A)) = N ((\i. Q i) \ A)" ``` wenzelm@61808 ` 558` ``` using Q Q_sets \A \ sets M\ ``` hoelzl@47694 ` 559` ``` by (subst suminf_emeasure) (auto simp: disjoint_family_on_def sets_eq) ``` hoelzl@63330 ` 560` ``` moreover ``` hoelzl@63330 ` 561` ``` have "(space M - (\x. Q x)) \ A \ (\x. Q x) = {}" ``` hoelzl@63330 ` 562` ``` by auto ``` hoelzl@63330 ` 563` ``` then have "\ * emeasure M ((space M - (\i. Q i)) \ A) = N ((space M - (\i. Q i)) \ A)" ``` hoelzl@63330 ` 564` ``` using in_Q0[of "(space M - (\i. Q i)) \ A"] \A \ sets M\ Q by (auto simp: ennreal_top_mult) ``` hoelzl@63330 ` 565` ``` moreover have "(space M - (\i. Q i)) \ A \ sets M" "((\i. Q i) \ A) \ sets M" ``` hoelzl@63330 ` 566` ``` using Q_sets \A \ sets M\ by auto ``` hoelzl@63330 ` 567` ``` moreover have "((\i. Q i) \ A) \ ((space M - (\i. Q i)) \ A) = A" "((\i. Q i) \ A) \ ((space M - (\i. Q i)) \ A) = {}" ``` hoelzl@63330 ` 568` ``` using \A \ sets M\ sets.sets_into_space by auto ``` wenzelm@53015 ` 569` ``` ultimately have "N A = (\\<^sup>+x. ?f x * indicator A x \M)" ``` hoelzl@63330 ` 570` ``` using plus_emeasure[of "(\i. Q i) \ A" N "(space M - (\i. Q i)) \ A"] by (simp add: sets_eq) ``` hoelzl@63330 ` 571` ``` with \A \ sets M\ borel Q show "emeasure (density M ?f) A = N A" ``` hoelzl@50003 ` 572` ``` by (auto simp: subset_eq emeasure_density) ``` hoelzl@47694 ` 573` ``` qed (simp add: sets_eq) ``` hoelzl@38656 ` 574` ``` qed ``` hoelzl@38656 ` 575` ```qed ``` hoelzl@38656 ` 576` hoelzl@38656 ` 577` ```lemma (in sigma_finite_measure) Radon_Nikodym: ``` hoelzl@47694 ` 578` ``` assumes ac: "absolutely_continuous M N" assumes sets_eq: "sets N = sets M" ``` hoelzl@63329 ` 579` ``` shows "\f \ borel_measurable M. density M f = N" ``` hoelzl@38656 ` 580` ```proof - ``` hoelzl@38656 ` 581` ``` from Ex_finite_integrable_function ``` hoelzl@56996 ` 582` ``` obtain h where finite: "integral\<^sup>N M h \ \" and ``` hoelzl@38656 ` 583` ``` borel: "h \ borel_measurable M" and ``` hoelzl@41981 ` 584` ``` nn: "\x. 0 \ h x" and ``` hoelzl@38656 ` 585` ``` pos: "\x. x \ space M \ 0 < h x" and ``` hoelzl@41981 ` 586` ``` "\x. x \ space M \ h x < \" by auto ``` wenzelm@53015 ` 587` ``` let ?T = "\A. (\\<^sup>+x. h x * indicator A x \M)" ``` hoelzl@47694 ` 588` ``` let ?MT = "density M h" ``` hoelzl@47694 ` 589` ``` from borel finite nn interpret T: finite_measure ?MT ``` hoelzl@56996 ` 590` ``` by (auto intro!: finite_measureI cong: nn_integral_cong simp: emeasure_density) ``` hoelzl@47694 ` 591` ``` have "absolutely_continuous ?MT N" "sets N = sets ?MT" ``` hoelzl@47694 ` 592` ``` proof (unfold absolutely_continuous_def, safe) ``` hoelzl@47694 ` 593` ``` fix A assume "A \ null_sets ?MT" ``` hoelzl@47694 ` 594` ``` with borel have "A \ sets M" "AE x in M. x \ A \ h x \ 0" ``` hoelzl@47694 ` 595` ``` by (auto simp add: null_sets_density_iff) ``` immler@50244 ` 596` ``` with pos sets.sets_into_space have "AE x in M. x \ A" ``` lp15@61810 ` 597` ``` by (elim eventually_mono) (auto simp: not_le[symmetric]) ``` hoelzl@47694 ` 598` ``` then have "A \ null_sets M" ``` wenzelm@61808 ` 599` ``` using \A \ sets M\ by (simp add: AE_iff_null_sets) ``` hoelzl@47694 ` 600` ``` with ac show "A \ null_sets N" ``` hoelzl@47694 ` 601` ``` by (auto simp: absolutely_continuous_def) ``` hoelzl@47694 ` 602` ``` qed (auto simp add: sets_eq) ``` hoelzl@47694 ` 603` ``` from T.Radon_Nikodym_finite_measure_infinite[OF this] ``` hoelzl@63329 ` 604` ``` obtain f where f_borel: "f \ borel_measurable M" "density ?MT f = N" by auto ``` hoelzl@47694 ` 605` ``` with nn borel show ?thesis ``` hoelzl@47694 ` 606` ``` by (auto intro!: bexI[of _ "\x. h x * f x"] simp: density_density_eq) ``` hoelzl@38656 ` 607` ```qed ``` hoelzl@38656 ` 608` wenzelm@61808 ` 609` ```subsection \Uniqueness of densities\ ``` hoelzl@40859 ` 610` hoelzl@47694 ` 611` ```lemma finite_density_unique: ``` hoelzl@40859 ` 612` ``` assumes borel: "f \ borel_measurable M" "g \ borel_measurable M" ``` hoelzl@47694 ` 613` ``` assumes pos: "AE x in M. 0 \ f x" "AE x in M. 0 \ g x" ``` hoelzl@56996 ` 614` ``` and fin: "integral\<^sup>N M f \ \" ``` hoelzl@49785 ` 615` ``` shows "density M f = density M g \ (AE x in M. f x = g x)" ``` hoelzl@40859 ` 616` ```proof (intro iffI ballI) ``` hoelzl@47694 ` 617` ``` fix A assume eq: "AE x in M. f x = g x" ``` hoelzl@49785 ` 618` ``` with borel show "density M f = density M g" ``` hoelzl@49785 ` 619` ``` by (auto intro: density_cong) ``` hoelzl@40859 ` 620` ```next ``` wenzelm@53015 ` 621` ``` let ?P = "\f A. \\<^sup>+ x. f x * indicator A x \M" ``` hoelzl@49785 ` 622` ``` assume "density M f = density M g" ``` hoelzl@49785 ` 623` ``` with borel have eq: "\A\sets M. ?P f A = ?P g A" ``` hoelzl@49785 ` 624` ``` by (simp add: emeasure_density[symmetric]) ``` immler@50244 ` 625` ``` from this[THEN bspec, OF sets.top] fin ``` hoelzl@56996 ` 626` ``` have g_fin: "integral\<^sup>N M g \ \" by (simp cong: nn_integral_cong) ``` hoelzl@40859 ` 627` ``` { fix f g assume borel: "f \ borel_measurable M" "g \ borel_measurable M" ``` hoelzl@47694 ` 628` ``` and pos: "AE x in M. 0 \ f x" "AE x in M. 0 \ g x" ``` hoelzl@56996 ` 629` ``` and g_fin: "integral\<^sup>N M g \ \" and eq: "\A\sets M. ?P f A = ?P g A" ``` hoelzl@40859 ` 630` ``` let ?N = "{x\space M. g x < f x}" ``` hoelzl@40859 ` 631` ``` have N: "?N \ sets M" using borel by simp ``` hoelzl@56996 ` 632` ``` have "?P g ?N \ integral\<^sup>N M g" using pos ``` hoelzl@56996 ` 633` ``` by (intro nn_integral_mono_AE) (auto split: split_indicator) ``` hoelzl@62975 ` 634` ``` then have Pg_fin: "?P g ?N \ \" using g_fin by (auto simp: top_unique) ``` wenzelm@53015 ` 635` ``` have "?P (\x. (f x - g x)) ?N = (\\<^sup>+x. f x * indicator ?N x - g x * indicator ?N x \M)" ``` hoelzl@56996 ` 636` ``` by (auto intro!: nn_integral_cong simp: indicator_def) ``` hoelzl@40859 ` 637` ``` also have "\ = ?P f ?N - ?P g ?N" ``` hoelzl@56996 ` 638` ``` proof (rule nn_integral_diff) ``` hoelzl@40859 ` 639` ``` show "(\x. f x * indicator ?N x) \ borel_measurable M" "(\x. g x * indicator ?N x) \ borel_measurable M" ``` hoelzl@40859 ` 640` ``` using borel N by auto ``` hoelzl@47694 ` 641` ``` show "AE x in M. g x * indicator ?N x \ f x * indicator ?N x" ``` hoelzl@41981 ` 642` ``` using pos by (auto split: split_indicator) ``` hoelzl@41981 ` 643` ``` qed fact ``` hoelzl@40859 ` 644` ``` also have "\ = 0" ``` hoelzl@62975 ` 645` ``` unfolding eq[THEN bspec, OF N] using Pg_fin by auto ``` hoelzl@47694 ` 646` ``` finally have "AE x in M. f x \ g x" ``` hoelzl@56996 ` 647` ``` using pos borel nn_integral_PInf_AE[OF borel(2) g_fin] ``` hoelzl@56996 ` 648` ``` by (subst (asm) nn_integral_0_iff_AE) ``` hoelzl@62975 ` 649` ``` (auto split: split_indicator simp: not_less ennreal_minus_eq_0) } ``` hoelzl@41981 ` 650` ``` from this[OF borel pos g_fin eq] this[OF borel(2,1) pos(2,1) fin] eq ``` hoelzl@47694 ` 651` ``` show "AE x in M. f x = g x" by auto ``` hoelzl@40859 ` 652` ```qed ``` hoelzl@40859 ` 653` hoelzl@40859 ` 654` ```lemma (in finite_measure) density_unique_finite_measure: ``` hoelzl@40859 ` 655` ``` assumes borel: "f \ borel_measurable M" "f' \ borel_measurable M" ``` hoelzl@47694 ` 656` ``` assumes pos: "AE x in M. 0 \ f x" "AE x in M. 0 \ f' x" ``` wenzelm@53015 ` 657` ``` assumes f: "\A. A \ sets M \ (\\<^sup>+x. f x * indicator A x \M) = (\\<^sup>+x. f' x * indicator A x \M)" ``` hoelzl@40859 ` 658` ``` (is "\A. A \ sets M \ ?P f A = ?P f' A") ``` hoelzl@47694 ` 659` ``` shows "AE x in M. f x = f' x" ``` hoelzl@40859 ` 660` ```proof - ``` hoelzl@47694 ` 661` ``` let ?D = "\f. density M f" ``` hoelzl@47694 ` 662` ``` let ?N = "\A. ?P f A" and ?N' = "\A. ?P f' A" ``` wenzelm@46731 ` 663` ``` let ?f = "\A x. f x * indicator A x" and ?f' = "\A x. f' x * indicator A x" ``` hoelzl@47694 ` 664` hoelzl@47694 ` 665` ``` have ac: "absolutely_continuous M (density M f)" "sets (density M f) = sets M" ``` lp15@61609 ` 666` ``` using borel by (auto intro!: absolutely_continuousI_density) ``` hoelzl@47694 ` 667` ``` from split_space_into_finite_sets_and_rest[OF this] ``` hoelzl@63330 ` 668` ``` obtain Q :: "nat \ 'a set" ``` hoelzl@40859 ` 669` ``` where Q: "disjoint_family Q" "range Q \ sets M" ``` hoelzl@63330 ` 670` ``` and in_Q0: "\A. A \ sets M \ A \ (\i. Q i) = {} \ emeasure M A = 0 \ ?D f A = 0 \ 0 < emeasure M A \ ?D f A = \" ``` hoelzl@47694 ` 671` ``` and Q_fin: "\i. ?D f (Q i) \ \" by force ``` hoelzl@63330 ` 672` ``` with borel pos have in_Q0: "\A. A \ sets M \ A \ (\i. Q i) = {} \ emeasure M A = 0 \ ?N A = 0 \ 0 < emeasure M A \ ?N A = \" ``` hoelzl@47694 ` 673` ``` and Q_fin: "\i. ?N (Q i) \ \" by (auto simp: emeasure_density subset_eq) ``` hoelzl@47694 ` 674` hoelzl@63330 ` 675` ``` from Q have Q_sets[measurable]: "\i. Q i \ sets M" by auto ``` hoelzl@47694 ` 676` ``` let ?D = "{x\space M. f x \ f' x}" ``` hoelzl@47694 ` 677` ``` have "?D \ sets M" using borel by auto ``` hoelzl@62975 ` 678` ``` have *: "\i x A. \y::ennreal. y * indicator (Q i) x * indicator A x = y * indicator (Q i \ A) x" ``` hoelzl@40859 ` 679` ``` unfolding indicator_def by auto ``` hoelzl@47694 ` 680` ``` have "\i. AE x in M. ?f (Q i) x = ?f' (Q i) x" using borel Q_fin Q pos ``` hoelzl@40859 ` 681` ``` by (intro finite_density_unique[THEN iffD1] allI) ``` hoelzl@50003 ` 682` ``` (auto intro!: f measure_eqI simp: emeasure_density * subset_eq) ``` hoelzl@63330 ` 683` ``` moreover have "AE x in M. ?f (space M - (\i. Q i)) x = ?f' (space M - (\i. Q i)) x" ``` hoelzl@40859 ` 684` ``` proof (rule AE_I') ``` hoelzl@62975 ` 685` ``` { fix f :: "'a \ ennreal" assume borel: "f \ borel_measurable M" ``` wenzelm@53015 ` 686` ``` and eq: "\A. A \ sets M \ ?N A = (\\<^sup>+x. f x * indicator A x \M)" ``` hoelzl@63330 ` 687` ``` let ?A = "\i. (space M - (\i. Q i)) \ {x \ space M. f x < (i::nat)}" ``` hoelzl@47694 ` 688` ``` have "(\i. ?A i) \ null_sets M" ``` hoelzl@40859 ` 689` ``` proof (rule null_sets_UN) ``` hoelzl@43923 ` 690` ``` fix i ::nat have "?A i \ sets M" ``` hoelzl@63330 ` 691` ``` using borel by auto ``` hoelzl@62975 ` 692` ``` have "?N (?A i) \ (\\<^sup>+x. (i::ennreal) * indicator (?A i) x \M)" ``` wenzelm@61808 ` 693` ``` unfolding eq[OF \?A i \ sets M\] ``` hoelzl@56996 ` 694` ``` by (auto intro!: nn_integral_mono simp: indicator_def) ``` hoelzl@47694 ` 695` ``` also have "\ = i * emeasure M (?A i)" ``` wenzelm@61808 ` 696` ``` using \?A i \ sets M\ by (auto intro!: nn_integral_cmult_indicator) ``` hoelzl@62975 ` 697` ``` also have "\ < \" using emeasure_real[of "?A i"] by (auto simp: ennreal_mult_less_top of_nat_less_top) ``` hoelzl@47694 ` 698` ``` finally have "?N (?A i) \ \" by simp ``` wenzelm@61808 ` 699` ``` then show "?A i \ null_sets M" using in_Q0[OF \?A i \ sets M\] \?A i \ sets M\ by auto ``` hoelzl@40859 ` 700` ``` qed ``` hoelzl@63330 ` 701` ``` also have "(\i. ?A i) = (space M - (\i. Q i)) \ {x\space M. f x \ \}" ``` hoelzl@62975 ` 702` ``` by (auto simp: ennreal_Ex_less_of_nat less_top[symmetric]) ``` hoelzl@63330 ` 703` ``` finally have "(space M - (\i. Q i)) \ {x\space M. f x \ \} \ null_sets M" by simp } ``` hoelzl@40859 ` 704` ``` from this[OF borel(1) refl] this[OF borel(2) f] ``` hoelzl@63330 ` 705` ``` have "(space M - (\i. Q i)) \ {x\space M. f x \ \} \ null_sets M" "(space M - (\i. Q i)) \ {x\space M. f' x \ \} \ null_sets M" by simp_all ``` hoelzl@63330 ` 706` ``` then show "((space M - (\i. Q i)) \ {x\space M. f x \ \}) \ ((space M - (\i. Q i)) \ {x\space M. f' x \ \}) \ null_sets M" by (rule null_sets.Un) ``` hoelzl@63330 ` 707` ``` show "{x \ space M. ?f (space M - (\i. Q i)) x \ ?f' (space M - (\i. Q i)) x} \ ``` hoelzl@63330 ` 708` ``` ((space M - (\i. Q i)) \ {x\space M. f x \ \}) \ ((space M - (\i. Q i)) \ {x\space M. f' x \ \})" by (auto simp: indicator_def) ``` hoelzl@40859 ` 709` ``` qed ``` hoelzl@63330 ` 710` ``` moreover have "AE x in M. (?f (space M - (\i. Q i)) x = ?f' (space M - (\i. Q i)) x) \ (\i. ?f (Q i) x = ?f' (Q i) x) \ ``` hoelzl@40859 ` 711` ``` ?f (space M) x = ?f' (space M) x" ``` hoelzl@63330 ` 712` ``` by (auto simp: indicator_def) ``` hoelzl@47694 ` 713` ``` ultimately have "AE x in M. ?f (space M) x = ?f' (space M) x" ``` hoelzl@47694 ` 714` ``` unfolding AE_all_countable[symmetric] ``` hoelzl@63330 ` 715` ``` by eventually_elim (auto split: if_split_asm simp: indicator_def) ``` hoelzl@47694 ` 716` ``` then show "AE x in M. f x = f' x" by auto ``` hoelzl@40859 ` 717` ```qed ``` hoelzl@40859 ` 718` hoelzl@40859 ` 719` ```lemma (in sigma_finite_measure) density_unique: ``` hoelzl@62975 ` 720` ``` assumes f: "f \ borel_measurable M" ``` hoelzl@62975 ` 721` ``` assumes f': "f' \ borel_measurable M" ``` hoelzl@47694 ` 722` ``` assumes density_eq: "density M f = density M f'" ``` hoelzl@47694 ` 723` ``` shows "AE x in M. f x = f' x" ``` hoelzl@40859 ` 724` ```proof - ``` hoelzl@40859 ` 725` ``` obtain h where h_borel: "h \ borel_measurable M" ``` hoelzl@56996 ` 726` ``` and fin: "integral\<^sup>N M h \ \" and pos: "\x. x \ space M \ 0 < h x \ h x < \" "\x. 0 \ h x" ``` hoelzl@40859 ` 727` ``` using Ex_finite_integrable_function by auto ``` hoelzl@47694 ` 728` ``` then have h_nn: "AE x in M. 0 \ h x" by auto ``` hoelzl@47694 ` 729` ``` let ?H = "density M h" ``` hoelzl@47694 ` 730` ``` interpret h: finite_measure ?H ``` hoelzl@47694 ` 731` ``` using fin h_borel pos ``` hoelzl@56996 ` 732` ``` by (intro finite_measureI) (simp cong: nn_integral_cong emeasure_density add: fin) ``` hoelzl@47694 ` 733` ``` let ?fM = "density M f" ``` hoelzl@47694 ` 734` ``` let ?f'M = "density M f'" ``` hoelzl@40859 ` 735` ``` { fix A assume "A \ sets M" ``` hoelzl@41981 ` 736` ``` then have "{x \ space M. h x * indicator A x \ 0} = A" ``` immler@50244 ` 737` ``` using pos(1) sets.sets_into_space by (force simp: indicator_def) ``` wenzelm@53015 ` 738` ``` then have "(\\<^sup>+x. h x * indicator A x \M) = 0 \ A \ null_sets M" ``` wenzelm@61808 ` 739` ``` using h_borel \A \ sets M\ h_nn by (subst nn_integral_0_iff) auto } ``` hoelzl@40859 ` 740` ``` note h_null_sets = this ``` hoelzl@40859 ` 741` ``` { fix A assume "A \ sets M" ``` wenzelm@53015 ` 742` ``` have "(\\<^sup>+x. f x * (h x * indicator A x) \M) = (\\<^sup>+x. h x * indicator A x \?fM)" ``` wenzelm@61808 ` 743` ``` using \A \ sets M\ h_borel h_nn f f' ``` hoelzl@56996 ` 744` ``` by (intro nn_integral_density[symmetric]) auto ``` wenzelm@53015 ` 745` ``` also have "\ = (\\<^sup>+x. h x * indicator A x \?f'M)" ``` hoelzl@47694 ` 746` ``` by (simp_all add: density_eq) ``` wenzelm@53015 ` 747` ``` also have "\ = (\\<^sup>+x. f' x * (h x * indicator A x) \M)" ``` wenzelm@61808 ` 748` ``` using \A \ sets M\ h_borel h_nn f f' ``` hoelzl@56996 ` 749` ``` by (intro nn_integral_density) auto ``` wenzelm@53015 ` 750` ``` finally have "(\\<^sup>+x. h x * (f x * indicator A x) \M) = (\\<^sup>+x. h x * (f' x * indicator A x) \M)" ``` hoelzl@41981 ` 751` ``` by (simp add: ac_simps) ``` wenzelm@53015 ` 752` ``` then have "(\\<^sup>+x. (f x * indicator A x) \?H) = (\\<^sup>+x. (f' x * indicator A x) \?H)" ``` wenzelm@61808 ` 753` ``` using \A \ sets M\ h_borel h_nn f f' ``` hoelzl@56996 ` 754` ``` by (subst (asm) (1 2) nn_integral_density[symmetric]) auto } ``` hoelzl@41981 ` 755` ``` then have "AE x in ?H. f x = f' x" using h_borel h_nn f f' ``` hoelzl@62975 ` 756` ``` by (intro h.density_unique_finite_measure absolutely_continuous_AE[of M]) auto ``` hoelzl@62975 ` 757` ``` with AE_space[of M] pos show "AE x in M. f x = f' x" ``` hoelzl@62975 ` 758` ``` unfolding AE_density[OF h_borel] by auto ``` hoelzl@40859 ` 759` ```qed ``` hoelzl@40859 ` 760` hoelzl@47694 ` 761` ```lemma (in sigma_finite_measure) density_unique_iff: ``` hoelzl@62975 ` 762` ``` assumes f: "f \ borel_measurable M" and f': "f' \ borel_measurable M" ``` hoelzl@47694 ` 763` ``` shows "density M f = density M f' \ (AE x in M. f x = f' x)" ``` hoelzl@47694 ` 764` ``` using density_unique[OF assms] density_cong[OF f f'] by auto ``` hoelzl@47694 ` 765` hoelzl@49785 ` 766` ```lemma sigma_finite_density_unique: ``` hoelzl@49785 ` 767` ``` assumes borel: "f \ borel_measurable M" "g \ borel_measurable M" ``` hoelzl@49785 ` 768` ``` and fin: "sigma_finite_measure (density M f)" ``` hoelzl@49785 ` 769` ``` shows "density M f = density M g \ (AE x in M. f x = g x)" ``` hoelzl@49785 ` 770` ```proof ``` lp15@61609 ` 771` ``` assume "AE x in M. f x = g x" with borel show "density M f = density M g" ``` hoelzl@49785 ` 772` ``` by (auto intro: density_cong) ``` hoelzl@49785 ` 773` ```next ``` hoelzl@49785 ` 774` ``` assume eq: "density M f = density M g" ``` wenzelm@61605 ` 775` ``` interpret f: sigma_finite_measure "density M f" by fact ``` hoelzl@49785 ` 776` ``` from f.sigma_finite_incseq guess A . note cover = this ``` hoelzl@49785 ` 777` hoelzl@49785 ` 778` ``` have "AE x in M. \i. x \ A i \ f x = g x" ``` hoelzl@49785 ` 779` ``` unfolding AE_all_countable ``` hoelzl@49785 ` 780` ``` proof ``` hoelzl@49785 ` 781` ``` fix i ``` hoelzl@49785 ` 782` ``` have "density (density M f) (indicator (A i)) = density (density M g) (indicator (A i))" ``` hoelzl@49785 ` 783` ``` unfolding eq .. ``` wenzelm@53015 ` 784` ``` moreover have "(\\<^sup>+x. f x * indicator (A i) x \M) \ \" ``` hoelzl@49785 ` 785` ``` using cover(1) cover(3)[of i] borel by (auto simp: emeasure_density subset_eq) ``` hoelzl@49785 ` 786` ``` ultimately have "AE x in M. f x * indicator (A i) x = g x * indicator (A i) x" ``` hoelzl@62975 ` 787` ``` using borel cover(1) ``` hoelzl@62975 ` 788` ``` by (intro finite_density_unique[THEN iffD1]) (auto simp: density_density_eq subset_eq) ``` hoelzl@49785 ` 789` ``` then show "AE x in M. x \ A i \ f x = g x" ``` hoelzl@49785 ` 790` ``` by auto ``` hoelzl@49785 ` 791` ``` qed ``` hoelzl@49785 ` 792` ``` with AE_space show "AE x in M. f x = g x" ``` hoelzl@49785 ` 793` ``` apply eventually_elim ``` hoelzl@49785 ` 794` ``` using cover(2)[symmetric] ``` hoelzl@49785 ` 795` ``` apply auto ``` hoelzl@49785 ` 796` ``` done ``` hoelzl@49785 ` 797` ```qed ``` hoelzl@49785 ` 798` hoelzl@49778 ` 799` ```lemma (in sigma_finite_measure) sigma_finite_iff_density_finite': ``` hoelzl@62975 ` 800` ``` assumes f: "f \ borel_measurable M" ``` hoelzl@47694 ` 801` ``` shows "sigma_finite_measure (density M f) \ (AE x in M. f x \ \)" ``` hoelzl@47694 ` 802` ``` (is "sigma_finite_measure ?N \ _") ``` hoelzl@40859 ` 803` ```proof ``` hoelzl@41689 ` 804` ``` assume "sigma_finite_measure ?N" ``` hoelzl@47694 ` 805` ``` then interpret N: sigma_finite_measure ?N . ``` hoelzl@47694 ` 806` ``` from N.Ex_finite_integrable_function obtain h where ``` hoelzl@56996 ` 807` ``` h: "h \ borel_measurable M" "integral\<^sup>N ?N h \ \" and ``` hoelzl@62975 ` 808` ``` fin: "\x\space M. 0 < h x \ h x < \" ``` hoelzl@62975 ` 809` ``` by auto ``` hoelzl@47694 ` 810` ``` have "AE x in M. f x * h x \ \" ``` hoelzl@40859 ` 811` ``` proof (rule AE_I') ``` hoelzl@62975 ` 812` ``` have "integral\<^sup>N ?N h = (\\<^sup>+x. f x * h x \M)" ``` hoelzl@62975 ` 813` ``` using f h by (auto intro!: nn_integral_density) ``` wenzelm@53015 ` 814` ``` then have "(\\<^sup>+x. f x * h x \M) \ \" ``` hoelzl@40859 ` 815` ``` using h(2) by simp ``` hoelzl@47694 ` 816` ``` then show "(\x. f x * h x) -` {\} \ space M \ null_sets M" ``` hoelzl@62975 ` 817` ``` using f h(1) by (auto intro!: nn_integral_PInf[unfolded infinity_ennreal_def] borel_measurable_vimage) ``` hoelzl@40859 ` 818` ``` qed auto ``` hoelzl@47694 ` 819` ``` then show "AE x in M. f x \ \" ``` hoelzl@62975 ` 820` ``` using fin by (auto elim!: AE_Ball_mp simp: less_top ennreal_mult_less_top) ``` hoelzl@40859 ` 821` ```next ``` hoelzl@47694 ` 822` ``` assume AE: "AE x in M. f x \ \" ``` hoelzl@57447 ` 823` ``` from sigma_finite guess Q . note Q = this ``` wenzelm@63040 ` 824` ``` define A where "A i = ``` wenzelm@63040 ` 825` ``` f -` (case i of 0 \ {\} | Suc n \ {.. ennreal(of_nat (Suc n))}) \ space M" for i ``` hoelzl@40859 ` 826` ``` { fix i j have "A i \ Q j \ sets M" ``` hoelzl@40859 ` 827` ``` unfolding A_def using f Q ``` immler@50244 ` 828` ``` apply (rule_tac sets.Int) ``` hoelzl@41981 ` 829` ``` by (cases i) (auto intro: measurable_sets[OF f(1)]) } ``` hoelzl@40859 ` 830` ``` note A_in_sets = this ``` hoelzl@57447 ` 831` hoelzl@41689 ` 832` ``` show "sigma_finite_measure ?N" ``` wenzelm@61169 ` 833` ``` proof (standard, intro exI conjI ballI) ``` hoelzl@57447 ` 834` ``` show "countable (range (\(i, j). A i \ Q j))" ``` hoelzl@57447 ` 835` ``` by auto ``` hoelzl@57447 ` 836` ``` show "range (\(i, j). A i \ Q j) \ sets (density M f)" ``` hoelzl@57447 ` 837` ``` using A_in_sets by auto ``` hoelzl@40859 ` 838` ``` next ``` hoelzl@57447 ` 839` ``` have "\range (\(i, j). A i \ Q j) = (\i j. A i \ Q j)" ``` hoelzl@57447 ` 840` ``` by auto ``` hoelzl@40859 ` 841` ``` also have "\ = (\i. A i) \ space M" using Q by auto ``` hoelzl@40859 ` 842` ``` also have "(\i. A i) = space M" ``` hoelzl@40859 ` 843` ``` proof safe ``` hoelzl@40859 ` 844` ``` fix x assume x: "x \ space M" ``` hoelzl@40859 ` 845` ``` show "x \ (\i. A i)" ``` hoelzl@62975 ` 846` ``` proof (cases "f x" rule: ennreal_cases) ``` hoelzl@62975 ` 847` ``` case top with x show ?thesis unfolding A_def by (auto intro: exI[of _ 0]) ``` hoelzl@40859 ` 848` ``` next ``` hoelzl@41981 ` 849` ``` case (real r) ``` hoelzl@62975 ` 850` ``` with ennreal_Ex_less_of_nat[of "f x"] obtain n :: nat where "f x < n" ``` hoelzl@62975 ` 851` ``` by auto ``` hoelzl@62975 ` 852` ``` also have "n < (Suc n :: ennreal)" ``` hoelzl@62975 ` 853` ``` by simp ``` hoelzl@62975 ` 854` ``` finally show ?thesis ``` hoelzl@62975 ` 855` ``` using x real by (auto simp: A_def ennreal_of_nat_eq_real_of_nat intro!: exI[of _ "Suc n"]) ``` hoelzl@40859 ` 856` ``` qed ``` hoelzl@40859 ` 857` ``` qed (auto simp: A_def) ``` hoelzl@57447 ` 858` ``` finally show "\range (\(i, j). A i \ Q j) = space ?N" by simp ``` hoelzl@40859 ` 859` ``` next ``` hoelzl@57447 ` 860` ``` fix X assume "X \ range (\(i, j). A i \ Q j)" ``` hoelzl@57447 ` 861` ``` then obtain i j where [simp]:"X = A i \ Q j" by auto ``` wenzelm@53015 ` 862` ``` have "(\\<^sup>+x. f x * indicator (A i \ Q j) x \M) \ \" ``` hoelzl@40859 ` 863` ``` proof (cases i) ``` hoelzl@40859 ` 864` ``` case 0 ``` hoelzl@47694 ` 865` ``` have "AE x in M. f x * indicator (A i \ Q j) x = 0" ``` wenzelm@61808 ` 866` ``` using AE by (auto simp: A_def \i = 0\) ``` hoelzl@56996 ` 867` ``` from nn_integral_cong_AE[OF this] show ?thesis by simp ``` hoelzl@40859 ` 868` ``` next ``` hoelzl@40859 ` 869` ``` case (Suc n) ``` wenzelm@53015 ` 870` ``` then have "(\\<^sup>+x. f x * indicator (A i \ Q j) x \M) \ ``` hoelzl@62975 ` 871` ``` (\\<^sup>+x. (Suc n :: ennreal) * indicator (Q j) x \M)" ``` hoelzl@62975 ` 872` ``` by (auto intro!: nn_integral_mono simp: indicator_def A_def ennreal_of_nat_eq_real_of_nat) ``` hoelzl@47694 ` 873` ``` also have "\ = Suc n * emeasure M (Q j)" ``` hoelzl@56996 ` 874` ``` using Q by (auto intro!: nn_integral_cmult_indicator) ``` hoelzl@41981 ` 875` ``` also have "\ < \" ``` hoelzl@62975 ` 876` ``` using Q by (auto simp: ennreal_mult_less_top less_top of_nat_less_top) ``` hoelzl@40859 ` 877` ``` finally show ?thesis by simp ``` hoelzl@40859 ` 878` ``` qed ``` hoelzl@57447 ` 879` ``` then show "emeasure ?N X \ \" ``` hoelzl@47694 ` 880` ``` using A_in_sets Q f by (auto simp: emeasure_density) ``` hoelzl@40859 ` 881` ``` qed ``` hoelzl@40859 ` 882` ```qed ``` hoelzl@40859 ` 883` hoelzl@49778 ` 884` ```lemma (in sigma_finite_measure) sigma_finite_iff_density_finite: ``` hoelzl@49778 ` 885` ``` "f \ borel_measurable M \ sigma_finite_measure (density M f) \ (AE x in M. f x \ \)" ``` hoelzl@62975 ` 886` ``` by (subst sigma_finite_iff_density_finite') ``` hoelzl@62975 ` 887` ``` (auto simp: max_def intro!: measurable_If) ``` hoelzl@49778 ` 888` wenzelm@61808 ` 889` ```subsection \Radon-Nikodym derivative\ ``` hoelzl@38656 ` 890` hoelzl@62975 ` 891` ```definition RN_deriv :: "'a measure \ 'a measure \ 'a \ ennreal" where ``` hoelzl@56993 ` 892` ``` "RN_deriv M N = ``` hoelzl@62975 ` 893` ``` (if \f. f \ borel_measurable M \ density M f = N ``` hoelzl@62975 ` 894` ``` then SOME f. f \ borel_measurable M \ density M f = N ``` hoelzl@56993 ` 895` ``` else (\_. 0))" ``` hoelzl@38656 ` 896` lp15@61609 ` 897` ```lemma RN_derivI: ``` hoelzl@62975 ` 898` ``` assumes "f \ borel_measurable M" "density M f = N" ``` hoelzl@56993 ` 899` ``` shows "density M (RN_deriv M N) = N" ``` hoelzl@40859 ` 900` ```proof - ``` wenzelm@63540 ` 901` ``` have *: "\f. f \ borel_measurable M \ density M f = N" ``` hoelzl@56993 ` 902` ``` using assms by auto ``` wenzelm@63540 ` 903` ``` then have "density M (SOME f. f \ borel_measurable M \ density M f = N) = N" ``` hoelzl@56993 ` 904` ``` by (rule someI2_ex) auto ``` wenzelm@63540 ` 905` ``` with * show ?thesis ``` hoelzl@56993 ` 906` ``` by (auto simp: RN_deriv_def) ``` hoelzl@40859 ` 907` ```qed ``` hoelzl@40859 ` 908` hoelzl@62975 ` 909` ```lemma borel_measurable_RN_deriv[measurable]: "RN_deriv M N \ borel_measurable M" ``` hoelzl@38656 ` 910` ```proof - ``` hoelzl@62975 ` 911` ``` { assume ex: "\f. f \ borel_measurable M \ density M f = N" ``` hoelzl@62975 ` 912` ``` have 1: "(SOME f. f \ borel_measurable M \ density M f = N) \ borel_measurable M" ``` hoelzl@62975 ` 913` ``` using ex by (rule someI2_ex) auto } ``` hoelzl@62975 ` 914` ``` from this show ?thesis ``` hoelzl@56993 ` 915` ``` by (auto simp: RN_deriv_def) ``` hoelzl@38656 ` 916` ```qed ``` hoelzl@38656 ` 917` hoelzl@56993 ` 918` ```lemma density_RN_deriv_density: ``` hoelzl@62975 ` 919` ``` assumes f: "f \ borel_measurable M" ``` hoelzl@56993 ` 920` ``` shows "density M (RN_deriv M (density M f)) = density M f" ``` hoelzl@62975 ` 921` ``` by (rule RN_derivI[OF f]) simp ``` hoelzl@56993 ` 922` hoelzl@56993 ` 923` ```lemma (in sigma_finite_measure) density_RN_deriv: ``` hoelzl@56993 ` 924` ``` "absolutely_continuous M N \ sets N = sets M \ density M (RN_deriv M N) = N" ``` hoelzl@56993 ` 925` ``` by (metis RN_derivI Radon_Nikodym) ``` hoelzl@56993 ` 926` hoelzl@56996 ` 927` ```lemma (in sigma_finite_measure) RN_deriv_nn_integral: ``` hoelzl@47694 ` 928` ``` assumes N: "absolutely_continuous M N" "sets N = sets M" ``` hoelzl@40859 ` 929` ``` and f: "f \ borel_measurable M" ``` hoelzl@56996 ` 930` ``` shows "integral\<^sup>N N f = (\\<^sup>+x. RN_deriv M N x * f x \M)" ``` hoelzl@40859 ` 931` ```proof - ``` hoelzl@56996 ` 932` ``` have "integral\<^sup>N N f = integral\<^sup>N (density M (RN_deriv M N)) f" ``` hoelzl@47694 ` 933` ``` using N by (simp add: density_RN_deriv) ``` wenzelm@53015 ` 934` ``` also have "\ = (\\<^sup>+x. RN_deriv M N x * f x \M)" ``` hoelzl@62975 ` 935` ``` using f by (simp add: nn_integral_density) ``` hoelzl@47694 ` 936` ``` finally show ?thesis by simp ``` hoelzl@40859 ` 937` ```qed ``` hoelzl@40859 ` 938` hoelzl@47694 ` 939` ```lemma (in sigma_finite_measure) RN_deriv_unique: ``` hoelzl@62975 ` 940` ``` assumes f: "f \ borel_measurable M" ``` hoelzl@47694 ` 941` ``` and eq: "density M f = N" ``` hoelzl@47694 ` 942` ``` shows "AE x in M. f x = RN_deriv M N x" ``` hoelzl@49785 ` 943` ``` unfolding eq[symmetric] ``` hoelzl@56993 ` 944` ``` by (intro density_unique_iff[THEN iffD1] f borel_measurable_RN_deriv ``` hoelzl@62975 ` 945` ``` density_RN_deriv_density[symmetric]) ``` hoelzl@49785 ` 946` hoelzl@49785 ` 947` ```lemma RN_deriv_unique_sigma_finite: ``` hoelzl@62975 ` 948` ``` assumes f: "f \ borel_measurable M" ``` hoelzl@49785 ` 949` ``` and eq: "density M f = N" and fin: "sigma_finite_measure N" ``` hoelzl@49785 ` 950` ``` shows "AE x in M. f x = RN_deriv M N x" ``` hoelzl@49785 ` 951` ``` using fin unfolding eq[symmetric] ``` hoelzl@56993 ` 952` ``` by (intro sigma_finite_density_unique[THEN iffD1] f borel_measurable_RN_deriv ``` hoelzl@62975 ` 953` ``` density_RN_deriv_density[symmetric]) ``` hoelzl@47694 ` 954` hoelzl@47694 ` 955` ```lemma (in sigma_finite_measure) RN_deriv_distr: ``` hoelzl@47694 ` 956` ``` fixes T :: "'a \ 'b" ``` hoelzl@47694 ` 957` ``` assumes T: "T \ measurable M M'" and T': "T' \ measurable M' M" ``` hoelzl@47694 ` 958` ``` and inv: "\x\space M. T' (T x) = x" ``` hoelzl@50021 ` 959` ``` and ac[simp]: "absolutely_continuous (distr M M' T) (distr N M' T)" ``` hoelzl@47694 ` 960` ``` and N: "sets N = sets M" ``` hoelzl@47694 ` 961` ``` shows "AE x in M. RN_deriv (distr M M' T) (distr N M' T) (T x) = RN_deriv M N x" ``` hoelzl@41832 ` 962` ```proof (rule RN_deriv_unique) ``` hoelzl@47694 ` 963` ``` have [simp]: "sets N = sets M" by fact ``` hoelzl@47694 ` 964` ``` note sets_eq_imp_space_eq[OF N, simp] ``` hoelzl@47694 ` 965` ``` have measurable_N[simp]: "\M'. measurable N M' = measurable M M'" by (auto simp: measurable_def) ``` hoelzl@47694 ` 966` ``` { fix A assume "A \ sets M" ``` immler@50244 ` 967` ``` with inv T T' sets.sets_into_space[OF this] ``` hoelzl@47694 ` 968` ``` have "T -` T' -` A \ T -` space M' \ space M = A" ``` hoelzl@47694 ` 969` ``` by (auto simp: measurable_def) } ``` hoelzl@47694 ` 970` ``` note eq = this[simp] ``` hoelzl@47694 ` 971` ``` { fix A assume "A \ sets M" ``` immler@50244 ` 972` ``` with inv T T' sets.sets_into_space[OF this] ``` hoelzl@47694 ` 973` ``` have "(T' \ T) -` A \ space M = A" ``` hoelzl@47694 ` 974` ``` by (auto simp: measurable_def) } ``` hoelzl@47694 ` 975` ``` note eq2 = this[simp] ``` hoelzl@47694 ` 976` ``` let ?M' = "distr M M' T" and ?N' = "distr N M' T" ``` hoelzl@47694 ` 977` ``` interpret M': sigma_finite_measure ?M' ``` hoelzl@41832 ` 978` ``` proof ``` hoelzl@57447 ` 979` ``` from sigma_finite_countable guess F .. note F = this ``` hoelzl@57447 ` 980` ``` show "\A. countable A \ A \ sets (distr M M' T) \ \A = space (distr M M' T) \ (\a\A. emeasure (distr M M' T) a \ \)" ``` hoelzl@57447 ` 981` ``` proof (intro exI conjI ballI) ``` hoelzl@57447 ` 982` ``` show *: "(\A. T' -` A \ space ?M') ` F \ sets ?M'" ``` hoelzl@47694 ` 983` ``` using F T' by (auto simp: measurable_def) ``` hoelzl@57447 ` 984` ``` show "\((\A. T' -` A \ space ?M')`F) = space ?M'" ``` hoelzl@57447 ` 985` ``` using F T'[THEN measurable_space] by (auto simp: set_eq_iff) ``` hoelzl@57447 ` 986` ``` next ``` hoelzl@57447 ` 987` ``` fix X assume "X \ (\A. T' -` A \ space ?M')`F" ``` hoelzl@57447 ` 988` ``` then obtain A where [simp]: "X = T' -` A \ space ?M'" and "A \ F" by auto ``` wenzelm@61808 ` 989` ``` have "X \ sets M'" using F T' \A\F\ by auto ``` hoelzl@41832 ` 990` ``` moreover ``` wenzelm@61808 ` 991` ``` have Fi: "A \ sets M" using F \A\F\ by auto ``` hoelzl@57447 ` 992` ``` ultimately show "emeasure ?M' X \ \" ``` wenzelm@61808 ` 993` ``` using F T T' \A\F\ by (simp add: emeasure_distr) ``` hoelzl@57447 ` 994` ``` qed (insert F, auto) ``` hoelzl@41832 ` 995` ``` qed ``` hoelzl@47694 ` 996` ``` have "(RN_deriv ?M' ?N') \ T \ borel_measurable M" ``` hoelzl@50021 ` 997` ``` using T ac by measurable ``` hoelzl@47694 ` 998` ``` then show "(\x. RN_deriv ?M' ?N' (T x)) \ borel_measurable M" ``` hoelzl@41832 ` 999` ``` by (simp add: comp_def) ``` hoelzl@47694 ` 1000` hoelzl@47694 ` 1001` ``` have "N = distr N M (T' \ T)" ``` hoelzl@47694 ` 1002` ``` by (subst measure_of_of_measure[of N, symmetric]) ``` immler@50244 ` 1003` ``` (auto simp add: distr_def sets.sigma_sets_eq intro!: measure_of_eq sets.space_closed) ``` hoelzl@47694 ` 1004` ``` also have "\ = distr (distr N M' T) M T'" ``` hoelzl@47694 ` 1005` ``` using T T' by (simp add: distr_distr) ``` hoelzl@47694 ` 1006` ``` also have "\ = distr (density (distr M M' T) (RN_deriv (distr M M' T) (distr N M' T))) M T'" ``` hoelzl@47694 ` 1007` ``` using ac by (simp add: M'.density_RN_deriv) ``` hoelzl@47694 ` 1008` ``` also have "\ = density M (RN_deriv (distr M M' T) (distr N M' T) \ T)" ``` hoelzl@56993 ` 1009` ``` by (simp add: distr_density_distr[OF T T', OF inv]) ``` hoelzl@47694 ` 1010` ``` finally show "density M (\x. RN_deriv (distr M M' T) (distr N M' T) (T x)) = N" ``` hoelzl@47694 ` 1011` ``` by (simp add: comp_def) ``` hoelzl@41832 ` 1012` ```qed ``` hoelzl@41832 ` 1013` hoelzl@40859 ` 1014` ```lemma (in sigma_finite_measure) RN_deriv_finite: ``` hoelzl@47694 ` 1015` ``` assumes N: "sigma_finite_measure N" and ac: "absolutely_continuous M N" "sets N = sets M" ``` hoelzl@47694 ` 1016` ``` shows "AE x in M. RN_deriv M N x \ \" ``` hoelzl@40859 ` 1017` ```proof - ``` hoelzl@47694 ` 1018` ``` interpret N: sigma_finite_measure N by fact ``` hoelzl@47694 ` 1019` ``` from N show ?thesis ``` hoelzl@62975 ` 1020` ``` using sigma_finite_iff_density_finite[OF borel_measurable_RN_deriv, of N] density_RN_deriv[OF ac] ``` hoelzl@62975 ` 1021` ``` by simp ``` hoelzl@40859 ` 1022` ```qed ``` hoelzl@40859 ` 1023` hoelzl@40859 ` 1024` ```lemma (in sigma_finite_measure) ``` hoelzl@47694 ` 1025` ``` assumes N: "sigma_finite_measure N" and ac: "absolutely_continuous M N" "sets N = sets M" ``` hoelzl@40859 ` 1026` ``` and f: "f \ borel_measurable M" ``` hoelzl@47694 ` 1027` ``` shows RN_deriv_integrable: "integrable N f \ ``` hoelzl@62975 ` 1028` ``` integrable M (\x. enn2real (RN_deriv M N x) * f x)" (is ?integrable) ``` hoelzl@62975 ` 1029` ``` and RN_deriv_integral: "integral\<^sup>L N f = (\x. enn2real (RN_deriv M N x) * f x \M)" (is ?integral) ``` hoelzl@40859 ` 1030` ```proof - ``` hoelzl@47694 ` 1031` ``` note ac(2)[simp] and sets_eq_imp_space_eq[OF ac(2), simp] ``` hoelzl@47694 ` 1032` ``` interpret N: sigma_finite_measure N by fact ``` hoelzl@56993 ` 1033` hoelzl@62975 ` 1034` ``` have eq: "density M (RN_deriv M N) = density M (\x. enn2real (RN_deriv M N x))" ``` hoelzl@56993 ` 1035` ``` proof (rule density_cong) ``` hoelzl@56993 ` 1036` ``` from RN_deriv_finite[OF assms(1,2,3)] ``` hoelzl@62975 ` 1037` ``` show "AE x in M. RN_deriv M N x = ennreal (enn2real (RN_deriv M N x))" ``` hoelzl@62975 ` 1038` ``` by eventually_elim (auto simp: less_top) ``` hoelzl@56993 ` 1039` ``` qed (insert ac, auto) ``` hoelzl@56993 ` 1040` hoelzl@56993 ` 1041` ``` show ?integrable ``` hoelzl@56993 ` 1042` ``` apply (subst density_RN_deriv[OF ac, symmetric]) ``` hoelzl@56993 ` 1043` ``` unfolding eq ``` hoelzl@62975 ` 1044` ``` apply (intro integrable_real_density f AE_I2 enn2real_nonneg) ``` hoelzl@56993 ` 1045` ``` apply (insert ac, auto) ``` hoelzl@56993 ` 1046` ``` done ``` hoelzl@56993 ` 1047` hoelzl@56993 ` 1048` ``` show ?integral ``` hoelzl@56993 ` 1049` ``` apply (subst density_RN_deriv[OF ac, symmetric]) ``` hoelzl@56993 ` 1050` ``` unfolding eq ``` hoelzl@62975 ` 1051` ``` apply (intro integral_real_density f AE_I2 enn2real_nonneg) ``` hoelzl@56993 ` 1052` ``` apply (insert ac, auto) ``` hoelzl@56993 ` 1053` ``` done ``` hoelzl@40859 ` 1054` ```qed ``` hoelzl@40859 ` 1055` hoelzl@43340 ` 1056` ```lemma (in sigma_finite_measure) real_RN_deriv: ``` hoelzl@47694 ` 1057` ``` assumes "finite_measure N" ``` hoelzl@47694 ` 1058` ``` assumes ac: "absolutely_continuous M N" "sets N = sets M" ``` hoelzl@43340 ` 1059` ``` obtains D where "D \ borel_measurable M" ``` hoelzl@62975 ` 1060` ``` and "AE x in M. RN_deriv M N x = ennreal (D x)" ``` hoelzl@47694 ` 1061` ``` and "AE x in N. 0 < D x" ``` hoelzl@43340 ` 1062` ``` and "\x. 0 \ D x" ``` hoelzl@43340 ` 1063` ```proof ``` hoelzl@47694 ` 1064` ``` interpret N: finite_measure N by fact ``` lp15@61609 ` 1065` hoelzl@62975 ` 1066` ``` note RN = borel_measurable_RN_deriv density_RN_deriv[OF ac] ``` hoelzl@43340 ` 1067` hoelzl@47694 ` 1068` ``` let ?RN = "\t. {x \ space M. RN_deriv M N x = t}" ``` hoelzl@43340 ` 1069` hoelzl@62975 ` 1070` ``` show "(\x. enn2real (RN_deriv M N x)) \ borel_measurable M" ``` hoelzl@43340 ` 1071` ``` using RN by auto ``` hoelzl@43340 ` 1072` wenzelm@53015 ` 1073` ``` have "N (?RN \) = (\\<^sup>+ x. RN_deriv M N x * indicator (?RN \) x \M)" ``` hoelzl@62975 ` 1074` ``` using RN(1) by (subst RN(2)[symmetric]) (auto simp: emeasure_density) ``` wenzelm@53015 ` 1075` ``` also have "\ = (\\<^sup>+ x. \ * indicator (?RN \) x \M)" ``` hoelzl@56996 ` 1076` ``` by (intro nn_integral_cong) (auto simp: indicator_def) ``` hoelzl@47694 ` 1077` ``` also have "\ = \ * emeasure M (?RN \)" ``` hoelzl@56996 ` 1078` ``` using RN by (intro nn_integral_cmult_indicator) auto ``` hoelzl@47694 ` 1079` ``` finally have eq: "N (?RN \) = \ * emeasure M (?RN \)" . ``` hoelzl@43340 ` 1080` ``` moreover ``` hoelzl@47694 ` 1081` ``` have "emeasure M (?RN \) = 0" ``` hoelzl@43340 ` 1082` ``` proof (rule ccontr) ``` hoelzl@47694 ` 1083` ``` assume "emeasure M {x \ space M. RN_deriv M N x = \} \ 0" ``` hoelzl@62975 ` 1084` ``` then have "0 < emeasure M {x \ space M. RN_deriv M N x = \}" ``` hoelzl@62975 ` 1085` ``` by (auto simp: zero_less_iff_neq_zero) ``` hoelzl@62975 ` 1086` ``` with eq have "N (?RN \) = \" by (simp add: ennreal_mult_eq_top_iff) ``` hoelzl@47694 ` 1087` ``` with N.emeasure_finite[of "?RN \"] RN show False by auto ``` hoelzl@43340 ` 1088` ``` qed ``` hoelzl@47694 ` 1089` ``` ultimately have "AE x in M. RN_deriv M N x < \" ``` hoelzl@62975 ` 1090` ``` using RN by (intro AE_iff_measurable[THEN iffD2]) (auto simp: less_top[symmetric]) ``` hoelzl@62975 ` 1091` ``` then show "AE x in M. RN_deriv M N x = ennreal (enn2real (RN_deriv M N x))" ``` hoelzl@62975 ` 1092` ``` by auto ``` hoelzl@62975 ` 1093` ``` then have eq: "AE x in N. RN_deriv M N x = ennreal (enn2real (RN_deriv M N x))" ``` hoelzl@47694 ` 1094` ``` using ac absolutely_continuous_AE by auto ``` hoelzl@43340 ` 1095` hoelzl@43340 ` 1096` wenzelm@53015 ` 1097` ``` have "N (?RN 0) = (\\<^sup>+ x. RN_deriv M N x * indicator (?RN 0) x \M)" ``` hoelzl@62975 ` 1098` ``` by (subst RN(2)[symmetric]) (auto simp: emeasure_density) ``` wenzelm@53015 ` 1099` ``` also have "\ = (\\<^sup>+ x. 0 \M)" ``` hoelzl@56996 ` 1100` ``` by (intro nn_integral_cong) (auto simp: indicator_def) ``` hoelzl@47694 ` 1101` ``` finally have "AE x in N. RN_deriv M N x \ 0" ``` hoelzl@47694 ` 1102` ``` using RN by (subst AE_iff_measurable[OF _ refl]) (auto simp: ac cong: sets_eq_imp_space_eq) ``` hoelzl@62975 ` 1103` ``` with eq show "AE x in N. 0 < enn2real (RN_deriv M N x)" ``` hoelzl@62975 ` 1104` ``` by (auto simp: enn2real_positive_iff less_top[symmetric] zero_less_iff_neq_zero) ``` hoelzl@62975 ` 1105` ```qed (rule enn2real_nonneg) ``` hoelzl@43340 ` 1106` hoelzl@38656 ` 1107` ```lemma (in sigma_finite_measure) RN_deriv_singleton: ``` hoelzl@47694 ` 1108` ``` assumes ac: "absolutely_continuous M N" "sets N = sets M" ``` hoelzl@47694 ` 1109` ``` and x: "{x} \ sets M" ``` hoelzl@47694 ` 1110` ``` shows "N {x} = RN_deriv M N x * emeasure M {x}" ``` hoelzl@38656 ` 1111` ```proof - ``` wenzelm@61808 ` 1112` ``` from \{x} \ sets M\ ``` wenzelm@53015 ` 1113` ``` have "density M (RN_deriv M N) {x} = (\\<^sup>+w. RN_deriv M N x * indicator {x} w \M)" ``` hoelzl@56996 ` 1114` ``` by (auto simp: indicator_def emeasure_density intro!: nn_integral_cong) ``` hoelzl@62975 ` 1115` ``` with x density_RN_deriv[OF ac] show ?thesis ``` hoelzl@62083 ` 1116` ``` by (auto simp: max_def) ``` hoelzl@38656 ` 1117` ```qed ``` hoelzl@38656 ` 1118` hoelzl@38656 ` 1119` ```end ```