38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 1` ```theory Radon_Nikodym ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 2` ```imports Lebesgue_Integration ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 3` ```begin ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 4` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 5` ```lemma (in sigma_finite_measure) Ex_finite_integrable_function: ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 6` ``` shows "\h\borel_measurable M. integral\<^isup>P M h \ \ \ (\x\space M. 0 < h x \ h x < \) \ (\x. 0 \ h x)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 7` ```proof - ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 8` ``` obtain A :: "nat \ 'a set" where ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 9` ``` range: "range A \ sets M" and ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 10` ``` space: "(\i. A i) = space M" and ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 11` ``` measure: "\i. \ (A i) \ \" and ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 12` ``` disjoint: "disjoint_family A" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 13` ``` using disjoint_sigma_finite by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 14` ``` let "?B i" = "2^Suc i * \ (A i)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 15` ``` have "\i. \x. 0 < x \ x < inverse (?B i)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 16` ``` proof ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 17` ``` fix i have Ai: "A i \ sets M" using range by auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 18` ``` from measure positive_measure[OF this] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 19` ``` show "\x. 0 < x \ x < inverse (?B i)" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 20` ``` by (auto intro!: extreal_dense simp: extreal_0_gt_inverse) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 21` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 22` ``` from choice[OF this] obtain n where n: "\i. 0 < n i" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 23` ``` "\i. n i < inverse (2^Suc i * \ (A i))" by auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 24` ``` { fix i have "0 \ n i" using n(1)[of i] by auto } note pos = this ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 25` ``` let "?h x" = "\i. n i * indicator (A i) x" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 26` ``` show ?thesis ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 27` ``` proof (safe intro!: bexI[of _ ?h] del: notI) ``` 39092 98de40859858 move lemmas to correct theory files hoelzl parents: 38656 diff changeset ` 28` ``` have "\i. A i \ sets M" ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 38656 diff changeset ` 29` ``` using range by fastsimp+ ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 30` ``` then have "integral\<^isup>P M ?h = (\i. n i * \ (A i))" using pos ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 31` ``` by (simp add: positive_integral_suminf positive_integral_cmult_indicator) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 32` ``` also have "\ \ (\i. (1 / 2)^Suc i)" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 33` ``` proof (rule suminf_le_pos) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 34` ``` fix N ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 35` ``` have "n N * \ (A N) \ inverse (2^Suc N * \ (A N)) * \ (A N)" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 36` ``` using positive_measure[OF `A N \ sets M`] n[of N] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 37` ``` by (intro extreal_mult_right_mono) auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 38` ``` also have "\ \ (1 / 2) ^ Suc N" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 39` ``` using measure[of N] n[of N] ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 40` ``` by (cases rule: extreal2_cases[of "n N" "\ (A N)"]) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 41` ``` (simp_all add: inverse_eq_divide power_divide one_extreal_def extreal_power_divide) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 42` ``` finally show "n N * \ (A N) \ (1 / 2) ^ Suc N" . ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 43` ``` show "0 \ n N * \ (A N)" using n[of N] `A N \ sets M` by simp ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 44` ``` qed ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 45` ``` finally show "integral\<^isup>P M ?h \ \" unfolding suminf_half_series_extreal by auto ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 46` ``` next ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 47` ``` { fix x assume "x \ space M" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 48` ``` then obtain i where "x \ A i" using space[symmetric] by auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 49` ``` with disjoint n have "?h x = n i" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 50` ``` by (auto intro!: suminf_cmult_indicator intro: less_imp_le) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 51` ``` then show "0 < ?h x" and "?h x < \" using n[of i] by auto } ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 52` ``` note pos = this ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 53` ``` fix x show "0 \ ?h x" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 54` ``` proof cases ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 55` ``` assume "x \ space M" then show "0 \ ?h x" using pos by (auto intro: less_imp_le) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 56` ``` next ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 57` ``` assume "x \ space M" then have "\i. x \ A i" using space by auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 58` ``` then show "0 \ ?h x" by auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 59` ``` qed ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 60` ``` next ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 61` ``` show "?h \ borel_measurable M" using range n ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 62` ``` by (auto intro!: borel_measurable_psuminf borel_measurable_extreal_times extreal_0_le_mult intro: less_imp_le) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 63` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 64` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 65` 40871 688f6ff859e1 Generalized simple_functionD and less_SUP_iff. hoelzl parents: 40859 diff changeset ` 66` ```subsection "Absolutely continuous" ``` 688f6ff859e1 Generalized simple_functionD and less_SUP_iff. hoelzl parents: 40859 diff changeset ` 67` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 68` ```definition (in measure_space) ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 69` ``` "absolutely_continuous \ = (\N\null_sets. \ N = (0 :: extreal))" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 70` 41832 27cb9113b1a0 add lemma RN_deriv_vimage hoelzl parents: 41705 diff changeset ` 71` ```lemma (in measure_space) absolutely_continuous_AE: ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 72` ``` assumes "measure_space M'" and [simp]: "sets M' = sets M" "space M' = space M" ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 73` ``` and "absolutely_continuous (measure M')" "AE x. P x" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 74` ``` shows "AE x in M'. P x" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 75` ```proof - ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 76` ``` interpret \: measure_space M' by fact ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 77` ``` from `AE x. P x` obtain N where N: "N \ null_sets" and "{x\space M. \ P x} \ N" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 78` ``` unfolding almost_everywhere_def by auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 79` ``` show "AE x in M'. P x" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 80` ``` proof (rule \.AE_I') ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 81` ``` show "{x\space M'. \ P x} \ N" by simp fact ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 82` ``` from `absolutely_continuous (measure M')` show "N \ \.null_sets" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 83` ``` using N unfolding absolutely_continuous_def by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 84` ``` qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 85` ```qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 86` 39097 943c7b348524 Moved lemmas to appropriate locations hoelzl parents: 39092 diff changeset ` 87` ```lemma (in finite_measure_space) absolutely_continuousI: ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 88` ``` assumes "finite_measure_space (M\ measure := \\)" (is "finite_measure_space ?\") ``` 39097 943c7b348524 Moved lemmas to appropriate locations hoelzl parents: 39092 diff changeset ` 89` ``` assumes v: "\x. \ x \ space M ; \ {x} = 0 \ \ \ {x} = 0" ``` 943c7b348524 Moved lemmas to appropriate locations hoelzl parents: 39092 diff changeset ` 90` ``` shows "absolutely_continuous \" ``` 943c7b348524 Moved lemmas to appropriate locations hoelzl parents: 39092 diff changeset ` 91` ```proof (unfold absolutely_continuous_def sets_eq_Pow, safe) ``` 943c7b348524 Moved lemmas to appropriate locations hoelzl parents: 39092 diff changeset ` 92` ``` fix N assume "\ N = 0" "N \ space M" ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 93` ``` interpret v: finite_measure_space ?\ by fact ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 94` ``` have "\ N = measure ?\ (\x\N. {x})" by simp ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 95` ``` also have "\ = (\x\N. measure ?\ {x})" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 96` ``` proof (rule v.measure_setsum[symmetric]) ``` 39097 943c7b348524 Moved lemmas to appropriate locations hoelzl parents: 39092 diff changeset ` 97` ``` show "finite N" using `N \ space M` finite_space by (auto intro: finite_subset) ``` 943c7b348524 Moved lemmas to appropriate locations hoelzl parents: 39092 diff changeset ` 98` ``` show "disjoint_family_on (\i. {i}) N" unfolding disjoint_family_on_def by auto ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 99` ``` fix x assume "x \ N" thus "{x} \ sets ?\" using `N \ space M` sets_eq_Pow by auto ``` 39097 943c7b348524 Moved lemmas to appropriate locations hoelzl parents: 39092 diff changeset ` 100` ``` qed ``` 943c7b348524 Moved lemmas to appropriate locations hoelzl parents: 39092 diff changeset ` 101` ``` also have "\ = 0" ``` 943c7b348524 Moved lemmas to appropriate locations hoelzl parents: 39092 diff changeset ` 102` ``` proof (safe intro!: setsum_0') ``` 943c7b348524 Moved lemmas to appropriate locations hoelzl parents: 39092 diff changeset ` 103` ``` fix x assume "x \ N" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 104` ``` hence "\ {x} \ \ N" "0 \ \ {x}" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 105` ``` using sets_eq_Pow `N \ space M` positive_measure[of "{x}"] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 106` ``` by (auto intro!: measure_mono) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 107` ``` then have "\ {x} = 0" using `\ N = 0` by simp ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 108` ``` thus "measure ?\ {x} = 0" using v[of x] `x \ N` `N \ space M` by auto ``` 39097 943c7b348524 Moved lemmas to appropriate locations hoelzl parents: 39092 diff changeset ` 109` ``` qed ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 110` ``` finally show "\ N = 0" by simp ``` 39097 943c7b348524 Moved lemmas to appropriate locations hoelzl parents: 39092 diff changeset ` 111` ```qed ``` 943c7b348524 Moved lemmas to appropriate locations hoelzl parents: 39092 diff changeset ` 112` 40871 688f6ff859e1 Generalized simple_functionD and less_SUP_iff. hoelzl parents: 40859 diff changeset ` 113` ```lemma (in measure_space) density_is_absolutely_continuous: ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 114` ``` assumes "\A. A \ sets M \ \ A = (\\<^isup>+x. f x * indicator A x \M)" ``` 40871 688f6ff859e1 Generalized simple_functionD and less_SUP_iff. hoelzl parents: 40859 diff changeset ` 115` ``` shows "absolutely_continuous \" ``` 688f6ff859e1 Generalized simple_functionD and less_SUP_iff. hoelzl parents: 40859 diff changeset ` 116` ``` using assms unfolding absolutely_continuous_def ``` 688f6ff859e1 Generalized simple_functionD and less_SUP_iff. hoelzl parents: 40859 diff changeset ` 117` ``` by (simp add: positive_integral_null_set) ``` 688f6ff859e1 Generalized simple_functionD and less_SUP_iff. hoelzl parents: 40859 diff changeset ` 118` 688f6ff859e1 Generalized simple_functionD and less_SUP_iff. hoelzl parents: 40859 diff changeset ` 119` ```subsection "Existence of the Radon-Nikodym derivative" ``` 688f6ff859e1 Generalized simple_functionD and less_SUP_iff. hoelzl parents: 40859 diff changeset ` 120` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 121` ```lemma (in finite_measure) Radon_Nikodym_aux_epsilon: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 122` ``` fixes e :: real assumes "0 < e" ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 123` ``` assumes "finite_measure (M\measure := \\)" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 124` ``` shows "\A\sets M. \' (space M) - finite_measure.\' (M\measure := \\) (space M) \ ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 125` ``` \' A - finite_measure.\' (M\measure := \\) A \ ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 126` ``` (\B\sets M. B \ A \ - e < \' B - finite_measure.\' (M\measure := \\) B)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 127` ```proof - ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 128` ``` interpret M': finite_measure "M\measure := \\" by fact ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 129` ``` let "?d A" = "\' A - M'.\' A" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 130` ``` let "?A A" = "if (\B\sets M. B \ space M - A \ -e < ?d B) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 131` ``` then {} ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 132` ``` else (SOME B. B \ sets M \ B \ space M - A \ ?d B \ -e)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 133` ``` def A \ "\n. ((\B. B \ ?A B) ^^ n) {}" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 134` ``` have A_simps[simp]: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 135` ``` "A 0 = {}" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 136` ``` "\n. A (Suc n) = (A n \ ?A (A n))" unfolding A_def by simp_all ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 137` ``` { fix A assume "A \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 138` ``` have "?A A \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 139` ``` by (auto intro!: someI2[of _ _ "\A. A \ sets M"] simp: not_less) } ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 140` ``` note A'_in_sets = this ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 141` ``` { fix n have "A n \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 142` ``` proof (induct n) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 143` ``` case (Suc n) thus "A (Suc n) \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 144` ``` using A'_in_sets[of "A n"] by (auto split: split_if_asm) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 145` ``` qed (simp add: A_def) } ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 146` ``` note A_in_sets = this ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 147` ``` hence "range A \ sets M" by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 148` ``` { fix n B ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 149` ``` assume Ex: "\B. B \ sets M \ B \ space M - A n \ ?d B \ -e" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 150` ``` hence False: "\ (\B\sets M. B \ space M - A n \ -e < ?d B)" by (auto simp: not_less) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 151` ``` have "?d (A (Suc n)) \ ?d (A n) - e" unfolding A_simps if_not_P[OF False] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 152` ``` proof (rule someI2_ex[OF Ex]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 153` ``` fix B assume "B \ sets M \ B \ space M - A n \ ?d B \ - e" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 154` ``` hence "A n \ B = {}" "B \ sets M" and dB: "?d B \ -e" by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 155` ``` hence "?d (A n \ B) = ?d (A n) + ?d B" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 156` ``` using `A n \ sets M` finite_measure_Union M'.finite_measure_Union by simp ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 157` ``` also have "\ \ ?d (A n) - e" using dB by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 158` ``` finally show "?d (A n \ B) \ ?d (A n) - e" . ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 159` ``` qed } ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 160` ``` note dA_epsilon = this ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 161` ``` { fix n have "?d (A (Suc n)) \ ?d (A n)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 162` ``` proof (cases "\B. B\sets M \ B \ space M - A n \ ?d B \ - e") ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 163` ``` case True from dA_epsilon[OF this] show ?thesis using `0 < e` by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 164` ``` next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 165` ``` case False ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 166` ``` hence "\B\sets M. B \ space M - A n \ -e < ?d B" by (auto simp: not_le) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 167` ``` thus ?thesis by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 168` ``` qed } ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 169` ``` note dA_mono = this ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 170` ``` show ?thesis ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 171` ``` proof (cases "\n. \B\sets M. B \ space M - A n \ -e < ?d B") ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 172` ``` case True then obtain n where B: "\B. \ B \ sets M; B \ space M - A n\ \ -e < ?d B" by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 173` ``` show ?thesis ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 174` ``` proof (safe intro!: bexI[of _ "space M - A n"]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 175` ``` fix B assume "B \ sets M" "B \ space M - A n" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 176` ``` from B[OF this] show "-e < ?d B" . ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 177` ``` next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 178` ``` show "space M - A n \ sets M" by (rule compl_sets) fact ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 179` ``` next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 180` ``` show "?d (space M) \ ?d (space M - A n)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 181` ``` proof (induct n) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 182` ``` fix n assume "?d (space M) \ ?d (space M - A n)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 183` ``` also have "\ \ ?d (space M - A (Suc n))" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 184` ``` using A_in_sets sets_into_space dA_mono[of n] ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 185` ``` by (simp del: A_simps add: finite_measure_Diff M'.finite_measure_Diff) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 186` ``` finally show "?d (space M) \ ?d (space M - A (Suc n))" . ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 187` ``` qed simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 188` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 189` ``` next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 190` ``` case False hence B: "\n. \B. B\sets M \ B \ space M - A n \ ?d B \ - e" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 191` ``` by (auto simp add: not_less) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 192` ``` { fix n have "?d (A n) \ - real n * e" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 193` ``` proof (induct n) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 194` ``` case (Suc n) with dA_epsilon[of n, OF B] show ?case by (simp del: A_simps add: real_of_nat_Suc field_simps) ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 195` ``` next ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 196` ``` case 0 with M'.empty_measure show ?case by (simp add: zero_extreal_def) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 197` ``` qed } note dA_less = this ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 198` ``` have decseq: "decseq (\n. ?d (A n))" unfolding decseq_eq_incseq ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 199` ``` proof (rule incseq_SucI) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 200` ``` fix n show "- ?d (A n) \ - ?d (A (Suc n))" using dA_mono[of n] by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 201` ``` qed ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 202` ``` have A: "incseq A" by (auto intro!: incseq_SucI) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 203` ``` from finite_continuity_from_below[OF _ A] `range A \ sets M` ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 204` ``` M'.finite_continuity_from_below[OF _ A] ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 205` ``` have convergent: "(\i. ?d (A i)) ----> ?d (\i. A i)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 206` ``` by (auto intro!: LIMSEQ_diff) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 207` ``` obtain n :: nat where "- ?d (\i. A i) / e < real n" using reals_Archimedean2 by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 208` ``` moreover from order_trans[OF decseq_le[OF decseq convergent] dA_less] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 209` ``` have "real n \ - ?d (\i. A i) / e" using `0 sets M" and X: "X \ S" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 216` ``` shows "finite_measure.\' (restricted_space S) X = \' X" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 217` ```proof cases ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 218` ``` note r = restricted_finite_measure[OF S] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 219` ``` { assume "X \ sets M" with S X show ?thesis ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 220` ``` unfolding finite_measure.\'_def[OF r] \'_def by auto } ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 221` ``` { assume "X \ sets M" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 222` ``` moreover then have "S \ X \ sets M" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 223` ``` using X by (simp add: Int_absorb1) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 224` ``` ultimately show ?thesis ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 225` ``` unfolding finite_measure.\'_def[OF r] \'_def using S by auto } ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 226` ```qed ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 227` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 228` ```lemma (in finite_measure) restricted_measure: ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 229` ``` assumes X: "S \ sets M" "X \ sets (restricted_space S)" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 230` ``` shows "finite_measure.\' (restricted_space S) X = \' X" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 231` ```proof - ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 232` ``` from X have "S \ sets M" "X \ S" by auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 233` ``` from restricted_measure_subset[OF this] show ?thesis . ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 234` ```qed ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 235` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 236` ```lemma (in finite_measure) Radon_Nikodym_aux: ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 237` ``` assumes "finite_measure (M\measure := \\)" (is "finite_measure ?M'") ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 238` ``` shows "\A\sets M. \' (space M) - finite_measure.\' (M\measure := \\) (space M) \ ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 239` ``` \' A - finite_measure.\' (M\measure := \\) A \ ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 240` ``` (\B\sets M. B \ A \ 0 \ \' B - finite_measure.\' (M\measure := \\) B)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 241` ```proof - ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 242` ``` interpret M': finite_measure ?M' where ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 243` ``` "space ?M' = space M" and "sets ?M' = sets M" and "measure ?M' = \" by fact auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 244` ``` let "?d A" = "\' A - M'.\' A" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 245` ``` let "?P A B n" = "A \ sets M \ A \ B \ ?d B \ ?d A \ (\C\sets M. C \ A \ - 1 / real (Suc n) < ?d C)" ``` 39092 98de40859858 move lemmas to correct theory files hoelzl parents: 38656 diff changeset ` 246` ``` let "?r S" = "restricted_space S" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 247` ``` { fix S n assume S: "S \ sets M" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 248` ``` note r = M'.restricted_finite_measure[of S] restricted_finite_measure[OF S] S ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 249` ``` then have "finite_measure (?r S)" "0 < 1 / real (Suc n)" ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 250` ``` "finite_measure (?r S\measure := \\)" by auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 251` ``` from finite_measure.Radon_Nikodym_aux_epsilon[OF this] guess X .. note X = this ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 252` ``` have "?P X S n" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 253` ``` proof (intro conjI ballI impI) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 254` ``` show "X \ sets M" "X \ S" using X(1) `S \ sets M` by auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 255` ``` have "S \ op \ S ` sets M" using `S \ sets M` by auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 256` ``` then show "?d S \ ?d X" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 257` ``` using S X restricted_measure[OF S] M'.restricted_measure[OF S] by simp ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 258` ``` fix C assume "C \ sets M" "C \ X" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 259` ``` then have "C \ sets (restricted_space S)" "C \ X" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 260` ``` using `S \ sets M` `X \ S` by auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 261` ``` with X(2) show "- 1 / real (Suc n) < ?d C" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 262` ``` using S X restricted_measure[OF S] M'.restricted_measure[OF S] by auto ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 263` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 264` ``` hence "\A. ?P A S n" by auto } ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 265` ``` note Ex_P = this ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 266` ``` def A \ "nat_rec (space M) (\n A. SOME B. ?P B A n)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 267` ``` have A_Suc: "\n. A (Suc n) = (SOME B. ?P B (A n) n)" by (simp add: A_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 268` ``` have A_0[simp]: "A 0 = space M" unfolding A_def by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 269` ``` { fix i have "A i \ sets M" unfolding A_def ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 270` ``` proof (induct i) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 271` ``` case (Suc i) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 272` ``` from Ex_P[OF this, of i] show ?case unfolding nat_rec_Suc ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 273` ``` by (rule someI2_ex) simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 274` ``` qed simp } ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 275` ``` note A_in_sets = this ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 276` ``` { fix n have "?P (A (Suc n)) (A n) n" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 277` ``` using Ex_P[OF A_in_sets] unfolding A_Suc ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 278` ``` by (rule someI2_ex) simp } ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 279` ``` note P_A = this ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 280` ``` have "range A \ sets M" using A_in_sets by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 281` ``` have A_mono: "\i. A (Suc i) \ A i" using P_A by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 282` ``` have mono_dA: "mono (\i. ?d (A i))" using P_A by (simp add: mono_iff_le_Suc) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 283` ``` have epsilon: "\C i. \ C \ sets M; C \ A (Suc i) \ \ - 1 / real (Suc i) < ?d C" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 284` ``` using P_A by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 285` ``` show ?thesis ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 286` ``` proof (safe intro!: bexI[of _ "\i. A i"]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 287` ``` show "(\i. A i) \ sets M" using A_in_sets by auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 288` ``` have A: "decseq A" using A_mono by (auto intro!: decseq_SucI) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 289` ``` from ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 290` ``` finite_continuity_from_above[OF `range A \ sets M` A] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 291` ``` M'.finite_continuity_from_above[OF `range A \ sets M` A] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 292` ``` have "(\i. ?d (A i)) ----> ?d (\i. A i)" by (intro LIMSEQ_diff) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 293` ``` thus "?d (space M) \ ?d (\i. A i)" using mono_dA[THEN monoD, of 0 _] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 294` ``` by (rule_tac LIMSEQ_le_const) (auto intro!: exI) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 295` ``` next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 296` ``` fix B assume B: "B \ sets M" "B \ (\i. A i)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 297` ``` show "0 \ ?d B" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 298` ``` proof (rule ccontr) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 299` ``` assume "\ 0 \ ?d B" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 300` ``` hence "0 < - ?d B" by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 301` ``` from ex_inverse_of_nat_Suc_less[OF this] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 302` ``` obtain n where *: "?d B < - 1 / real (Suc n)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 303` ``` by (auto simp: real_eq_of_nat inverse_eq_divide field_simps) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 304` ``` have "B \ A (Suc n)" using B by (auto simp del: nat_rec_Suc) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 305` ``` from epsilon[OF B(1) this] * ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 306` ``` show False by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 307` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 308` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 309` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 310` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 311` ```lemma (in finite_measure) real_measure: ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 312` ``` assumes A: "A \ sets M" shows "\r. 0 \ r \ \ A = extreal r" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 313` ``` using finite_measure[OF A] positive_measure[OF A] by (cases "\ A") auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 314` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 315` ```lemma (in finite_measure) Radon_Nikodym_finite_measure: ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 316` ``` assumes "finite_measure (M\ measure := \\)" (is "finite_measure ?M'") ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 317` ``` assumes "absolutely_continuous \" ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 318` ``` shows "\f \ borel_measurable M. \A\sets M. \ A = (\\<^isup>+x. f x * indicator A x \M)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 319` ```proof - ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 320` ``` interpret M': finite_measure ?M' ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 321` ``` where "space ?M' = space M" and "sets ?M' = sets M" and "measure ?M' = \" ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 322` ``` using assms(1) by auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 323` ``` def G \ "{g \ borel_measurable M. (\x. 0 \ g x) \ (\A\sets M. (\\<^isup>+x. g x * indicator A x \M) \ \ A)}" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 324` ``` have "(\x. 0) \ G" unfolding G_def by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 325` ``` hence "G \ {}" by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 326` ``` { fix f g assume f: "f \ G" and g: "g \ G" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 327` ``` have "(\x. max (g x) (f x)) \ G" (is "?max \ G") unfolding G_def ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 328` ``` proof safe ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 329` ``` show "?max \ borel_measurable M" using f g unfolding G_def by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 330` ``` let ?A = "{x \ space M. f x \ g x}" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 331` ``` have "?A \ sets M" using f g unfolding G_def by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 332` ``` fix A assume "A \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 333` ``` hence sets: "?A \ A \ sets M" "(space M - ?A) \ A \ sets M" using `?A \ sets M` by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 334` ``` have union: "((?A \ A) \ ((space M - ?A) \ A)) = A" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 335` ``` using sets_into_space[OF `A \ sets M`] by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 336` ``` have "\x. x \ space M \ max (g x) (f x) * indicator A x = ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 337` ``` g x * indicator (?A \ A) x + f x * indicator ((space M - ?A) \ A) x" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 338` ``` by (auto simp: indicator_def max_def) ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 339` ``` hence "(\\<^isup>+x. max (g x) (f x) * indicator A x \M) = ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 340` ``` (\\<^isup>+x. g x * indicator (?A \ A) x \M) + ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 341` ``` (\\<^isup>+x. f x * indicator ((space M - ?A) \ A) x \M)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 342` ``` using f g sets unfolding G_def ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 343` ``` by (auto cong: positive_integral_cong intro!: positive_integral_add borel_measurable_indicator) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 344` ``` also have "\ \ \ (?A \ A) + \ ((space M - ?A) \ A)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 345` ``` using f g sets unfolding G_def by (auto intro!: add_mono) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 346` ``` also have "\ = \ A" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 347` ``` using M'.measure_additive[OF sets] union by auto ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 348` ``` finally show "(\\<^isup>+x. max (g x) (f x) * indicator A x \M) \ \ A" . ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 349` ``` next ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 350` ``` fix x show "0 \ max (g x) (f x)" using f g by (auto simp: G_def split: split_max) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 351` ``` qed } ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 352` ``` note max_in_G = this ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 353` ``` { fix f assume "incseq f" and f: "\i. f i \ G" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 354` ``` have "(\x. SUP i. f i x) \ G" unfolding G_def ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 355` ``` proof safe ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 356` ``` show "(\x. SUP i. f i x) \ borel_measurable M" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 357` ``` using f by (auto simp: G_def) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 358` ``` { fix x show "0 \ (SUP i. f i x)" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 359` ``` using f by (auto simp: G_def intro: le_SUPI2) } ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 360` ``` next ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 361` ``` fix A assume "A \ sets M" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 362` ``` have "(\\<^isup>+x. (SUP i. f i x) * indicator A x \M) = ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 363` ``` (\\<^isup>+x. (SUP i. f i x * indicator A x) \M)" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 364` ``` by (intro positive_integral_cong) (simp split: split_indicator) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 365` ``` also have "\ = (SUP i. (\\<^isup>+x. f i x * indicator A x \M))" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 366` ``` using `incseq f` f `A \ sets M` ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 367` ``` by (intro positive_integral_monotone_convergence_SUP) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 368` ``` (auto simp: G_def incseq_Suc_iff le_fun_def split: split_indicator) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 369` ``` finally show "(\\<^isup>+x. (SUP i. f i x) * indicator A x \M) \ \ A" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 370` ``` using f `A \ sets M` by (auto intro!: SUP_leI simp: G_def) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 371` ``` qed } ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 372` ``` note SUP_in_G = this ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 373` ``` let ?y = "SUP g : G. integral\<^isup>P M g" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 374` ``` have "?y \ \ (space M)" unfolding G_def ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 375` ``` proof (safe intro!: SUP_leI) ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 376` ``` fix g assume "\A\sets M. (\\<^isup>+x. g x * indicator A x \M) \ \ A" ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 377` ``` from this[THEN bspec, OF top] show "integral\<^isup>P M g \ \ (space M)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 378` ``` by (simp cong: positive_integral_cong) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 379` ``` qed ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 380` ``` from SUPR_countable_SUPR[OF `G \ {}`, of "integral\<^isup>P M"] guess ys .. note ys = this ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 381` ``` then have "\n. \g. g\G \ integral\<^isup>P M g = ys n" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 382` ``` proof safe ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 383` ``` fix n assume "range ys \ integral\<^isup>P M ` G" ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 384` ``` hence "ys n \ integral\<^isup>P M ` G" by auto ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 385` ``` thus "\g. g\G \ integral\<^isup>P M g = ys n" by auto ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 386` ``` qed ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 387` ``` from choice[OF this] obtain gs where "\i. gs i \ G" "\n. integral\<^isup>P M (gs n) = ys n" by auto ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 388` ``` hence y_eq: "?y = (SUP i. integral\<^isup>P M (gs i))" using ys by auto ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 389` ``` let "?g i x" = "Max ((\n. gs n x) ` {..i})" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 390` ``` def f \ "\x. SUP i. ?g i x" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 391` ``` let "?F A x" = "f x * indicator A x" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 392` ``` have gs_not_empty: "\i x. (\n. gs n x) ` {..i} \ {}" by auto ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 393` ``` { fix i have "?g i \ G" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 394` ``` proof (induct i) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 395` ``` case 0 thus ?case by simp fact ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 396` ``` next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 397` ``` case (Suc i) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 398` ``` with Suc gs_not_empty `gs (Suc i) \ G` show ?case ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 399` ``` by (auto simp add: atMost_Suc intro!: max_in_G) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 400` ``` qed } ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 401` ``` note g_in_G = this ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 402` ``` have "incseq ?g" using gs_not_empty ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 403` ``` by (auto intro!: incseq_SucI le_funI simp add: atMost_Suc) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 404` ``` from SUP_in_G[OF this g_in_G] have "f \ G" unfolding f_def . ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 405` ``` then have [simp, intro]: "f \ borel_measurable M" unfolding G_def by auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 406` ``` have "integral\<^isup>P M f = (SUP i. integral\<^isup>P M (?g i))" unfolding f_def ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 407` ``` using g_in_G `incseq ?g` ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 408` ``` by (auto intro!: positive_integral_monotone_convergence_SUP simp: G_def) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 409` ``` also have "\ = ?y" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 410` ``` proof (rule antisym) ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 411` ``` show "(SUP i. integral\<^isup>P M (?g i)) \ ?y" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 412` ``` using g_in_G by (auto intro!: exI Sup_mono simp: SUPR_def) ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 413` ``` show "?y \ (SUP i. integral\<^isup>P M (?g i))" unfolding y_eq ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 414` ``` by (auto intro!: SUP_mono positive_integral_mono Max_ge) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 415` ``` qed ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 416` ``` finally have int_f_eq_y: "integral\<^isup>P M f = ?y" . ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 417` ``` have "\x. 0 \ f x" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 418` ``` unfolding f_def using `\i. gs i \ G` ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 419` ``` by (auto intro!: le_SUPI2 Max_ge_iff[THEN iffD2] simp: G_def) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 420` ``` let "?t A" = "\ A - (\\<^isup>+x. ?F A x \M)" ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 421` ``` let ?M = "M\ measure := ?t\" ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 422` ``` interpret M: sigma_algebra ?M ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 423` ``` by (intro sigma_algebra_cong) auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 424` ``` have f_le_\: "\A. A \ sets M \ (\\<^isup>+x. ?F A x \M) \ \ A" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 425` ``` using `f \ G` unfolding G_def by auto ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 426` ``` have fmM: "finite_measure ?M" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 427` ``` proof (default, simp_all add: countably_additive_def positive_def, safe del: notI) ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 428` ``` fix A :: "nat \ 'a set" assume A: "range A \ sets M" "disjoint_family A" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 429` ``` have "(\n. (\\<^isup>+x. ?F (A n) x \M)) = (\\<^isup>+x. (\n. ?F (A n) x) \M)" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 430` ``` using `range A \ sets M` `\x. 0 \ f x` ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 431` ``` by (intro positive_integral_suminf[symmetric]) auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 432` ``` also have "\ = (\\<^isup>+x. ?F (\n. A n) x \M)" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 433` ``` using `\x. 0 \ f x` ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 434` ``` by (intro positive_integral_cong) (simp add: suminf_cmult_extreal suminf_indicator[OF `disjoint_family A`]) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 435` ``` finally have "(\n. (\\<^isup>+x. ?F (A n) x \M)) = (\\<^isup>+x. ?F (\n. A n) x \M)" . ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 436` ``` moreover have "(\n. \ (A n)) = \ (\n. A n)" ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 437` ``` using M'.measure_countably_additive A by (simp add: comp_def) ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 438` ``` moreover have v_fin: "\ (\i. A i) \ \" using M'.finite_measure A by (simp add: countable_UN) ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 439` ``` moreover { ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 440` ``` have "(\\<^isup>+x. ?F (\i. A i) x \M) \ \ (\i. A i)" ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 441` ``` using A `f \ G` unfolding G_def by (auto simp: countable_UN) ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 442` ``` also have "\ (\i. A i) < \" using v_fin by simp ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 443` ``` finally have "(\\<^isup>+x. ?F (\i. A i) x \M) \ \" by simp } ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 444` ``` moreover have "\i. (\\<^isup>+x. ?F (A i) x \M) \ \ (A i)" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 445` ``` using A by (intro f_le_\) auto ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 446` ``` ultimately ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 447` ``` show "(\n. ?t (A n)) = ?t (\i. A i)" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 448` ``` by (subst suminf_extreal_minus) (simp_all add: positive_integral_positive) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 449` ``` next ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 450` ``` fix A assume A: "A \ sets M" show "0 \ \ A - \\<^isup>+ x. ?F A x \M" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 451` ``` using f_le_\[OF A] `f \ G` M'.finite_measure[OF A] by (auto simp: G_def extreal_le_minus_iff) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 452` ``` next ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 453` ``` show "\ (space M) - (\\<^isup>+ x. ?F (space M) x \M) \ \" (is "?a - ?b \ _") ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 454` ``` using positive_integral_positive[of "?F (space M)"] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 455` ``` by (cases rule: extreal2_cases[of ?a ?b]) auto ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 456` ``` qed ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 457` ``` then interpret M: finite_measure ?M ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 458` ``` where "space ?M = space M" and "sets ?M = sets M" and "measure ?M = ?t" ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 459` ``` by (simp_all add: fmM) ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 460` ``` have ac: "absolutely_continuous ?t" unfolding absolutely_continuous_def ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 461` ``` proof ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 462` ``` fix N assume N: "N \ null_sets" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 463` ``` with `absolutely_continuous \` have "\ N = 0" unfolding absolutely_continuous_def by auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 464` ``` moreover with N have "(\\<^isup>+ x. ?F N x \M) \ \ N" using `f \ G` by (auto simp: G_def) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 465` ``` ultimately show "\ N - (\\<^isup>+ x. ?F N x \M) = 0" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 466` ``` using positive_integral_positive by (auto intro!: antisym) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 467` ``` qed ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 468` ``` have upper_bound: "\A\sets M. ?t A \ 0" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 469` ``` proof (rule ccontr) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 470` ``` assume "\ ?thesis" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 471` ``` then obtain A where A: "A \ sets M" and pos: "0 < ?t A" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 472` ``` by (auto simp: not_le) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 473` ``` note pos ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 474` ``` also have "?t A \ ?t (space M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 475` ``` using M.measure_mono[of A "space M"] A sets_into_space by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 476` ``` finally have pos_t: "0 < ?t (space M)" by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 477` ``` moreover ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 478` ``` then have "\ (space M) \ 0" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 479` ``` using ac unfolding absolutely_continuous_def by auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 480` ``` then have pos_M: "0 < \ (space M)" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 481` ``` using positive_measure[OF top] by (simp add: le_less) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 482` ``` moreover ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 483` ``` have "(\\<^isup>+x. f x * indicator (space M) x \M) \ \ (space M)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 484` ``` using `f \ G` unfolding G_def by auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 485` ``` hence "(\\<^isup>+x. f x * indicator (space M) x \M) \ \" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 486` ``` using M'.finite_measure_of_space by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 487` ``` moreover ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 488` ``` def b \ "?t (space M) / \ (space M) / 2" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 489` ``` ultimately have b: "b \ 0 \ 0 \ b \ b \ \" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 490` ``` using M'.finite_measure_of_space positive_integral_positive[of "?F (space M)"] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 491` ``` by (cases rule: extreal3_cases[of "integral\<^isup>P M (?F (space M))" "\ (space M)" "\ (space M)"]) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 492` ``` (simp_all add: field_simps) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 493` ``` then have b: "b \ 0" "0 \ b" "0 < b" "b \ \" by auto ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 494` ``` let ?Mb = "?M\measure := \A. b * \ A\" ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 495` ``` interpret b: sigma_algebra ?Mb by (intro sigma_algebra_cong) auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 496` ``` have Mb: "finite_measure ?Mb" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 497` ``` proof ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 498` ``` show "positive ?Mb (measure ?Mb)" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 499` ``` using `0 \ b` by (auto simp: positive_def) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 500` ``` show "countably_additive ?Mb (measure ?Mb)" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 501` ``` using `0 \ b` measure_countably_additive ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 502` ``` by (auto simp: countably_additive_def suminf_cmult_extreal subset_eq) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 503` ``` show "measure ?Mb (space ?Mb) \ \" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 504` ``` using b by auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 505` ``` qed ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 506` ``` from M.Radon_Nikodym_aux[OF this] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 507` ``` obtain A0 where "A0 \ sets M" and ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 508` ``` space_less_A0: "real (?t (space M)) - real (b * \ (space M)) \ real (?t A0) - real (b * \ A0)" and ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 509` ``` *: "\B. \ B \ sets M ; B \ A0 \ \ 0 \ real (?t B) - real (b * \ B)" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 510` ``` unfolding M.\'_def finite_measure.\'_def[OF Mb] by auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 511` ``` { fix B assume B: "B \ sets M" "B \ A0" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 512` ``` with *[OF this] have "b * \ B \ ?t B" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 513` ``` using M'.finite_measure b finite_measure M.positive_measure[OF B(1)] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 514` ``` by (cases rule: extreal2_cases[of "?t B" "b * \ B"]) auto } ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 515` ``` note bM_le_t = this ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 516` ``` let "?f0 x" = "f x + b * indicator A0 x" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 517` ``` { fix A assume A: "A \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 518` ``` hence "A \ A0 \ sets M" using `A0 \ sets M` by auto ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 519` ``` have "(\\<^isup>+x. ?f0 x * indicator A x \M) = ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 520` ``` (\\<^isup>+x. f x * indicator A x + b * indicator (A \ A0) x \M)" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 521` ``` by (auto intro!: positive_integral_cong split: split_indicator) ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 522` ``` hence "(\\<^isup>+x. ?f0 x * indicator A x \M) = ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 523` ``` (\\<^isup>+x. f x * indicator A x \M) + b * \ (A \ A0)" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 524` ``` using `A0 \ sets M` `A \ A0 \ sets M` A b `f \ G` ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 525` ``` by (simp add: G_def positive_integral_add positive_integral_cmult_indicator) } ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 526` ``` note f0_eq = this ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 527` ``` { fix A assume A: "A \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 528` ``` hence "A \ A0 \ sets M" using `A0 \ sets M` by auto ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 529` ``` have f_le_v: "(\\<^isup>+x. f x * indicator A x \M) \ \ A" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 530` ``` using `f \ G` A unfolding G_def by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 531` ``` note f0_eq[OF A] ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 532` ``` also have "(\\<^isup>+x. f x * indicator A x \M) + b * \ (A \ A0) \ ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 533` ``` (\\<^isup>+x. f x * indicator A x \M) + ?t (A \ A0)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 534` ``` using bM_le_t[OF `A \ A0 \ sets M`] `A \ sets M` `A0 \ sets M` ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 535` ``` by (auto intro!: add_left_mono) ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 536` ``` also have "\ \ (\\<^isup>+x. f x * indicator A x \M) + ?t A" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 537` ``` using M.measure_mono[simplified, OF _ `A \ A0 \ sets M` `A \ sets M`] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 538` ``` by (auto intro!: add_left_mono) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 539` ``` also have "\ \ \ A" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 540` ``` using f_le_v M'.finite_measure[simplified, OF `A \ sets M`] positive_integral_positive[of "?F A"] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 541` ``` by (cases "\\<^isup>+x. ?F A x \M", cases "\ A") auto ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 542` ``` finally have "(\\<^isup>+x. ?f0 x * indicator A x \M) \ \ A" . } ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 543` ``` hence "?f0 \ G" using `A0 \ sets M` b `f \ G` unfolding G_def ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 544` ``` by (auto intro!: borel_measurable_indicator borel_measurable_extreal_add ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 545` ``` borel_measurable_extreal_times extreal_add_nonneg_nonneg) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 546` ``` have real: "?t (space M) \ \" "?t A0 \ \" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 547` ``` "b * \ (space M) \ \" "b * \ A0 \ \" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 548` ``` using `A0 \ sets M` b ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 549` ``` finite_measure[of A0] M.finite_measure[of A0] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 550` ``` finite_measure_of_space M.finite_measure_of_space ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 551` ``` by auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 552` ``` have int_f_finite: "integral\<^isup>P M f \ \" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 553` ``` using M'.finite_measure_of_space pos_t unfolding extreal_less_minus_iff ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 554` ``` by (auto cong: positive_integral_cong) ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 555` ``` have "0 < ?t (space M) - b * \ (space M)" unfolding b_def ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 556` ``` using finite_measure_of_space M'.finite_measure_of_space pos_t pos_M ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 557` ``` using positive_integral_positive[of "?F (space M)"] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 558` ``` by (cases rule: extreal3_cases[of "\ (space M)" "\ (space M)" "integral\<^isup>P M (?F (space M))"]) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 559` ``` (auto simp: field_simps mult_less_cancel_left) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 560` ``` also have "\ \ ?t A0 - b * \ A0" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 561` ``` using space_less_A0 b ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 562` ``` using ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 563` ``` `A0 \ sets M`[THEN M.real_measure] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 564` ``` top[THEN M.real_measure] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 565` ``` apply safe ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 566` ``` apply simp ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 567` ``` using ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 568` ``` `A0 \ sets M`[THEN real_measure] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 569` ``` `A0 \ sets M`[THEN M'.real_measure] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 570` ``` top[THEN real_measure] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 571` ``` top[THEN M'.real_measure] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 572` ``` by (cases b) auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 573` ``` finally have 1: "b * \ A0 < ?t A0" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 574` ``` using ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 575` ``` `A0 \ sets M`[THEN M.real_measure] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 576` ``` apply safe ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 577` ``` apply simp ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 578` ``` using ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 579` ``` `A0 \ sets M`[THEN real_measure] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 580` ``` `A0 \ sets M`[THEN M'.real_measure] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 581` ``` by (cases b) auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 582` ``` have "0 < ?t A0" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 583` ``` using b `A0 \ sets M` by (auto intro!: le_less_trans[OF _ 1]) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 584` ``` then have "\ A0 \ 0" using ac unfolding absolutely_continuous_def ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 585` ``` using `A0 \ sets M` by auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 586` ``` then have "0 < \ A0" using positive_measure[OF `A0 \ sets M`] by auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 587` ``` hence "0 < b * \ A0" using b by (auto simp: extreal_zero_less_0_iff) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 588` ``` with int_f_finite have "?y + 0 < integral\<^isup>P M f + b * \ A0" unfolding int_f_eq_y ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 589` ``` using `f \ G` ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 590` ``` by (intro extreal_add_strict_mono) (auto intro!: le_SUPI2 positive_integral_positive) ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 591` ``` also have "\ = integral\<^isup>P M ?f0" using f0_eq[OF top] `A0 \ sets M` sets_into_space ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 592` ``` by (simp cong: positive_integral_cong) ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 593` ``` finally have "?y < integral\<^isup>P M ?f0" by simp ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 594` ``` moreover from `?f0 \ G` have "integral\<^isup>P M ?f0 \ ?y" by (auto intro!: le_SUPI) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 595` ``` ultimately show False by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 596` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 597` ``` show ?thesis ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 598` ``` proof (safe intro!: bexI[of _ f]) ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 599` ``` fix A assume A: "A\sets M" ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 600` ``` show "\ A = (\\<^isup>+x. f x * indicator A x \M)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 601` ``` proof (rule antisym) ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 602` ``` show "(\\<^isup>+x. f x * indicator A x \M) \ \ A" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 603` ``` using `f \ G` `A \ sets M` unfolding G_def by auto ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 604` ``` show "\ A \ (\\<^isup>+x. f x * indicator A x \M)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 605` ``` using upper_bound[THEN bspec, OF `A \ sets M`] ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 606` ``` using M'.real_measure[OF A] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 607` ``` by (cases "integral\<^isup>P M (?F A)") auto ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 608` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 609` ``` qed simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 610` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 611` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 612` ```lemma (in finite_measure) split_space_into_finite_sets_and_rest: ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 613` ``` assumes "measure_space (M\measure := \\)" (is "measure_space ?N") ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 614` ``` assumes ac: "absolutely_continuous \" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 615` ``` shows "\A0\sets M. \B::nat\'a set. disjoint_family B \ range B \ sets M \ A0 = space M - (\i. B i) \ ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 616` ``` (\A\sets M. A \ A0 \ (\ A = 0 \ \ A = 0) \ (\ A > 0 \ \ A = \)) \ ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 617` ``` (\i. \ (B i) \ \)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 618` ```proof - ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 619` ``` interpret v: measure_space ?N ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 620` ``` where "space ?N = space M" and "sets ?N = sets M" and "measure ?N = \" ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 621` ``` by fact auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 622` ``` let ?Q = "{Q\sets M. \ Q \ \}" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 623` ``` let ?a = "SUP Q:?Q. \ Q" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 624` ``` have "{} \ ?Q" using v.empty_measure by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 625` ``` then have Q_not_empty: "?Q \ {}" by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 626` ``` have "?a \ \ (space M)" using sets_into_space ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 627` ``` by (auto intro!: SUP_leI measure_mono top) ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 628` ``` then have "?a \ \" using finite_measure_of_space ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 629` ``` by auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 630` ``` from SUPR_countable_SUPR[OF Q_not_empty, of \] ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 631` ``` obtain Q'' where "range Q'' \ \ ` ?Q" and a: "?a = (SUP i::nat. Q'' i)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 632` ``` by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 633` ``` then have "\i. \Q'. Q'' i = \ Q' \ Q' \ ?Q" by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 634` ``` from choice[OF this] obtain Q' where Q': "\i. Q'' i = \ (Q' i)" "\i. Q' i \ ?Q" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 635` ``` by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 636` ``` then have a_Lim: "?a = (SUP i::nat. \ (Q' i))" using a by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 637` ``` let "?O n" = "\i\n. Q' i" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 638` ``` have Union: "(SUP i. \ (?O i)) = \ (\i. ?O i)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 639` ``` proof (rule continuity_from_below[of ?O]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 640` ``` show "range ?O \ sets M" using Q' by (auto intro!: finite_UN) ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 641` ``` show "incseq ?O" by (fastsimp intro!: incseq_SucI) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 642` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 643` ``` have Q'_sets: "\i. Q' i \ sets M" using Q' by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 644` ``` have O_sets: "\i. ?O i \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 645` ``` using Q' by (auto intro!: finite_UN Un) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 646` ``` then have O_in_G: "\i. ?O i \ ?Q" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 647` ``` proof (safe del: notI) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 648` ``` fix i have "Q' ` {..i} \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 649` ``` using Q' by (auto intro: finite_UN) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 650` ``` with v.measure_finitely_subadditive[of "{.. i}" Q'] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 651` ``` have "\ (?O i) \ (\i\i. \ (Q' i))" by auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 652` ``` also have "\ < \" using Q' by (simp add: setsum_Pinfty) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 653` ``` finally show "\ (?O i) \ \" by simp ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 654` ``` qed auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 655` ``` have O_mono: "\n. ?O n \ ?O (Suc n)" by fastsimp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 656` ``` have a_eq: "?a = \ (\i. ?O i)" unfolding Union[symmetric] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 657` ``` proof (rule antisym) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 658` ``` show "?a \ (SUP i. \ (?O i))" unfolding a_Lim ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 659` ``` using Q' by (auto intro!: SUP_mono measure_mono finite_UN) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 660` ``` show "(SUP i. \ (?O i)) \ ?a" unfolding SUPR_def ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 661` ``` proof (safe intro!: Sup_mono, unfold bex_simps) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 662` ``` fix i ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 663` ``` have *: "(\Q' ` {..i}) = ?O i" by auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 664` ``` then show "\x. (x \ sets M \ \ x \ \) \ ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 665` ``` \ (\Q' ` {..i}) \ \ x" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 666` ``` using O_in_G[of i] by (auto intro!: exI[of _ "?O i"]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 667` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 668` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 669` ``` let "?O_0" = "(\i. ?O i)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 670` ``` have "?O_0 \ sets M" using Q' by auto ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 671` ``` def Q \ "\i. case i of 0 \ Q' 0 | Suc n \ ?O (Suc n) - ?O n" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 672` ``` { fix i have "Q i \ sets M" unfolding Q_def using Q'[of 0] by (cases i) (auto intro: O_sets) } ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 673` ``` note Q_sets = this ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 674` ``` show ?thesis ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 675` ``` proof (intro bexI exI conjI ballI impI allI) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 676` ``` show "disjoint_family Q" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 677` ``` by (fastsimp simp: disjoint_family_on_def Q_def ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 678` ``` split: nat.split_asm) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 679` ``` show "range Q \ sets M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 680` ``` using Q_sets by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 681` ``` { fix A assume A: "A \ sets M" "A \ space M - ?O_0" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 682` ``` show "\ A = 0 \ \ A = 0 \ 0 < \ A \ \ A = \" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 683` ``` proof (rule disjCI, simp) ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 684` ``` assume *: "0 < \ A \ \ A \ \" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 685` ``` show "\ A = 0 \ \ A = 0" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 686` ``` proof cases ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 687` ``` assume "\ A = 0" moreover with ac A have "\ A = 0" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 688` ``` unfolding absolutely_continuous_def by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 689` ``` ultimately show ?thesis by simp ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 690` ``` next ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 691` ``` assume "\ A \ 0" with * have "\ A \ \" using positive_measure[OF A(1)] by auto ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 692` ``` with A have "\ ?O_0 + \ A = \ (?O_0 \ A)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 693` ``` using Q' by (auto intro!: measure_additive countable_UN) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 694` ``` also have "\ = (SUP i. \ (?O i \ A))" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 695` ``` proof (rule continuity_from_below[of "\i. ?O i \ A", symmetric, simplified]) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 696` ``` show "range (\i. ?O i \ A) \ sets M" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 697` ``` using `\ A \ \` O_sets A by auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 698` ``` qed (fastsimp intro!: incseq_SucI) ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 699` ``` also have "\ \ ?a" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 700` ``` proof (safe intro!: SUP_leI) ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 701` ``` fix i have "?O i \ A \ ?Q" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 702` ``` proof (safe del: notI) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 703` ``` show "?O i \ A \ sets M" using O_sets A by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 704` ``` from O_in_G[of i] ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 705` ``` moreover have "\ (?O i \ A) \ \ (?O i) + \ A" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 706` ``` using v.measure_subadditive[of "?O i" A] A O_sets by auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 707` ``` ultimately show "\ (?O i \ A) \ \" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 708` ``` using `\ A \ \` by auto ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 709` ``` qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 710` ``` then show "\ (?O i \ A) \ ?a" by (rule le_SUPI) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 711` ``` qed ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 712` ``` finally have "\ A = 0" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 713` ``` unfolding a_eq using real_measure[OF `?O_0 \ sets M`] real_measure[OF A(1)] by auto ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 714` ``` with `\ A \ 0` show ?thesis by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 715` ``` qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 716` ``` qed } ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 717` ``` { fix i show "\ (Q i) \ \" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 718` ``` proof (cases i) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 719` ``` case 0 then show ?thesis ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 720` ``` unfolding Q_def using Q'[of 0] by simp ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 721` ``` next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 722` ``` case (Suc n) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 723` ``` then show ?thesis unfolding Q_def ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 724` ``` using `?O n \ ?Q` `?O (Suc n) \ ?Q` ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 725` ``` using v.measure_mono[OF O_mono, of n] v.positive_measure[of "?O n"] v.positive_measure[of "?O (Suc n)"] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 726` ``` using v.measure_Diff[of "?O n" "?O (Suc n)", OF _ _ _ O_mono] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 727` ``` by (cases rule: extreal2_cases[of "\ (\ x\Suc n. Q' x)" "\ (\ i\n. Q' i)"]) auto ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 728` ``` qed } ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 729` ``` show "space M - ?O_0 \ sets M" using Q'_sets by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 730` ``` { fix j have "(\i\j. ?O i) = (\i\j. Q i)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 731` ``` proof (induct j) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 732` ``` case 0 then show ?case by (simp add: Q_def) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 733` ``` next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 734` ``` case (Suc j) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 735` ``` have eq: "\j. (\i\j. ?O i) = (\i\j. Q' i)" by fastsimp ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 736` ``` have "{..j} \ {..Suc j} = {..Suc j}" by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 737` ``` then have "(\i\Suc j. Q' i) = (\i\j. Q' i) \ Q (Suc j)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 738` ``` by (simp add: UN_Un[symmetric] Q_def del: UN_Un) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 739` ``` then show ?case using Suc by (auto simp add: eq atMost_Suc) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 740` ``` qed } ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 741` ``` then have "(\j. (\i\j. ?O i)) = (\j. (\i\j. Q i))" by simp ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 742` ``` then show "space M - ?O_0 = space M - (\i. Q i)" by fastsimp ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 743` ``` qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 744` ```qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 745` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 746` ```lemma (in finite_measure) Radon_Nikodym_finite_measure_infinite: ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 747` ``` assumes "measure_space (M\measure := \\)" (is "measure_space ?N") ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 748` ``` assumes "absolutely_continuous \" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 749` ``` shows "\f \ borel_measurable M. (\x. 0 \ f x) \ (\A\sets M. \ A = (\\<^isup>+x. f x * indicator A x \M))" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 750` ```proof - ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 751` ``` interpret v: measure_space ?N ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 752` ``` where "space ?N = space M" and "sets ?N = sets M" and "measure ?N = \" ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 753` ``` by fact auto ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 754` ``` from split_space_into_finite_sets_and_rest[OF assms] ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 755` ``` obtain Q0 and Q :: "nat \ 'a set" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 756` ``` where Q: "disjoint_family Q" "range Q \ sets M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 757` ``` and Q0: "Q0 \ sets M" "Q0 = space M - (\i. Q i)" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 758` ``` and in_Q0: "\A. A \ sets M \ A \ Q0 \ \ A = 0 \ \ A = 0 \ 0 < \ A \ \ A = \" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 759` ``` and Q_fin: "\i. \ (Q i) \ \" by force ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 760` ``` from Q have Q_sets: "\i. Q i \ sets M" by auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 761` ``` have "\i. \f. f\borel_measurable M \ (\x. 0 \ f x) \ (\A\sets M. ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 762` ``` \ (Q i \ A) = (\\<^isup>+x. f x * indicator (Q i \ A) x \M))" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 763` ``` proof ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 764` ``` fix i ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 765` ``` have indicator_eq: "\f x A. (f x :: extreal) * indicator (Q i \ A) x * indicator (Q i) x ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 766` ``` = (f x * indicator (Q i) x) * indicator A x" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 767` ``` unfolding indicator_def by auto ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 768` ``` have fm: "finite_measure (restricted_space (Q i))" ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 769` ``` (is "finite_measure ?R") by (rule restricted_finite_measure[OF Q_sets[of i]]) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 770` ``` then interpret R: finite_measure ?R . ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 771` ``` have fmv: "finite_measure (restricted_space (Q i) \ measure := \\)" (is "finite_measure ?Q") ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 772` ``` unfolding finite_measure_def finite_measure_axioms_def ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 773` ``` proof ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 774` ``` show "measure_space ?Q" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 775` ``` using v.restricted_measure_space Q_sets[of i] by auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 776` ``` show "measure ?Q (space ?Q) \ \" using Q_fin by simp ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 777` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 778` ``` have "R.absolutely_continuous \" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 779` ``` using `absolutely_continuous \` `Q i \ sets M` ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 780` ``` by (auto simp: R.absolutely_continuous_def absolutely_continuous_def) ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 781` ``` from R.Radon_Nikodym_finite_measure[OF fmv this] ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 782` ``` obtain f where f: "(\x. f x * indicator (Q i) x) \ borel_measurable M" ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 783` ``` and f_int: "\A. A\sets M \ \ (Q i \ A) = (\\<^isup>+x. (f x * indicator (Q i) x) * indicator A x \M)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 784` ``` unfolding Bex_def borel_measurable_restricted[OF `Q i \ sets M`] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 785` ``` positive_integral_restricted[OF `Q i \ sets M`] by (auto simp: indicator_eq) ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 786` ``` then show "\f. f\borel_measurable M \ (\x. 0 \ f x) \ (\A\sets M. ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 787` ``` \ (Q i \ A) = (\\<^isup>+x. f x * indicator (Q i \ A) x \M))" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 788` ``` by (auto intro!: exI[of _ "\x. max 0 (f x * indicator (Q i) x)"] positive_integral_cong_pos ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 789` ``` split: split_indicator split_if_asm simp: max_def) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 790` ``` qed ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 791` ``` from choice[OF this] obtain f where borel: "\i. f i \ borel_measurable M" "\i x. 0 \ f i x" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 792` ``` and f: "\A i. A \ sets M \ ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 793` ``` \ (Q i \ A) = (\\<^isup>+x. f i x * indicator (Q i \ A) x \M)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 794` ``` by auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 795` ``` let "?f x" = "(\i. f i x * indicator (Q i) x) + \ * indicator Q0 x" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 796` ``` show ?thesis ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 797` ``` proof (safe intro!: bexI[of _ ?f]) ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 798` ``` show "?f \ borel_measurable M" using Q0 borel Q_sets ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 799` ``` by (auto intro!: measurable_If) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 800` ``` show "\x. 0 \ ?f x" using borel by (auto intro!: suminf_0_le simp: indicator_def) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 801` ``` fix A assume "A \ sets M" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 802` ``` have Qi: "\i. Q i \ sets M" using Q by auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 803` ``` have [intro,simp]: "\i. (\x. f i x * indicator (Q i \ A) x) \ borel_measurable M" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 804` ``` "\i. AE x. 0 \ f i x * indicator (Q i \ A) x" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 805` ``` using borel Qi Q0(1) `A \ sets M` by (auto intro!: borel_measurable_extreal_times) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 806` ``` have "(\\<^isup>+x. ?f x * indicator A x \M) = (\\<^isup>+x. (\i. f i x * indicator (Q i \ A) x) + \ * indicator (Q0 \ A) x \M)" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 807` ``` using borel by (intro positive_integral_cong) (auto simp: indicator_def) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 808` ``` also have "\ = (\\<^isup>+x. (\i. f i x * indicator (Q i \ A) x) \M) + \ * \ (Q0 \ A)" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 809` ``` using borel Qi Q0(1) `A \ sets M` ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 810` ``` by (subst positive_integral_add) (auto simp del: extreal_infty_mult ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 811` ``` simp add: positive_integral_cmult_indicator Int intro!: suminf_0_le) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 812` ``` also have "\ = (\i. \ (Q i \ A)) + \ * \ (Q0 \ A)" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 813` ``` by (subst f[OF `A \ sets M`], subst positive_integral_suminf) auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 814` ``` finally have "(\\<^isup>+x. ?f x * indicator A x \M) = (\i. \ (Q i \ A)) + \ * \ (Q0 \ A)" . ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 815` ``` moreover have "(\i. \ (Q i \ A)) = \ ((\i. Q i) \ A)" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 816` ``` using Q Q_sets `A \ sets M` ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 817` ``` by (intro v.measure_countably_additive[of "\i. Q i \ A", unfolded comp_def, simplified]) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 818` ``` (auto simp: disjoint_family_on_def) ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 819` ``` moreover have "\ * \ (Q0 \ A) = \ (Q0 \ A)" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 820` ``` proof - ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 821` ``` have "Q0 \ A \ sets M" using Q0(1) `A \ sets M` by blast ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 822` ``` from in_Q0[OF this] show ?thesis by auto ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 823` ``` qed ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 824` ``` moreover have "Q0 \ A \ sets M" "((\i. Q i) \ A) \ sets M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 825` ``` using Q_sets `A \ sets M` Q0(1) by (auto intro!: countable_UN) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 826` ``` moreover have "((\i. Q i) \ A) \ (Q0 \ A) = A" "((\i. Q i) \ A) \ (Q0 \ A) = {}" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 827` ``` using `A \ sets M` sets_into_space Q0 by auto ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 828` ``` ultimately show "\ A = (\\<^isup>+x. ?f x * indicator A x \M)" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 829` ``` using v.measure_additive[simplified, of "(\i. Q i) \ A" "Q0 \ A"] ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 830` ``` by simp ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 831` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 832` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 833` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 834` ```lemma (in sigma_finite_measure) Radon_Nikodym: ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 835` ``` assumes "measure_space (M\measure := \\)" (is "measure_space ?N") ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 836` ``` assumes ac: "absolutely_continuous \" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 837` ``` shows "\f \ borel_measurable M. (\x. 0 \ f x) \ (\A\sets M. \ A = (\\<^isup>+x. f x * indicator A x \M))" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 838` ```proof - ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 839` ``` from Ex_finite_integrable_function ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 840` ``` obtain h where finite: "integral\<^isup>P M h \ \" and ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 841` ``` borel: "h \ borel_measurable M" and ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 842` ``` nn: "\x. 0 \ h x" and ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 843` ``` pos: "\x. x \ space M \ 0 < h x" and ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 844` ``` "\x. x \ space M \ h x < \" by auto ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 845` ``` let "?T A" = "(\\<^isup>+x. h x * indicator A x \M)" ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 846` ``` let ?MT = "M\ measure := ?T \" ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 847` ``` interpret T: finite_measure ?MT ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 848` ``` where "space ?MT = space M" and "sets ?MT = sets M" and "measure ?MT = ?T" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 849` ``` unfolding finite_measure_def finite_measure_axioms_def using borel finite nn ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 850` ``` by (auto intro!: measure_space_density cong: positive_integral_cong) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 851` ``` have "T.absolutely_continuous \" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 852` ``` proof (unfold T.absolutely_continuous_def, safe) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 853` ``` fix N assume "N \ sets M" "(\\<^isup>+x. h x * indicator N x \M) = 0" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 854` ``` with borel ac pos have "AE x. x \ N" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 855` ``` by (subst (asm) positive_integral_0_iff_AE) (auto split: split_indicator simp: not_le) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 856` ``` then have "N \ null_sets" using `N \ sets M` sets_into_space ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 857` ``` by (subst (asm) AE_iff_measurable[OF `N \ sets M`]) auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 858` ``` then show "\ N = 0" using ac by (auto simp: absolutely_continuous_def) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 859` ``` qed ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 860` ``` from T.Radon_Nikodym_finite_measure_infinite[simplified, OF assms(1) this] ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 861` ``` obtain f where f_borel: "f \ borel_measurable M" "\x. 0 \ f x" and ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 862` ``` fT: "\A. A \ sets M \ \ A = (\\<^isup>+ x. f x * indicator A x \?MT)" ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 863` ``` by (auto simp: measurable_def) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 864` ``` show ?thesis ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 865` ``` proof (safe intro!: bexI[of _ "\x. h x * f x"]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 866` ``` show "(\x. h x * f x) \ borel_measurable M" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 867` ``` using borel f_borel by (auto intro: borel_measurable_extreal_times) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 868` ``` show "\x. 0 \ h x * f x" using nn f_borel by auto ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 869` ``` fix A assume "A \ sets M" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 870` ``` then show "\ A = (\\<^isup>+x. h x * f x * indicator A x \M)" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 871` ``` unfolding fT[OF `A \ sets M`] mult_assoc using nn borel f_borel ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 872` ``` by (intro positive_integral_translated_density) auto ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 873` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 874` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 875` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 876` ```section "Uniqueness of densities" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 877` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 878` ```lemma (in measure_space) finite_density_unique: ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 879` ``` assumes borel: "f \ borel_measurable M" "g \ borel_measurable M" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 880` ``` assumes pos: "AE x. 0 \ f x" "AE x. 0 \ g x" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 881` ``` and fin: "integral\<^isup>P M f \ \" ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 882` ``` shows "(\A\sets M. (\\<^isup>+x. f x * indicator A x \M) = (\\<^isup>+x. g x * indicator A x \M)) ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 883` ``` \ (AE x. f x = g x)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 884` ``` (is "(\A\sets M. ?P f A = ?P g A) \ _") ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 885` ```proof (intro iffI ballI) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 886` ``` fix A assume eq: "AE x. f x = g x" ``` 41705 1100512e16d8 add auto support for AE_mp hoelzl parents: 41689 diff changeset ` 887` ``` then show "?P f A = ?P g A" ``` 1100512e16d8 add auto support for AE_mp hoelzl parents: 41689 diff changeset ` 888` ``` by (auto intro: positive_integral_cong_AE) ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 889` ```next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 890` ``` assume eq: "\A\sets M. ?P f A = ?P g A" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 891` ``` from this[THEN bspec, OF top] fin ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 892` ``` have g_fin: "integral\<^isup>P M g \ \" by (simp cong: positive_integral_cong) ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 893` ``` { fix f g assume borel: "f \ borel_measurable M" "g \ borel_measurable M" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 894` ``` and pos: "AE x. 0 \ f x" "AE x. 0 \ g x" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 895` ``` and g_fin: "integral\<^isup>P M g \ \" and eq: "\A\sets M. ?P f A = ?P g A" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 896` ``` let ?N = "{x\space M. g x < f x}" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 897` ``` have N: "?N \ sets M" using borel by simp ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 898` ``` have "?P g ?N \ integral\<^isup>P M g" using pos ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 899` ``` by (intro positive_integral_mono_AE) (auto split: split_indicator) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 900` ``` then have Pg_fin: "?P g ?N \ \" using g_fin by auto ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 901` ``` have "?P (\x. (f x - g x)) ?N = (\\<^isup>+x. f x * indicator ?N x - g x * indicator ?N x \M)" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 902` ``` by (auto intro!: positive_integral_cong simp: indicator_def) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 903` ``` also have "\ = ?P f ?N - ?P g ?N" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 904` ``` proof (rule positive_integral_diff) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 905` ``` show "(\x. f x * indicator ?N x) \ borel_measurable M" "(\x. g x * indicator ?N x) \ borel_measurable M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 906` ``` using borel N by auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 907` ``` show "AE x. g x * indicator ?N x \ f x * indicator ?N x" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 908` ``` "AE x. 0 \ g x * indicator ?N x" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 909` ``` using pos by (auto split: split_indicator) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 910` ``` qed fact ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 911` ``` also have "\ = 0" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 912` ``` unfolding eq[THEN bspec, OF N] using positive_integral_positive Pg_fin by auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 913` ``` finally have "AE x. f x \ g x" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 914` ``` using pos borel positive_integral_PInf_AE[OF borel(2) g_fin] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 915` ``` by (subst (asm) positive_integral_0_iff_AE) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 916` ``` (auto split: split_indicator simp: not_less extreal_minus_le_iff) } ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 917` ``` from this[OF borel pos g_fin eq] this[OF borel(2,1) pos(2,1) fin] eq ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 918` ``` show "AE x. f x = g x" by auto ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 919` ```qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 920` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 921` ```lemma (in finite_measure) density_unique_finite_measure: ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 922` ``` assumes borel: "f \ borel_measurable M" "f' \ borel_measurable M" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 923` ``` assumes pos: "AE x. 0 \ f x" "AE x. 0 \ f' x" ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 924` ``` assumes f: "\A. A \ sets M \ (\\<^isup>+x. f x * indicator A x \M) = (\\<^isup>+x. f' x * indicator A x \M)" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 925` ``` (is "\A. A \ sets M \ ?P f A = ?P f' A") ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 926` ``` shows "AE x. f x = f' x" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 927` ```proof - ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 928` ``` let "?\ A" = "?P f A" and "?\' A" = "?P f' A" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 929` ``` let "?f A x" = "f x * indicator A x" and "?f' A x" = "f' x * indicator A x" ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 930` ``` interpret M: measure_space "M\ measure := ?\\" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 931` ``` using borel(1) pos(1) by (rule measure_space_density) simp ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 932` ``` have ac: "absolutely_continuous ?\" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 933` ``` using f by (rule density_is_absolutely_continuous) ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 934` ``` from split_space_into_finite_sets_and_rest[OF `measure_space (M\ measure := ?\\)` ac] ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 935` ``` obtain Q0 and Q :: "nat \ 'a set" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 936` ``` where Q: "disjoint_family Q" "range Q \ sets M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 937` ``` and Q0: "Q0 \ sets M" "Q0 = space M - (\i. Q i)" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 938` ``` and in_Q0: "\A. A \ sets M \ A \ Q0 \ \ A = 0 \ ?\ A = 0 \ 0 < \ A \ ?\ A = \" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 939` ``` and Q_fin: "\i. ?\ (Q i) \ \" by force ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 940` ``` from Q have Q_sets: "\i. Q i \ sets M" by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 941` ``` let ?N = "{x\space M. f x \ f' x}" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 942` ``` have "?N \ sets M" using borel by auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 943` ``` have *: "\i x A. \y::extreal. y * indicator (Q i) x * indicator A x = y * indicator (Q i \ A) x" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 944` ``` unfolding indicator_def by auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 945` ``` have "\i. AE x. ?f (Q i) x = ?f' (Q i) x" using borel Q_fin Q pos ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 946` ``` by (intro finite_density_unique[THEN iffD1] allI) ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 947` ``` (auto intro!: borel_measurable_extreal_times f Int simp: *) ``` 41705 1100512e16d8 add auto support for AE_mp hoelzl parents: 41689 diff changeset ` 948` ``` moreover have "AE x. ?f Q0 x = ?f' Q0 x" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 949` ``` proof (rule AE_I') ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 950` ``` { fix f :: "'a \ extreal" assume borel: "f \ borel_measurable M" ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 951` ``` and eq: "\A. A \ sets M \ ?\ A = (\\<^isup>+x. f x * indicator A x \M)" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 952` ``` let "?A i" = "Q0 \ {x \ space M. f x < of_nat i}" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 953` ``` have "(\i. ?A i) \ null_sets" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 954` ``` proof (rule null_sets_UN) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 955` ``` fix i have "?A i \ sets M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 956` ``` using borel Q0(1) by auto ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 957` ``` have "?\ (?A i) \ (\\<^isup>+x. of_nat i * indicator (?A i) x \M)" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 958` ``` unfolding eq[OF `?A i \ sets M`] ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 959` ``` by (auto intro!: positive_integral_mono simp: indicator_def) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 960` ``` also have "\ = of_nat i * \ (?A i)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 961` ``` using `?A i \ sets M` by (auto intro!: positive_integral_cmult_indicator) ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 962` ``` also have "\ < \" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 963` ``` using `?A i \ sets M`[THEN finite_measure] by auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 964` ``` finally have "?\ (?A i) \ \" by simp ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 965` ``` then show "?A i \ null_sets" using in_Q0[OF `?A i \ sets M`] `?A i \ sets M` by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 966` ``` qed ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 967` ``` also have "(\i. ?A i) = Q0 \ {x\space M. f x \ \}" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 968` ``` by (auto simp: less_PInf_Ex_of_nat real_eq_of_nat) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 969` ``` finally have "Q0 \ {x\space M. f x \ \} \ null_sets" by simp } ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 970` ``` from this[OF borel(1) refl] this[OF borel(2) f] ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 971` ``` have "Q0 \ {x\space M. f x \ \} \ null_sets" "Q0 \ {x\space M. f' x \ \} \ null_sets" by simp_all ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 972` ``` then show "(Q0 \ {x\space M. f x \ \}) \ (Q0 \ {x\space M. f' x \ \}) \ null_sets" by (rule null_sets_Un) ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 973` ``` show "{x \ space M. ?f Q0 x \ ?f' Q0 x} \ ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 974` ``` (Q0 \ {x\space M. f x \ \}) \ (Q0 \ {x\space M. f' x \ \})" by (auto simp: indicator_def) ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 975` ``` qed ``` 41705 1100512e16d8 add auto support for AE_mp hoelzl parents: 41689 diff changeset ` 976` ``` moreover have "\x. (?f Q0 x = ?f' Q0 x) \ (\i. ?f (Q i) x = ?f' (Q i) x) \ ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 977` ``` ?f (space M) x = ?f' (space M) x" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 978` ``` by (auto simp: indicator_def Q0) ``` 41705 1100512e16d8 add auto support for AE_mp hoelzl parents: 41689 diff changeset ` 979` ``` ultimately have "AE x. ?f (space M) x = ?f' (space M) x" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 980` ``` by (auto simp: AE_all_countable[symmetric]) ``` 41705 1100512e16d8 add auto support for AE_mp hoelzl parents: 41689 diff changeset ` 981` ``` then show "AE x. f x = f' x" by auto ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 982` ```qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 983` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 984` ```lemma (in sigma_finite_measure) density_unique: ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 985` ``` assumes f: "f \ borel_measurable M" "AE x. 0 \ f x" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 986` ``` assumes f': "f' \ borel_measurable M" "AE x. 0 \ f' x" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 987` ``` assumes eq: "\A. A \ sets M \ (\\<^isup>+x. f x * indicator A x \M) = (\\<^isup>+x. f' x * indicator A x \M)" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 988` ``` (is "\A. A \ sets M \ ?P f A = ?P f' A") ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 989` ``` shows "AE x. f x = f' x" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 990` ```proof - ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 991` ``` obtain h where h_borel: "h \ borel_measurable M" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 992` ``` and fin: "integral\<^isup>P M h \ \" and pos: "\x. x \ space M \ 0 < h x \ h x < \" "\x. 0 \ h x" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 993` ``` using Ex_finite_integrable_function by auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 994` ``` then have h_nn: "AE x. 0 \ h x" by auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 995` ``` let ?H = "M\ measure := \A. (\\<^isup>+x. h x * indicator A x \M) \" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 996` ``` have H: "measure_space ?H" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 997` ``` using h_borel h_nn by (rule measure_space_density) simp ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 998` ``` then interpret h: measure_space ?H . ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 999` ``` interpret h: finite_measure "M\ measure := \A. (\\<^isup>+x. h x * indicator A x \M) \" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1000` ``` by default (simp cong: positive_integral_cong add: fin) ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1001` ``` let ?fM = "M\measure := \A. (\\<^isup>+x. f x * indicator A x \M)\" ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1002` ``` interpret f: measure_space ?fM ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1003` ``` using f by (rule measure_space_density) simp ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1004` ``` let ?f'M = "M\measure := \A. (\\<^isup>+x. f' x * indicator A x \M)\" ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1005` ``` interpret f': measure_space ?f'M ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1006` ``` using f' by (rule measure_space_density) simp ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1007` ``` { fix A assume "A \ sets M" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1008` ``` then have "{x \ space M. h x * indicator A x \ 0} = A" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1009` ``` using pos(1) sets_into_space by (force simp: indicator_def) ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1010` ``` then have "(\\<^isup>+x. h x * indicator A x \M) = 0 \ A \ null_sets" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1011` ``` using h_borel `A \ sets M` h_nn by (subst positive_integral_0_iff) auto } ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1012` ``` note h_null_sets = this ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1013` ``` { fix A assume "A \ sets M" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1014` ``` have "(\\<^isup>+x. f x * (h x * indicator A x) \M) = (\\<^isup>+x. h x * indicator A x \?fM)" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1015` ``` using `A \ sets M` h_borel h_nn f f' ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1016` ``` by (intro positive_integral_translated_density[symmetric]) auto ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1017` ``` also have "\ = (\\<^isup>+x. h x * indicator A x \?f'M)" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1018` ``` by (rule f'.positive_integral_cong_measure) (simp_all add: eq) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1019` ``` also have "\ = (\\<^isup>+x. f' x * (h x * indicator A x) \M)" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1020` ``` using `A \ sets M` h_borel h_nn f f' ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1021` ``` by (intro positive_integral_translated_density) auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1022` ``` finally have "(\\<^isup>+x. h x * (f x * indicator A x) \M) = (\\<^isup>+x. h x * (f' x * indicator A x) \M)" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1023` ``` by (simp add: ac_simps) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1024` ``` then have "(\\<^isup>+x. (f x * indicator A x) \?H) = (\\<^isup>+x. (f' x * indicator A x) \?H)" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1025` ``` using `A \ sets M` h_borel h_nn f f' ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1026` ``` by (subst (asm) (1 2) positive_integral_translated_density[symmetric]) auto } ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1027` ``` then have "AE x in ?H. f x = f' x" using h_borel h_nn f f' ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1028` ``` by (intro h.density_unique_finite_measure absolutely_continuous_AE[OF H] density_is_absolutely_continuous) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1029` ``` simp_all ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1030` ``` then show "AE x. f x = f' x" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1031` ``` unfolding h.almost_everywhere_def almost_everywhere_def ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1032` ``` by (auto simp add: h_null_sets) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1033` ```qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1034` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1035` ```lemma (in sigma_finite_measure) sigma_finite_iff_density_finite: ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1036` ``` assumes \: "measure_space (M\measure := \\)" (is "measure_space ?N") ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1037` ``` and f: "f \ borel_measurable M" "AE x. 0 \ f x" ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1038` ``` and eq: "\A. A \ sets M \ \ A = (\\<^isup>+x. f x * indicator A x \M)" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1039` ``` shows "sigma_finite_measure (M\measure := \\) \ (AE x. f x \ \)" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1040` ```proof ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1041` ``` assume "sigma_finite_measure ?N" ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1042` ``` then interpret \: sigma_finite_measure ?N ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1043` ``` where "borel_measurable ?N = borel_measurable M" and "measure ?N = \" ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1044` ``` and "sets ?N = sets M" and "space ?N = space M" by (auto simp: measurable_def) ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1045` ``` from \.Ex_finite_integrable_function obtain h where ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1046` ``` h: "h \ borel_measurable M" "integral\<^isup>P ?N h \ \" and ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1047` ``` h_nn: "\x. 0 \ h x" and ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1048` ``` fin: "\x\space M. 0 < h x \ h x < \" by auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1049` ``` have "AE x. f x * h x \ \" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1050` ``` proof (rule AE_I') ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1051` ``` have "integral\<^isup>P ?N h = (\\<^isup>+x. f x * h x \M)" using f h h_nn ``` 41705 1100512e16d8 add auto support for AE_mp hoelzl parents: 41689 diff changeset ` 1052` ``` by (subst \.positive_integral_cong_measure[symmetric, ``` 1100512e16d8 add auto support for AE_mp hoelzl parents: 41689 diff changeset ` 1053` ``` of "M\ measure := \ A. \\<^isup>+x. f x * indicator A x \M \"]) ``` 1100512e16d8 add auto support for AE_mp hoelzl parents: 41689 diff changeset ` 1054` ``` (auto intro!: positive_integral_translated_density simp: eq) ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1055` ``` then have "(\\<^isup>+x. f x * h x \M) \ \" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1056` ``` using h(2) by simp ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1057` ``` then show "(\x. f x * h x) -` {\} \ space M \ null_sets" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1058` ``` using f h(1) by (auto intro!: positive_integral_PInf borel_measurable_vimage) ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1059` ``` qed auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1060` ``` then show "AE x. f x \ \" ``` 41705 1100512e16d8 add auto support for AE_mp hoelzl parents: 41689 diff changeset ` 1061` ``` using fin by (auto elim!: AE_Ball_mp) ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1062` ```next ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1063` ``` assume AE: "AE x. f x \ \" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1064` ``` from sigma_finite guess Q .. note Q = this ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1065` ``` interpret \: measure_space ?N ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1066` ``` where "borel_measurable ?N = borel_measurable M" and "measure ?N = \" ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1067` ``` and "sets ?N = sets M" and "space ?N = space M" using \ by (auto simp: measurable_def) ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1068` ``` def A \ "\i. f -` (case i of 0 \ {\} | Suc n \ {.. of_nat (Suc n)}) \ space M" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1069` ``` { fix i j have "A i \ Q j \ sets M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1070` ``` unfolding A_def using f Q ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1071` ``` apply (rule_tac Int) ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1072` ``` by (cases i) (auto intro: measurable_sets[OF f(1)]) } ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1073` ``` note A_in_sets = this ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1074` ``` let "?A n" = "case prod_decode n of (i,j) \ A i \ Q j" ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1075` ``` show "sigma_finite_measure ?N" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1076` ``` proof (default, intro exI conjI subsetI allI) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1077` ``` fix x assume "x \ range ?A" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1078` ``` then obtain n where n: "x = ?A n" by auto ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1079` ``` then show "x \ sets ?N" using A_in_sets by (cases "prod_decode n") auto ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1080` ``` next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1081` ``` have "(\i. ?A i) = (\i j. A i \ Q j)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1082` ``` proof safe ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1083` ``` fix x i j assume "x \ A i" "x \ Q j" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1084` ``` then show "x \ (\i. case prod_decode i of (i, j) \ A i \ Q j)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1085` ``` by (intro UN_I[of "prod_encode (i,j)"]) auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1086` ``` qed auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1087` ``` also have "\ = (\i. A i) \ space M" using Q by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1088` ``` also have "(\i. A i) = space M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1089` ``` proof safe ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1090` ``` fix x assume x: "x \ space M" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1091` ``` show "x \ (\i. A i)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1092` ``` proof (cases "f x") ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1093` ``` case PInf with x show ?thesis unfolding A_def by (auto intro: exI[of _ 0]) ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1094` ``` next ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1095` ``` case (real r) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1096` ``` with less_PInf_Ex_of_nat[of "f x"] obtain n where "f x < of_nat n" by (auto simp: real_eq_of_nat) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1097` ``` then show ?thesis using x real unfolding A_def by (auto intro!: exI[of _ "Suc n"]) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1098` ``` next ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1099` ``` case MInf with x show ?thesis ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1100` ``` unfolding A_def by (auto intro!: exI[of _ "Suc 0"]) ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1101` ``` qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1102` ``` qed (auto simp: A_def) ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1103` ``` finally show "(\i. ?A i) = space ?N" by simp ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1104` ``` next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1105` ``` fix n obtain i j where ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1106` ``` [simp]: "prod_decode n = (i, j)" by (cases "prod_decode n") auto ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1107` ``` have "(\\<^isup>+x. f x * indicator (A i \ Q j) x \M) \ \" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1108` ``` proof (cases i) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1109` ``` case 0 ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1110` ``` have "AE x. f x * indicator (A i \ Q j) x = 0" ``` 41705 1100512e16d8 add auto support for AE_mp hoelzl parents: 41689 diff changeset ` 1111` ``` using AE by (auto simp: A_def `i = 0`) ``` 1100512e16d8 add auto support for AE_mp hoelzl parents: 41689 diff changeset ` 1112` ``` from positive_integral_cong_AE[OF this] show ?thesis by simp ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1113` ``` next ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1114` ``` case (Suc n) ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1115` ``` then have "(\\<^isup>+x. f x * indicator (A i \ Q j) x \M) \ ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1116` ``` (\\<^isup>+x. of_nat (Suc n) * indicator (Q j) x \M)" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1117` ``` by (auto intro!: positive_integral_mono simp: indicator_def A_def) ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1118` ``` also have "\ = of_nat (Suc n) * \ (Q j)" ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1119` ``` using Q by (auto intro!: positive_integral_cmult_indicator) ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1120` ``` also have "\ < \" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1121` ``` using Q by (auto simp: real_eq_of_nat[symmetric]) ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1122` ``` finally show ?thesis by simp ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1123` ``` qed ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1124` ``` then show "measure ?N (?A n) \ \" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1125` ``` using A_in_sets Q eq by auto ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1126` ``` qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1127` ```qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1128` 40871 688f6ff859e1 Generalized simple_functionD and less_SUP_iff. hoelzl parents: 40859 diff changeset ` 1129` ```section "Radon-Nikodym derivative" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 1130` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1131` ```definition ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1132` ``` "RN_deriv M \ \ SOME f. f \ borel_measurable M \ (\x. 0 \ f x) \ ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1133` ``` (\A \ sets M. \ A = (\\<^isup>+x. f x * indicator A x \M))" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 1134` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1135` ```lemma (in sigma_finite_measure) RN_deriv_cong: ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1136` ``` assumes cong: "\A. A \ sets M \ measure M' A = \ A" "sets M' = sets M" "space M' = space M" ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1137` ``` and \: "\A. A \ sets M \ \' A = \ A" ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1138` ``` shows "RN_deriv M' \' x = RN_deriv M \ x" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1139` ```proof - ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1140` ``` interpret \': sigma_finite_measure M' ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1141` ``` using cong by (rule sigma_finite_measure_cong) ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1142` ``` show ?thesis ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1143` ``` unfolding RN_deriv_def ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1144` ``` by (simp add: cong \ positive_integral_cong_measure[OF cong] measurable_def) ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1145` ```qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1146` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 1147` ```lemma (in sigma_finite_measure) RN_deriv: ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1148` ``` assumes "measure_space (M\measure := \\)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 1149` ``` assumes "absolutely_continuous \" ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1150` ``` shows "RN_deriv M \ \ borel_measurable M" (is ?borel) ``` 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1151` ``` and "\A. A \ sets M \ \ A = (\\<^isup>+x. RN_deriv M \ x * indicator A x \M)" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 1152` ``` (is "\A. _ \ ?int A") ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1153` ``` and "0 \ RN_deriv M \ x" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 1154` ```proof - ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 1155` ``` note Ex = Radon_Nikodym[OF assms, unfolded Bex_def] ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1156` ``` then show ?borel unfolding RN_deriv_def by (rule someI2_ex) auto ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1157` ``` from Ex show "0 \ RN_deriv M \ x" unfolding RN_deriv_def ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1158` ``` by (rule someI2_ex) simp ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 1159` ``` fix A assume "A \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 1160` ``` from Ex show "?int A" unfolding RN_deriv_def ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 1161` ``` by (rule someI2_ex) (simp add: `A \ sets M`) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 1162` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: diff changeset ` 1163` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1164` ```lemma (in sigma_finite_measure) RN_deriv_positive_integral: ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1165` ``` assumes \: "measure_space (M\measure := \\)" "absolutely_continuous \" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1166` ``` and f: "f \ borel_measurable M" ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1167` ``` shows "integral\<^isup>P (M\measure := \\) f = (\\<^isup>+x. RN_deriv M \ x * f x \M)" ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1168` ```proof - ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1169` ``` interpret \: measure_space "M\measure := \\" by fact ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1170` ``` note RN = RN_deriv[OF \] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1171` ``` have "integral\<^isup>P (M\measure := \\) f = (\\<^isup>+x. max 0 (f x) \M\measure := \\)" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1172` ``` unfolding positive_integral_max_0 .. ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1173` ``` also have "(\\<^isup>+x. max 0 (f x) \M\measure := \\) = ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1174` ``` (\\<^isup>+x. max 0 (f x) \M\measure := \A. (\\<^isup>+x. RN_deriv M \ x * indicator A x \M)\)" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1175` ``` by (intro \.positive_integral_cong_measure[symmetric]) (simp_all add: RN(2)) ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1176` ``` also have "\ = (\\<^isup>+x. RN_deriv M \ x * max 0 (f x) \M)" ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1177` ``` by (intro positive_integral_translated_density) (auto simp add: RN f) ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1178` ``` also have "\ = (\\<^isup>+x. RN_deriv M \ x * f x \M)" ``` 41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1179` ``` using RN_deriv(3)[OF \] ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1180` ``` by (auto intro!: positive_integral_cong_pos split: split_if_asm ``` cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41832 diff changeset ` 1181` ``` simp: max_def extreal_mult_le_0_iff) ``` 40859 de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1182` ``` finally show ?thesis . ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1183` ```qed ``` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1184` de0b30e6c2d2 Support product spaces on sigma finite measures. hoelzl parents: 39097 diff changeset ` 1185` ```lemma (in sigma_finite_measure) RN_deriv_unique: ``` 41689 3e39b0e730d6 the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale; hoelzl parents: 41661 diff changeset ` 1186` ``` assumes \: "measure_space (M\measure := \\)" "absolutely_continuous \" ```