changeset 41544 c3b977fee8a3 parent 41097 a1abfa4e2b44 child 41661 baf1964bc468
equal 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 `