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