src/HOL/Probability/Radon_Nikodym.thy
changeset 41544 c3b977fee8a3
parent 41097 a1abfa4e2b44
child 41661 baf1964bc468
equal deleted inserted replaced
41543:646a1399e792 41544:c3b977fee8a3
   112   qed
   112   qed
   113   finally show "\<nu> N = 0" .
   113   finally show "\<nu> N = 0" .
   114 qed
   114 qed
   115 
   115 
   116 lemma (in measure_space) density_is_absolutely_continuous:
   116 lemma (in measure_space) density_is_absolutely_continuous:
   117   assumes "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
   117   assumes "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
   118   shows "absolutely_continuous \<nu>"
   118   shows "absolutely_continuous \<nu>"
   119   using assms unfolding absolutely_continuous_def
   119   using assms unfolding absolutely_continuous_def
   120   by (simp add: positive_integral_null_set)
   120   by (simp add: positive_integral_null_set)
   121 
   121 
   122 subsection "Existence of the Radon-Nikodym derivative"
   122 subsection "Existence of the Radon-Nikodym derivative"
   287 qed
   287 qed
   288 
   288 
   289 lemma (in finite_measure) Radon_Nikodym_finite_measure:
   289 lemma (in finite_measure) Radon_Nikodym_finite_measure:
   290   assumes "finite_measure M \<nu>"
   290   assumes "finite_measure M \<nu>"
   291   assumes "absolutely_continuous \<nu>"
   291   assumes "absolutely_continuous \<nu>"
   292   shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
   292   shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
   293 proof -
   293 proof -
   294   interpret M': finite_measure M \<nu> using assms(1) .
   294   interpret M': finite_measure M \<nu> using assms(1) .
   295   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}"
   295   def G \<equiv> "{g \<in> borel_measurable M. \<forall>A\<in>sets M. (\<integral>\<^isup>+x. g x * indicator A x) \<le> \<nu> A}"
   296   have "(\<lambda>x. 0) \<in> G" unfolding G_def by auto
   296   have "(\<lambda>x. 0) \<in> G" unfolding G_def by auto
   297   hence "G \<noteq> {}" by auto
   297   hence "G \<noteq> {}" by auto
   298   { fix f g assume f: "f \<in> G" and g: "g \<in> G"
   298   { fix f g assume f: "f \<in> G" and g: "g \<in> G"
   299     have "(\<lambda>x. max (g x) (f x)) \<in> G" (is "?max \<in> G") unfolding G_def
   299     have "(\<lambda>x. max (g x) (f x)) \<in> G" (is "?max \<in> G") unfolding G_def
   300     proof safe
   300     proof safe
   306       have union: "((?A \<inter> A) \<union> ((space M - ?A) \<inter> A)) = A"
   306       have union: "((?A \<inter> A) \<union> ((space M - ?A) \<inter> A)) = A"
   307         using sets_into_space[OF `A \<in> sets M`] by auto
   307         using sets_into_space[OF `A \<in> sets M`] by auto
   308       have "\<And>x. x \<in> space M \<Longrightarrow> max (g x) (f x) * indicator A x =
   308       have "\<And>x. x \<in> space M \<Longrightarrow> max (g x) (f x) * indicator A x =
   309         g x * indicator (?A \<inter> A) x + f x * indicator ((space M - ?A) \<inter> A) x"
   309         g x * indicator (?A \<inter> A) x + f x * indicator ((space M - ?A) \<inter> A) x"
   310         by (auto simp: indicator_def max_def)
   310         by (auto simp: indicator_def max_def)
   311       hence "positive_integral (\<lambda>x. max (g x) (f x) * indicator A x) =
   311       hence "(\<integral>\<^isup>+x. max (g x) (f x) * indicator A x) =
   312         positive_integral (\<lambda>x. g x * indicator (?A \<inter> A) x) +
   312         (\<integral>\<^isup>+x. g x * indicator (?A \<inter> A) x) +
   313         positive_integral (\<lambda>x. f x * indicator ((space M - ?A) \<inter> A) x)"
   313         (\<integral>\<^isup>+x. f x * indicator ((space M - ?A) \<inter> A) x)"
   314         using f g sets unfolding G_def
   314         using f g sets unfolding G_def
   315         by (auto cong: positive_integral_cong intro!: positive_integral_add borel_measurable_indicator)
   315         by (auto cong: positive_integral_cong intro!: positive_integral_add borel_measurable_indicator)
   316       also have "\<dots> \<le> \<nu> (?A \<inter> A) + \<nu> ((space M - ?A) \<inter> A)"
   316       also have "\<dots> \<le> \<nu> (?A \<inter> A) + \<nu> ((space M - ?A) \<inter> A)"
   317         using f g sets unfolding G_def by (auto intro!: add_mono)
   317         using f g sets unfolding G_def by (auto intro!: add_mono)
   318       also have "\<dots> = \<nu> A"
   318       also have "\<dots> = \<nu> A"
   319         using M'.measure_additive[OF sets] union by auto
   319         using M'.measure_additive[OF sets] union by auto
   320       finally show "positive_integral (\<lambda>x. max (g x) (f x) * indicator A x) \<le> \<nu> A" .
   320       finally show "(\<integral>\<^isup>+x. max (g x) (f x) * indicator A x) \<le> \<nu> A" .
   321     qed }
   321     qed }
   322   note max_in_G = this
   322   note max_in_G = this
   323   { fix f g assume  "f \<up> g" and f: "\<And>i. f i \<in> G"
   323   { fix f g assume  "f \<up> g" and f: "\<And>i. f i \<in> G"
   324     have "g \<in> G" unfolding G_def
   324     have "g \<in> G" unfolding G_def
   325     proof safe
   325     proof safe
   329       thus "g \<in> borel_measurable M" by auto
   329       thus "g \<in> borel_measurable M" by auto
   330       fix A assume "A \<in> sets M"
   330       fix A assume "A \<in> sets M"
   331       hence "\<And>i. (\<lambda>x. f i x * indicator A x) \<in> borel_measurable M"
   331       hence "\<And>i. (\<lambda>x. f i x * indicator A x) \<in> borel_measurable M"
   332         using f_borel by (auto intro!: borel_measurable_indicator)
   332         using f_borel by (auto intro!: borel_measurable_indicator)
   333       from positive_integral_isoton[OF isoton_indicator[OF `f \<up> g`] this]
   333       from positive_integral_isoton[OF isoton_indicator[OF `f \<up> g`] this]
   334       have SUP: "positive_integral (\<lambda>x. g x * indicator A x) =
   334       have SUP: "(\<integral>\<^isup>+x. g x * indicator A x) =
   335           (SUP i. positive_integral (\<lambda>x. f i x * indicator A x))"
   335           (SUP i. (\<integral>\<^isup>+x. f i x * indicator A x))"
   336         unfolding isoton_def by simp
   336         unfolding isoton_def by simp
   337       show "positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A" unfolding SUP
   337       show "(\<integral>\<^isup>+x. g x * indicator A x) \<le> \<nu> A" unfolding SUP
   338         using f `A \<in> sets M` unfolding G_def by (auto intro!: SUP_leI)
   338         using f `A \<in> sets M` unfolding G_def by (auto intro!: SUP_leI)
   339     qed }
   339     qed }
   340   note SUP_in_G = this
   340   note SUP_in_G = this
   341   let ?y = "SUP g : G. positive_integral g"
   341   let ?y = "SUP g : G. positive_integral g"
   342   have "?y \<le> \<nu> (space M)" unfolding G_def
   342   have "?y \<le> \<nu> (space M)" unfolding G_def
   343   proof (safe intro!: SUP_leI)
   343   proof (safe intro!: SUP_leI)
   344     fix g assume "\<forall>A\<in>sets M. positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A"
   344     fix g assume "\<forall>A\<in>sets M. (\<integral>\<^isup>+x. g x * indicator A x) \<le> \<nu> A"
   345     from this[THEN bspec, OF top] show "positive_integral g \<le> \<nu> (space M)"
   345     from this[THEN bspec, OF top] show "positive_integral g \<le> \<nu> (space M)"
   346       by (simp cong: positive_integral_cong)
   346       by (simp cong: positive_integral_cong)
   347   qed
   347   qed
   348   hence "?y \<noteq> \<omega>" using M'.finite_measure_of_space by auto
   348   hence "?y \<noteq> \<omega>" using M'.finite_measure_of_space by auto
   349   from SUPR_countable_SUPR[OF this `G \<noteq> {}`] guess ys .. note ys = this
   349   from SUPR_countable_SUPR[OF this `G \<noteq> {}`] guess ys .. note ys = this
   382       using g_in_G by (auto intro!: exI Sup_mono simp: SUPR_def)
   382       using g_in_G by (auto intro!: exI Sup_mono simp: SUPR_def)
   383     show "?y \<le> (SUP i. positive_integral (?g i))" unfolding y_eq
   383     show "?y \<le> (SUP i. positive_integral (?g i))" unfolding y_eq
   384       by (auto intro!: SUP_mono positive_integral_mono Max_ge)
   384       by (auto intro!: SUP_mono positive_integral_mono Max_ge)
   385   qed
   385   qed
   386   finally have int_f_eq_y: "positive_integral f = ?y" .
   386   finally have int_f_eq_y: "positive_integral f = ?y" .
   387   let "?t A" = "\<nu> A - positive_integral (\<lambda>x. f x * indicator A x)"
   387   let "?t A" = "\<nu> A - (\<integral>\<^isup>+x. f x * indicator A x)"
   388   have "finite_measure M ?t"
   388   have "finite_measure M ?t"
   389   proof
   389   proof
   390     show "?t {} = 0" by simp
   390     show "?t {} = 0" by simp
   391     show "?t (space M) \<noteq> \<omega>" using M'.finite_measure by simp
   391     show "?t (space M) \<noteq> \<omega>" using M'.finite_measure by simp
   392     show "countably_additive M ?t" unfolding countably_additive_def
   392     show "countably_additive M ?t" unfolding countably_additive_def
   393     proof safe
   393     proof safe
   394       fix A :: "nat \<Rightarrow> 'a set"  assume A: "range A \<subseteq> sets M" "disjoint_family A"
   394       fix A :: "nat \<Rightarrow> 'a set"  assume A: "range A \<subseteq> sets M" "disjoint_family A"
   395       have "(\<Sum>\<^isub>\<infinity> n. positive_integral (\<lambda>x. f x * indicator (A n) x))
   395       have "(\<Sum>\<^isub>\<infinity> n. (\<integral>\<^isup>+x. f x * indicator (A n) x))
   396         = positive_integral (\<lambda>x. (\<Sum>\<^isub>\<infinity>n. f x * indicator (A n) x))"
   396         = (\<integral>\<^isup>+x. (\<Sum>\<^isub>\<infinity>n. f x * indicator (A n) x))"
   397         using `range A \<subseteq> sets M`
   397         using `range A \<subseteq> sets M`
   398         by (rule_tac positive_integral_psuminf[symmetric]) (auto intro!: borel_measurable_indicator)
   398         by (rule_tac positive_integral_psuminf[symmetric]) (auto intro!: borel_measurable_indicator)
   399       also have "\<dots> = positive_integral (\<lambda>x. f x * indicator (\<Union>n. A n) x)"
   399       also have "\<dots> = (\<integral>\<^isup>+x. f x * indicator (\<Union>n. A n) x)"
   400         apply (rule positive_integral_cong)
   400         apply (rule positive_integral_cong)
   401         apply (subst psuminf_cmult_right)
   401         apply (subst psuminf_cmult_right)
   402         unfolding psuminf_indicator[OF `disjoint_family A`] ..
   402         unfolding psuminf_indicator[OF `disjoint_family A`] ..
   403       finally have "(\<Sum>\<^isub>\<infinity> n. positive_integral (\<lambda>x. f x * indicator (A n) x))
   403       finally have "(\<Sum>\<^isub>\<infinity> n. (\<integral>\<^isup>+x. f x * indicator (A n) x))
   404         = positive_integral (\<lambda>x. f x * indicator (\<Union>n. A n) x)" .
   404         = (\<integral>\<^isup>+x. f x * indicator (\<Union>n. A n) x)" .
   405       moreover have "(\<Sum>\<^isub>\<infinity>n. \<nu> (A n)) = \<nu> (\<Union>n. A n)"
   405       moreover have "(\<Sum>\<^isub>\<infinity>n. \<nu> (A n)) = \<nu> (\<Union>n. A n)"
   406         using M'.measure_countably_additive A by (simp add: comp_def)
   406         using M'.measure_countably_additive A by (simp add: comp_def)
   407       moreover have "\<And>i. positive_integral (\<lambda>x. f x * indicator (A i) x) \<le> \<nu> (A i)"
   407       moreover have "\<And>i. (\<integral>\<^isup>+x. f x * indicator (A i) x) \<le> \<nu> (A i)"
   408           using A `f \<in> G` unfolding G_def by auto
   408           using A `f \<in> G` unfolding G_def by auto
   409       moreover have v_fin: "\<nu> (\<Union>i. A i) \<noteq> \<omega>" using M'.finite_measure A by (simp add: countable_UN)
   409       moreover have v_fin: "\<nu> (\<Union>i. A i) \<noteq> \<omega>" using M'.finite_measure A by (simp add: countable_UN)
   410       moreover {
   410       moreover {
   411         have "positive_integral (\<lambda>x. f x * indicator (\<Union>i. A i) x) \<le> \<nu> (\<Union>i. A i)"
   411         have "(\<integral>\<^isup>+x. f x * indicator (\<Union>i. A i) x) \<le> \<nu> (\<Union>i. A i)"
   412           using A `f \<in> G` unfolding G_def by (auto simp: countable_UN)
   412           using A `f \<in> G` unfolding G_def by (auto simp: countable_UN)
   413         also have "\<nu> (\<Union>i. A i) < \<omega>" using v_fin by (simp add: pextreal_less_\<omega>)
   413         also have "\<nu> (\<Union>i. A i) < \<omega>" using v_fin by (simp add: pextreal_less_\<omega>)
   414         finally have "positive_integral (\<lambda>x. f x * indicator (\<Union>i. A i) x) \<noteq> \<omega>"
   414         finally have "(\<integral>\<^isup>+x. f x * indicator (\<Union>i. A i) x) \<noteq> \<omega>"
   415           by (simp add: pextreal_less_\<omega>) }
   415           by (simp add: pextreal_less_\<omega>) }
   416       ultimately
   416       ultimately
   417       show "(\<Sum>\<^isub>\<infinity> n. ?t (A n)) = ?t (\<Union>i. A i)"
   417       show "(\<Sum>\<^isub>\<infinity> n. ?t (A n)) = ?t (\<Union>i. A i)"
   418         apply (subst psuminf_minus) by simp_all
   418         apply (subst psuminf_minus) by simp_all
   419     qed
   419     qed
   431     finally have pos_t: "0 < ?t (space M)" by simp
   431     finally have pos_t: "0 < ?t (space M)" by simp
   432     moreover
   432     moreover
   433     hence pos_M: "0 < \<mu> (space M)"
   433     hence pos_M: "0 < \<mu> (space M)"
   434       using ac top unfolding absolutely_continuous_def by auto
   434       using ac top unfolding absolutely_continuous_def by auto
   435     moreover
   435     moreover
   436     have "positive_integral (\<lambda>x. f x * indicator (space M) x) \<le> \<nu> (space M)"
   436     have "(\<integral>\<^isup>+x. f x * indicator (space M) x) \<le> \<nu> (space M)"
   437       using `f \<in> G` unfolding G_def by auto
   437       using `f \<in> G` unfolding G_def by auto
   438     hence "positive_integral (\<lambda>x. f x * indicator (space M) x) \<noteq> \<omega>"
   438     hence "(\<integral>\<^isup>+x. f x * indicator (space M) x) \<noteq> \<omega>"
   439       using M'.finite_measure_of_space by auto
   439       using M'.finite_measure_of_space by auto
   440     moreover
   440     moreover
   441     def b \<equiv> "?t (space M) / \<mu> (space M) / 2"
   441     def b \<equiv> "?t (space M) / \<mu> (space M) / 2"
   442     ultimately have b: "b \<noteq> 0" "b \<noteq> \<omega>"
   442     ultimately have b: "b \<noteq> 0" "b \<noteq> \<omega>"
   443       using M'.finite_measure_of_space
   443       using M'.finite_measure_of_space
   460         by (cases "b * \<mu> B", cases "?t B") (auto simp: field_simps) }
   460         by (cases "b * \<mu> B", cases "?t B") (auto simp: field_simps) }
   461     note bM_le_t = this
   461     note bM_le_t = this
   462     let "?f0 x" = "f x + b * indicator A0 x"
   462     let "?f0 x" = "f x + b * indicator A0 x"
   463     { fix A assume A: "A \<in> sets M"
   463     { fix A assume A: "A \<in> sets M"
   464       hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
   464       hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
   465       have "positive_integral (\<lambda>x. ?f0 x  * indicator A x) =
   465       have "(\<integral>\<^isup>+x. ?f0 x  * indicator A x) =
   466         positive_integral (\<lambda>x. f x * indicator A x + b * indicator (A \<inter> A0) x)"
   466         (\<integral>\<^isup>+x. f x * indicator A x + b * indicator (A \<inter> A0) x)"
   467         by (auto intro!: positive_integral_cong simp: field_simps indicator_inter_arith)
   467         by (auto intro!: positive_integral_cong simp: field_simps indicator_inter_arith)
   468       hence "positive_integral (\<lambda>x. ?f0 x * indicator A x) =
   468       hence "(\<integral>\<^isup>+x. ?f0 x * indicator A x) =
   469           positive_integral (\<lambda>x. f x * indicator A x) + b * \<mu> (A \<inter> A0)"
   469           (\<integral>\<^isup>+x. f x * indicator A x) + b * \<mu> (A \<inter> A0)"
   470         using `A0 \<in> sets M` `A \<inter> A0 \<in> sets M` A
   470         using `A0 \<in> sets M` `A \<inter> A0 \<in> sets M` A
   471         by (simp add: borel_measurable_indicator positive_integral_add positive_integral_cmult_indicator) }
   471         by (simp add: borel_measurable_indicator positive_integral_add positive_integral_cmult_indicator) }
   472     note f0_eq = this
   472     note f0_eq = this
   473     { fix A assume A: "A \<in> sets M"
   473     { fix A assume A: "A \<in> sets M"
   474       hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
   474       hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
   475       have f_le_v: "positive_integral (\<lambda>x. f x * indicator A x) \<le> \<nu> A"
   475       have f_le_v: "(\<integral>\<^isup>+x. f x * indicator A x) \<le> \<nu> A"
   476         using `f \<in> G` A unfolding G_def by auto
   476         using `f \<in> G` A unfolding G_def by auto
   477       note f0_eq[OF A]
   477       note f0_eq[OF A]
   478       also have "positive_integral (\<lambda>x. f x * indicator A x) + b * \<mu> (A \<inter> A0) \<le>
   478       also have "(\<integral>\<^isup>+x. f x * indicator A x) + b * \<mu> (A \<inter> A0) \<le>
   479           positive_integral (\<lambda>x. f x * indicator A x) + ?t (A \<inter> A0)"
   479           (\<integral>\<^isup>+x. f x * indicator A x) + ?t (A \<inter> A0)"
   480         using bM_le_t[OF `A \<inter> A0 \<in> sets M`] `A \<in> sets M` `A0 \<in> sets M`
   480         using bM_le_t[OF `A \<inter> A0 \<in> sets M`] `A \<in> sets M` `A0 \<in> sets M`
   481         by (auto intro!: add_left_mono)
   481         by (auto intro!: add_left_mono)
   482       also have "\<dots> \<le> positive_integral (\<lambda>x. f x * indicator A x) + ?t A"
   482       also have "\<dots> \<le> (\<integral>\<^isup>+x. f x * indicator A x) + ?t A"
   483         using M.measure_mono[simplified, OF _ `A \<inter> A0 \<in> sets M` `A \<in> sets M`]
   483         using M.measure_mono[simplified, OF _ `A \<inter> A0 \<in> sets M` `A \<in> sets M`]
   484         by (auto intro!: add_left_mono)
   484         by (auto intro!: add_left_mono)
   485       also have "\<dots> \<le> \<nu> A"
   485       also have "\<dots> \<le> \<nu> A"
   486         using f_le_v M'.finite_measure[simplified, OF `A \<in> sets M`]
   486         using f_le_v M'.finite_measure[simplified, OF `A \<in> sets M`]
   487         by (cases "positive_integral (\<lambda>x. f x * indicator A x)", cases "\<nu> A", auto)
   487         by (cases "(\<integral>\<^isup>+x. f x * indicator A x)", cases "\<nu> A", auto)
   488       finally have "positive_integral (\<lambda>x. ?f0 x * indicator A x) \<le> \<nu> A" . }
   488       finally have "(\<integral>\<^isup>+x. ?f0 x * indicator A x) \<le> \<nu> A" . }
   489     hence "?f0 \<in> G" using `A0 \<in> sets M` unfolding G_def
   489     hence "?f0 \<in> G" using `A0 \<in> sets M` unfolding G_def
   490       by (auto intro!: borel_measurable_indicator borel_measurable_pextreal_add borel_measurable_pextreal_times)
   490       by (auto intro!: borel_measurable_indicator borel_measurable_pextreal_add borel_measurable_pextreal_times)
   491     have real: "?t (space M) \<noteq> \<omega>" "?t A0 \<noteq> \<omega>"
   491     have real: "?t (space M) \<noteq> \<omega>" "?t A0 \<noteq> \<omega>"
   492       "b * \<mu> (space M) \<noteq> \<omega>" "b * \<mu> A0 \<noteq> \<omega>"
   492       "b * \<mu> (space M) \<noteq> \<omega>" "b * \<mu> A0 \<noteq> \<omega>"
   493       using `A0 \<in> sets M` b
   493       using `A0 \<in> sets M` b
   523     ultimately show False by auto
   523     ultimately show False by auto
   524   qed
   524   qed
   525   show ?thesis
   525   show ?thesis
   526   proof (safe intro!: bexI[of _ f])
   526   proof (safe intro!: bexI[of _ f])
   527     fix A assume "A\<in>sets M"
   527     fix A assume "A\<in>sets M"
   528     show "\<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
   528     show "\<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
   529     proof (rule antisym)
   529     proof (rule antisym)
   530       show "positive_integral (\<lambda>x. f x * indicator A x) \<le> \<nu> A"
   530       show "(\<integral>\<^isup>+x. f x * indicator A x) \<le> \<nu> A"
   531         using `f \<in> G` `A \<in> sets M` unfolding G_def by auto
   531         using `f \<in> G` `A \<in> sets M` unfolding G_def by auto
   532       show "\<nu> A \<le> positive_integral (\<lambda>x. f x * indicator A x)"
   532       show "\<nu> A \<le> (\<integral>\<^isup>+x. f x * indicator A x)"
   533         using upper_bound[THEN bspec, OF `A \<in> sets M`]
   533         using upper_bound[THEN bspec, OF `A \<in> sets M`]
   534          by (simp add: pextreal_zero_le_diff)
   534          by (simp add: pextreal_zero_le_diff)
   535     qed
   535     qed
   536   qed simp
   536   qed simp
   537 qed
   537 qed
   667 qed
   667 qed
   668 
   668 
   669 lemma (in finite_measure) Radon_Nikodym_finite_measure_infinite:
   669 lemma (in finite_measure) Radon_Nikodym_finite_measure_infinite:
   670   assumes "measure_space M \<nu>"
   670   assumes "measure_space M \<nu>"
   671   assumes "absolutely_continuous \<nu>"
   671   assumes "absolutely_continuous \<nu>"
   672   shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
   672   shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
   673 proof -
   673 proof -
   674   interpret v: measure_space M \<nu> by fact
   674   interpret v: measure_space M \<nu> by fact
   675   from split_space_into_finite_sets_and_rest[OF assms]
   675   from split_space_into_finite_sets_and_rest[OF assms]
   676   obtain Q0 and Q :: "nat \<Rightarrow> 'a set"
   676   obtain Q0 and Q :: "nat \<Rightarrow> 'a set"
   677     where Q: "disjoint_family Q" "range Q \<subseteq> sets M"
   677     where Q: "disjoint_family Q" "range Q \<subseteq> sets M"
   678     and Q0: "Q0 \<in> sets M" "Q0 = space M - (\<Union>i. Q i)"
   678     and Q0: "Q0 \<in> sets M" "Q0 = space M - (\<Union>i. Q i)"
   679     and in_Q0: "\<And>A. A \<in> sets M \<Longrightarrow> A \<subseteq> Q0 \<Longrightarrow> \<mu> A = 0 \<and> \<nu> A = 0 \<or> 0 < \<mu> A \<and> \<nu> A = \<omega>"
   679     and in_Q0: "\<And>A. A \<in> sets M \<Longrightarrow> A \<subseteq> Q0 \<Longrightarrow> \<mu> A = 0 \<and> \<nu> A = 0 \<or> 0 < \<mu> A \<and> \<nu> A = \<omega>"
   680     and Q_fin: "\<And>i. \<nu> (Q i) \<noteq> \<omega>" by force
   680     and Q_fin: "\<And>i. \<nu> (Q i) \<noteq> \<omega>" by force
   681   from Q have Q_sets: "\<And>i. Q i \<in> sets M" by auto
   681   from Q have Q_sets: "\<And>i. Q i \<in> sets M" by auto
   682   have "\<forall>i. \<exists>f. f\<in>borel_measurable M \<and> (\<forall>A\<in>sets M.
   682   have "\<forall>i. \<exists>f. f\<in>borel_measurable M \<and> (\<forall>A\<in>sets M.
   683     \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f x * indicator (Q i \<inter> A) x))"
   683     \<nu> (Q i \<inter> A) = (\<integral>\<^isup>+x. f x * indicator (Q i \<inter> A) x))"
   684   proof
   684   proof
   685     fix i
   685     fix i
   686     have indicator_eq: "\<And>f x A. (f x :: pextreal) * indicator (Q i \<inter> A) x * indicator (Q i) x
   686     have indicator_eq: "\<And>f x A. (f x :: pextreal) * indicator (Q i \<inter> A) x * indicator (Q i) x
   687       = (f x * indicator (Q i) x) * indicator A x"
   687       = (f x * indicator (Q i) x) * indicator A x"
   688       unfolding indicator_def by auto
   688       unfolding indicator_def by auto
   700     have "R.absolutely_continuous \<nu>"
   700     have "R.absolutely_continuous \<nu>"
   701       using `absolutely_continuous \<nu>` `Q i \<in> sets M`
   701       using `absolutely_continuous \<nu>` `Q i \<in> sets M`
   702       by (auto simp: R.absolutely_continuous_def absolutely_continuous_def)
   702       by (auto simp: R.absolutely_continuous_def absolutely_continuous_def)
   703     from finite_measure.Radon_Nikodym_finite_measure[OF fm fmv this]
   703     from finite_measure.Radon_Nikodym_finite_measure[OF fm fmv this]
   704     obtain f where f: "(\<lambda>x. f x * indicator (Q i) x) \<in> borel_measurable M"
   704     obtain f where f: "(\<lambda>x. f x * indicator (Q i) x) \<in> borel_measurable M"
   705       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)"
   705       and f_int: "\<And>A. A\<in>sets M \<Longrightarrow> \<nu> (Q i \<inter> A) = (\<integral>\<^isup>+x. (f x * indicator (Q i) x) * indicator A x)"
   706       unfolding Bex_def borel_measurable_restricted[OF `Q i \<in> sets M`]
   706       unfolding Bex_def borel_measurable_restricted[OF `Q i \<in> sets M`]
   707         positive_integral_restricted[OF `Q i \<in> sets M`] by (auto simp: indicator_eq)
   707         positive_integral_restricted[OF `Q i \<in> sets M`] by (auto simp: indicator_eq)
   708     then show "\<exists>f. f\<in>borel_measurable M \<and> (\<forall>A\<in>sets M.
   708     then show "\<exists>f. f\<in>borel_measurable M \<and> (\<forall>A\<in>sets M.
   709       \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f x * indicator (Q i \<inter> A) x))"
   709       \<nu> (Q i \<inter> A) = (\<integral>\<^isup>+x. f x * indicator (Q i \<inter> A) x))"
   710       by (fastsimp intro!: exI[of _ "\<lambda>x. f x * indicator (Q i) x"] positive_integral_cong
   710       by (fastsimp intro!: exI[of _ "\<lambda>x. f x * indicator (Q i) x"] positive_integral_cong
   711           simp: indicator_def)
   711           simp: indicator_def)
   712   qed
   712   qed
   713   from choice[OF this] obtain f where borel: "\<And>i. f i \<in> borel_measurable M"
   713   from choice[OF this] obtain f where borel: "\<And>i. f i \<in> borel_measurable M"
   714     and f: "\<And>A i. A \<in> sets M \<Longrightarrow>
   714     and f: "\<And>A i. A \<in> sets M \<Longrightarrow>
   715       \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f i x * indicator (Q i \<inter> A) x)"
   715       \<nu> (Q i \<inter> A) = (\<integral>\<^isup>+x. f i x * indicator (Q i \<inter> A) x)"
   716     by auto
   716     by auto
   717   let "?f x" =
   717   let "?f x" =
   718     "(\<Sum>\<^isub>\<infinity> i. f i x * indicator (Q i) x) + \<omega> * indicator Q0 x"
   718     "(\<Sum>\<^isub>\<infinity> i. f i x * indicator (Q i) x) + \<omega> * indicator Q0 x"
   719   show ?thesis
   719   show ?thesis
   720   proof (safe intro!: bexI[of _ ?f])
   720   proof (safe intro!: bexI[of _ ?f])
   726     have *:
   726     have *:
   727       "\<And>x i. indicator A x * (f i x * indicator (Q i) x) =
   727       "\<And>x i. indicator A x * (f i x * indicator (Q i) x) =
   728         f i x * indicator (Q i \<inter> A) x"
   728         f i x * indicator (Q i \<inter> A) x"
   729       "\<And>x i. (indicator A x * indicator Q0 x :: pextreal) =
   729       "\<And>x i. (indicator A x * indicator Q0 x :: pextreal) =
   730         indicator (Q0 \<inter> A) x" by (auto simp: indicator_def)
   730         indicator (Q0 \<inter> A) x" by (auto simp: indicator_def)
   731     have "positive_integral (\<lambda>x. ?f x * indicator A x) =
   731     have "(\<integral>\<^isup>+x. ?f x * indicator A x) =
   732       (\<Sum>\<^isub>\<infinity> i. \<nu> (Q i \<inter> A)) + \<omega> * \<mu> (Q0 \<inter> A)"
   732       (\<Sum>\<^isub>\<infinity> i. \<nu> (Q i \<inter> A)) + \<omega> * \<mu> (Q0 \<inter> A)"
   733       unfolding f[OF `A \<in> sets M`]
   733       unfolding f[OF `A \<in> sets M`]
   734       apply (simp del: pextreal_times(2) add: field_simps *)
   734       apply (simp del: pextreal_times(2) add: field_simps *)
   735       apply (subst positive_integral_add)
   735       apply (subst positive_integral_add)
   736       apply (fastsimp intro: Q0 `A \<in> sets M`)
   736       apply (fastsimp intro: Q0 `A \<in> sets M`)
   753     qed
   753     qed
   754     moreover have "Q0 \<inter> A \<in> sets M" "((\<Union>i. Q i) \<inter> A) \<in> sets M"
   754     moreover have "Q0 \<inter> A \<in> sets M" "((\<Union>i. Q i) \<inter> A) \<in> sets M"
   755       using Q_sets `A \<in> sets M` Q0(1) by (auto intro!: countable_UN)
   755       using Q_sets `A \<in> sets M` Q0(1) by (auto intro!: countable_UN)
   756     moreover have "((\<Union>i. Q i) \<inter> A) \<union> (Q0 \<inter> A) = A" "((\<Union>i. Q i) \<inter> A) \<inter> (Q0 \<inter> A) = {}"
   756     moreover have "((\<Union>i. Q i) \<inter> A) \<union> (Q0 \<inter> A) = A" "((\<Union>i. Q i) \<inter> A) \<inter> (Q0 \<inter> A) = {}"
   757       using `A \<in> sets M` sets_into_space Q0 by auto
   757       using `A \<in> sets M` sets_into_space Q0 by auto
   758     ultimately show "\<nu> A = positive_integral (\<lambda>x. ?f x * indicator A x)"
   758     ultimately show "\<nu> A = (\<integral>\<^isup>+x. ?f x * indicator A x)"
   759       using v.measure_additive[simplified, of "(\<Union>i. Q i) \<inter> A" "Q0 \<inter> A"]
   759       using v.measure_additive[simplified, of "(\<Union>i. Q i) \<inter> A" "Q0 \<inter> A"]
   760       by simp
   760       by simp
   761   qed
   761   qed
   762 qed
   762 qed
   763 
   763 
   764 lemma (in sigma_finite_measure) Radon_Nikodym:
   764 lemma (in sigma_finite_measure) Radon_Nikodym:
   765   assumes "measure_space M \<nu>"
   765   assumes "measure_space M \<nu>"
   766   assumes "absolutely_continuous \<nu>"
   766   assumes "absolutely_continuous \<nu>"
   767   shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
   767   shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
   768 proof -
   768 proof -
   769   from Ex_finite_integrable_function
   769   from Ex_finite_integrable_function
   770   obtain h where finite: "positive_integral h \<noteq> \<omega>" and
   770   obtain h where finite: "positive_integral h \<noteq> \<omega>" and
   771     borel: "h \<in> borel_measurable M" and
   771     borel: "h \<in> borel_measurable M" and
   772     pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x" and
   772     pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x" and
   773     "\<And>x. x \<in> space M \<Longrightarrow> h x < \<omega>" by auto
   773     "\<And>x. x \<in> space M \<Longrightarrow> h x < \<omega>" by auto
   774   let "?T A" = "positive_integral (\<lambda>x. h x * indicator A x)"
   774   let "?T A" = "(\<integral>\<^isup>+x. h x * indicator A x)"
   775   from measure_space_density[OF borel] finite
   775   from measure_space_density[OF borel] finite
   776   interpret T: finite_measure M ?T
   776   interpret T: finite_measure M ?T
   777     unfolding finite_measure_def finite_measure_axioms_def
   777     unfolding finite_measure_def finite_measure_axioms_def
   778     by (simp cong: positive_integral_cong)
   778     by (simp cong: positive_integral_cong)
   779   have "\<And>N. N \<in> sets M \<Longrightarrow> {x \<in> space M. h x \<noteq> 0 \<and> indicator N x \<noteq> (0::pextreal)} = N"
   779   have "\<And>N. N \<in> sets M \<Longrightarrow> {x \<in> space M. h x \<noteq> 0 \<and> indicator N x \<noteq> (0::pextreal)} = N"
   790       using borel f_borel by (auto intro: borel_measurable_pextreal_times)
   790       using borel f_borel by (auto intro: borel_measurable_pextreal_times)
   791     fix A assume "A \<in> sets M"
   791     fix A assume "A \<in> sets M"
   792     then have "(\<lambda>x. f x * indicator A x) \<in> borel_measurable M"
   792     then have "(\<lambda>x. f x * indicator A x) \<in> borel_measurable M"
   793       using f_borel by (auto intro: borel_measurable_pextreal_times borel_measurable_indicator)
   793       using f_borel by (auto intro: borel_measurable_pextreal_times borel_measurable_indicator)
   794     from positive_integral_translated_density[OF borel this]
   794     from positive_integral_translated_density[OF borel this]
   795     show "\<nu> A = positive_integral (\<lambda>x. h x * f x * indicator A x)"
   795     show "\<nu> A = (\<integral>\<^isup>+x. h x * f x * indicator A x)"
   796       unfolding fT[OF `A \<in> sets M`] by (simp add: field_simps)
   796       unfolding fT[OF `A \<in> sets M`] by (simp add: field_simps)
   797   qed
   797   qed
   798 qed
   798 qed
   799 
   799 
   800 section "Uniqueness of densities"
   800 section "Uniqueness of densities"
   801 
   801 
   802 lemma (in measure_space) finite_density_unique:
   802 lemma (in measure_space) finite_density_unique:
   803   assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   803   assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   804   and fin: "positive_integral f < \<omega>"
   804   and fin: "positive_integral f < \<omega>"
   805   shows "(\<forall>A\<in>sets M. positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. g x * indicator A x))
   805   shows "(\<forall>A\<in>sets M. (\<integral>\<^isup>+x. f x * indicator A x) = (\<integral>\<^isup>+x. g x * indicator A x))
   806     \<longleftrightarrow> (AE x. f x = g x)"
   806     \<longleftrightarrow> (AE x. f x = g x)"
   807     (is "(\<forall>A\<in>sets M. ?P f A = ?P g A) \<longleftrightarrow> _")
   807     (is "(\<forall>A\<in>sets M. ?P f A = ?P g A) \<longleftrightarrow> _")
   808 proof (intro iffI ballI)
   808 proof (intro iffI ballI)
   809   fix A assume eq: "AE x. f x = g x"
   809   fix A assume eq: "AE x. f x = g x"
   810   show "?P f A = ?P g A"
   810   show "?P f A = ?P g A"
   815   have g_fin: "positive_integral g < \<omega>" by (simp cong: positive_integral_cong)
   815   have g_fin: "positive_integral g < \<omega>" by (simp cong: positive_integral_cong)
   816   { fix f g assume borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   816   { fix f g assume borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   817       and g_fin: "positive_integral g < \<omega>" and eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
   817       and g_fin: "positive_integral g < \<omega>" and eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
   818     let ?N = "{x\<in>space M. g x < f x}"
   818     let ?N = "{x\<in>space M. g x < f x}"
   819     have N: "?N \<in> sets M" using borel by simp
   819     have N: "?N \<in> sets M" using borel by simp
   820     have "?P (\<lambda>x. (f x - g x)) ?N = positive_integral (\<lambda>x. f x * indicator ?N x - g x * indicator ?N x)"
   820     have "?P (\<lambda>x. (f x - g x)) ?N = (\<integral>\<^isup>+x. f x * indicator ?N x - g x * indicator ?N x)"
   821       by (auto intro!: positive_integral_cong simp: indicator_def)
   821       by (auto intro!: positive_integral_cong simp: indicator_def)
   822     also have "\<dots> = ?P f ?N - ?P g ?N"
   822     also have "\<dots> = ?P f ?N - ?P g ?N"
   823     proof (rule positive_integral_diff)
   823     proof (rule positive_integral_diff)
   824       show "(\<lambda>x. f x * indicator ?N x) \<in> borel_measurable M" "(\<lambda>x. g x * indicator ?N x) \<in> borel_measurable M"
   824       show "(\<lambda>x. f x * indicator ?N x) \<in> borel_measurable M" "(\<lambda>x. g x * indicator ?N x) \<in> borel_measurable M"
   825         using borel N by auto
   825         using borel N by auto
   846     unfolding almost_everywhere_def by auto
   846     unfolding almost_everywhere_def by auto
   847 qed
   847 qed
   848 
   848 
   849 lemma (in finite_measure) density_unique_finite_measure:
   849 lemma (in finite_measure) density_unique_finite_measure:
   850   assumes borel: "f \<in> borel_measurable M" "f' \<in> borel_measurable M"
   850   assumes borel: "f \<in> borel_measurable M" "f' \<in> borel_measurable M"
   851   assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. f' x * indicator A x)"
   851   assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+x. f x * indicator A x) = (\<integral>\<^isup>+x. f' x * indicator A x)"
   852     (is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A")
   852     (is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A")
   853   shows "AE x. f x = f' x"
   853   shows "AE x. f x = f' x"
   854 proof -
   854 proof -
   855   let "?\<nu> A" = "?P f A" and "?\<nu>' A" = "?P f' A"
   855   let "?\<nu> A" = "?P f A" and "?\<nu>' A" = "?P f' A"
   856   let "?f A x" = "f x * indicator A x" and "?f' A x" = "f' x * indicator A x"
   856   let "?f A x" = "f x * indicator A x" and "?f' A x" = "f' x * indicator A x"
   874     by (intro finite_density_unique[THEN iffD1] allI)
   874     by (intro finite_density_unique[THEN iffD1] allI)
   875        (auto intro!: borel_measurable_pextreal_times f Int simp: *)
   875        (auto intro!: borel_measurable_pextreal_times f Int simp: *)
   876   have 2: "AE x. ?f Q0 x = ?f' Q0 x"
   876   have 2: "AE x. ?f Q0 x = ?f' Q0 x"
   877   proof (rule AE_I')
   877   proof (rule AE_I')
   878     { fix f :: "'a \<Rightarrow> pextreal" assume borel: "f \<in> borel_measurable M"
   878     { fix f :: "'a \<Rightarrow> pextreal" assume borel: "f \<in> borel_measurable M"
   879         and eq: "\<And>A. A \<in> sets M \<Longrightarrow> ?\<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
   879         and eq: "\<And>A. A \<in> sets M \<Longrightarrow> ?\<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
   880       let "?A i" = "Q0 \<inter> {x \<in> space M. f x < of_nat i}"
   880       let "?A i" = "Q0 \<inter> {x \<in> space M. f x < of_nat i}"
   881       have "(\<Union>i. ?A i) \<in> null_sets"
   881       have "(\<Union>i. ?A i) \<in> null_sets"
   882       proof (rule null_sets_UN)
   882       proof (rule null_sets_UN)
   883         fix i have "?A i \<in> sets M"
   883         fix i have "?A i \<in> sets M"
   884           using borel Q0(1) by auto
   884           using borel Q0(1) by auto
   885         have "?\<nu> (?A i) \<le> positive_integral (\<lambda>x. of_nat i * indicator (?A i) x)"
   885         have "?\<nu> (?A i) \<le> (\<integral>\<^isup>+x. of_nat i * indicator (?A i) x)"
   886           unfolding eq[OF `?A i \<in> sets M`]
   886           unfolding eq[OF `?A i \<in> sets M`]
   887           by (auto intro!: positive_integral_mono simp: indicator_def)
   887           by (auto intro!: positive_integral_mono simp: indicator_def)
   888         also have "\<dots> = of_nat i * \<mu> (?A i)"
   888         also have "\<dots> = of_nat i * \<mu> (?A i)"
   889           using `?A i \<in> sets M` by (auto intro!: positive_integral_cmult_indicator)
   889           using `?A i \<in> sets M` by (auto intro!: positive_integral_cmult_indicator)
   890         also have "\<dots> < \<omega>"
   890         also have "\<dots> < \<omega>"
   910     by (rule AE_mp) (auto intro!: AE_cong simp: indicator_def)
   910     by (rule AE_mp) (auto intro!: AE_cong simp: indicator_def)
   911 qed
   911 qed
   912 
   912 
   913 lemma (in sigma_finite_measure) density_unique:
   913 lemma (in sigma_finite_measure) density_unique:
   914   assumes borel: "f \<in> borel_measurable M" "f' \<in> borel_measurable M"
   914   assumes borel: "f \<in> borel_measurable M" "f' \<in> borel_measurable M"
   915   assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. f' x * indicator A x)"
   915   assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+x. f x * indicator A x) = (\<integral>\<^isup>+x. f' x * indicator A x)"
   916     (is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A")
   916     (is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A")
   917   shows "AE x. f x = f' x"
   917   shows "AE x. f x = f' x"
   918 proof -
   918 proof -
   919   obtain h where h_borel: "h \<in> borel_measurable M"
   919   obtain h where h_borel: "h \<in> borel_measurable M"
   920     and fin: "positive_integral h \<noteq> \<omega>" and pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<omega>"
   920     and fin: "positive_integral h \<noteq> \<omega>" and pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<omega>"
   921     using Ex_finite_integrable_function by auto
   921     using Ex_finite_integrable_function by auto
   922   interpret h: measure_space M "\<lambda>A. positive_integral (\<lambda>x. h x * indicator A x)"
   922   interpret h: measure_space M "\<lambda>A. (\<integral>\<^isup>+x. h x * indicator A x)"
   923     using h_borel by (rule measure_space_density)
   923     using h_borel by (rule measure_space_density)
   924   interpret h: finite_measure M "\<lambda>A. positive_integral (\<lambda>x. h x * indicator A x)"
   924   interpret h: finite_measure M "\<lambda>A. (\<integral>\<^isup>+x. h x * indicator A x)"
   925     by default (simp cong: positive_integral_cong add: fin)
   925     by default (simp cong: positive_integral_cong add: fin)
   926   interpret f: measure_space M "\<lambda>A. positive_integral (\<lambda>x. f x * indicator A x)"
   926   interpret f: measure_space M "\<lambda>A. (\<integral>\<^isup>+x. f x * indicator A x)"
   927     using borel(1) by (rule measure_space_density)
   927     using borel(1) by (rule measure_space_density)
   928   interpret f': measure_space M "\<lambda>A. positive_integral (\<lambda>x. f' x * indicator A x)"
   928   interpret f': measure_space M "\<lambda>A. (\<integral>\<^isup>+x. f' x * indicator A x)"
   929     using borel(2) by (rule measure_space_density)
   929     using borel(2) by (rule measure_space_density)
   930   { fix A assume "A \<in> sets M"
   930   { fix A assume "A \<in> sets M"
   931     then have " {x \<in> space M. h x \<noteq> 0 \<and> indicator A x \<noteq> (0::pextreal)} = A"
   931     then have " {x \<in> space M. h x \<noteq> 0 \<and> indicator A x \<noteq> (0::pextreal)} = A"
   932       using pos sets_into_space by (force simp: indicator_def)
   932       using pos sets_into_space by (force simp: indicator_def)
   933     then have "positive_integral (\<lambda>xa. h xa * indicator A xa) = 0 \<longleftrightarrow> A \<in> null_sets"
   933     then have "(\<integral>\<^isup>+x. h x * indicator A x) = 0 \<longleftrightarrow> A \<in> null_sets"
   934       using h_borel `A \<in> sets M` by (simp add: positive_integral_0_iff) }
   934       using h_borel `A \<in> sets M` by (simp add: positive_integral_0_iff) }
   935   note h_null_sets = this
   935   note h_null_sets = this
   936   { fix A assume "A \<in> sets M"
   936   { fix A assume "A \<in> sets M"
   937     have "positive_integral (\<lambda>x. h x * (f x * indicator A x)) =
   937     have "(\<integral>\<^isup>+x. h x * (f x * indicator A x)) =
   938       f.positive_integral (\<lambda>x. h x * indicator A x)"
   938       f.positive_integral (\<lambda>x. h x * indicator A x)"
   939       using `A \<in> sets M` h_borel borel
   939       using `A \<in> sets M` h_borel borel
   940       by (simp add: positive_integral_translated_density ac_simps cong: positive_integral_cong)
   940       by (simp add: positive_integral_translated_density ac_simps cong: positive_integral_cong)
   941     also have "\<dots> = f'.positive_integral (\<lambda>x. h x * indicator A x)"
   941     also have "\<dots> = f'.positive_integral (\<lambda>x. h x * indicator A x)"
   942       by (rule f'.positive_integral_cong_measure) (rule f)
   942       by (rule f'.positive_integral_cong_measure) (rule f)
   943     also have "\<dots> = positive_integral (\<lambda>x. h x * (f' x * indicator A x))"
   943     also have "\<dots> = (\<integral>\<^isup>+x. h x * (f' x * indicator A x))"
   944       using `A \<in> sets M` h_borel borel
   944       using `A \<in> sets M` h_borel borel
   945       by (simp add: positive_integral_translated_density ac_simps cong: positive_integral_cong)
   945       by (simp add: positive_integral_translated_density ac_simps cong: positive_integral_cong)
   946     finally have "positive_integral (\<lambda>x. h x * (f x * indicator A x)) = positive_integral (\<lambda>x. h x * (f' x * indicator A x))" . }
   946     finally have "(\<integral>\<^isup>+x. h x * (f x * indicator A x)) = (\<integral>\<^isup>+x. h x * (f' x * indicator A x))" . }
   947   then have "h.almost_everywhere (\<lambda>x. f x = f' x)"
   947   then have "h.almost_everywhere (\<lambda>x. f x = f' x)"
   948     using h_borel borel
   948     using h_borel borel
   949     by (intro h.density_unique_finite_measure[OF borel])
   949     by (intro h.density_unique_finite_measure[OF borel])
   950        (simp add: positive_integral_translated_density)
   950        (simp add: positive_integral_translated_density)
   951   then show "AE x. f x = f' x"
   951   then show "AE x. f x = f' x"
   953     by (auto simp add: h_null_sets)
   953     by (auto simp add: h_null_sets)
   954 qed
   954 qed
   955 
   955 
   956 lemma (in sigma_finite_measure) sigma_finite_iff_density_finite:
   956 lemma (in sigma_finite_measure) sigma_finite_iff_density_finite:
   957   assumes \<nu>: "measure_space M \<nu>" and f: "f \<in> borel_measurable M"
   957   assumes \<nu>: "measure_space M \<nu>" and f: "f \<in> borel_measurable M"
   958     and eq: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
   958     and eq: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
   959   shows "sigma_finite_measure M \<nu> \<longleftrightarrow> (AE x. f x \<noteq> \<omega>)"
   959   shows "sigma_finite_measure M \<nu> \<longleftrightarrow> (AE x. f x \<noteq> \<omega>)"
   960 proof
   960 proof
   961   assume "sigma_finite_measure M \<nu>"
   961   assume "sigma_finite_measure M \<nu>"
   962   then interpret \<nu>: sigma_finite_measure M \<nu> .
   962   then interpret \<nu>: sigma_finite_measure M \<nu> .
   963   from \<nu>.Ex_finite_integrable_function obtain h where
   963   from \<nu>.Ex_finite_integrable_function obtain h where
   964     h: "h \<in> borel_measurable M" "\<nu>.positive_integral h \<noteq> \<omega>"
   964     h: "h \<in> borel_measurable M" "\<nu>.positive_integral h \<noteq> \<omega>"
   965     and fin: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<omega>" by auto
   965     and fin: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<omega>" by auto
   966   have "AE x. f x * h x \<noteq> \<omega>"
   966   have "AE x. f x * h x \<noteq> \<omega>"
   967   proof (rule AE_I')
   967   proof (rule AE_I')
   968     have "\<nu>.positive_integral h = positive_integral (\<lambda>x. f x * h x)"
   968     have "\<nu>.positive_integral h = (\<integral>\<^isup>+x. f x * h x)"
   969       by (simp add: \<nu>.positive_integral_cong_measure[symmetric, OF eq[symmetric]])
   969       by (simp add: \<nu>.positive_integral_cong_measure[symmetric, OF eq[symmetric]])
   970          (intro positive_integral_translated_density f h)
   970          (intro positive_integral_translated_density f h)
   971     then have "positive_integral (\<lambda>x. f x * h x) \<noteq> \<omega>"
   971     then have "(\<integral>\<^isup>+x. f x * h x) \<noteq> \<omega>"
   972       using h(2) by simp
   972       using h(2) by simp
   973     then show "(\<lambda>x. f x * h x) -` {\<omega>} \<inter> space M \<in> null_sets"
   973     then show "(\<lambda>x. f x * h x) -` {\<omega>} \<inter> space M \<in> null_sets"
   974       using f h(1) by (auto intro!: positive_integral_omega borel_measurable_vimage)
   974       using f h(1) by (auto intro!: positive_integral_omega borel_measurable_vimage)
   975   qed auto
   975   qed auto
   976   then show "AE x. f x \<noteq> \<omega>"
   976   then show "AE x. f x \<noteq> \<omega>"
  1016     qed (auto simp: A_def)
  1016     qed (auto simp: A_def)
  1017     finally show "(\<Union>i. ?A i) = space M" by simp
  1017     finally show "(\<Union>i. ?A i) = space M" by simp
  1018   next
  1018   next
  1019     fix n obtain i j where
  1019     fix n obtain i j where
  1020       [simp]: "prod_decode n = (i, j)" by (cases "prod_decode n") auto
  1020       [simp]: "prod_decode n = (i, j)" by (cases "prod_decode n") auto
  1021     have "positive_integral (\<lambda>x. f x * indicator (A i \<inter> Q j) x) \<noteq> \<omega>"
  1021     have "(\<integral>\<^isup>+x. f x * indicator (A i \<inter> Q j) x) \<noteq> \<omega>"
  1022     proof (cases i)
  1022     proof (cases i)
  1023       case 0
  1023       case 0
  1024       have "AE x. f x * indicator (A i \<inter> Q j) x = 0"
  1024       have "AE x. f x * indicator (A i \<inter> Q j) x = 0"
  1025         using AE by (rule AE_mp) (auto intro!: AE_cong simp: A_def `i = 0`)
  1025         using AE by (rule AE_mp) (auto intro!: AE_cong simp: A_def `i = 0`)
  1026       then have "positive_integral (\<lambda>x. f x * indicator (A i \<inter> Q j) x) = 0"
  1026       then have "(\<integral>\<^isup>+x. f x * indicator (A i \<inter> Q j) x) = 0"
  1027         using A_in_sets f
  1027         using A_in_sets f
  1028         apply (subst positive_integral_0_iff)
  1028         apply (subst positive_integral_0_iff)
  1029         apply fast
  1029         apply fast
  1030         apply (subst (asm) AE_iff_null_set)
  1030         apply (subst (asm) AE_iff_null_set)
  1031         apply (intro borel_measurable_pextreal_neq_const)
  1031         apply (intro borel_measurable_pextreal_neq_const)
  1032         apply fast
  1032         apply fast
  1033         by simp
  1033         by simp
  1034       then show ?thesis by simp
  1034       then show ?thesis by simp
  1035     next
  1035     next
  1036       case (Suc n)
  1036       case (Suc n)
  1037       then have "positive_integral (\<lambda>x. f x * indicator (A i \<inter> Q j) x) \<le>
  1037       then have "(\<integral>\<^isup>+x. f x * indicator (A i \<inter> Q j) x) \<le>
  1038         positive_integral (\<lambda>x. of_nat (Suc n) * indicator (Q j) x)"
  1038         (\<integral>\<^isup>+x. of_nat (Suc n) * indicator (Q j) x)"
  1039         by (auto intro!: positive_integral_mono simp: indicator_def A_def)
  1039         by (auto intro!: positive_integral_mono simp: indicator_def A_def)
  1040       also have "\<dots> = of_nat (Suc n) * \<mu> (Q j)"
  1040       also have "\<dots> = of_nat (Suc n) * \<mu> (Q j)"
  1041         using Q by (auto intro!: positive_integral_cmult_indicator)
  1041         using Q by (auto intro!: positive_integral_cmult_indicator)
  1042       also have "\<dots> < \<omega>"
  1042       also have "\<dots> < \<omega>"
  1043         using Q by auto
  1043         using Q by auto
  1050 
  1050 
  1051 section "Radon-Nikodym derivative"
  1051 section "Radon-Nikodym derivative"
  1052 
  1052 
  1053 definition (in sigma_finite_measure)
  1053 definition (in sigma_finite_measure)
  1054   "RN_deriv \<nu> \<equiv> SOME f. f \<in> borel_measurable M \<and>
  1054   "RN_deriv \<nu> \<equiv> SOME f. f \<in> borel_measurable M \<and>
  1055     (\<forall>A \<in> sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x))"
  1055     (\<forall>A \<in> sets M. \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x))"
  1056 
  1056 
  1057 lemma (in sigma_finite_measure) RN_deriv_cong:
  1057 lemma (in sigma_finite_measure) RN_deriv_cong:
  1058   assumes cong: "\<And>A. A \<in> sets M \<Longrightarrow> \<mu>' A = \<mu> A" "\<And>A. A \<in> sets M \<Longrightarrow> \<nu>' A = \<nu> A"
  1058   assumes cong: "\<And>A. A \<in> sets M \<Longrightarrow> \<mu>' A = \<mu> A" "\<And>A. A \<in> sets M \<Longrightarrow> \<nu>' A = \<nu> A"
  1059   shows "sigma_finite_measure.RN_deriv M \<mu>' \<nu>' x = RN_deriv \<nu> x"
  1059   shows "sigma_finite_measure.RN_deriv M \<mu>' \<nu>' x = RN_deriv \<nu> x"
  1060 proof -
  1060 proof -
  1067 
  1067 
  1068 lemma (in sigma_finite_measure) RN_deriv:
  1068 lemma (in sigma_finite_measure) RN_deriv:
  1069   assumes "measure_space M \<nu>"
  1069   assumes "measure_space M \<nu>"
  1070   assumes "absolutely_continuous \<nu>"
  1070   assumes "absolutely_continuous \<nu>"
  1071   shows "RN_deriv \<nu> \<in> borel_measurable M" (is ?borel)
  1071   shows "RN_deriv \<nu> \<in> borel_measurable M" (is ?borel)
  1072   and "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)"
  1072   and "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = (\<integral>\<^isup>+x. RN_deriv \<nu> x * indicator A x)"
  1073     (is "\<And>A. _ \<Longrightarrow> ?int A")
  1073     (is "\<And>A. _ \<Longrightarrow> ?int A")
  1074 proof -
  1074 proof -
  1075   note Ex = Radon_Nikodym[OF assms, unfolded Bex_def]
  1075   note Ex = Radon_Nikodym[OF assms, unfolded Bex_def]
  1076   thus ?borel unfolding RN_deriv_def by (rule someI2_ex) auto
  1076   thus ?borel unfolding RN_deriv_def by (rule someI2_ex) auto
  1077   fix A assume "A \<in> sets M"
  1077   fix A assume "A \<in> sets M"
  1080 qed
  1080 qed
  1081 
  1081 
  1082 lemma (in sigma_finite_measure) RN_deriv_positive_integral:
  1082 lemma (in sigma_finite_measure) RN_deriv_positive_integral:
  1083   assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
  1083   assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
  1084     and f: "f \<in> borel_measurable M"
  1084     and f: "f \<in> borel_measurable M"
  1085   shows "measure_space.positive_integral M \<nu> f = positive_integral (\<lambda>x. RN_deriv \<nu> x * f x)"
  1085   shows "measure_space.positive_integral M \<nu> f = (\<integral>\<^isup>+x. RN_deriv \<nu> x * f x)"
  1086 proof -
  1086 proof -
  1087   interpret \<nu>: measure_space M \<nu> by fact
  1087   interpret \<nu>: measure_space M \<nu> by fact
  1088   have "\<nu>.positive_integral f =
  1088   have "\<nu>.positive_integral f =
  1089     measure_space.positive_integral M (\<lambda>A. positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)) f"
  1089     measure_space.positive_integral M (\<lambda>A. (\<integral>\<^isup>+x. RN_deriv \<nu> x * indicator A x)) f"
  1090     by (intro \<nu>.positive_integral_cong_measure[symmetric] RN_deriv(2)[OF \<nu>, symmetric])
  1090     by (intro \<nu>.positive_integral_cong_measure[symmetric] RN_deriv(2)[OF \<nu>, symmetric])
  1091   also have "\<dots> = positive_integral (\<lambda>x. RN_deriv \<nu> x * f x)"
  1091   also have "\<dots> = (\<integral>\<^isup>+x. RN_deriv \<nu> x * f x)"
  1092     by (intro positive_integral_translated_density RN_deriv[OF \<nu>] f)
  1092     by (intro positive_integral_translated_density RN_deriv[OF \<nu>] f)
  1093   finally show ?thesis .
  1093   finally show ?thesis .
  1094 qed
  1094 qed
  1095 
  1095 
  1096 lemma (in sigma_finite_measure) RN_deriv_unique:
  1096 lemma (in sigma_finite_measure) RN_deriv_unique:
  1097   assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
  1097   assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
  1098   and f: "f \<in> borel_measurable M"
  1098   and f: "f \<in> borel_measurable M"
  1099   and eq: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
  1099   and eq: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
  1100   shows "AE x. f x = RN_deriv \<nu> x"
  1100   shows "AE x. f x = RN_deriv \<nu> x"
  1101 proof (rule density_unique[OF f RN_deriv(1)[OF \<nu>]])
  1101 proof (rule density_unique[OF f RN_deriv(1)[OF \<nu>]])
  1102   fix A assume A: "A \<in> sets M"
  1102   fix A assume A: "A \<in> sets M"
  1103   show "positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)"
  1103   show "(\<integral>\<^isup>+x. f x * indicator A x) = (\<integral>\<^isup>+x. RN_deriv \<nu> x * indicator A x)"
  1104     unfolding eq[OF A, symmetric] RN_deriv(2)[OF \<nu> A, symmetric] ..
  1104     unfolding eq[OF A, symmetric] RN_deriv(2)[OF \<nu> A, symmetric] ..
  1105 qed
  1105 qed
  1106 
  1106 
  1107 lemma (in sigma_finite_measure) RN_deriv_vimage:
  1107 lemma (in sigma_finite_measure) RN_deriv_vimage:
  1108   fixes f :: "'b \<Rightarrow> 'a"
  1108   fixes f :: "'b \<Rightarrow> 'a"
  1128   fix A assume "A \<in> sets M"
  1128   fix A assume "A \<in> sets M"
  1129   then have *: "\<And>x. x \<in> space M \<Longrightarrow> indicator (f -` A \<inter> S) (g x) = (indicator A x :: pextreal)"
  1129   then have *: "\<And>x. x \<in> space M \<Longrightarrow> indicator (f -` A \<inter> S) (g x) = (indicator A x :: pextreal)"
  1130     using f by (auto simp: bij_inv_def indicator_def)
  1130     using f by (auto simp: bij_inv_def indicator_def)
  1131   have "\<nu> (f ` (f -` A \<inter> S)) = sf.positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) x * indicator (f -` A \<inter> S) x)"
  1131   have "\<nu> (f ` (f -` A \<inter> S)) = sf.positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) x * indicator (f -` A \<inter> S) x)"
  1132     using `A \<in> sets M` by (force intro!: sf.RN_deriv(2)[OF \<nu>' ac])
  1132     using `A \<in> sets M` by (force intro!: sf.RN_deriv(2)[OF \<nu>' ac])
  1133   also have "\<dots> = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
  1133   also have "\<dots> = (\<integral>\<^isup>+x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
  1134     unfolding positive_integral_vimage_inv[OF f]
  1134     unfolding positive_integral_vimage_inv[OF f]
  1135     by (simp add: * cong: positive_integral_cong)
  1135     by (simp add: * cong: positive_integral_cong)
  1136   finally show "\<nu> A = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
  1136   finally show "\<nu> A = (\<integral>\<^isup>+x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
  1137     unfolding A_f[OF `A \<in> sets M`] .
  1137     unfolding A_f[OF `A \<in> sets M`] .
  1138 qed
  1138 qed
  1139 
  1139 
  1140 lemma (in sigma_finite_measure) RN_deriv_finite:
  1140 lemma (in sigma_finite_measure) RN_deriv_finite:
  1141   assumes sfm: "sigma_finite_measure M \<nu>" and ac: "absolutely_continuous \<nu>"
  1141   assumes sfm: "sigma_finite_measure M \<nu>" and ac: "absolutely_continuous \<nu>"
  1148 qed
  1148 qed
  1149 
  1149 
  1150 lemma (in sigma_finite_measure)
  1150 lemma (in sigma_finite_measure)
  1151   assumes \<nu>: "sigma_finite_measure M \<nu>" "absolutely_continuous \<nu>"
  1151   assumes \<nu>: "sigma_finite_measure M \<nu>" "absolutely_continuous \<nu>"
  1152     and f: "f \<in> borel_measurable M"
  1152     and f: "f \<in> borel_measurable M"
  1153   shows RN_deriv_integral: "measure_space.integral M \<nu> f = integral (\<lambda>x. real (RN_deriv \<nu> x) * f x)" (is ?integral)
  1153   shows RN_deriv_integral: "measure_space.integral M \<nu> f = (\<integral>x. real (RN_deriv \<nu> x) * f x)" (is ?integral)
  1154     and RN_deriv_integrable: "measure_space.integrable M \<nu> f \<longleftrightarrow> integrable (\<lambda>x. real (RN_deriv \<nu> x) * f x)" (is ?integrable)
  1154     and RN_deriv_integrable: "measure_space.integrable M \<nu> f \<longleftrightarrow> integrable (\<lambda>x. real (RN_deriv \<nu> x) * f x)" (is ?integrable)
  1155 proof -
  1155 proof -
  1156   interpret \<nu>: sigma_finite_measure M \<nu> by fact
  1156   interpret \<nu>: sigma_finite_measure M \<nu> by fact
  1157   have ms: "measure_space M \<nu>" by default
  1157   have ms: "measure_space M \<nu>" by default
  1158   have minus_cong: "\<And>A B A' B'::pextreal. A = A' \<Longrightarrow> B = B' \<Longrightarrow> real A - real B = real A' - real B'" by simp
  1158   have minus_cong: "\<And>A B A' B'::pextreal. A = A' \<Longrightarrow> B = B' \<Longrightarrow> real A - real B = real A' - real B'" by simp
  1162       have "Real (real (RN_deriv \<nu> x)) * Real (f x) = Real (real (RN_deriv \<nu> x) * f x)"
  1162       have "Real (real (RN_deriv \<nu> x)) * Real (f x) = Real (real (RN_deriv \<nu> x) * f x)"
  1163         by (simp add: mult_le_0_iff)
  1163         by (simp add: mult_le_0_iff)
  1164       then have "RN_deriv \<nu> x * Real (f x) = Real (real (RN_deriv \<nu> x) * f x)"
  1164       then have "RN_deriv \<nu> x * Real (f x) = Real (real (RN_deriv \<nu> x) * f x)"
  1165         using * by (simp add: Real_real) }
  1165         using * by (simp add: Real_real) }
  1166     note * = this
  1166     note * = this
  1167     have "positive_integral (\<lambda>x. RN_deriv \<nu> x * Real (f x)) = positive_integral (\<lambda>x. Real (real (RN_deriv \<nu> x) * f x))"
  1167     have "(\<integral>\<^isup>+x. RN_deriv \<nu> x * Real (f x)) = (\<integral>\<^isup>+x. Real (real (RN_deriv \<nu> x) * f x))"
  1168       apply (rule positive_integral_cong_AE)
  1168       apply (rule positive_integral_cong_AE)
  1169       apply (rule AE_mp[OF RN_deriv_finite[OF \<nu>]])
  1169       apply (rule AE_mp[OF RN_deriv_finite[OF \<nu>]])
  1170       by (auto intro!: AE_cong simp: *) }
  1170       by (auto intro!: AE_cong simp: *) }
  1171   with this[OF f] this[OF f'] f f'
  1171   with this[OF f] this[OF f'] f f'
  1172   show ?integral ?integrable
  1172   show ?integral ?integrable
  1180   and "{x} \<in> sets M"
  1180   and "{x} \<in> sets M"
  1181   shows "\<nu> {x} = RN_deriv \<nu> x * \<mu> {x}"
  1181   shows "\<nu> {x} = RN_deriv \<nu> x * \<mu> {x}"
  1182 proof -
  1182 proof -
  1183   note deriv = RN_deriv[OF assms(1, 2)]
  1183   note deriv = RN_deriv[OF assms(1, 2)]
  1184   from deriv(2)[OF `{x} \<in> sets M`]
  1184   from deriv(2)[OF `{x} \<in> sets M`]
  1185   have "\<nu> {x} = positive_integral (\<lambda>w. RN_deriv \<nu> x * indicator {x} w)"
  1185   have "\<nu> {x} = (\<integral>\<^isup>+w. RN_deriv \<nu> x * indicator {x} w)"
  1186     by (auto simp: indicator_def intro!: positive_integral_cong)
  1186     by (auto simp: indicator_def intro!: positive_integral_cong)
  1187   thus ?thesis using positive_integral_cmult_indicator[OF `{x} \<in> sets M`]
  1187   thus ?thesis using positive_integral_cmult_indicator[OF `{x} \<in> sets M`]
  1188     by auto
  1188     by auto
  1189 qed
  1189 qed
  1190 
  1190