Quelle Radon_Nikodym.thy Sprache: Isabelle

(*  Title:      HOL/Analysis/Radon_Nikodym.thy
    Author:     Johannes Hölzl, TU München
*)

section \<open>Radon-Nikod{\'y}m Derivative\<close>

theory Radon_Nikodym
imports Bochner_Integration
begin

definition\<^marker>\<open>tag important\<close> diff_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
where
  "diff_measure M N = measure_of (space M) (sets M) (\A. emeasure M A - emeasure N A)"

lemma
  shows space_diff_measure[simp]: "space (diff_measure M N) = space M"
    and sets_diff_measure[simp]: "sets (diff_measure M N) = sets M"
  by (auto simp: diff_measure_def)

lemma emeasure_diff_measure:
  assumes fin: "finite_measure M" "finite_measure N" and sets_eq: "sets M = sets N"
  assumes pos: "\A. A \ sets M \ emeasure N A \ emeasure M A" and A: "A \ sets M"
  shows "emeasure (diff_measure M N) A = emeasure M A - emeasure N A" (is "_ = ?\ A")
  unfolding diff_measure_def
proof (rule emeasure_measure_of_sigma)
  show "sigma_algebra (space M) (sets M)" ..
  show "positive (sets M) ?\"
    using pos by (simp add: positive_def)
  show "countably_additive (sets M) ?\"
  proof (rule countably_additiveI)
    fix A :: "nat \ _" assume A: "range A \ sets M" and "disjoint_family A"
    then have suminf:
      "(\i. emeasure M (A i)) = emeasure M (\i. A i)"
      "(\i. emeasure N (A i)) = emeasure N (\i. A i)"
      by (simp_all add: suminf_emeasure sets_eq)
    with A have "(\i. emeasure M (A i) - emeasure N (A i)) =
      (\<Sum>i. emeasure M (A i)) - (\<Sum>i. emeasure N (A i))"
      using fin pos[of "A _"]
      by (intro ennreal_suminf_minus)
         (auto simp: sets_eq finite_measure.emeasure_eq_measure suminf_emeasure)
    then show "(\i. emeasure M (A i) - emeasure N (A i)) =
      emeasure M (\<Union>i. A i) - emeasure N (\<Union>i. A i) "
      by (simp add: suminf)
  qed
qed fact

text \<open>An equivalent characterization of sigma-finite spaces is the existence of integrable
positive functions (or, still equivalently, the existence of a probability measure which is in
the same measure class as the original measure).\<close>

proposition (in sigma_finite_measure) obtain_positive_integrable_function:
  obtains f::"'a \ real" where
    "f \ borel_measurable M"
    "\x. f x > 0"
    "\x. f x \ 1"
    "integrable M f"
proof -
  obtain A :: "nat \ 'a set" where "range A \ sets M" "(\i. A i) = space M" "\i. emeasure M (A i) \ \"
    using sigma_finite by auto
  then have [measurable]:"A n \ sets M" for n by auto
  define g where "g = (\x. (\n. (1/2)^(Suc n) * indicator (A n) x / (1+ measure M (A n))))"
  have [measurable]: "g \ borel_measurable M" unfolding g_def by auto
  have *: "summable (\n. (1/2)^(Suc n) * indicator (A n) x / (1+ measure M (A n)))" for x
    apply (rule summable_comparison_test'[of "\n. (1/2)^(Suc n)" 0])
    using power_half_series summable_def by (auto simp add: indicator_def divide_simps)
  have "g x \ (\n. (1/2)^(Suc n))" for x unfolding g_def
    apply (rule suminf_le) using * power_half_series summable_def by (auto simp add: indicator_def divide_simps)
  then have g_le_1: "g x \ 1" for x using power_half_series sums_unique by fastforce

  have g_pos: "g x > 0" if "x \ space M" for x
  unfolding g_def proof (subst suminf_pos_iff[OF *[of x]], auto)
    obtain i where "x \ A i" using \(\i. A i) = space M\ \x \ space M\ by auto
    then have "0 < (1 / 2) ^ Suc i * indicator (A i) x / (1 + Sigma_Algebra.measure M (A i))"
      unfolding indicator_def apply (auto simp add: divide_simps) using measure_nonneg[of M "A i"]
      by (auto, meson add_nonneg_nonneg linorder_not_le mult_nonneg_nonneg zero_le_numeral zero_le_one zero_le_power)
    then show "\i. 0 < (1 / 2) ^ i * indicator (A i) x / (2 + 2 * Sigma_Algebra.measure M (A i))"
      by auto
  qed

  have "integrable M g"
  unfolding g_def proof (rule integrable_suminf)
    fix n
    show "integrable M (\x. (1 / 2) ^ Suc n * indicator (A n) x / (1 + Sigma_Algebra.measure M (A n)))"
      using \<open>emeasure M (A n) \<noteq> \<infinity>\<close>
      by (auto intro!: integrable_mult_right integrable_divide_zero integrable_real_indicator simp add: top.not_eq_extremum)
  next
    show "AE x in M. summable (\n. norm ((1 / 2) ^ Suc n * indicator (A n) x / (1 + Sigma_Algebra.measure M (A n))))"
      using * by auto
    show "summable (\n. (\x. norm ((1 / 2) ^ Suc n * indicator (A n) x / (1 + Sigma_Algebra.measure M (A n))) \M))"
      apply (rule summable_comparison_test'[of "\n. (1/2)^(Suc n)" 0], auto)
      using power_half_series summable_def apply auto[1]
      apply (auto simp add: field_split_simps) using measure_nonneg[of M] not_less by fastforce
  qed

  define f where "f = (\x. if x \ space M then g x else 1)"
  have "f x > 0" for x unfolding f_def using g_pos by auto
  moreover have "f x \ 1" for x unfolding f_def using g_le_1 by auto
  moreover have [measurable]: "f \ borel_measurable M" unfolding f_def by auto
  moreover have "integrable M f"
    apply (subst integrable_cong[of _ _ _ g]) unfolding f_def using \<open>integrable M g\<close> by auto
  ultimately show "(\f. f \ borel_measurable M \ (\x. 0 < f x) \ (\x. f x \ 1) \ integrable M f \ thesis) \ thesis"
    by (meson that)
qed

lemma (in sigma_finite_measure) Ex_finite_integrable_function:
  "\h\borel_measurable M. integral\<^sup>N M h \ \ \ (\x\space M. 0 < h x \ h x < \)"
proof -
  obtain A :: "nat \ 'a set" where
    range[measurable]: "range A \ sets M" and
    space: "(\i. A i) = space M" and
    measure: "\i. emeasure M (A i) \ \" and
    disjoint: "disjoint_family A"
    using sigma_finite_disjoint by blast
  let ?B = "\i. 2^Suc i * emeasure M (A i)"
  have [measurable]: "\i. A i \ sets M"
    using range by fastforce+
  have "\i. \x. 0 < x \ x < inverse (?B i)"
  proof
    fix i show "\x. 0 < x \ x < inverse (?B i)"
      using measure[of i]
      by (auto intro!: dense simp: ennreal_inverse_positive ennreal_mult_eq_top_iff power_eq_top_ennreal)
  qed
  from choice[OF this] obtain n where n: "\i. 0 < n i"
    "\i. n i < inverse (2^Suc i * emeasure M (A i))" by auto
  { fix i have "0 \ n i" using n(1)[of i] by auto } note pos = this
  let ?h = "\x. \i. n i * indicator (A i) x"
  show ?thesis
  proof (safe intro!: bexI[of _ ?h] del: notI)
    have "integral\<^sup>N M ?h = (\i. n i * emeasure M (A i))" using pos
      by (simp add: nn_integral_suminf nn_integral_cmult_indicator)
    also have "\ \ (\i. ennreal ((1/2)^Suc i))"
    proof (intro suminf_le allI)
      fix N
      have "n N * emeasure M (A N) \ inverse (2^Suc N * emeasure M (A N)) * emeasure M (A N)"
        using n[of N] by (intro mult_right_mono) auto
      also have "\ = (1/2)^Suc N * (inverse (emeasure M (A N)) * emeasure M (A N))"
        using measure[of N]
        by (simp add: ennreal_inverse_power divide_ennreal_def ennreal_inverse_mult
                      power_eq_top_ennreal less_top[symmetric] mult_ac
                 del: power_Suc)
      also have "\ \ inverse (ennreal 2) ^ Suc N"
        using measure[of N]
        by (cases "emeasure M (A N)"; cases "emeasure M (A N) = 0")
           (auto simp: inverse_ennreal ennreal_mult[symmetric] divide_ennreal_def simp del: power_Suc)
      also have "\ = ennreal (inverse 2 ^ Suc N)"
        by (subst ennreal_power[symmetric], simp) (simp add: inverse_ennreal)
      finally show "n N * emeasure M (A N) \ ennreal ((1/2)^Suc N)"
        by simp
    qed auto
    also have "\ < top"
      unfolding less_top[symmetric]
      by (rule ennreal_suminf_neq_top)
         (auto simp: summable_geometric summable_Suc_iff simp del: power_Suc)
    finally show "integral\<^sup>N M ?h \ \"
      by (auto simp: top_unique)
  next
    { fix x assume "x \ space M"
      then obtain i where "x \ A i" using space[symmetric] by auto
      with disjoint n have "?h x = n i"
        by (auto intro!: suminf_cmult_indicator intro: less_imp_le)
      then show "0 < ?h x" and "?h x < \" using n[of i] by (auto simp: less_top[symmetric]) }
    note pos = this
  qed measurable
qed

subsection "Absolutely continuous"

definition\<^marker>\<open>tag important\<close> absolutely_continuous :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
  "absolutely_continuous M N \ null_sets M \ null_sets N"

lemma absolutely_continuousI_count_space: "absolutely_continuous (count_space A) M"
  unfolding absolutely_continuous_def by (auto simp: null_sets_count_space)

lemma absolutely_continuousI_density:
  "f \ borel_measurable M \ absolutely_continuous M (density M f)"
  by (force simp add: absolutely_continuous_def null_sets_density_iff dest: AE_not_in)

lemma absolutely_continuousI_point_measure_finite:
  "(\x. \ x \ A ; f x \ 0 \ \ g x \ 0) \ absolutely_continuous (point_measure A f) (point_measure A g)"
  unfolding absolutely_continuous_def by (force simp: null_sets_point_measure_iff)

lemma absolutely_continuousD:
  "absolutely_continuous M N \ A \ sets M \ emeasure M A = 0 \ emeasure N A = 0"
  by (auto simp: absolutely_continuous_def null_sets_def)

lemma absolutely_continuous_AE:
  assumes sets_eq: "sets M' = sets M"
    and "absolutely_continuous M M'" "AE x in M. P x"
   shows "AE x in M'. P x"
proof -
  from \<open>AE x in M. P x\<close> obtain N where N: "N \<in> null_sets M" "{x\<in>space M. \<not> P x} \<subseteq> N"
    unfolding eventually_ae_filter by auto
  show "AE x in M'. P x"
  proof (rule AE_I')
    show "{x\space M'. \ P x} \ N" using sets_eq_imp_space_eq[OF sets_eq] N(2) by simp
    from \<open>absolutely_continuous M M'\<close> show "N \<in> null_sets M'"
      using N unfolding absolutely_continuous_def sets_eq null_sets_def by auto
  qed
qed

subsection "Existence of the Radon-Nikodym derivative"

proposition
(in finite_measure) Radon_Nikodym_finite_measure:
  assumes "finite_measure N" and sets_eq[simp]: "sets N = sets M"
  assumes "absolutely_continuous M N"
  shows "\f \ borel_measurable M. density M f = N"
proof -
  interpret N: finite_measure N by fact
  define G where "G = {g \ borel_measurable M. \A\sets M. (\\<^sup>+x. g x * indicator A x \M) \ N A}"
  have [measurable_dest]: "f \ G \ f \ borel_measurable M"
    and G_D: "\A. f \ G \ A \ sets M \ (\\<^sup>+x. f x * indicator A x \M) \ N A" for f
    by (auto simp: G_def)
  note this[measurable_dest]
  have "(\x. 0) \ G" unfolding G_def by auto
  hence "G \ {}" by auto
  { fix f g assume f[measurable]: "f \ G" and g[measurable]: "g \ G"
    have "(\x. max (g x) (f x)) \ G" (is "?max \ G") unfolding G_def
    proof safe
      let ?A = "{x \ space M. f x \ g x}"
      have "?A \ sets M" using f g unfolding G_def by auto
      fix A assume [measurable]: "A \ sets M"
      have union: "((?A \ A) \ ((space M - ?A) \ A)) = A"
        using sets.sets_into_space[OF \<open>A \<in> sets M\<close>] by auto
      have "\x. x \ space M \ max (g x) (f x) * indicator A x =
        g x * indicator (?A \<inter> A) x + f x * indicator ((space M - ?A) \<inter> A) x"
        by (auto simp: indicator_def max_def)
      hence "(\\<^sup>+x. max (g x) (f x) * indicator A x \M) =
        (\<integral>\<^sup>+x. g x * indicator (?A \<inter> A) x \<partial>M) +
        (\<integral>\<^sup>+x. f x * indicator ((space M - ?A) \<inter> A) x \<partial>M)"
        by (auto cong: nn_integral_cong intro!: nn_integral_add)
      also have "\ \ N (?A \ A) + N ((space M - ?A) \ A)"
        using f g unfolding G_def by (auto intro!: add_mono)
      also have "\ = N A"
        using union by (subst plus_emeasure) auto
      finally show "(\\<^sup>+x. max (g x) (f x) * indicator A x \M) \ N A" .
    qed auto }
  note max_in_G = this
  { fix f assume  "incseq f" and f: "\i. f i \ G"
    then have [measurable]: "\i. f i \ borel_measurable M" by (auto simp: G_def)
    have "(\x. SUP i. f i x) \ G" unfolding G_def
    proof safe
      show "(\x. SUP i. f i x) \ borel_measurable M" by measurable
    next
      fix A assume "A \ sets M"
      have "(\\<^sup>+x. (SUP i. f i x) * indicator A x \M) =
        (\<integral>\<^sup>+x. (SUP i. f i x * indicator A x) \<partial>M)"
        by (intro nn_integral_cong) (simp split: split_indicator)
      also have "\ = (SUP i. (\\<^sup>+x. f i x * indicator A x \M))"
        using \<open>incseq f\<close> f \<open>A \<in> sets M\<close>
        by (intro nn_integral_monotone_convergence_SUP)
           (auto simp: G_def incseq_Suc_iff le_fun_def split: split_indicator)
      finally show "(\\<^sup>+x. (SUP i. f i x) * indicator A x \M) \ N A"
        using f \<open>A \<in> sets M\<close> by (auto intro!: SUP_least simp: G_D)
    qed }
  note SUP_in_G = this
  let ?y = "SUP g \ G. integral\<^sup>N M g"
  have y_le: "?y \ N (space M)" unfolding G_def
  proof (safe intro!: SUP_least)
    fix g assume "\A\sets M. (\\<^sup>+x. g x * indicator A x \M) \ N A"
    from this[THEN bspec, OF sets.top] show "integral\<^sup>N M g \ N (space M)"
      by (simp cong: nn_integral_cong)
  qed
  from ennreal_SUP_countable_SUP [OF \<open>G \<noteq> {}\<close>, of "integral\<^sup>N M"]
  obtain ys :: "nat \ ennreal"
    where ys: "range ys \ integral\<^sup>N M ` G \ Sup (integral\<^sup>N M ` G) = Sup (range ys)"
    by auto
  then have "\n. \g. g\G \ integral\<^sup>N M g = ys n"
  proof safe
    fix n assume "range ys \ integral\<^sup>N M ` G"
    hence "ys n \ integral\<^sup>N M ` G" by auto
    thus "\g. g\G \ integral\<^sup>N M g = ys n" by auto
  qed
  from choice[OF this] obtain gs where "\i. gs i \ G" "\n. integral\<^sup>N M (gs n) = ys n" by auto
  hence y_eq: "?y = (SUP i. integral\<^sup>N M (gs i))" using ys by auto
  let ?g = "\i x. Max ((\n. gs n x) ` {..i})"
  define f where [abs_def]: "f x = (SUP i. ?g i x)" for x
  let ?F = "\A x. f x * indicator A x"
  have gs_not_empty: "\i x. (\n. gs n x) ` {..i} \ {}" by auto
  { fix i have "?g i \ G"
    proof (induct i)
      case 0 thus ?case by simp fact
    next
      case (Suc i)
      with Suc gs_not_empty \<open>gs (Suc i) \<in> G\<close> show ?case
        by (auto simp add: atMost_Suc intro!: max_in_G)
    qed }
  note g_in_G = this
  have "incseq ?g" using gs_not_empty
    by (auto intro!: incseq_SucI le_funI simp add: atMost_Suc)

  from SUP_in_G[OF this g_in_G] have [measurable]: "f \ G" unfolding f_def .
  then have [measurable]: "f \ borel_measurable M" unfolding G_def by auto

  have "integral\<^sup>N M f = (SUP i. integral\<^sup>N M (?g i))" unfolding f_def
    using g_in_G \<open>incseq ?g\<close> by (auto intro!: nn_integral_monotone_convergence_SUP simp: G_def)
  also have "\ = ?y"
  proof (rule antisym)
    show "(SUP i. integral\<^sup>N M (?g i)) \ ?y"
      using g_in_G by (auto intro: SUP_mono)
    show "?y \ (SUP i. integral\<^sup>N M (?g i))" unfolding y_eq
      by (auto intro!: SUP_mono nn_integral_mono Max_ge)
  qed
  finally have int_f_eq_y: "integral\<^sup>N M f = ?y" .

  have upper_bound: "\A\sets M. N A \ density M f A"
  proof (rule ccontr)
    assume "\ ?thesis"
    then obtain A where A[measurable]: "A \ sets M" and f_less_N: "density M f A < N A"
      by (auto simp: not_le)
    then have pos_A: "0 < M A"
      using \<open>absolutely_continuous M N\<close>[THEN absolutely_continuousD, OF A]
      by (auto simp: zero_less_iff_neq_zero)

    define b where "b = (N A - density M f A) / M A / 2"
    with f_less_N pos_A have "0 < b" "b \ top"
      by (auto intro!: diff_gr0_ennreal simp: zero_less_iff_neq_zero diff_eq_0_iff_ennreal ennreal_divide_eq_top_iff)

    let ?f = "\x. f x + b"
    have "nn_integral M f \ top"
      using \<open>f \<in> G\<close>[THEN G_D, of "space M"] by (auto simp: top_unique cong: nn_integral_cong)
    with \<open>b \<noteq> top\<close> interpret Mf: finite_measure "density M ?f"
      by (intro finite_measureI)
         (auto simp: field_simps mult_indicator_subset ennreal_mult_eq_top_iff
                     emeasure_density nn_integral_cmult_indicator nn_integral_add
               cong: nn_integral_cong)

    from unsigned_Hahn_decomposition[of "density M ?f" N A]
    obtain Y where [measurable]: "Y \ sets M" and [simp]: "Y \ A"
       and Y1: "\C. C \ sets M \ C \ Y \ density M ?f C \ N C"
       and Y2: "\C. C \ sets M \ C \ A \ C \ Y = {} \ N C \ density M ?f C"
       by auto

    let ?f' = "\x. f x + b * indicator Y x"
    have "M Y \ 0"
    proof
      assume "M Y = 0"
      then have "N Y = 0"
        using \<open>absolutely_continuous M N\<close>[THEN absolutely_continuousD, of Y] by auto
      then have "N A = N (A - Y)"
        by (subst emeasure_Diff) auto
      also have "\ \ density M ?f (A - Y)"
        by (rule Y2) auto
      also have "\ \ density M ?f A - density M ?f Y"
        by (subst emeasure_Diff) auto
      also have "\ \ density M ?f A - 0"
        by (intro ennreal_minus_mono) auto
      also have "density M ?f A = b * M A + density M f A"
        by (simp add: emeasure_density field_simps mult_indicator_subset nn_integral_add nn_integral_cmult_indicator)
      also have "\ < N A"
        using f_less_N pos_A
        by (cases "density M f A"; cases "M A"; cases "N A")
           (auto simp: b_def ennreal_less_iff ennreal_minus divide_ennreal ennreal_numeral[symmetric]
                       ennreal_plus[symmetric] ennreal_mult[symmetric] field_simps
                    simp del: ennreal_numeral ennreal_plus)
      finally show False
        by simp
    qed
    then have "nn_integral M f < nn_integral M ?f'"
      using \<open>0 < b\<close> \<open>nn_integral M f \<noteq> top\<close>
      by (simp add: nn_integral_add nn_integral_cmult_indicator ennreal_zero_less_mult_iff zero_less_iff_neq_zero)
    moreover
    have "?f' \ G"
      unfolding G_def
    proof safe
      fix X assume [measurable]: "X \ sets M"
      have "(\\<^sup>+ x. ?f' x * indicator X x \M) = density M f (X - Y) + density M ?f (X \ Y)"
        by (auto simp add: emeasure_density nn_integral_add[symmetric] split: split_indicator intro!: nn_integral_cong)
      also have "\ \ N (X - Y) + N (X \ Y)"
        using G_D[OF \<open>f \<in> G\<close>] by (intro add_mono Y1) (auto simp: emeasure_density)
      also have "\ = N X"
        by (subst plus_emeasure) (auto intro!: arg_cong2[where f=emeasure])
      finally show "(\\<^sup>+ x. ?f' x * indicator X x \M) \ N X" .
    qed simp
    then have "nn_integral M ?f' \ ?y"
      by (rule SUP_upper)
    ultimately show False
      by (simp add: int_f_eq_y)
  qed
  show ?thesis
  proof (intro bexI[of _ f] measure_eqI conjI antisym)
    fix A assume "A \ sets (density M f)" then show "emeasure (density M f) A \ emeasure N A"
      by (auto simp: emeasure_density intro!: G_D[OF \<open>f \<in> G\<close>])
  next
    fix A assume A: "A \ sets (density M f)" then show "emeasure N A \ emeasure (density M f) A"
      using upper_bound by auto
  qed auto
qed

lemma (in finite_measure) split_space_into_finite_sets_and_rest:
  assumes ac: "absolutely_continuous M N" and sets_eq[simp]: "sets N = sets M"
  shows "\B::nat\'a set. disjoint_family B \ range B \ sets M \ (\i. N (B i) \ \) \
    (\<forall>A\<in>sets M. A \<inter> (\<Union>i. B i) = {} \<longrightarrow> (emeasure M A = 0 \<and> N A = 0) \<or> (emeasure M A > 0 \<and> N A = \<infinity>))"
proof -
  let ?Q = "{Q\sets M. N Q \ \}"
  let ?a = "SUP Q\?Q. emeasure M Q"
  have "{} \ ?Q" by auto
  then have Q_not_empty: "?Q \ {}" by blast
  have "?a \ emeasure M (space M)" using sets.sets_into_space
    by (auto intro!: SUP_least emeasure_mono)
  then have "?a \ \"
    using finite_emeasure_space
    by (auto simp: less_top[symmetric] top_unique simp del: SUP_eq_top_iff Sup_eq_top_iff)
  from ennreal_SUP_countable_SUP [OF Q_not_empty, of "emeasure M"]
  obtain Q'' where "range Q'' \ emeasure M ` ?Q" and a: "?a = (SUP i::nat. Q'' i)"
    by auto
  then have "\i. \Q'. Q'' i = emeasure M Q' \ Q' \ ?Q" by auto
  from choice[OF this] obtain Q' where Q': "\i. Q'' i = emeasure M (Q' i)" "\i. Q' i \ ?Q"
    by auto
  then have a_Lim: "?a = (SUP i. emeasure M (Q' i))" using a by simp
  let ?O = "\n. \i\n. Q' i"
  have Union: "(SUP i. emeasure M (?O i)) = emeasure M (\i. ?O i)"
  proof (rule SUP_emeasure_incseq[of ?O])
    show "range ?O \ sets M" using Q' by auto
    show "incseq ?O" by (fastforce intro!: incseq_SucI)
  qed
  have Q'_sets[measurable]: "\i. Q' i \ sets M" using Q' by auto
  have O_sets: "\i. ?O i \ sets M" using Q' by auto
  then have O_in_G: "\i. ?O i \ ?Q"
  proof (safe del: notI)
    fix i have "Q' ` {..i} \ sets M" using Q' by auto
    then have "N (?O i) \ (\i\i. N (Q' i))"
      by (simp add: emeasure_subadditive_finite)
    also have "\ < \" using Q' by (simp add: less_top)
    finally show "N (?O i) \ \" by simp
  qed auto
  have O_mono: "\n. ?O n \ ?O (Suc n)" by fastforce
  have a_eq: "?a = emeasure M (\i. ?O i)" unfolding Union[symmetric]
  proof (rule antisym)
    show "?a \ (SUP i. emeasure M (?O i))" unfolding a_Lim
      using Q' by (auto intro!: SUP_mono emeasure_mono)
    show "(SUP i. emeasure M (?O i)) \ ?a"
    proof (safe intro!: Sup_mono, unfold bex_simps)
      fix i
      have *: "(\(Q' ` {..i})) = ?O i" by auto
      then show "\x. (x \ sets M \ N x \ \) \
        emeasure M (\<Union>(Q' ` {..i})) \<le> emeasure M x"
        using O_in_G[of i] by (auto intro!: exI[of _ "?O i"])
    qed
  qed
  let ?O_0 = "(\i. ?O i)"
  have "?O_0 \ sets M" using Q' by auto
  have "disjointed Q' i \ sets M" for i
    using sets.range_disjointed_sets[of Q' M] using Q'_sets by (auto simp: subset_eq)
  note Q_sets = this
  show ?thesis
  proof (intro bexI exI conjI ballI impI allI)
    show "disjoint_family (disjointed Q')"
      by (rule disjoint_family_disjointed)
    show "range (disjointed Q') \ sets M"
      using Q'_sets by (intro sets.range_disjointed_sets) auto
    { fix A assume A: "A \ sets M" "A \ (\i. disjointed Q' i) = {}"
      then have A1: "A \ (\i. Q' i) = {}"
        unfolding UN_disjointed_eq by auto
      show "emeasure M A = 0 \ N A = 0 \ 0 < emeasure M A \ N A = \"
      proof (rule disjCI, simp)
        assume *: "emeasure M A = 0 \ N A \ top"
        show "emeasure M A = 0 \ N A = 0"
        proof (cases "emeasure M A = 0")
          case True
          with ac A have "N A = 0"
            unfolding absolutely_continuous_def by auto
          with True show ?thesis by simp
        next
          case False
          with * have "N A \ \" by auto
          with A have "emeasure M ?O_0 + emeasure M A = emeasure M (?O_0 \ A)"
            using Q' A1 by (auto intro!: plus_emeasure simp: set_eq_iff)
          also have "\ = (SUP i. emeasure M (?O i \ A))"
          proof (rule SUP_emeasure_incseq[of "\i. ?O i \ A", symmetric, simplified])
            show "range (\i. ?O i \ A) \ sets M"
              using \<open>N A \<noteq> \<infinity>\<close> O_sets A by auto
          qed (fastforce intro!: incseq_SucI)
          also have "\ \ ?a"
          proof (safe intro!: SUP_least)
            fix i have "?O i \ A \ ?Q"
            proof (safe del: notI)
              show "?O i \ A \ sets M" using O_sets A by auto
              from O_in_G[of i] have "N (?O i \ A) \ N (?O i) + N A"
                using emeasure_subadditive[of "?O i" N A] A O_sets by auto
              with O_in_G[of i] show "N (?O i \ A) \ \"
                using \<open>N A \<noteq> \<infinity>\<close> by (auto simp: top_unique)
            qed
            then show "emeasure M (?O i \ A) \ ?a" by (rule SUP_upper)
          qed
          finally have "emeasure M A = 0"
            unfolding a_eq using measure_nonneg[of M A] by (simp add: emeasure_eq_measure)
          with \<open>emeasure M A \<noteq> 0\<close> show ?thesis by auto
        qed
      qed }
    { fix i
      have "N (disjointed Q' i) \ N (Q' i)"
        by (auto intro!: emeasure_mono simp: disjointed_def)
      then show "N (disjointed Q' i) \ \"
        using Q'(2)[of i] by (auto simp: top_unique) }
  qed
qed

proposition (in finite_measure) Radon_Nikodym_finite_measure_infinite:
  assumes "absolutely_continuous M N" and sets_eq: "sets N = sets M"
  shows "\f\borel_measurable M. density M f = N"
proof -
  from split_space_into_finite_sets_and_rest[OF assms]
  obtain Q :: "nat \ 'a set"
    where Q: "disjoint_family Q" "range Q \ sets M"
    and in_Q0: "\A. A \ sets M \ A \ (\i. Q i) = {} \ emeasure M A = 0 \ N A = 0 \ 0 < emeasure M A \ N A = \"
    and Q_fin: "\i. N (Q i) \ \" by force
  from Q have Q_sets: "\i. Q i \ sets M" by auto
  let ?N = "\i. density N (indicator (Q i))" and ?M = "\i. density M (indicator (Q i))"
  have "\i. \f\borel_measurable (?M i). density (?M i) f = ?N i"
  proof (intro allI finite_measure.Radon_Nikodym_finite_measure)
    fix i
    from Q show "finite_measure (?M i)"
      by (auto intro!: finite_measureI cong: nn_integral_cong
               simp add: emeasure_density subset_eq sets_eq)
    from Q have "emeasure (?N i) (space N) = emeasure N (Q i)"
      by (simp add: sets_eq[symmetric] emeasure_density subset_eq cong: nn_integral_cong)
    with Q_fin show "finite_measure (?N i)"
      by (auto intro!: finite_measureI)
    show "sets (?N i) = sets (?M i)" by (simp add: sets_eq)
    have [measurable]: "\A. A \ sets M \ A \ sets N" by (simp add: sets_eq)
    show "absolutely_continuous (?M i) (?N i)"
      using \<open>absolutely_continuous M N\<close> \<open>Q i \<in> sets M\<close>
      by (auto simp: absolutely_continuous_def null_sets_density_iff sets_eq
               intro!: absolutely_continuous_AE[OF sets_eq])
  qed
  from choice[OF this[unfolded Bex_def]]
  obtain f where borel: "\i. f i \ borel_measurable M" "\i x. 0 \ f i x"
    and f_density: "\i. density (?M i) (f i) = ?N i"
    by force
  { fix A i assume A: "A \ sets M"
    with Q borel have "(\\<^sup>+x. f i x * indicator (Q i \ A) x \M) = emeasure (density (?M i) (f i)) A"
      by (auto simp add: emeasure_density nn_integral_density subset_eq
               intro!: nn_integral_cong split: split_indicator)
    also have "\ = emeasure N (Q i \ A)"
      using A Q by (simp add: f_density emeasure_restricted subset_eq sets_eq)
    finally have "emeasure N (Q i \ A) = (\\<^sup>+x. f i x * indicator (Q i \ A) x \M)" .. }
  note integral_eq = this
  let ?f = "\x. (\i. f i x * indicator (Q i) x) + \ * indicator (space M - (\i. Q i)) x"
  show ?thesis
  proof (safe intro!: bexI[of _ ?f])
    show "?f \ borel_measurable M" using borel Q_sets
      by (auto intro!: measurable_If)
    show "density M ?f = N"
    proof (rule measure_eqI)
      fix A assume "A \ sets (density M ?f)"
      then have "A \ sets M" by simp
      have Qi: "\i. Q i \ sets M" using Q by auto
      have [intro,simp]: "\i. (\x. f i x * indicator (Q i \ A) x) \ borel_measurable M"
        "\i. AE x in M. 0 \ f i x * indicator (Q i \ A) x"
        using borel Qi \<open>A \<in> sets M\<close> by auto
      have "(\\<^sup>+x. ?f x * indicator A x \M) = (\\<^sup>+x. (\i. f i x * indicator (Q i \ A) x) + \ * indicator ((space M - (\i. Q i)) \ A) x \M)"
        using borel by (intro nn_integral_cong) (auto simp: indicator_def)
      also have "\ = (\\<^sup>+x. (\i. f i x * indicator (Q i \ A) x) \M) + \ * emeasure M ((space M - (\i. Q i)) \ A)"
        using borel Qi \<open>A \<in> sets M\<close>
        by (subst nn_integral_add)
           (auto simp add: nn_integral_cmult_indicator sets.Int intro!: suminf_0_le)
      also have "\ = (\i. N (Q i \ A)) + \ * emeasure M ((space M - (\i. Q i)) \ A)"
        by (subst integral_eq[OF \<open>A \<in> sets M\<close>], subst nn_integral_suminf) auto
      finally have "(\\<^sup>+x. ?f x * indicator A x \M) = (\i. N (Q i \ A)) + \ * emeasure M ((space M - (\i. Q i)) \ A)" .
      moreover have "(\i. N (Q i \ A)) = N ((\i. Q i) \ A)"
        using Q Q_sets \<open>A \<in> sets M\<close>
        by (subst suminf_emeasure) (auto simp: disjoint_family_on_def sets_eq)
      moreover
      have "(space M - (\x. Q x)) \ A \ (\x. Q x) = {}"
        by auto
      then have "\ * emeasure M ((space M - (\i. Q i)) \ A) = N ((space M - (\i. Q i)) \ A)"
        using in_Q0[of "(space M - (\i. Q i)) \ A"] \A \ sets M\ Q by (auto simp: ennreal_top_mult)
      moreover have "(space M - (\i. Q i)) \ A \ sets M" "((\i. Q i) \ A) \ sets M"
        using Q_sets \<open>A \<in> sets M\<close> by auto
      moreover have "((\i. Q i) \ A) \ ((space M - (\i. Q i)) \ A) = A" "((\i. Q i) \ A) \ ((space M - (\i. Q i)) \ A) = {}"
        using \<open>A \<in> sets M\<close> sets.sets_into_space by auto
      ultimately have "N A = (\\<^sup>+x. ?f x * indicator A x \M)"
        using plus_emeasure[of "(\i. Q i) \ A" N "(space M - (\i. Q i)) \ A"] by (simp add: sets_eq)
      with \<open>A \<in> sets M\<close> borel Q show "emeasure (density M ?f) A = N A"
        by (auto simp: subset_eq emeasure_density)
    qed (simp add: sets_eq)
  qed
qed

theorem (in sigma_finite_measure) Radon_Nikodym:
  assumes ac: "absolutely_continuous M N" assumes sets_eq: "sets N = sets M"
  shows "\f \ borel_measurable M. density M f = N"
proof -
  from Ex_finite_integrable_function
  obtain h where finite: "integral\<^sup>N M h \ \" and
    borel: "h \ borel_measurable M" and
    nn: "\x. 0 \ h x" and
    pos: "\x. x \ space M \ 0 < h x" and
    "\x. x \ space M \ h x < \" by auto
  let ?T = "\A. (\\<^sup>+x. h x * indicator A x \M)"
  let ?MT = "density M h"
  from borel finite nn interpret T: finite_measure ?MT
    by (auto intro!: finite_measureI cong: nn_integral_cong simp: emeasure_density)
  have "absolutely_continuous ?MT N" "sets N = sets ?MT"
  proof (unfold absolutely_continuous_def, safe)
    fix A assume "A \ null_sets ?MT"
    with borel have "A \ sets M" "AE x in M. x \ A \ h x \ 0"
      by (auto simp add: null_sets_density_iff)
    with pos sets.sets_into_space have "AE x in M. x \ A"
      by (elim eventually_mono) (auto simp: not_le[symmetric])
    then have "A \ null_sets M"
      using \<open>A \<in> sets M\<close> by (simp add: AE_iff_null_sets)
    with ac show "A \ null_sets N"
      by (auto simp: absolutely_continuous_def)
  qed (auto simp add: sets_eq)
  from T.Radon_Nikodym_finite_measure_infinite[OF this]
  obtain f where f_borel: "f \ borel_measurable M" "density ?MT f = N" by auto
  with nn borel show ?thesis
    by (auto intro!: bexI[of _ "\x. h x * f x"] simp: density_density_eq)
qed

subsection \<open>Uniqueness of densities\<close>

lemma finite_density_unique:
  assumes borel: "f \ borel_measurable M" "g \ borel_measurable M"
  assumes pos: "AE x in M. 0 \ f x" "AE x in M. 0 \ g x"
  and fin: "integral\<^sup>N M f \ \"
  shows "density M f = density M g \ (AE x in M. f x = g x)"
proof (intro iffI ballI)
  fix A assume eq: "AE x in M. f x = g x"
  with borel show "density M f = density M g"
    by (auto intro: density_cong)
next
  let ?P = "\f A. \\<^sup>+ x. f x * indicator A x \M"
  assume "density M f = density M g"
  with borel have eq: "\A\sets M. ?P f A = ?P g A"
    by (simp add: emeasure_density[symmetric])
  from this[THEN bspec, OF sets.top] fin
  have g_fin: "integral\<^sup>N M g \ \" by (simp cong: nn_integral_cong)
  { fix f g assume borel: "f \ borel_measurable M" "g \ borel_measurable M"
      and pos: "AE x in M. 0 \ f x" "AE x in M. 0 \ g x"
      and g_fin: "integral\<^sup>N M g \ \" and eq: "\A\sets M. ?P f A = ?P g A"
    let ?N = "{x\space M. g x < f x}"
    have N: "?N \ sets M" using borel by simp
    have "?P g ?N \ integral\<^sup>N M g" using pos
      by (intro nn_integral_mono_AE) (auto split: split_indicator)
    then have Pg_fin: "?P g ?N \ \" using g_fin by (auto simp: top_unique)
    have "?P (\x. (f x - g x)) ?N = (\\<^sup>+x. f x * indicator ?N x - g x * indicator ?N x \M)"
      by (auto intro!: nn_integral_cong simp: indicator_def)
    also have "\ = ?P f ?N - ?P g ?N"
    proof (rule nn_integral_diff)
      show "(\x. f x * indicator ?N x) \ borel_measurable M" "(\x. g x * indicator ?N x) \ borel_measurable M"
        using borel N by auto
      show "AE x in M. g x * indicator ?N x \ f x * indicator ?N x"
        using pos by (auto split: split_indicator)
    qed fact
    also have "\ = 0"
      unfolding eq[THEN bspec, OF N] using Pg_fin by auto
    finally have "AE x in M. f x \ g x"
      using pos borel nn_integral_PInf_AE[OF borel(2) g_fin]
      by (subst (asm) nn_integral_0_iff_AE)
         (auto split: split_indicator simp: not_less ennreal_minus_eq_0) }
  from this[OF borel pos g_fin eq] this[OF borel(2,1) pos(2,1) fin] eq
  show "AE x in M. f x = g x" by auto
qed

lemma (in finite_measure) density_unique_finite_measure:
  assumes borel: "f \ borel_measurable M" "f' \ borel_measurable M"
  assumes pos: "AE x in M. 0 \ f x" "AE x in M. 0 \ f' x"
  assumes f: "\A. A \ sets M \ (\\<^sup>+x. f x * indicator A x \M) = (\\<^sup>+x. f' x * indicator A x \M)"
    (is "\A. A \ sets M \ ?P f A = ?P f' A")
  shows "AE x in M. f x = f' x"
proof -
  let ?D = "\f. density M f"
  let ?N = "\A. ?P f A" and ?N' = "\A. ?P f' A"
  let ?f = "\A x. f x * indicator A x" and ?f' = "\A x. f' x * indicator A x"

  have ac: "absolutely_continuous M (density M f)" "sets (density M f) = sets M"
    using borel by (auto intro!: absolutely_continuousI_density)
  from split_space_into_finite_sets_and_rest[OF this]
  obtain Q :: "nat \ 'a set"
    where Q: "disjoint_family Q" "range Q \ sets M"
    and in_Q0: "\A. A \ sets M \ A \ (\i. Q i) = {} \ emeasure M A = 0 \ ?D f A = 0 \ 0 < emeasure M A \ ?D f A = \"
    and Q_fin: "\i. ?D f (Q i) \ \" by force
  with borel pos have in_Q0: "\A. A \ sets M \ A \ (\i. Q i) = {} \ emeasure M A = 0 \ ?N A = 0 \ 0 < emeasure M A \ ?N A = \"
    and Q_fin: "\i. ?N (Q i) \ \" by (auto simp: emeasure_density subset_eq)

  from Q have Q_sets[measurable]: "\i. Q i \ sets M" by auto
  let ?D = "{x\space M. f x \ f' x}"
  have "?D \ sets M" using borel by auto
  have *: "\i x A. \y::ennreal. y * indicator (Q i) x * indicator A x = y * indicator (Q i \ A) x"
    unfolding indicator_def by auto
  have "\i. AE x in M. ?f (Q i) x = ?f' (Q i) x" using borel Q_fin Q pos
    by (intro finite_density_unique[THEN iffD1] allI)
       (auto intro!: f measure_eqI simp: emeasure_density * subset_eq)
  moreover have "AE x in M. ?f (space M - (\i. Q i)) x = ?f' (space M - (\i. Q i)) x"
  proof (rule AE_I')
    { fix f :: "'a \ ennreal" assume borel: "f \ borel_measurable M"
        and eq: "\A. A \ sets M \ ?N A = (\\<^sup>+x. f x * indicator A x \M)"
      let ?A = "\i. (space M - (\i. Q i)) \ {x \ space M. f x < (i::nat)}"
      have "(\i. ?A i) \ null_sets M"
      proof (rule null_sets_UN)
        fix i ::nat have "?A i \ sets M"
          using borel by auto
        have "?N (?A i) \ (\\<^sup>+x. (i::ennreal) * indicator (?A i) x \M)"
          unfolding eq[OF \<open>?A i \<in> sets M\<close>]
          by (auto intro!: nn_integral_mono simp: indicator_def)
        also have "\ = i * emeasure M (?A i)"
          using \<open>?A i \<in> sets M\<close> by (auto intro!: nn_integral_cmult_indicator)
        also have "\ < \" using emeasure_real[of "?A i"] by (auto simp: ennreal_mult_less_top of_nat_less_top)
        finally have "?N (?A i) \ \" by simp
        then show "?A i \ null_sets M" using in_Q0[OF \?A i \ sets M\] \?A i \ sets M\ by auto
      qed
      also have "(\i. ?A i) = (space M - (\i. Q i)) \ {x\space M. f x \ \}"
        by (auto simp: ennreal_Ex_less_of_nat less_top[symmetric])
      finally have "(space M - (\i. Q i)) \ {x\space M. f x \ \} \ null_sets M" by simp }
    from this[OF borel(1) refl] this[OF borel(2) f]
    have "(space M - (\i. Q i)) \ {x\space M. f x \ \} \ null_sets M" "(space M - (\i. Q i)) \ {x\space M. f' x \ \} \ null_sets M" by simp_all
    then show "((space M - (\i. Q i)) \ {x\space M. f x \ \}) \ ((space M - (\i. Q i)) \ {x\space M. f' x \ \}) \ null_sets M" by (rule null_sets.Un)
    show "{x \ space M. ?f (space M - (\i. Q i)) x \ ?f' (space M - (\i. Q i)) x} \
      ((space M - (\<Union>i. Q i)) \<inter> {x\<in>space M. f x \<noteq> \<infinity>}) \<union> ((space M - (\<Union>i. Q i)) \<inter> {x\<in>space M. f' x \<noteq> \<infinity>})" by (auto simp: indicator_def)
  qed
  moreover have "AE x in M. (?f (space M - (\i. Q i)) x = ?f' (space M - (\i. Q i)) x) \ (\i. ?f (Q i) x = ?f' (Q i) x) \
    ?f (space M) x = ?f' (space M) x"
    by (auto simp: indicator_def)
  ultimately have "AE x in M. ?f (space M) x = ?f' (space M) x"
    unfolding AE_all_countable[symmetric]
    by eventually_elim (auto split: if_split_asm simp: indicator_def)
  then show "AE x in M. f x = f' x" by auto
qed

proposition (in sigma_finite_measure) density_unique:
  assumes f: "f \ borel_measurable M"
  assumes f': "f' \<in> borel_measurable M"
  assumes density_eq: "density M f = density M f'"
  shows "AE x in M. f x = f' x"
proof -
  obtain h where h_borel: "h \ borel_measurable M"
    and fin: "integral\<^sup>N M h \ \" and pos: "\x. x \ space M \ 0 < h x \ h x < \" "\x. 0 \ h x"
    using Ex_finite_integrable_function by auto
  then have h_nn: "AE x in M. 0 \ h x" by auto
  let ?H = "density M h"
  interpret h: finite_measure ?H
    using fin h_borel pos
    by (intro finite_measureI) (simp cong: nn_integral_cong emeasure_density add: fin)
  let ?fM = "density M f"
  let ?f'M = "density M f'"
  { fix A assume "A \ sets M"
    then have "{x \ space M. h x * indicator A x \ 0} = A"
      using pos(1) sets.sets_into_space by (force simp: indicator_def)
    then have "(\\<^sup>+x. h x * indicator A x \M) = 0 \ A \ null_sets M"
      using h_borel \<open>A \<in> sets M\<close> h_nn by (subst nn_integral_0_iff) auto }
  note h_null_sets = this
  { fix A assume "A \ sets M"
    have "(\\<^sup>+x. f x * (h x * indicator A x) \M) = (\\<^sup>+x. h x * indicator A x \?fM)"
      using \<open>A \<in> sets M\<close> h_borel h_nn f f'
      by (intro nn_integral_density[symmetric]) auto
    also have "\ = (\\<^sup>+x. h x * indicator A x \?f'M)"
      by (simp_all add: density_eq)
    also have "\ = (\\<^sup>+x. f' x * (h x * indicator A x) \M)"
      using \<open>A \<in> sets M\<close> h_borel h_nn f f'
      by (intro nn_integral_density) auto
    finally have "(\\<^sup>+x. h x * (f x * indicator A x) \M) = (\\<^sup>+x. h x * (f' x * indicator A x) \M)"
      by (simp add: ac_simps)
    then have "(\\<^sup>+x. (f x * indicator A x) \?H) = (\\<^sup>+x. (f' x * indicator A x) \?H)"
      using \<open>A \<in> sets M\<close> h_borel h_nn f f'
      by (subst (asm) (1 2) nn_integral_density[symmetric]) auto }
  then have "AE x in ?H. f x = f' x" using h_borel h_nn f f'
    by (intro h.density_unique_finite_measure absolutely_continuous_AE[of M]) auto
  with AE_space[of M] pos show "AE x in M. f x = f' x"
    unfolding AE_density[OF h_borel] by auto
qed

lemma (in sigma_finite_measure) density_unique_iff:
  assumes f: "f \ borel_measurable M" and f': "f' \ borel_measurable M"
  shows "density M f = density M f' \ (AE x in M. f x = f' x)"
  using density_unique[OF assms] density_cong[OF f f'] by auto

lemma sigma_finite_density_unique:
  assumes borel: "f \ borel_measurable M" "g \ borel_measurable M"
  and fin: "sigma_finite_measure (density M f)"
  shows "density M f = density M g \ (AE x in M. f x = g x)"
proof
  assume "AE x in M. f x = g x" with borel show "density M f = density M g"
    by (auto intro: density_cong)
next
  assume eq: "density M f = density M g"
  interpret f: sigma_finite_measure "density M f" by fact
  from f.sigma_finite_incseq obtain A where cover: "range A \ sets (density M f)"
    "\ (range A) = space (density M f)"
    "\i. emeasure (density M f) (A i) \ \"
    "incseq A"
    by auto
  have "AE x in M. \i. x \ A i \ f x = g x"
    unfolding AE_all_countable
  proof
    fix i
    have "density (density M f) (indicator (A i)) = density (density M g) (indicator (A i))"
      unfolding eq ..
    moreover have "(\\<^sup>+x. f x * indicator (A i) x \M) \ \"
      using cover(1) cover(3)[of i] borel by (auto simp: emeasure_density subset_eq)
    ultimately have "AE x in M. f x * indicator (A i) x = g x * indicator (A i) x"
      using borel cover(1)
      by (intro finite_density_unique[THEN iffD1]) (auto simp: density_density_eq subset_eq)
    then show "AE x in M. x \ A i \ f x = g x"
      by auto
  qed
  with AE_space show "AE x in M. f x = g x"
    apply eventually_elim
    using cover(2)[symmetric]
    apply auto
    done
qed

lemma (in sigma_finite_measure) sigma_finite_iff_density_finite':
  assumes f: "f \ borel_measurable M"
  shows "sigma_finite_measure (density M f) \ (AE x in M. f x \ \)"
    (is "sigma_finite_measure ?N \ _")
proof
  assume "sigma_finite_measure ?N"
  then interpret N: sigma_finite_measure ?N .
  from N.Ex_finite_integrable_function obtain h where
    h: "h \ borel_measurable M" "integral\<^sup>N ?N h \ \" and
    fin: "\x\space M. 0 < h x \ h x < \"
    by auto
  have "AE x in M. f x * h x \ \"
  proof (rule AE_I')
    have "integral\<^sup>N ?N h = (\\<^sup>+x. f x * h x \M)"
      using f h by (auto intro!: nn_integral_density)
    then have "(\\<^sup>+x. f x * h x \M) \ \"
      using h(2) by simp
    then show "(\x. f x * h x) -` {\} \ space M \ null_sets M"
      using f h(1) by (auto intro!: nn_integral_PInf[unfolded infinity_ennreal_def] borel_measurable_vimage)
  qed auto
  then show "AE x in M. f x \ \"
    using fin by (auto elim!: AE_Ball_mp simp: less_top ennreal_mult_less_top)
next
  assume AE: "AE x in M. f x \ \"
  from sigma_finite obtain Q :: "nat \ 'a set"
    where Q: "range Q \ sets M" "\ (range Q) = space M" "\i. emeasure M (Q i) \ \"
    by auto
  define A where "A i =
    f -` (case i of 0 \<Rightarrow> {\<infinity>} | Suc n \<Rightarrow> {.. ennreal(of_nat (Suc n))}) \<inter> space M" for i
  { fix i j have "A i \ Q j \ sets M"
    unfolding A_def using f Q
    apply (rule_tac sets.Int)
    by (cases i) (auto intro: measurable_sets[OF f(1)]) }
  note A_in_sets = this

  show "sigma_finite_measure ?N"
  proof (standard, intro exI conjI ballI)
    show "countable (range (\(i, j). A i \ Q j))"
      by auto
    show "range (\(i, j). A i \ Q j) \ sets (density M f)"
      using A_in_sets by auto
  next
    have "\(range (\(i, j). A i \ Q j)) = (\i j. A i \ Q j)"
      by auto
    also have "\ = (\i. A i) \ space M" using Q by auto
    also have "(\i. A i) = space M"
    proof safe
      fix x assume x: "x \ space M"
      show "x \ (\i. A i)"
      proof (cases "f x" rule: ennreal_cases)
        case top with x show ?thesis unfolding A_def by (auto intro: exI[of _ 0])
      next
        case (real r)
        with ennreal_Ex_less_of_nat[of "f x"] obtain n :: nat where "f x < n"
          by auto
        also have "n < (Suc n :: ennreal)"
          by simp
        finally show ?thesis
          using x real by (auto simp: A_def ennreal_of_nat_eq_real_of_nat intro!: exI[of _ "Suc n"])
      qed
    qed (auto simp: A_def)
    finally show "\(range (\(i, j). A i \ Q j)) = space ?N" by simp
  next
    fix X assume "X \ range (\(i, j). A i \ Q j)"
    then obtain i j where [simp]:"X = A i \ Q j" by auto
    have "(\\<^sup>+x. f x * indicator (A i \ Q j) x \M) \ \"
    proof (cases i)
      case 0
      have "AE x in M. f x * indicator (A i \ Q j) x = 0"
        using AE by (auto simp: A_def \<open>i = 0\<close>)
      from nn_integral_cong_AE[OF this] show ?thesis by simp
    next
      case (Suc n)
      then have "(\\<^sup>+x. f x * indicator (A i \ Q j) x \M) \
        (\<integral>\<^sup>+x. (Suc n :: ennreal) * indicator (Q j) x \<partial>M)"
        by (auto intro!: nn_integral_mono simp: indicator_def A_def ennreal_of_nat_eq_real_of_nat)
      also have "\ = Suc n * emeasure M (Q j)"
        using Q by (auto intro!: nn_integral_cmult_indicator)
      also have "\ < \"
        using Q by (auto simp: ennreal_mult_less_top less_top of_nat_less_top)
      finally show ?thesis by simp
    qed
    then show "emeasure ?N X \ \"
      using A_in_sets Q f by (auto simp: emeasure_density)
  qed
qed

lemma (in sigma_finite_measure) sigma_finite_iff_density_finite:
  "f \ borel_measurable M \ sigma_finite_measure (density M f) \ (AE x in M. f x \ \)"
  by (subst sigma_finite_iff_density_finite')
     (auto simp: max_def intro!: measurable_If)

subsection \<open>Radon-Nikodym derivative\<close>

definition\<^marker>\<open>tag important\<close> RN_deriv :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a \<Rightarrow> ennreal" where
  "RN_deriv M N =
    (if \<exists>f. f \<in> borel_measurable M \<and> density M f = N
       then SOME f. f \<in> borel_measurable M \<and> density M f = N
       else (\<lambda>_. 0))"

lemma RN_derivI:
  assumes "f \ borel_measurable M" "density M f = N"
  shows "density M (RN_deriv M N) = N"
proof -
  have *: "\f. f \ borel_measurable M \ density M f = N"
    using assms by auto
  then have "density M (SOME f. f \ borel_measurable M \ density M f = N) = N"
    by (rule someI2_ex) auto
  with * show ?thesis
    by (auto simp: RN_deriv_def)
qed

lemma borel_measurable_RN_deriv[measurable]: "RN_deriv M N \ borel_measurable M"
proof -
  { assume ex: "\f. f \ borel_measurable M \ density M f = N"
    have 1: "(SOME f. f \ borel_measurable M \ density M f = N) \ borel_measurable M"
      using ex by (rule someI2_ex) auto }
  from this show ?thesis
    by (auto simp: RN_deriv_def)
qed

lemma density_RN_deriv_density:
  assumes f: "f \ borel_measurable M"
  shows "density M (RN_deriv M (density M f)) = density M f"
  by (rule RN_derivI[OF f]) simp

lemma (in sigma_finite_measure) density_RN_deriv:
  "absolutely_continuous M N \ sets N = sets M \ density M (RN_deriv M N) = N"
  by (metis RN_derivI Radon_Nikodym)

lemma (in sigma_finite_measure) RN_deriv_nn_integral:
  assumes N: "absolutely_continuous M N" "sets N = sets M"
    and f: "f \ borel_measurable M"
  shows "integral\<^sup>N N f = (\\<^sup>+x. RN_deriv M N x * f x \M)"
proof -
  have "integral\<^sup>N N f = integral\<^sup>N (density M (RN_deriv M N)) f"
    using N by (simp add: density_RN_deriv)
  also have "\ = (\\<^sup>+x. RN_deriv M N x * f x \M)"
    using f by (simp add: nn_integral_density)
  finally show ?thesis by simp
qed

lemma (in sigma_finite_measure) RN_deriv_unique:
  assumes f: "f \ borel_measurable M"
  and eq: "density M f = N"
  shows "AE x in M. f x = RN_deriv M N x"
  unfolding eq[symmetric]
  by (intro density_unique_iff[THEN iffD1] f borel_measurable_RN_deriv
            density_RN_deriv_density[symmetric])

lemma RN_deriv_unique_sigma_finite:
  assumes f: "f \ borel_measurable M"
  and eq: "density M f = N" and fin: "sigma_finite_measure N"
  shows "AE x in M. f x = RN_deriv M N x"
  using fin unfolding eq[symmetric]
  by (intro sigma_finite_density_unique[THEN iffD1] f borel_measurable_RN_deriv
            density_RN_deriv_density[symmetric])

lemma (in sigma_finite_measure) RN_deriv_distr:
  fixes T :: "'a \ 'b"
  assumes T: "T \ measurable M M'" and T': "T' \ measurable M' M"
    and inv: "\x\space M. T' (T x) = x"
  and ac[simp]: "absolutely_continuous (distr M M' T) (distr N M' T)"
  and N: "sets N = sets M"
  shows "AE x in M. RN_deriv (distr M M' T) (distr N M' T) (T x) = RN_deriv M N x"
proof (rule RN_deriv_unique)
  have [simp]: "sets N = sets M" by fact
  note sets_eq_imp_space_eq[OF N, simp]
  have measurable_N[simp]: "\M'. measurable N M' = measurable M M'" by (auto simp: measurable_def)
  { fix A assume "A \ sets M"
    with inv T T' sets.sets_into_space[OF this]
    have "T -` T' -` A \ T -` space M' \ space M = A"
      by (auto simp: measurable_def) }
  note eq = this[simp]
  { fix A assume "A \ sets M"
    with inv T T' sets.sets_into_space[OF this]
    have "(T' \ T) -` A \ space M = A"
      by (auto simp: measurable_def) }
  note eq2 = this[simp]
  let ?M' = "distr M M' T" and ?N' = "distr N M' T"
  interpret M': sigma_finite_measure ?M'
  proof
    from sigma_finite_countable obtain F
      where F: "countable F \ F \ sets M \ \ F = space M \ (\a\F. emeasure M a \ \)" ..
    show "\A. countable A \ A \ sets (distr M M' T) \ \A = space (distr M M' T) \ (\a\A. emeasure (distr M M' T) a \ \)"
    proof (intro exI conjI ballI)
      show *: "(\A. T' -` A \ space ?M') ` F \ sets ?M'"
        using F T' by (auto simp: measurable_def)
      show "\((\A. T' -` A \ space ?M')`F) = space ?M'"
        using F T'[THEN measurable_space] by (auto simp: set_eq_iff)
    next
      fix X assume "X \ (\A. T' -` A \ space ?M')`F"
      then obtain A where [simp]: "X = T' -` A \ space ?M'" and "A \ F" by auto
      have "X \ sets M'" using F T' \A\F\ by auto
      moreover
      have Fi: "A \ sets M" using F \A\F\ by auto
      ultimately show "emeasure ?M' X \ \"
        using F T T' \A\F\ by (simp add: emeasure_distr)
    qed (use F in auto)
  qed
  have "(RN_deriv ?M' ?N') \ T \ borel_measurable M"
    using T ac by measurable
  then show "(\x. RN_deriv ?M' ?N' (T x)) \ borel_measurable M"
    by (simp add: comp_def)

  have "N = distr N M (T' \ T)"
    by (subst measure_of_of_measure[of N, symmetric])
       (auto simp add: distr_def sets.sigma_sets_eq intro!: measure_of_eq sets.space_closed)
  also have "\ = distr (distr N M' T) M T'"
    using T T' by (simp add: distr_distr)
  also have "\ = distr (density (distr M M' T) (RN_deriv (distr M M' T) (distr N M' T))) M T'"
    using ac by (simp add: M'.density_RN_deriv)
  also have "\ = density M (RN_deriv (distr M M' T) (distr N M' T) \ T)"
    by (simp add: distr_density_distr[OF T T', OF inv])
  finally show "density M (\x. RN_deriv (distr M M' T) (distr N M' T) (T x)) = N"
    by (simp add: comp_def)
qed

lemma (in sigma_finite_measure) RN_deriv_finite:
  assumes N: "sigma_finite_measure N" and ac: "absolutely_continuous M N" "sets N = sets M"
  shows "AE x in M. RN_deriv M N x \ \"
proof -
  interpret N: sigma_finite_measure N by fact
  from N show ?thesis
    using sigma_finite_iff_density_finite[OF borel_measurable_RN_deriv, of N] density_RN_deriv[OF ac]
    by simp
qed

lemma (in sigma_finite_measure)
  assumes N: "sigma_finite_measure N" and ac: "absolutely_continuous M N" "sets N = sets M"
    and f: "f \ borel_measurable M"
  shows RN_deriv_integrable: "integrable N f \
      integrable M (\<lambda>x. enn2real (RN_deriv M N x) * f x)" (is ?integrable)
    and RN_deriv_integral: "integral\<^sup>L N f = (\x. enn2real (RN_deriv M N x) * f x \M)" (is ?integral)
proof -
  note ac(2)[simp] and sets_eq_imp_space_eq[OF ac(2), simp]
  interpret N: sigma_finite_measure N by fact

  have eq: "density M (RN_deriv M N) = density M (\x. enn2real (RN_deriv M N x))"
  proof (rule density_cong)
    from RN_deriv_finite[OF assms(1,2,3)]
    show "AE x in M. RN_deriv M N x = ennreal (enn2real (RN_deriv M N x))"
      by eventually_elim (auto simp: less_top)
  qed (insert ac, auto)

  show ?integrable
    apply (subst density_RN_deriv[OF ac, symmetric])
    unfolding eq
    apply (intro integrable_real_density f AE_I2 enn2real_nonneg)
    apply (insert ac, auto)
    done

  show ?integral
    apply (subst density_RN_deriv[OF ac, symmetric])
    unfolding eq
    apply (intro integral_real_density f AE_I2 enn2real_nonneg)
    apply (insert ac, auto)
    done
qed

proposition (in sigma_finite_measure) real_RN_deriv:
  assumes "finite_measure N"
  assumes ac: "absolutely_continuous M N" "sets N = sets M"
  obtains D where "D \ borel_measurable M"
    and "AE x in M. RN_deriv M N x = ennreal (D x)"
    and "AE x in N. 0 < D x"
    and "\x. 0 \ D x"
proof
  interpret N: finite_measure N by fact

  note RN = borel_measurable_RN_deriv density_RN_deriv[OF ac]

  let ?RN = "\t. {x \ space M. RN_deriv M N x = t}"

  show "(\x. enn2real (RN_deriv M N x)) \ borel_measurable M"
    using RN by auto

  have "N (?RN \) = (\\<^sup>+ x. RN_deriv M N x * indicator (?RN \) x \M)"
    using RN(1) by (subst RN(2)[symmetric]) (auto simp: emeasure_density)
  also have "\ = (\\<^sup>+ x. \ * indicator (?RN \) x \M)"
    by (intro nn_integral_cong) (auto simp: indicator_def)
  also have "\ = \ * emeasure M (?RN \)"
    using RN by (intro nn_integral_cmult_indicator) auto
  finally have eq: "N (?RN \) = \ * emeasure M (?RN \)" .
  moreover
  have "emeasure M (?RN \) = 0"
  proof (rule ccontr)
    assume "emeasure M {x \ space M. RN_deriv M N x = \} \ 0"
    then have "0 < emeasure M {x \ space M. RN_deriv M N x = \}"
      by (auto simp: zero_less_iff_neq_zero)
    with eq have "N (?RN \) = \" by (simp add: ennreal_mult_eq_top_iff)
    with N.emeasure_finite[of "?RN \"] RN show False by auto
  qed
  ultimately have "AE x in M. RN_deriv M N x < \"
    using RN by (intro AE_iff_measurable[THEN iffD2]) (auto simp: less_top[symmetric])
  then show "AE x in M. RN_deriv M N x = ennreal (enn2real (RN_deriv M N x))"
    by auto
  then have eq: "AE x in N. RN_deriv M N x = ennreal (enn2real (RN_deriv M N x))"
    using ac absolutely_continuous_AE by auto

  have "N (?RN 0) = (\\<^sup>+ x. RN_deriv M N x * indicator (?RN 0) x \M)"
    by (subst RN(2)[symmetric]) (auto simp: emeasure_density)
  also have "\ = (\\<^sup>+ x. 0 \M)"
    by (intro nn_integral_cong) (auto simp: indicator_def)
  finally have "AE x in N. RN_deriv M N x \ 0"
    using RN by (subst AE_iff_measurable[OF _ refl]) (auto simp: ac cong: sets_eq_imp_space_eq)
  with eq show "AE x in N. 0 < enn2real (RN_deriv M N x)"
    by (auto simp: enn2real_positive_iff less_top[symmetric] zero_less_iff_neq_zero)
qed (rule enn2real_nonneg)

lemma (in sigma_finite_measure) RN_deriv_singleton:
  assumes ac: "absolutely_continuous M N" "sets N = sets M"
  and x: "{x} \ sets M"
  shows "N {x} = RN_deriv M N x * emeasure M {x}"
proof -
  from \<open>{x} \<in> sets M\<close>
  have "density M (RN_deriv M N) {x} = (\\<^sup>+w. RN_deriv M N x * indicator {x} w \M)"
    by (auto simp: indicator_def emeasure_density intro!: nn_integral_cong)
  with x density_RN_deriv[OF ac] show ?thesis
    by (auto simp: max_def)
qed

end

quality100%

¤ Dauer der Verarbeitung: 0.26 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.