src/HOL/Probability/Radon_Nikodym.thy
 changeset 38656 d5d342611edb child 39092 98de40859858
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Mon Aug 23 19:35:57 2010 +0200
1.3 @@ -0,0 +1,1059 @@
1.4 +theory Radon_Nikodym
1.5 +imports Lebesgue_Integration
1.6 +begin
1.7 +
1.8 +lemma (in measure_space) measure_finitely_subadditive:
1.9 +  assumes "finite I" "A ` I \<subseteq> sets M"
1.10 +  shows "\<mu> (\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. \<mu> (A i))"
1.11 +using assms proof induct
1.12 +  case (insert i I)
1.13 +  then have "(\<Union>i\<in>I. A i) \<in> sets M" by (auto intro: finite_UN)
1.14 +  then have "\<mu> (\<Union>i\<in>insert i I. A i) \<le> \<mu> (A i) + \<mu> (\<Union>i\<in>I. A i)"
1.15 +    using insert by (simp add: measure_subadditive)
1.16 +  also have "\<dots> \<le> (\<Sum>i\<in>insert i I. \<mu> (A i))"
1.17 +    using insert by (auto intro!: add_left_mono)
1.18 +  finally show ?case .
1.19 +qed simp
1.20 +
1.21 +lemma (in sigma_algebra) borel_measurable_restricted:
1.22 +  fixes f :: "'a \<Rightarrow> pinfreal" assumes "A \<in> sets M"
1.23 +  shows "f \<in> borel_measurable (M\<lparr> space := A, sets := op \<inter> A ` sets M \<rparr>) \<longleftrightarrow>
1.24 +    (\<lambda>x. f x * indicator A x) \<in> borel_measurable M"
1.25 +    (is "f \<in> borel_measurable ?R \<longleftrightarrow> ?f \<in> borel_measurable M")
1.26 +proof -
1.27 +  interpret R: sigma_algebra ?R by (rule restricted_sigma_algebra[OF `A \<in> sets M`])
1.28 +  have *: "f \<in> borel_measurable ?R \<longleftrightarrow> ?f \<in> borel_measurable ?R"
1.29 +    by (auto intro!: measurable_cong)
1.30 +  show ?thesis unfolding *
1.31 +    unfolding in_borel_measurable_borel_space
1.32 +  proof (simp, safe)
1.33 +    fix S :: "pinfreal set" assume "S \<in> sets borel_space"
1.34 +      "\<forall>S\<in>sets borel_space. ?f -` S \<inter> A \<in> op \<inter> A ` sets M"
1.35 +    then have "?f -` S \<inter> A \<in> op \<inter> A ` sets M" by auto
1.36 +    then have f: "?f -` S \<inter> A \<in> sets M"
1.37 +      using `A \<in> sets M` sets_into_space by fastsimp
1.38 +    show "?f -` S \<inter> space M \<in> sets M"
1.39 +    proof cases
1.40 +      assume "0 \<in> S"
1.41 +      then have "?f -` S \<inter> space M = ?f -` S \<inter> A \<union> (space M - A)"
1.42 +        using `A \<in> sets M` sets_into_space by auto
1.43 +      then show ?thesis using f `A \<in> sets M` by (auto intro!: Un Diff)
1.44 +    next
1.45 +      assume "0 \<notin> S"
1.46 +      then have "?f -` S \<inter> space M = ?f -` S \<inter> A"
1.47 +        using `A \<in> sets M` sets_into_space
1.48 +        by (auto simp: indicator_def split: split_if_asm)
1.49 +      then show ?thesis using f by auto
1.50 +    qed
1.51 +  next
1.52 +    fix S :: "pinfreal set" assume "S \<in> sets borel_space"
1.53 +      "\<forall>S\<in>sets borel_space. ?f -` S \<inter> space M \<in> sets M"
1.54 +    then have f: "?f -` S \<inter> space M \<in> sets M" by auto
1.55 +    then show "?f -` S \<inter> A \<in> op \<inter> A ` sets M"
1.56 +      using `A \<in> sets M` sets_into_space
1.57 +      apply (simp add: image_iff)
1.58 +      apply (rule bexI[OF _ f])
1.59 +      by auto
1.60 +  qed
1.61 +qed
1.62 +
1.63 +lemma (in sigma_algebra) simple_function_eq_borel_measurable:
1.64 +  fixes f :: "'a \<Rightarrow> pinfreal"
1.65 +  shows "simple_function f \<longleftrightarrow>
1.66 +    finite (f`space M) \<and> f \<in> borel_measurable M"
1.67 +  using simple_function_borel_measurable[of f]
1.68 +    borel_measurable_simple_function[of f]
1.69 +  by (fastsimp simp: simple_function_def)
1.70 +
1.71 +lemma (in measure_space) simple_function_restricted:
1.72 +  fixes f :: "'a \<Rightarrow> pinfreal" assumes "A \<in> sets M"
1.73 +  shows "sigma_algebra.simple_function (M\<lparr> space := A, sets := op \<inter> A ` sets M \<rparr>) f \<longleftrightarrow> simple_function (\<lambda>x. f x * indicator A x)"
1.74 +    (is "sigma_algebra.simple_function ?R f \<longleftrightarrow> simple_function ?f")
1.75 +proof -
1.76 +  interpret R: sigma_algebra ?R by (rule restricted_sigma_algebra[OF `A \<in> sets M`])
1.77 +  have "finite (f`A) \<longleftrightarrow> finite (?f`space M)"
1.78 +  proof cases
1.79 +    assume "A = space M"
1.80 +    then have "f`A = ?f`space M" by (fastsimp simp: image_iff)
1.81 +    then show ?thesis by simp
1.82 +  next
1.83 +    assume "A \<noteq> space M"
1.84 +    then obtain x where x: "x \<in> space M" "x \<notin> A"
1.85 +      using sets_into_space `A \<in> sets M` by auto
1.86 +    have *: "?f`space M = f`A \<union> {0}"
1.87 +    proof (auto simp add: image_iff)
1.88 +      show "\<exists>x\<in>space M. f x = 0 \<or> indicator A x = 0"
1.89 +        using x by (auto intro!: bexI[of _ x])
1.90 +    next
1.91 +      fix x assume "x \<in> A"
1.92 +      then show "\<exists>y\<in>space M. f x = f y * indicator A y"
1.93 +        using `A \<in> sets M` sets_into_space by (auto intro!: bexI[of _ x])
1.94 +    next
1.95 +      fix x
1.96 +      assume "indicator A x \<noteq> (0::pinfreal)"
1.97 +      then have "x \<in> A" by (auto simp: indicator_def split: split_if_asm)
1.98 +      moreover assume "x \<in> space M" "\<forall>y\<in>A. ?f x \<noteq> f y"
1.99 +      ultimately show "f x = 0" by auto
1.100 +    qed
1.101 +    then show ?thesis by auto
1.102 +  qed
1.103 +  then show ?thesis
1.104 +    unfolding simple_function_eq_borel_measurable
1.105 +      R.simple_function_eq_borel_measurable
1.106 +    unfolding borel_measurable_restricted[OF `A \<in> sets M`]
1.107 +    by auto
1.108 +qed
1.109 +
1.110 +lemma (in measure_space) simple_integral_restricted:
1.111 +  assumes "A \<in> sets M"
1.112 +  assumes sf: "simple_function (\<lambda>x. f x * indicator A x)"
1.113 +  shows "measure_space.simple_integral (M\<lparr> space := A, sets := op \<inter> A ` sets M \<rparr>) \<mu> f = simple_integral (\<lambda>x. f x * indicator A x)"
1.114 +    (is "_ = simple_integral ?f")
1.115 +  unfolding measure_space.simple_integral_def[OF restricted_measure_space[OF `A \<in> sets M`]]
1.116 +  unfolding simple_integral_def
1.117 +proof (simp, safe intro!: setsum_mono_zero_cong_left)
1.118 +  from sf show "finite (?f ` space M)"
1.119 +    unfolding simple_function_def by auto
1.120 +next
1.121 +  fix x assume "x \<in> A"
1.122 +  then show "f x \<in> ?f ` space M"
1.123 +    using sets_into_space `A \<in> sets M` by (auto intro!: image_eqI[of _ _ x])
1.124 +next
1.125 +  fix x assume "x \<in> space M" "?f x \<notin> f`A"
1.126 +  then have "x \<notin> A" by (auto simp: image_iff)
1.127 +  then show "?f x * \<mu> (?f -` {?f x} \<inter> space M) = 0" by simp
1.128 +next
1.129 +  fix x assume "x \<in> A"
1.130 +  then have "f x \<noteq> 0 \<Longrightarrow>
1.131 +    f -` {f x} \<inter> A = ?f -` {f x} \<inter> space M"
1.132 +    using `A \<in> sets M` sets_into_space
1.133 +    by (auto simp: indicator_def split: split_if_asm)
1.134 +  then show "f x * \<mu> (f -` {f x} \<inter> A) =
1.135 +    f x * \<mu> (?f -` {f x} \<inter> space M)"
1.136 +    unfolding pinfreal_mult_cancel_left by auto
1.137 +qed
1.138 +
1.139 +lemma (in measure_space) positive_integral_restricted:
1.140 +  assumes "A \<in> sets M"
1.141 +  shows "measure_space.positive_integral (M\<lparr> space := A, sets := op \<inter> A ` sets M \<rparr>) \<mu> f = positive_integral (\<lambda>x. f x * indicator A x)"
1.142 +    (is "measure_space.positive_integral ?R \<mu> f = positive_integral ?f")
1.143 +proof -
1.144 +  have msR: "measure_space ?R \<mu>" by (rule restricted_measure_space[OF `A \<in> sets M`])
1.145 +  then interpret R: measure_space ?R \<mu> .
1.146 +  have saR: "sigma_algebra ?R" by fact
1.147 +  have *: "R.positive_integral f = R.positive_integral ?f"
1.148 +    by (auto intro!: R.positive_integral_cong)
1.149 +  show ?thesis
1.150 +    unfolding * R.positive_integral_def positive_integral_def
1.151 +    unfolding simple_function_restricted[OF `A \<in> sets M`]
1.152 +    apply (simp add: SUPR_def)
1.153 +    apply (rule arg_cong[where f=Sup])
1.154 +  proof (auto simp: image_iff simple_integral_restricted[OF `A \<in> sets M`])
1.155 +    fix g assume "simple_function (\<lambda>x. g x * indicator A x)"
1.156 +      "g \<le> f" "\<forall>x\<in>A. \<omega> \<noteq> g x"
1.157 +    then show "\<exists>x. simple_function x \<and> x \<le> (\<lambda>x. f x * indicator A x) \<and> (\<forall>y\<in>space M. \<omega> \<noteq> x y) \<and>
1.158 +      simple_integral (\<lambda>x. g x * indicator A x) = simple_integral x"
1.159 +      apply (rule_tac exI[of _ "\<lambda>x. g x * indicator A x"])
1.160 +      by (auto simp: indicator_def le_fun_def)
1.161 +  next
1.162 +    fix g assume g: "simple_function g" "g \<le> (\<lambda>x. f x * indicator A x)"
1.163 +      "\<forall>x\<in>space M. \<omega> \<noteq> g x"
1.164 +    then have *: "(\<lambda>x. g x * indicator A x) = g"
1.165 +      "\<And>x. g x * indicator A x = g x"
1.166 +      "\<And>x. g x \<le> f x"
1.167 +      by (auto simp: le_fun_def expand_fun_eq indicator_def split: split_if_asm)
1.168 +    from g show "\<exists>x. simple_function (\<lambda>xa. x xa * indicator A xa) \<and> x \<le> f \<and> (\<forall>xa\<in>A. \<omega> \<noteq> x xa) \<and>
1.169 +      simple_integral g = simple_integral (\<lambda>xa. x xa * indicator A xa)"
1.170 +      using `A \<in> sets M`[THEN sets_into_space]
1.171 +      apply (rule_tac exI[of _ "\<lambda>x. g x * indicator A x"])
1.172 +      by (fastsimp simp: le_fun_def *)
1.173 +  qed
1.174 +qed
1.175 +
1.176 +lemma (in sigma_algebra) borel_measurable_psuminf:
1.177 +  assumes "\<And>i. f i \<in> borel_measurable M"
1.178 +  shows "(\<lambda>x. (\<Sum>\<^isub>\<infinity> i. f i x)) \<in> borel_measurable M"
1.179 +  using assms unfolding psuminf_def
1.180 +  by (auto intro!: borel_measurable_SUP[unfolded SUPR_fun_expand])
1.181 +
1.182 +lemma (in sigma_finite_measure) disjoint_sigma_finite:
1.183 +  "\<exists>A::nat\<Rightarrow>'a set. range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and>
1.184 +    (\<forall>i. \<mu> (A i) \<noteq> \<omega>) \<and> disjoint_family A"
1.185 +proof -
1.186 +  obtain A :: "nat \<Rightarrow> 'a set" where
1.187 +    range: "range A \<subseteq> sets M" and
1.188 +    space: "(\<Union>i. A i) = space M" and
1.189 +    measure: "\<And>i. \<mu> (A i) \<noteq> \<omega>"
1.190 +    using sigma_finite by auto
1.191 +
1.192 +  note range' = range_disjointed_sets[OF range] range
1.193 +
1.194 +  { fix i
1.195 +    have "\<mu> (disjointed A i) \<le> \<mu> (A i)"
1.196 +      using range' disjointed_subset[of A i] by (auto intro!: measure_mono)
1.197 +    then have "\<mu> (disjointed A i) \<noteq> \<omega>"
1.198 +      using measure[of i] by auto }
1.199 +  with disjoint_family_disjointed UN_disjointed_eq[of A] space range'
1.200 +  show ?thesis by (auto intro!: exI[of _ "disjointed A"])
1.201 +qed
1.202 +
1.203 +lemma (in sigma_finite_measure) Ex_finite_integrable_function:
1.204 +  shows "\<exists>h\<in>borel_measurable M. positive_integral h \<noteq> \<omega> \<and> (\<forall>x\<in>space M. 0 < h x \<and> h x < \<omega>)"
1.205 +proof -
1.206 +  obtain A :: "nat \<Rightarrow> 'a set" where
1.207 +    range: "range A \<subseteq> sets M" and
1.208 +    space: "(\<Union>i. A i) = space M" and
1.209 +    measure: "\<And>i. \<mu> (A i) \<noteq> \<omega>" and
1.210 +    disjoint: "disjoint_family A"
1.211 +    using disjoint_sigma_finite by auto
1.212 +
1.213 +  let "?B i" = "2^Suc i * \<mu> (A i)"
1.214 +  have "\<forall>i. \<exists>x. 0 < x \<and> x < inverse (?B i)"
1.215 +  proof
1.216 +    fix i show "\<exists>x. 0 < x \<and> x < inverse (?B i)"
1.217 +    proof cases
1.218 +      assume "\<mu> (A i) = 0"
1.219 +      then show ?thesis by (auto intro!: exI[of _ 1])
1.220 +    next
1.221 +      assume not_0: "\<mu> (A i) \<noteq> 0"
1.222 +      then have "?B i \<noteq> \<omega>" using measure[of i] by auto
1.223 +      then have "inverse (?B i) \<noteq> 0" unfolding pinfreal_inverse_eq_0 by simp
1.224 +      then show ?thesis using measure[of i] not_0
1.225 +        by (auto intro!: exI[of _ "inverse (?B i) / 2"]
1.226 +                 simp: pinfreal_noteq_omega_Ex zero_le_mult_iff zero_less_mult_iff mult_le_0_iff power_le_zero_eq)
1.227 +    qed
1.228 +  qed
1.229 +  from choice[OF this] obtain n where n: "\<And>i. 0 < n i"
1.230 +    "\<And>i. n i < inverse (2^Suc i * \<mu> (A i))" by auto
1.231 +
1.232 +  let "?h x" = "\<Sum>\<^isub>\<infinity> i. n i * indicator (A i) x"
1.233 +  show ?thesis
1.234 +  proof (safe intro!: bexI[of _ ?h] del: notI)
1.235 +    have "positive_integral ?h = (\<Sum>\<^isub>\<infinity> i. n i * \<mu> (A i))"
1.236 +      apply (subst positive_integral_psuminf)
1.237 +      using range apply (fastsimp intro!: borel_measurable_pinfreal_times borel_measurable_const borel_measurable_indicator)
1.238 +      apply (subst positive_integral_cmult_indicator)
1.239 +      using range by auto
1.240 +    also have "\<dots> \<le> (\<Sum>\<^isub>\<infinity> i. Real ((1 / 2)^Suc i))"
1.241 +    proof (rule psuminf_le)
1.242 +      fix N show "n N * \<mu> (A N) \<le> Real ((1 / 2) ^ Suc N)"
1.243 +        using measure[of N] n[of N]
1.244 +        by (cases "n N") (auto simp: pinfreal_noteq_omega_Ex field_simps zero_le_mult_iff mult_le_0_iff mult_less_0_iff power_less_zero_eq power_le_zero_eq inverse_eq_divide less_divide_eq power_divide split: split_if_asm)
1.245 +    qed
1.246 +    also have "\<dots> = Real 1"
1.247 +      by (rule suminf_imp_psuminf, rule power_half_series, auto)
1.248 +    finally show "positive_integral ?h \<noteq> \<omega>" by auto
1.249 +  next
1.250 +    fix x assume "x \<in> space M"
1.251 +    then obtain i where "x \<in> A i" using space[symmetric] by auto
1.252 +    from psuminf_cmult_indicator[OF disjoint, OF this]
1.253 +    have "?h x = n i" by simp
1.254 +    then show "0 < ?h x" and "?h x < \<omega>" using n[of i] by auto
1.255 +  next
1.256 +    show "?h \<in> borel_measurable M" using range
1.257 +      by (auto intro!: borel_measurable_psuminf borel_measurable_pinfreal_times borel_measurable_indicator)
1.258 +  qed
1.259 +qed
1.260 +
1.261 +definition (in measure_space)
1.262 +  "absolutely_continuous \<nu> = (\<forall>N\<in>null_sets. \<nu> N = (0 :: pinfreal))"
1.263 +
1.264 +lemma (in finite_measure) Radon_Nikodym_aux_epsilon:
1.265 +  fixes e :: real assumes "0 < e"
1.266 +  assumes "finite_measure M s"
1.267 +  shows "\<exists>A\<in>sets M. real (\<mu> (space M)) - real (s (space M)) \<le>
1.268 +                    real (\<mu> A) - real (s A) \<and>
1.269 +                    (\<forall>B\<in>sets M. B \<subseteq> A \<longrightarrow> - e < real (\<mu> B) - real (s B))"
1.270 +proof -
1.271 +  let "?d A" = "real (\<mu> A) - real (s A)"
1.272 +  interpret M': finite_measure M s by fact
1.273 +
1.274 +  let "?A A" = "if (\<forall>B\<in>sets M. B \<subseteq> space M - A \<longrightarrow> -e < ?d B)
1.275 +    then {}
1.276 +    else (SOME B. B \<in> sets M \<and> B \<subseteq> space M - A \<and> ?d B \<le> -e)"
1.277 +  def A \<equiv> "\<lambda>n. ((\<lambda>B. B \<union> ?A B) ^^ n) {}"
1.278 +
1.279 +  have A_simps[simp]:
1.280 +    "A 0 = {}"
1.281 +    "\<And>n. A (Suc n) = (A n \<union> ?A (A n))" unfolding A_def by simp_all
1.282 +
1.283 +  { fix A assume "A \<in> sets M"
1.284 +    have "?A A \<in> sets M"
1.285 +      by (auto intro!: someI2[of _ _ "\<lambda>A. A \<in> sets M"] simp: not_less) }
1.286 +  note A'_in_sets = this
1.287 +
1.288 +  { fix n have "A n \<in> sets M"
1.289 +    proof (induct n)
1.290 +      case (Suc n) thus "A (Suc n) \<in> sets M"
1.291 +        using A'_in_sets[of "A n"] by (auto split: split_if_asm)
1.292 +    qed (simp add: A_def) }
1.293 +  note A_in_sets = this
1.294 +  hence "range A \<subseteq> sets M" by auto
1.295 +
1.296 +  { fix n B
1.297 +    assume Ex: "\<exists>B. B \<in> sets M \<and> B \<subseteq> space M - A n \<and> ?d B \<le> -e"
1.298 +    hence False: "\<not> (\<forall>B\<in>sets M. B \<subseteq> space M - A n \<longrightarrow> -e < ?d B)" by (auto simp: not_less)
1.299 +    have "?d (A (Suc n)) \<le> ?d (A n) - e" unfolding A_simps if_not_P[OF False]
1.300 +    proof (rule someI2_ex[OF Ex])
1.301 +      fix B assume "B \<in> sets M \<and> B \<subseteq> space M - A n \<and> ?d B \<le> - e"
1.302 +      hence "A n \<inter> B = {}" "B \<in> sets M" and dB: "?d B \<le> -e" by auto
1.303 +      hence "?d (A n \<union> B) = ?d (A n) + ?d B"
1.304 +        using `A n \<in> sets M` real_finite_measure_Union M'.real_finite_measure_Union by simp
1.305 +      also have "\<dots> \<le> ?d (A n) - e" using dB by simp
1.306 +      finally show "?d (A n \<union> B) \<le> ?d (A n) - e" .
1.307 +    qed }
1.308 +  note dA_epsilon = this
1.309 +
1.310 +  { fix n have "?d (A (Suc n)) \<le> ?d (A n)"
1.311 +    proof (cases "\<exists>B. B\<in>sets M \<and> B \<subseteq> space M - A n \<and> ?d B \<le> - e")
1.312 +      case True from dA_epsilon[OF this] show ?thesis using `0 < e` by simp
1.313 +    next
1.314 +      case False
1.315 +      hence "\<forall>B\<in>sets M. B \<subseteq> space M - A n \<longrightarrow> -e < ?d B" by (auto simp: not_le)
1.316 +      thus ?thesis by simp
1.317 +    qed }
1.318 +  note dA_mono = this
1.319 +
1.320 +  show ?thesis
1.321 +  proof (cases "\<exists>n. \<forall>B\<in>sets M. B \<subseteq> space M - A n \<longrightarrow> -e < ?d B")
1.322 +    case True then obtain n where B: "\<And>B. \<lbrakk> B \<in> sets M; B \<subseteq> space M - A n\<rbrakk> \<Longrightarrow> -e < ?d B" by blast
1.323 +    show ?thesis
1.324 +    proof (safe intro!: bexI[of _ "space M - A n"])
1.325 +      fix B assume "B \<in> sets M" "B \<subseteq> space M - A n"
1.326 +      from B[OF this] show "-e < ?d B" .
1.327 +    next
1.328 +      show "space M - A n \<in> sets M" by (rule compl_sets) fact
1.329 +    next
1.330 +      show "?d (space M) \<le> ?d (space M - A n)"
1.331 +      proof (induct n)
1.332 +        fix n assume "?d (space M) \<le> ?d (space M - A n)"
1.333 +        also have "\<dots> \<le> ?d (space M - A (Suc n))"
1.334 +          using A_in_sets sets_into_space dA_mono[of n]
1.335 +            real_finite_measure_Diff[of "space M"]
1.336 +            real_finite_measure_Diff[of "space M"]
1.337 +            M'.real_finite_measure_Diff[of "space M"]
1.338 +            M'.real_finite_measure_Diff[of "space M"]
1.339 +          by (simp del: A_simps)
1.340 +        finally show "?d (space M) \<le> ?d (space M - A (Suc n))" .
1.341 +      qed simp
1.342 +    qed
1.343 +  next
1.344 +    case False hence B: "\<And>n. \<exists>B. B\<in>sets M \<and> B \<subseteq> space M - A n \<and> ?d B \<le> - e"
1.345 +      by (auto simp add: not_less)
1.346 +    { fix n have "?d (A n) \<le> - real n * e"
1.347 +      proof (induct n)
1.348 +        case (Suc n) with dA_epsilon[of n, OF B] show ?case by (simp del: A_simps add: real_of_nat_Suc field_simps)
1.349 +      qed simp } note dA_less = this
1.350 +    have decseq: "decseq (\<lambda>n. ?d (A n))" unfolding decseq_eq_incseq
1.351 +    proof (rule incseq_SucI)
1.352 +      fix n show "- ?d (A n) \<le> - ?d (A (Suc n))" using dA_mono[of n] by auto
1.353 +    qed
1.354 +    from real_finite_continuity_from_below[of A] `range A \<subseteq> sets M`
1.355 +      M'.real_finite_continuity_from_below[of A]
1.356 +    have convergent: "(\<lambda>i. ?d (A i)) ----> ?d (\<Union>i. A i)"
1.357 +      by (auto intro!: LIMSEQ_diff)
1.358 +    obtain n :: nat where "- ?d (\<Union>i. A i) / e < real n" using reals_Archimedean2 by auto
1.359 +    moreover from order_trans[OF decseq_le[OF decseq convergent] dA_less]
1.360 +    have "real n \<le> - ?d (\<Union>i. A i) / e" using `0<e` by (simp add: field_simps)
1.361 +    ultimately show ?thesis by auto
1.362 +  qed
1.363 +qed
1.364 +
1.365 +lemma (in finite_measure) Radon_Nikodym_aux:
1.366 +  assumes "finite_measure M s"
1.367 +  shows "\<exists>A\<in>sets M. real (\<mu> (space M)) - real (s (space M)) \<le>
1.368 +                    real (\<mu> A) - real (s A) \<and>
1.369 +                    (\<forall>B\<in>sets M. B \<subseteq> A \<longrightarrow> 0 \<le> real (\<mu> B) - real (s B))"
1.370 +proof -
1.371 +  let "?d A" = "real (\<mu> A) - real (s A)"
1.372 +  let "?P A B n" = "A \<in> sets M \<and> A \<subseteq> B \<and> ?d B \<le> ?d A \<and> (\<forall>C\<in>sets M. C \<subseteq> A \<longrightarrow> - 1 / real (Suc n) < ?d C)"
1.373 +
1.374 +  interpret M': finite_measure M s by fact
1.375 +
1.376 +  let "?r S" = "M\<lparr> space := S, sets := (\<lambda>C. S \<inter> C)`sets M\<rparr>"
1.377 +
1.378 +  { fix S n
1.379 +    assume S: "S \<in> sets M"
1.380 +    hence **: "\<And>X. X \<in> op \<inter> S ` sets M \<longleftrightarrow> X \<in> sets M \<and> X \<subseteq> S" by auto
1.381 +    from M'.restricted_finite_measure[of S] restricted_finite_measure[of S] S
1.382 +    have "finite_measure (?r S) \<mu>" "0 < 1 / real (Suc n)"
1.383 +      "finite_measure (?r S) s" by auto
1.384 +    from finite_measure.Radon_Nikodym_aux_epsilon[OF this] guess X ..
1.385 +    hence "?P X S n"
1.386 +    proof (simp add: **, safe)
1.387 +      fix C assume C: "C \<in> sets M" "C \<subseteq> X" "X \<subseteq> S" and
1.388 +        *: "\<forall>B\<in>sets M. S \<inter> B \<subseteq> X \<longrightarrow> - (1 / real (Suc n)) < ?d (S \<inter> B)"
1.389 +      hence "C \<subseteq> S" "C \<subseteq> X" "S \<inter> C = C" by auto
1.390 +      with *[THEN bspec, OF `C \<in> sets M`]
1.391 +      show "- (1 / real (Suc n)) < ?d C" by auto
1.392 +    qed
1.393 +    hence "\<exists>A. ?P A S n" by auto }
1.394 +  note Ex_P = this
1.395 +
1.396 +  def A \<equiv> "nat_rec (space M) (\<lambda>n A. SOME B. ?P B A n)"
1.397 +  have A_Suc: "\<And>n. A (Suc n) = (SOME B. ?P B (A n) n)" by (simp add: A_def)
1.398 +  have A_0[simp]: "A 0 = space M" unfolding A_def by simp
1.399 +
1.400 +  { fix i have "A i \<in> sets M" unfolding A_def
1.401 +    proof (induct i)
1.402 +      case (Suc i)
1.403 +      from Ex_P[OF this, of i] show ?case unfolding nat_rec_Suc
1.404 +        by (rule someI2_ex) simp
1.405 +    qed simp }
1.406 +  note A_in_sets = this
1.407 +
1.408 +  { fix n have "?P (A (Suc n)) (A n) n"
1.409 +      using Ex_P[OF A_in_sets] unfolding A_Suc
1.410 +      by (rule someI2_ex) simp }
1.411 +  note P_A = this
1.412 +
1.413 +  have "range A \<subseteq> sets M" using A_in_sets by auto
1.414 +
1.415 +  have A_mono: "\<And>i. A (Suc i) \<subseteq> A i" using P_A by simp
1.416 +  have mono_dA: "mono (\<lambda>i. ?d (A i))" using P_A by (simp add: mono_iff_le_Suc)
1.417 +  have epsilon: "\<And>C i. \<lbrakk> C \<in> sets M; C \<subseteq> A (Suc i) \<rbrakk> \<Longrightarrow> - 1 / real (Suc i) < ?d C"
1.418 +      using P_A by auto
1.419 +
1.420 +  show ?thesis
1.421 +  proof (safe intro!: bexI[of _ "\<Inter>i. A i"])
1.422 +    show "(\<Inter>i. A i) \<in> sets M" using A_in_sets by auto
1.423 +    from `range A \<subseteq> sets M` A_mono
1.424 +      real_finite_continuity_from_above[of A]
1.425 +      M'.real_finite_continuity_from_above[of A]
1.426 +    have "(\<lambda>i. ?d (A i)) ----> ?d (\<Inter>i. A i)" by (auto intro!: LIMSEQ_diff)
1.427 +    thus "?d (space M) \<le> ?d (\<Inter>i. A i)" using mono_dA[THEN monoD, of 0 _]
1.428 +      by (rule_tac LIMSEQ_le_const) (auto intro!: exI)
1.429 +  next
1.430 +    fix B assume B: "B \<in> sets M" "B \<subseteq> (\<Inter>i. A i)"
1.431 +    show "0 \<le> ?d B"
1.432 +    proof (rule ccontr)
1.433 +      assume "\<not> 0 \<le> ?d B"
1.434 +      hence "0 < - ?d B" by auto
1.435 +      from ex_inverse_of_nat_Suc_less[OF this]
1.436 +      obtain n where *: "?d B < - 1 / real (Suc n)"
1.437 +        by (auto simp: real_eq_of_nat inverse_eq_divide field_simps)
1.438 +      have "B \<subseteq> A (Suc n)" using B by (auto simp del: nat_rec_Suc)
1.439 +      from epsilon[OF B(1) this] *
1.440 +      show False by auto
1.441 +    qed
1.442 +  qed
1.443 +qed
1.444 +
1.445 +lemma (in finite_measure) Radon_Nikodym_finite_measure:
1.446 +  assumes "finite_measure M \<nu>"
1.447 +  assumes "absolutely_continuous \<nu>"
1.448 +  shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
1.449 +proof -
1.450 +  interpret M': finite_measure M \<nu> using assms(1) .
1.451 +
1.452 +  def G \<equiv> "{g \<in> borel_measurable M. \<forall>A\<in>sets M. positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A}"
1.453 +  have "(\<lambda>x. 0) \<in> G" unfolding G_def by auto
1.454 +  hence "G \<noteq> {}" by auto
1.455 +
1.456 +  { fix f g assume f: "f \<in> G" and g: "g \<in> G"
1.457 +    have "(\<lambda>x. max (g x) (f x)) \<in> G" (is "?max \<in> G") unfolding G_def
1.458 +    proof safe
1.459 +      show "?max \<in> borel_measurable M" using f g unfolding G_def by auto
1.460 +
1.461 +      let ?A = "{x \<in> space M. f x \<le> g x}"
1.462 +      have "?A \<in> sets M" using f g unfolding G_def by auto
1.463 +
1.464 +      fix A assume "A \<in> sets M"
1.465 +      hence sets: "?A \<inter> A \<in> sets M" "(space M - ?A) \<inter> A \<in> sets M" using `?A \<in> sets M` by auto
1.466 +      have union: "((?A \<inter> A) \<union> ((space M - ?A) \<inter> A)) = A"
1.467 +        using sets_into_space[OF `A \<in> sets M`] by auto
1.468 +
1.469 +      have "\<And>x. x \<in> space M \<Longrightarrow> max (g x) (f x) * indicator A x =
1.470 +        g x * indicator (?A \<inter> A) x + f x * indicator ((space M - ?A) \<inter> A) x"
1.471 +        by (auto simp: indicator_def max_def)
1.472 +      hence "positive_integral (\<lambda>x. max (g x) (f x) * indicator A x) =
1.473 +        positive_integral (\<lambda>x. g x * indicator (?A \<inter> A) x) +
1.474 +        positive_integral (\<lambda>x. f x * indicator ((space M - ?A) \<inter> A) x)"
1.475 +        using f g sets unfolding G_def
1.476 +        by (auto cong: positive_integral_cong intro!: positive_integral_add borel_measurable_indicator)
1.477 +      also have "\<dots> \<le> \<nu> (?A \<inter> A) + \<nu> ((space M - ?A) \<inter> A)"
1.478 +        using f g sets unfolding G_def by (auto intro!: add_mono)
1.479 +      also have "\<dots> = \<nu> A"
1.480 +        using M'.measure_additive[OF sets] union by auto
1.481 +      finally show "positive_integral (\<lambda>x. max (g x) (f x) * indicator A x) \<le> \<nu> A" .
1.482 +    qed }
1.483 +  note max_in_G = this
1.484 +
1.485 +  { fix f g assume  "f \<up> g" and f: "\<And>i. f i \<in> G"
1.486 +    have "g \<in> G" unfolding G_def
1.487 +    proof safe
1.488 +      from `f \<up> g` have [simp]: "g = (SUP i. f i)" unfolding isoton_def by simp
1.489 +      have f_borel: "\<And>i. f i \<in> borel_measurable M" using f unfolding G_def by simp
1.490 +      thus "g \<in> borel_measurable M" by (auto intro!: borel_measurable_SUP)
1.491 +
1.492 +      fix A assume "A \<in> sets M"
1.493 +      hence "\<And>i. (\<lambda>x. f i x * indicator A x) \<in> borel_measurable M"
1.494 +        using f_borel by (auto intro!: borel_measurable_indicator)
1.495 +      from positive_integral_isoton[OF isoton_indicator[OF `f \<up> g`] this]
1.496 +      have SUP: "positive_integral (\<lambda>x. g x * indicator A x) =
1.497 +          (SUP i. positive_integral (\<lambda>x. f i x * indicator A x))"
1.498 +        unfolding isoton_def by simp
1.499 +      show "positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A" unfolding SUP
1.500 +        using f `A \<in> sets M` unfolding G_def by (auto intro!: SUP_leI)
1.501 +    qed }
1.502 +  note SUP_in_G = this
1.503 +
1.504 +  let ?y = "SUP g : G. positive_integral g"
1.505 +  have "?y \<le> \<nu> (space M)" unfolding G_def
1.506 +  proof (safe intro!: SUP_leI)
1.507 +    fix g assume "\<forall>A\<in>sets M. positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A"
1.508 +    from this[THEN bspec, OF top] show "positive_integral g \<le> \<nu> (space M)"
1.509 +      by (simp cong: positive_integral_cong)
1.510 +  qed
1.511 +  hence "?y \<noteq> \<omega>" using M'.finite_measure_of_space by auto
1.512 +  from SUPR_countable_SUPR[OF this `G \<noteq> {}`] guess ys .. note ys = this
1.513 +  hence "\<forall>n. \<exists>g. g\<in>G \<and> positive_integral g = ys n"
1.514 +  proof safe
1.515 +    fix n assume "range ys \<subseteq> positive_integral ` G"
1.516 +    hence "ys n \<in> positive_integral ` G" by auto
1.517 +    thus "\<exists>g. g\<in>G \<and> positive_integral g = ys n" by auto
1.518 +  qed
1.519 +  from choice[OF this] obtain gs where "\<And>i. gs i \<in> G" "\<And>n. positive_integral (gs n) = ys n" by auto
1.520 +  hence y_eq: "?y = (SUP i. positive_integral (gs i))" using ys by auto
1.521 +  let "?g i x" = "Max ((\<lambda>n. gs n x) ` {..i})"
1.522 +  def f \<equiv> "SUP i. ?g i"
1.523 +  have gs_not_empty: "\<And>i. (\<lambda>n. gs n x) ` {..i} \<noteq> {}" by auto
1.524 +  { fix i have "?g i \<in> G"
1.525 +    proof (induct i)
1.526 +      case 0 thus ?case by simp fact
1.527 +    next
1.528 +      case (Suc i)
1.529 +      with Suc gs_not_empty `gs (Suc i) \<in> G` show ?case
1.530 +        by (auto simp add: atMost_Suc intro!: max_in_G)
1.531 +    qed }
1.532 +  note g_in_G = this
1.533 +  have "\<And>x. \<forall>i. ?g i x \<le> ?g (Suc i) x"
1.534 +    using gs_not_empty by (simp add: atMost_Suc)
1.535 +  hence isoton_g: "?g \<up> f" by (simp add: isoton_def le_fun_def f_def)
1.536 +  from SUP_in_G[OF this g_in_G] have "f \<in> G" .
1.537 +  hence [simp, intro]: "f \<in> borel_measurable M" unfolding G_def by auto
1.538 +
1.539 +  have "(\<lambda>i. positive_integral (?g i)) \<up> positive_integral f"
1.540 +    using isoton_g g_in_G by (auto intro!: positive_integral_isoton simp: G_def f_def)
1.541 +  hence "positive_integral f = (SUP i. positive_integral (?g i))"
1.542 +    unfolding isoton_def by simp
1.543 +  also have "\<dots> = ?y"
1.544 +  proof (rule antisym)
1.545 +    show "(SUP i. positive_integral (?g i)) \<le> ?y"
1.546 +      using g_in_G by (auto intro!: exI Sup_mono simp: SUPR_def)
1.547 +    show "?y \<le> (SUP i. positive_integral (?g i))" unfolding y_eq
1.548 +      by (auto intro!: SUP_mono positive_integral_mono Max_ge)
1.549 +  qed
1.550 +  finally have int_f_eq_y: "positive_integral f = ?y" .
1.551 +
1.552 +  let "?t A" = "\<nu> A - positive_integral (\<lambda>x. f x * indicator A x)"
1.553 +
1.554 +  have "finite_measure M ?t"
1.555 +  proof
1.556 +    show "?t {} = 0" by simp
1.557 +    show "?t (space M) \<noteq> \<omega>" using M'.finite_measure by simp
1.558 +    show "countably_additive M ?t" unfolding countably_additive_def
1.559 +    proof safe
1.560 +      fix A :: "nat \<Rightarrow> 'a set"  assume A: "range A \<subseteq> sets M" "disjoint_family A"
1.561 +      have "(\<Sum>\<^isub>\<infinity> n. positive_integral (\<lambda>x. f x * indicator (A n) x))
1.562 +        = positive_integral (\<lambda>x. (\<Sum>\<^isub>\<infinity>n. f x * indicator (A n) x))"
1.563 +        using `range A \<subseteq> sets M`
1.564 +        by (rule_tac positive_integral_psuminf[symmetric]) (auto intro!: borel_measurable_indicator)
1.565 +      also have "\<dots> = positive_integral (\<lambda>x. f x * indicator (\<Union>n. A n) x)"
1.566 +        apply (rule positive_integral_cong)
1.567 +        apply (subst psuminf_cmult_right)
1.568 +        unfolding psuminf_indicator[OF `disjoint_family A`] ..
1.569 +      finally have "(\<Sum>\<^isub>\<infinity> n. positive_integral (\<lambda>x. f x * indicator (A n) x))
1.570 +        = positive_integral (\<lambda>x. f x * indicator (\<Union>n. A n) x)" .
1.571 +      moreover have "(\<Sum>\<^isub>\<infinity>n. \<nu> (A n)) = \<nu> (\<Union>n. A n)"
1.572 +        using M'.measure_countably_additive A by (simp add: comp_def)
1.573 +      moreover have "\<And>i. positive_integral (\<lambda>x. f x * indicator (A i) x) \<le> \<nu> (A i)"
1.574 +          using A `f \<in> G` unfolding G_def by auto
1.575 +      moreover have v_fin: "\<nu> (\<Union>i. A i) \<noteq> \<omega>" using M'.finite_measure A by (simp add: countable_UN)
1.576 +      moreover {
1.577 +        have "positive_integral (\<lambda>x. f x * indicator (\<Union>i. A i) x) \<le> \<nu> (\<Union>i. A i)"
1.578 +          using A `f \<in> G` unfolding G_def by (auto simp: countable_UN)
1.579 +        also have "\<nu> (\<Union>i. A i) < \<omega>" using v_fin by (simp add: pinfreal_less_\<omega>)
1.580 +        finally have "positive_integral (\<lambda>x. f x * indicator (\<Union>i. A i) x) \<noteq> \<omega>"
1.581 +          by (simp add: pinfreal_less_\<omega>) }
1.582 +      ultimately
1.583 +      show "(\<Sum>\<^isub>\<infinity> n. ?t (A n)) = ?t (\<Union>i. A i)"
1.584 +        apply (subst psuminf_minus) by simp_all
1.585 +    qed
1.586 +  qed
1.587 +  then interpret M: finite_measure M ?t .
1.588 +
1.589 +  have ac: "absolutely_continuous ?t" using `absolutely_continuous \<nu>` unfolding absolutely_continuous_def by auto
1.590 +
1.591 +  have upper_bound: "\<forall>A\<in>sets M. ?t A \<le> 0"
1.592 +  proof (rule ccontr)
1.593 +    assume "\<not> ?thesis"
1.594 +    then obtain A where A: "A \<in> sets M" and pos: "0 < ?t A"
1.595 +      by (auto simp: not_le)
1.596 +    note pos
1.597 +    also have "?t A \<le> ?t (space M)"
1.598 +      using M.measure_mono[of A "space M"] A sets_into_space by simp
1.599 +    finally have pos_t: "0 < ?t (space M)" by simp
1.600 +    moreover
1.601 +    hence pos_M: "0 < \<mu> (space M)"
1.602 +      using ac top unfolding absolutely_continuous_def by auto
1.603 +    moreover
1.604 +    have "positive_integral (\<lambda>x. f x * indicator (space M) x) \<le> \<nu> (space M)"
1.605 +      using `f \<in> G` unfolding G_def by auto
1.606 +    hence "positive_integral (\<lambda>x. f x * indicator (space M) x) \<noteq> \<omega>"
1.607 +      using M'.finite_measure_of_space by auto
1.608 +    moreover
1.609 +    def b \<equiv> "?t (space M) / \<mu> (space M) / 2"
1.610 +    ultimately have b: "b \<noteq> 0" "b \<noteq> \<omega>"
1.611 +      using M'.finite_measure_of_space
1.612 +      by (auto simp: pinfreal_inverse_eq_0 finite_measure_of_space)
1.613 +
1.614 +    have "finite_measure M (\<lambda>A. b * \<mu> A)" (is "finite_measure M ?b")
1.615 +    proof
1.616 +      show "?b {} = 0" by simp
1.617 +      show "?b (space M) \<noteq> \<omega>" using finite_measure_of_space b by auto
1.618 +      show "countably_additive M ?b"
1.619 +        unfolding countably_additive_def psuminf_cmult_right
1.620 +        using measure_countably_additive by auto
1.621 +    qed
1.622 +
1.623 +    from M.Radon_Nikodym_aux[OF this]
1.624 +    obtain A0 where "A0 \<in> sets M" and
1.625 +      space_less_A0: "real (?t (space M)) - real (b * \<mu> (space M)) \<le> real (?t A0) - real (b * \<mu> A0)" and
1.626 +      *: "\<And>B. \<lbrakk> B \<in> sets M ; B \<subseteq> A0 \<rbrakk> \<Longrightarrow> 0 \<le> real (?t B) - real (b * \<mu> B)" by auto
1.627 +    { fix B assume "B \<in> sets M" "B \<subseteq> A0"
1.628 +      with *[OF this] have "b * \<mu> B \<le> ?t B"
1.629 +        using M'.finite_measure b finite_measure
1.630 +        by (cases "b * \<mu> B", cases "?t B") (auto simp: field_simps) }
1.631 +    note bM_le_t = this
1.632 +
1.633 +    let "?f0 x" = "f x + b * indicator A0 x"
1.634 +
1.635 +    { fix A assume A: "A \<in> sets M"
1.636 +      hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
1.637 +      have "positive_integral (\<lambda>x. ?f0 x  * indicator A x) =
1.638 +        positive_integral (\<lambda>x. f x * indicator A x + b * indicator (A \<inter> A0) x)"
1.639 +        by (auto intro!: positive_integral_cong simp: field_simps indicator_inter_arith)
1.640 +      hence "positive_integral (\<lambda>x. ?f0 x * indicator A x) =
1.641 +          positive_integral (\<lambda>x. f x * indicator A x) + b * \<mu> (A \<inter> A0)"
1.642 +        using `A0 \<in> sets M` `A \<inter> A0 \<in> sets M` A
1.643 +        by (simp add: borel_measurable_indicator positive_integral_add positive_integral_cmult_indicator) }
1.644 +    note f0_eq = this
1.645 +
1.646 +    { fix A assume A: "A \<in> sets M"
1.647 +      hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
1.648 +      have f_le_v: "positive_integral (\<lambda>x. f x * indicator A x) \<le> \<nu> A"
1.649 +        using `f \<in> G` A unfolding G_def by auto
1.650 +      note f0_eq[OF A]
1.651 +      also have "positive_integral (\<lambda>x. f x * indicator A x) + b * \<mu> (A \<inter> A0) \<le>
1.652 +          positive_integral (\<lambda>x. f x * indicator A x) + ?t (A \<inter> A0)"
1.653 +        using bM_le_t[OF `A \<inter> A0 \<in> sets M`] `A \<in> sets M` `A0 \<in> sets M`
1.654 +        by (auto intro!: add_left_mono)
1.655 +      also have "\<dots> \<le> positive_integral (\<lambda>x. f x * indicator A x) + ?t A"
1.656 +        using M.measure_mono[simplified, OF _ `A \<inter> A0 \<in> sets M` `A \<in> sets M`]
1.657 +        by (auto intro!: add_left_mono)
1.658 +      also have "\<dots> \<le> \<nu> A"
1.659 +        using f_le_v M'.finite_measure[simplified, OF `A \<in> sets M`]
1.660 +        by (cases "positive_integral (\<lambda>x. f x * indicator A x)", cases "\<nu> A", auto)
1.661 +      finally have "positive_integral (\<lambda>x. ?f0 x * indicator A x) \<le> \<nu> A" . }
1.662 +    hence "?f0 \<in> G" using `A0 \<in> sets M` unfolding G_def
1.663 +      by (auto intro!: borel_measurable_indicator borel_measurable_pinfreal_add borel_measurable_pinfreal_times)
1.664 +
1.665 +    have real: "?t (space M) \<noteq> \<omega>" "?t A0 \<noteq> \<omega>"
1.666 +      "b * \<mu> (space M) \<noteq> \<omega>" "b * \<mu> A0 \<noteq> \<omega>"
1.667 +      using `A0 \<in> sets M` b
1.668 +        finite_measure[of A0] M.finite_measure[of A0]
1.669 +        finite_measure_of_space M.finite_measure_of_space
1.670 +      by auto
1.671 +
1.672 +    have int_f_finite: "positive_integral f \<noteq> \<omega>"
1.673 +      using M'.finite_measure_of_space pos_t unfolding pinfreal_zero_less_diff_iff
1.674 +      by (auto cong: positive_integral_cong)
1.675 +
1.676 +    have "?t (space M) > b * \<mu> (space M)" unfolding b_def
1.677 +      apply (simp add: field_simps)
1.678 +      apply (subst mult_assoc[symmetric])
1.679 +      apply (subst pinfreal_mult_inverse)
1.680 +      using finite_measure_of_space M'.finite_measure_of_space pos_t pos_M
1.681 +      using pinfreal_mult_strict_right_mono[of "Real (1/2)" 1 "?t (space M)"]
1.682 +      by simp_all
1.683 +    hence  "0 < ?t (space M) - b * \<mu> (space M)"
1.684 +      by (simp add: pinfreal_zero_less_diff_iff)
1.685 +    also have "\<dots> \<le> ?t A0 - b * \<mu> A0"
1.686 +      using space_less_A0 pos_M pos_t b real[unfolded pinfreal_noteq_omega_Ex] by auto
1.687 +    finally have "b * \<mu> A0 < ?t A0" unfolding pinfreal_zero_less_diff_iff .
1.688 +    hence "0 < ?t A0" by auto
1.689 +    hence "0 < \<mu> A0" using ac unfolding absolutely_continuous_def
1.690 +      using `A0 \<in> sets M` by auto
1.691 +    hence "0 < b * \<mu> A0" using b by auto
1.692 +
1.693 +    from int_f_finite this
1.694 +    have "?y + 0 < positive_integral f + b * \<mu> A0" unfolding int_f_eq_y
1.695 +      by (rule pinfreal_less_add)
1.696 +    also have "\<dots> = positive_integral ?f0" using f0_eq[OF top] `A0 \<in> sets M` sets_into_space
1.697 +      by (simp cong: positive_integral_cong)
1.698 +    finally have "?y < positive_integral ?f0" by simp
1.699 +
1.700 +    moreover from `?f0 \<in> G` have "positive_integral ?f0 \<le> ?y" by (auto intro!: le_SUPI)
1.701 +    ultimately show False by auto
1.702 +  qed
1.703 +
1.704 +  show ?thesis
1.705 +  proof (safe intro!: bexI[of _ f])
1.706 +    fix A assume "A\<in>sets M"
1.707 +    show "\<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
1.708 +    proof (rule antisym)
1.709 +      show "positive_integral (\<lambda>x. f x * indicator A x) \<le> \<nu> A"
1.710 +        using `f \<in> G` `A \<in> sets M` unfolding G_def by auto
1.711 +      show "\<nu> A \<le> positive_integral (\<lambda>x. f x * indicator A x)"
1.712 +        using upper_bound[THEN bspec, OF `A \<in> sets M`]
1.713 +         by (simp add: pinfreal_zero_le_diff)
1.714 +    qed
1.715 +  qed simp
1.716 +qed
1.717 +
1.718 +lemma (in finite_measure) Radon_Nikodym_finite_measure_infinite:
1.719 +  assumes "measure_space M \<nu>"
1.720 +  assumes "absolutely_continuous \<nu>"
1.721 +  shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
1.722 +proof -
1.723 +  interpret v: measure_space M \<nu> by fact
1.724 +  let ?Q = "{Q\<in>sets M. \<nu> Q \<noteq> \<omega>}"
1.725 +  let ?a = "SUP Q:?Q. \<mu> Q"
1.726 +
1.727 +  have "{} \<in> ?Q" using v.empty_measure by auto
1.728 +  then have Q_not_empty: "?Q \<noteq> {}" by blast
1.729 +
1.730 +  have "?a \<le> \<mu> (space M)" using sets_into_space
1.731 +    by (auto intro!: SUP_leI measure_mono top)
1.732 +  then have "?a \<noteq> \<omega>" using finite_measure_of_space
1.733 +    by auto
1.734 +  from SUPR_countable_SUPR[OF this Q_not_empty]
1.735 +  obtain Q'' where "range Q'' \<subseteq> \<mu> ` ?Q" and a: "?a = (SUP i::nat. Q'' i)"
1.736 +    by auto
1.737 +  then have "\<forall>i. \<exists>Q'. Q'' i = \<mu> Q' \<and> Q' \<in> ?Q" by auto
1.738 +  from choice[OF this] obtain Q' where Q': "\<And>i. Q'' i = \<mu> (Q' i)" "\<And>i. Q' i \<in> ?Q"
1.739 +    by auto
1.740 +  then have a_Lim: "?a = (SUP i::nat. \<mu> (Q' i))" using a by simp
1.741 +  let "?O n" = "\<Union>i\<le>n. Q' i"
1.742 +  have Union: "(SUP i. \<mu> (?O i)) = \<mu> (\<Union>i. ?O i)"
1.743 +  proof (rule continuity_from_below[of ?O])
1.744 +    show "range ?O \<subseteq> sets M" using Q' by (auto intro!: finite_UN)
1.745 +    show "\<And>i. ?O i \<subseteq> ?O (Suc i)" by fastsimp
1.746 +  qed
1.747 +
1.748 +  have Q'_sets: "\<And>i. Q' i \<in> sets M" using Q' by auto
1.749 +
1.750 +  have O_sets: "\<And>i. ?O i \<in> sets M"
1.751 +     using Q' by (auto intro!: finite_UN Un)
1.752 +  then have O_in_G: "\<And>i. ?O i \<in> ?Q"
1.753 +  proof (safe del: notI)
1.754 +    fix i have "Q' ` {..i} \<subseteq> sets M"
1.755 +      using Q' by (auto intro: finite_UN)
1.756 +    with v.measure_finitely_subadditive[of "{.. i}" Q']
1.757 +    have "\<nu> (?O i) \<le> (\<Sum>i\<le>i. \<nu> (Q' i))" by auto
1.758 +    also have "\<dots> < \<omega>" unfolding setsum_\<omega> pinfreal_less_\<omega> using Q' by auto
1.759 +    finally show "\<nu> (?O i) \<noteq> \<omega>" unfolding pinfreal_less_\<omega> by auto
1.760 +  qed auto
1.761 +  have O_mono: "\<And>n. ?O n \<subseteq> ?O (Suc n)" by fastsimp
1.762 +
1.763 +  have a_eq: "?a = \<mu> (\<Union>i. ?O i)" unfolding Union[symmetric]
1.764 +  proof (rule antisym)
1.765 +    show "?a \<le> (SUP i. \<mu> (?O i))" unfolding a_Lim
1.766 +      using Q' by (auto intro!: SUP_mono measure_mono finite_UN)
1.767 +    show "(SUP i. \<mu> (?O i)) \<le> ?a" unfolding SUPR_def
1.768 +    proof (safe intro!: Sup_mono, unfold bex_simps)
1.769 +      fix i
1.770 +      have *: "(\<Union>Q' ` {..i}) = ?O i" by auto
1.771 +      then show "\<exists>x. (x \<in> sets M \<and> \<nu> x \<noteq> \<omega>) \<and>
1.772 +        \<mu> (\<Union>Q' ` {..i}) \<le> \<mu> x"
1.773 +        using O_in_G[of i] by (auto intro!: exI[of _ "?O i"])
1.774 +    qed
1.775 +  qed
1.776 +
1.777 +  let "?O_0" = "(\<Union>i. ?O i)"
1.778 +  have "?O_0 \<in> sets M" using Q' by auto
1.779 +
1.780 +  { fix A assume *: "A \<in> ?Q" "A \<subseteq> space M - ?O_0"
1.781 +    then have "\<mu> ?O_0 + \<mu> A = \<mu> (?O_0 \<union> A)"
1.782 +      using Q' by (auto intro!: measure_additive countable_UN)
1.783 +    also have "\<dots> = (SUP i. \<mu> (?O i \<union> A))"
1.784 +    proof (rule continuity_from_below[of "\<lambda>i. ?O i \<union> A", symmetric, simplified])
1.785 +      show "range (\<lambda>i. ?O i \<union> A) \<subseteq> sets M"
1.786 +        using * O_sets by auto
1.787 +    qed fastsimp
1.788 +    also have "\<dots> \<le> ?a"
1.789 +    proof (safe intro!: SUPR_bound)
1.790 +      fix i have "?O i \<union> A \<in> ?Q"
1.791 +      proof (safe del: notI)
1.792 +        show "?O i \<union> A \<in> sets M" using O_sets * by auto
1.793 +        from O_in_G[of i]
1.794 +        moreover have "\<nu> (?O i \<union> A) \<le> \<nu> (?O i) + \<nu> A"
1.795 +          using v.measure_subadditive[of "?O i" A] * O_sets by auto
1.796 +        ultimately show "\<nu> (?O i \<union> A) \<noteq> \<omega>"
1.797 +          using * by auto
1.798 +      qed
1.799 +      then show "\<mu> (?O i \<union> A) \<le> ?a" by (rule le_SUPI)
1.800 +    qed
1.801 +    finally have "\<mu> A = 0" unfolding a_eq using finite_measure[OF `?O_0 \<in> sets M`]
1.802 +      by (cases "\<mu> A") (auto simp: pinfreal_noteq_omega_Ex) }
1.803 +  note stetic = this
1.804 +
1.805 +  def Q \<equiv> "\<lambda>i. case i of 0 \<Rightarrow> ?O 0 | Suc n \<Rightarrow> ?O (Suc n) - ?O n"
1.806 +
1.807 +  { fix i have "Q i \<in> sets M" unfolding Q_def using Q'[of 0] by (cases i) (auto intro: O_sets) }
1.808 +  note Q_sets = this
1.809 +
1.810 +  { fix i have "\<nu> (Q i) \<noteq> \<omega>"
1.811 +    proof (cases i)
1.812 +      case 0 then show ?thesis
1.813 +        unfolding Q_def using Q'[of 0] by simp
1.814 +    next
1.815 +      case (Suc n)
1.816 +      then show ?thesis unfolding Q_def
1.817 +        using `?O n \<in> ?Q` `?O (Suc n) \<in> ?Q` O_mono
1.818 +        using v.measure_Diff[of "?O n" "?O (Suc n)"] by auto
1.819 +    qed }
1.820 +  note Q_omega = this
1.821 +
1.822 +  { fix j have "(\<Union>i\<le>j. ?O i) = (\<Union>i\<le>j. Q i)"
1.823 +    proof (induct j)
1.824 +      case 0 then show ?case by (simp add: Q_def)
1.825 +    next
1.826 +      case (Suc j)
1.827 +      have eq: "\<And>j. (\<Union>i\<le>j. ?O i) = (\<Union>i\<le>j. Q' i)" by fastsimp
1.828 +      have "{..j} \<union> {..Suc j} = {..Suc j}" by auto
1.829 +      then have "(\<Union>i\<le>Suc j. Q' i) = (\<Union>i\<le>j. Q' i) \<union> Q (Suc j)"
1.830 +        by (simp add: UN_Un[symmetric] Q_def del: UN_Un)
1.831 +      then show ?case using Suc by (auto simp add: eq atMost_Suc)
1.832 +    qed }
1.833 +  then have "(\<Union>j. (\<Union>i\<le>j. ?O i)) = (\<Union>j. (\<Union>i\<le>j. Q i))" by simp
1.834 +  then have O_0_eq_Q: "?O_0 = (\<Union>j. Q j)" by fastsimp
1.835 +
1.836 +  have "\<forall>i. \<exists>f. f\<in>borel_measurable M \<and> (\<forall>A\<in>sets M.
1.837 +    \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f x * indicator (Q i \<inter> A) x))"
1.838 +  proof
1.839 +    fix i
1.840 +    have indicator_eq: "\<And>f x A. (f x :: pinfreal) * indicator (Q i \<inter> A) x * indicator (Q i) x
1.841 +      = (f x * indicator (Q i) x) * indicator A x"
1.842 +      unfolding indicator_def by auto
1.843 +
1.844 +    have fm: "finite_measure (M\<lparr>space := Q i, sets := op \<inter> (Q i) ` sets M\<rparr>) \<mu>"
1.845 +      (is "finite_measure ?R \<mu>") by (rule restricted_finite_measure[OF Q_sets[of i]])
1.846 +    then interpret R: finite_measure ?R .
1.847 +    have fmv: "finite_measure ?R \<nu>"
1.848 +      unfolding finite_measure_def finite_measure_axioms_def
1.849 +    proof
1.850 +      show "measure_space ?R \<nu>"
1.851 +        using v.restricted_measure_space Q_sets[of i] by auto
1.852 +      show "\<nu>  (space ?R) \<noteq> \<omega>"
1.853 +        using Q_omega by simp
1.854 +    qed
1.855 +    have "R.absolutely_continuous \<nu>"
1.856 +      using `absolutely_continuous \<nu>` `Q i \<in> sets M`
1.857 +      by (auto simp: R.absolutely_continuous_def absolutely_continuous_def)
1.858 +    from finite_measure.Radon_Nikodym_finite_measure[OF fm fmv this]
1.859 +    obtain f where f: "(\<lambda>x. f x * indicator (Q i) x) \<in> borel_measurable M"
1.860 +      and f_int: "\<And>A. A\<in>sets M \<Longrightarrow> \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. (f x * indicator (Q i) x) * indicator A x)"
1.861 +      unfolding Bex_def borel_measurable_restricted[OF `Q i \<in> sets M`]
1.862 +        positive_integral_restricted[OF `Q i \<in> sets M`] by (auto simp: indicator_eq)
1.863 +    then show "\<exists>f. f\<in>borel_measurable M \<and> (\<forall>A\<in>sets M.
1.864 +      \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f x * indicator (Q i \<inter> A) x))"
1.865 +      by (fastsimp intro!: exI[of _ "\<lambda>x. f x * indicator (Q i) x"] positive_integral_cong
1.866 +          simp: indicator_def)
1.867 +  qed
1.868 +  from choice[OF this] obtain f where borel: "\<And>i. f i \<in> borel_measurable M"
1.869 +    and f: "\<And>A i. A \<in> sets M \<Longrightarrow>
1.870 +      \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f i x * indicator (Q i \<inter> A) x)"
1.871 +    by auto
1.872 +  let "?f x" =
1.873 +    "(\<Sum>\<^isub>\<infinity> i. f i x * indicator (Q i) x) + \<omega> * indicator (space M - ?O_0) x"
1.874 +  show ?thesis
1.875 +  proof (safe intro!: bexI[of _ ?f])
1.876 +    show "?f \<in> borel_measurable M"
1.877 +      by (safe intro!: borel_measurable_psuminf borel_measurable_pinfreal_times
1.878 +        borel_measurable_pinfreal_add borel_measurable_indicator
1.879 +        borel_measurable_const borel Q_sets O_sets Diff countable_UN)
1.880 +    fix A assume "A \<in> sets M"
1.881 +    let ?C = "(space M - (\<Union>i. Q i)) \<inter> A"
1.882 +    have *:
1.883 +      "\<And>x i. indicator A x * (f i x * indicator (Q i) x) =
1.884 +        f i x * indicator (Q i \<inter> A) x"
1.885 +      "\<And>x i. (indicator A x * indicator (space M - (\<Union>i. UNION {..i} Q')) x :: pinfreal) =
1.886 +        indicator ?C x" unfolding O_0_eq_Q by (auto simp: indicator_def)
1.887 +    have "positive_integral (\<lambda>x. ?f x * indicator A x) =
1.888 +      (\<Sum>\<^isub>\<infinity> i. \<nu> (Q i \<inter> A)) + \<omega> * \<mu> ?C"
1.889 +      unfolding f[OF `A \<in> sets M`]
1.890 +      apply (simp del: pinfreal_times(2) add: field_simps)
1.891 +      apply (subst positive_integral_add)
1.892 +      apply (safe intro!: borel_measurable_pinfreal_times Diff borel_measurable_const
1.893 +        borel_measurable_psuminf borel_measurable_indicator `A \<in> sets M` Q_sets borel countable_UN Q'_sets)
1.894 +      unfolding psuminf_cmult_right[symmetric]
1.895 +      apply (subst positive_integral_psuminf)
1.896 +      apply (safe intro!: borel_measurable_pinfreal_times Diff borel_measurable_const
1.897 +        borel_measurable_psuminf borel_measurable_indicator `A \<in> sets M` Q_sets borel countable_UN Q'_sets)
1.898 +      apply (subst positive_integral_cmult)
1.899 +      apply (safe intro!: borel_measurable_pinfreal_times Diff borel_measurable_const
1.900 +        borel_measurable_psuminf borel_measurable_indicator `A \<in> sets M` Q_sets borel countable_UN Q'_sets)
1.901 +      unfolding *
1.902 +      apply (subst positive_integral_indicator)
1.903 +      apply (safe intro!: borel_measurable_pinfreal_times Diff borel_measurable_const Int
1.904 +        borel_measurable_psuminf borel_measurable_indicator `A \<in> sets M` Q_sets borel countable_UN Q'_sets)
1.905 +      by simp
1.906 +    moreover have "(\<Sum>\<^isub>\<infinity>i. \<nu> (Q i \<inter> A)) = \<nu> ((\<Union>i. Q i) \<inter> A)"
1.907 +    proof (rule v.measure_countably_additive[of "\<lambda>i. Q i \<inter> A", unfolded comp_def, simplified])
1.908 +      show "range (\<lambda>i. Q i \<inter> A) \<subseteq> sets M"
1.909 +        using Q_sets `A \<in> sets M` by auto
1.910 +      show "disjoint_family (\<lambda>i. Q i \<inter> A)"
1.911 +        by (fastsimp simp: disjoint_family_on_def Q_def
1.912 +          split: nat.split_asm)
1.913 +    qed
1.914 +    moreover have "\<omega> * \<mu> ?C = \<nu> ?C"
1.915 +    proof cases
1.916 +      assume null: "\<mu> ?C = 0"
1.917 +      hence "?C \<in> null_sets" using Q_sets `A \<in> sets M` by auto
1.918 +      with `absolutely_continuous \<nu>` and null
1.919 +      show ?thesis by (simp add: absolutely_continuous_def)
1.920 +    next
1.921 +      assume not_null: "\<mu> ?C \<noteq> 0"
1.922 +      have "\<nu> ?C = \<omega>"
1.923 +      proof (rule ccontr)
1.924 +        assume "\<nu> ?C \<noteq> \<omega>"
1.925 +        then have "?C \<in> ?Q"
1.926 +          using Q_sets `A \<in> sets M` by auto
1.927 +        from stetic[OF this] not_null
1.928 +        show False unfolding O_0_eq_Q by auto
1.929 +      qed
1.930 +      then show ?thesis using not_null by simp
1.931 +    qed
1.932 +    moreover have "?C \<in> sets M" "((\<Union>i. Q i) \<inter> A) \<in> sets M"
1.933 +      using Q_sets `A \<in> sets M` by (auto intro!: countable_UN)
1.934 +    moreover have "((\<Union>i. Q i) \<inter> A) \<union> ?C = A" "((\<Union>i. Q i) \<inter> A) \<inter> ?C = {}"
1.935 +      using `A \<in> sets M` sets_into_space by auto
1.936 +    ultimately show "\<nu> A = positive_integral (\<lambda>x. ?f x * indicator A x)"
1.937 +      using v.measure_additive[simplified, of "(\<Union>i. Q i) \<inter> A" ?C] by auto
1.938 +  qed
1.939 +qed
1.940 +
1.941 +lemma (in measure_space) positive_integral_translated_density:
1.942 +  assumes "f \<in> borel_measurable M" "g \<in> borel_measurable M"
1.943 +  shows "measure_space.positive_integral M (\<lambda>A. positive_integral (\<lambda>x. f x * indicator A x)) g =
1.944 +    positive_integral (\<lambda>x. f x * g x)" (is "measure_space.positive_integral M ?T _ = _")
1.945 +proof -
1.946 +  from measure_space_density[OF assms(1)]
1.947 +  interpret T: measure_space M ?T .
1.948 +
1.949 +  from borel_measurable_implies_simple_function_sequence[OF assms(2)]
1.950 +  obtain G where G: "\<And>i. simple_function (G i)" "G \<up> g" by blast
1.951 +  note G_borel = borel_measurable_simple_function[OF this(1)]
1.952 +
1.953 +  from T.positive_integral_isoton[OF `G \<up> g` G_borel]
1.954 +  have *: "(\<lambda>i. T.positive_integral (G i)) \<up> T.positive_integral g" .
1.955 +
1.956 +  { fix i
1.957 +    have [simp]: "finite (G i ` space M)"
1.958 +      using G(1) unfolding simple_function_def by auto
1.959 +    have "T.positive_integral (G i) = T.simple_integral (G i)"
1.960 +      using G T.positive_integral_eq_simple_integral by simp
1.961 +    also have "\<dots> = positive_integral (\<lambda>x. f x * (\<Sum>y\<in>G i`space M. y * indicator (G i -` {y} \<inter> space M) x))"
1.962 +      apply (simp add: T.simple_integral_def)
1.963 +      apply (subst positive_integral_cmult[symmetric])
1.964 +      using G_borel assms(1) apply (fastsimp intro: borel_measurable_indicator borel_measurable_vimage)
1.965 +      apply (subst positive_integral_setsum[symmetric])
1.966 +      using G_borel assms(1) apply (fastsimp intro: borel_measurable_indicator borel_measurable_vimage)
1.967 +      by (simp add: setsum_right_distrib field_simps)
1.968 +    also have "\<dots> = positive_integral (\<lambda>x. f x * G i x)"
1.969 +      by (auto intro!: positive_integral_cong
1.970 +               simp: indicator_def if_distrib setsum_cases)
1.971 +    finally have "T.positive_integral (G i) = positive_integral (\<lambda>x. f x * G i x)" . }
1.972 +  with * have eq_Tg: "(\<lambda>i. positive_integral (\<lambda>x. f x * G i x)) \<up> T.positive_integral g" by simp
1.973 +
1.974 +  from G(2) have "(\<lambda>i x. f x * G i x) \<up> (\<lambda>x. f x * g x)"
1.975 +    unfolding isoton_fun_expand by (auto intro!: isoton_cmult_right)
1.976 +  then have "(\<lambda>i. positive_integral (\<lambda>x. f x * G i x)) \<up> positive_integral (\<lambda>x. f x * g x)"
1.977 +    using assms(1) G_borel by (auto intro!: positive_integral_isoton borel_measurable_pinfreal_times)
1.978 +  with eq_Tg show "T.positive_integral g = positive_integral (\<lambda>x. f x * g x)"
1.979 +    unfolding isoton_def by simp
1.980 +qed
1.981 +
1.982 +lemma (in sigma_finite_measure) Radon_Nikodym:
1.983 +  assumes "measure_space M \<nu>"
1.984 +  assumes "absolutely_continuous \<nu>"
1.985 +  shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
1.986 +proof -
1.987 +  from Ex_finite_integrable_function
1.988 +  obtain h where finite: "positive_integral h \<noteq> \<omega>" and
1.989 +    borel: "h \<in> borel_measurable M" and
1.990 +    pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x" and
1.991 +    "\<And>x. x \<in> space M \<Longrightarrow> h x < \<omega>" by auto
1.992 +  let "?T A" = "positive_integral (\<lambda>x. h x * indicator A x)"
1.993 +  from measure_space_density[OF borel] finite
1.994 +  interpret T: finite_measure M ?T
1.995 +    unfolding finite_measure_def finite_measure_axioms_def
1.996 +    by (simp cong: positive_integral_cong)
1.997 +  have "\<And>N. N \<in> sets M \<Longrightarrow> {x \<in> space M. h x \<noteq> 0 \<and> indicator N x \<noteq> (0::pinfreal)} = N"
1.998 +    using sets_into_space pos by (force simp: indicator_def)
1.999 +  then have "T.absolutely_continuous \<nu>" using assms(2) borel
1.1000 +    unfolding T.absolutely_continuous_def absolutely_continuous_def
1.1001 +    by (fastsimp simp: borel_measurable_indicator positive_integral_0_iff)
1.1002 +  from T.Radon_Nikodym_finite_measure_infinite[simplified, OF assms(1) this]
1.1003 +  obtain f where f_borel: "f \<in> borel_measurable M" and
1.1004 +    fT: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = T.positive_integral (\<lambda>x. f x * indicator A x)" by auto
1.1005 +  show ?thesis
1.1006 +  proof (safe intro!: bexI[of _ "\<lambda>x. h x * f x"])
1.1007 +    show "(\<lambda>x. h x * f x) \<in> borel_measurable M"
1.1008 +      using borel f_borel by (auto intro: borel_measurable_pinfreal_times)
1.1009 +    fix A assume "A \<in> sets M"
1.1010 +    then have "(\<lambda>x. f x * indicator A x) \<in> borel_measurable M"
1.1011 +      using f_borel by (auto intro: borel_measurable_pinfreal_times borel_measurable_indicator)
1.1012 +    from positive_integral_translated_density[OF borel this]
1.1013 +    show "\<nu> A = positive_integral (\<lambda>x. h x * f x * indicator A x)"
1.1014 +      unfolding fT[OF `A \<in> sets M`] by (simp add: field_simps)
1.1015 +  qed
1.1016 +qed
1.1017 +
1.1018 +section "Radon Nikodym derivative"
1.1019 +
1.1020 +definition (in sigma_finite_measure)
1.1021 +  "RN_deriv \<nu> \<equiv> SOME f. f \<in> borel_measurable M \<and>
1.1022 +    (\<forall>A \<in> sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x))"
1.1023 +
1.1024 +lemma (in sigma_finite_measure) RN_deriv:
1.1025 +  assumes "measure_space M \<nu>"
1.1026 +  assumes "absolutely_continuous \<nu>"
1.1027 +  shows "RN_deriv \<nu> \<in> borel_measurable M" (is ?borel)
1.1028 +  and "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)"
1.1029 +    (is "\<And>A. _ \<Longrightarrow> ?int A")
1.1030 +proof -
1.1031 +  note Ex = Radon_Nikodym[OF assms, unfolded Bex_def]
1.1032 +  thus ?borel unfolding RN_deriv_def by (rule someI2_ex) auto
1.1033 +  fix A assume "A \<in> sets M"
1.1034 +  from Ex show "?int A" unfolding RN_deriv_def
1.1035 +    by (rule someI2_ex) (simp add: `A \<in> sets M`)
1.1036 +qed
1.1037 +
1.1038 +lemma (in sigma_finite_measure) RN_deriv_singleton:
1.1039 +  assumes "measure_space M \<nu>"
1.1040 +  and ac: "absolutely_continuous \<nu>"
1.1041 +  and "{x} \<in> sets M"
1.1042 +  shows "\<nu> {x} = RN_deriv \<nu> x * \<mu> {x}"
1.1043 +proof -
1.1044 +  note deriv = RN_deriv[OF assms(1, 2)]
1.1045 +  from deriv(2)[OF `{x} \<in> sets M`]
1.1046 +  have "\<nu> {x} = positive_integral (\<lambda>w. RN_deriv \<nu> x * indicator {x} w)"
1.1047 +    by (auto simp: indicator_def intro!: positive_integral_cong)
1.1048 +  thus ?thesis using positive_integral_cmult_indicator[OF `{x} \<in> sets M`]
1.1049 +    by auto
1.1050 +qed
1.1051 +
1.1052 +theorem (in finite_measure_space) RN_deriv_finite_measure:
1.1053 +  assumes "measure_space M \<nu>"
1.1054 +  and ac: "absolutely_continuous \<nu>"
1.1055 +  and "x \<in> space M"
1.1056 +  shows "\<nu> {x} = RN_deriv \<nu> x * \<mu> {x}"
1.1057 +proof -
1.1058 +  have "{x} \<in> sets M" using sets_eq_Pow `x \<in> space M` by auto
1.1059 +  from RN_deriv_singleton[OF assms(1,2) this] show ?thesis .
1.1060 +qed
1.1061 +
1.1062 +end
```