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