Support product spaces on sigma finite measures.
Introduce the almost everywhere quantifier.
Introduce 'morphism' theorems for most constants.
Prove uniqueness of measures on cut stable generators.
Prove uniqueness of the Radon-Nikodym derivative.
Removed misleading suffix from borel_space and lebesgue_space.
Use product spaces to introduce Fubini on the Lebesgue integral.
Combine Euclidean_Lebesgue and Lebesgue_Measure.
Generalize theorems about mutual information and entropy to arbitrary probability spaces.
Remove simproc mult_log as it does not work with interpretations.
Introduce completion of measure spaces.
Change type of sigma.
Introduce dynkin systems.
theory Radon_Nikodym
imports Lebesgue_Integration
begin
lemma less_\<omega>_Ex_of_nat: "x < \<omega> \<longleftrightarrow> (\<exists>n. x < of_nat n)"
proof safe
assume "x < \<omega>"
then obtain r where "0 \<le> r" "x = Real r" by (cases x) auto
moreover obtain n where "r < of_nat n" using ex_less_of_nat by auto
ultimately show "\<exists>n. x < of_nat n" by (auto simp: real_eq_of_nat)
qed auto
lemma (in sigma_finite_measure) Ex_finite_integrable_function:
shows "\<exists>h\<in>borel_measurable M. positive_integral h \<noteq> \<omega> \<and> (\<forall>x\<in>space M. 0 < h x \<and> h x < \<omega>)"
proof -
obtain A :: "nat \<Rightarrow> 'a set" where
range: "range A \<subseteq> sets M" and
space: "(\<Union>i. A i) = space M" and
measure: "\<And>i. \<mu> (A i) \<noteq> \<omega>" and
disjoint: "disjoint_family A"
using disjoint_sigma_finite by auto
let "?B i" = "2^Suc i * \<mu> (A i)"
have "\<forall>i. \<exists>x. 0 < x \<and> x < inverse (?B i)"
proof
fix i show "\<exists>x. 0 < x \<and> x < inverse (?B i)"
proof cases
assume "\<mu> (A i) = 0"
then show ?thesis by (auto intro!: exI[of _ 1])
next
assume not_0: "\<mu> (A i) \<noteq> 0"
then have "?B i \<noteq> \<omega>" using measure[of i] by auto
then have "inverse (?B i) \<noteq> 0" unfolding pinfreal_inverse_eq_0 by simp
then show ?thesis using measure[of i] not_0
by (auto intro!: exI[of _ "inverse (?B i) / 2"]
simp: pinfreal_noteq_omega_Ex zero_le_mult_iff zero_less_mult_iff mult_le_0_iff power_le_zero_eq)
qed
qed
from choice[OF this] obtain n where n: "\<And>i. 0 < n i"
"\<And>i. n i < inverse (2^Suc i * \<mu> (A i))" by auto
let "?h x" = "\<Sum>\<^isub>\<infinity> i. n i * indicator (A i) x"
show ?thesis
proof (safe intro!: bexI[of _ ?h] del: notI)
have "\<And>i. A i \<in> sets M"
using range by fastsimp+
then have "positive_integral ?h = (\<Sum>\<^isub>\<infinity> i. n i * \<mu> (A i))"
by (simp add: positive_integral_psuminf positive_integral_cmult_indicator)
also have "\<dots> \<le> (\<Sum>\<^isub>\<infinity> i. Real ((1 / 2)^Suc i))"
proof (rule psuminf_le)
fix N show "n N * \<mu> (A N) \<le> Real ((1 / 2) ^ Suc N)"
using measure[of N] n[of N]
by (cases "n N")
(auto simp: pinfreal_noteq_omega_Ex field_simps zero_le_mult_iff
mult_le_0_iff mult_less_0_iff power_less_zero_eq
power_le_zero_eq inverse_eq_divide less_divide_eq
power_divide split: split_if_asm)
qed
also have "\<dots> = Real 1"
by (rule suminf_imp_psuminf, rule power_half_series, auto)
finally show "positive_integral ?h \<noteq> \<omega>" by auto
next
fix x assume "x \<in> space M"
then obtain i where "x \<in> A i" using space[symmetric] by auto
from psuminf_cmult_indicator[OF disjoint, OF this]
have "?h x = n i" by simp
then show "0 < ?h x" and "?h x < \<omega>" using n[of i] by auto
next
show "?h \<in> borel_measurable M" using range
by (auto intro!: borel_measurable_psuminf borel_measurable_pinfreal_times)
qed
qed
definition (in measure_space)
"absolutely_continuous \<nu> = (\<forall>N\<in>null_sets. \<nu> N = (0 :: pinfreal))"
lemma (in sigma_finite_measure) absolutely_continuous_AE:
assumes "measure_space M \<nu>" "absolutely_continuous \<nu>" "AE x. P x"
shows "measure_space.almost_everywhere M \<nu> P"
proof -
interpret \<nu>: measure_space M \<nu> by fact
from `AE x. P x` obtain N where N: "N \<in> null_sets" and "{x\<in>space M. \<not> P x} \<subseteq> N"
unfolding almost_everywhere_def by auto
show "\<nu>.almost_everywhere P"
proof (rule \<nu>.AE_I')
show "{x\<in>space M. \<not> P x} \<subseteq> N" by fact
from `absolutely_continuous \<nu>` show "N \<in> \<nu>.null_sets"
using N unfolding absolutely_continuous_def by auto
qed
qed
lemma (in finite_measure_space) absolutely_continuousI:
assumes "finite_measure_space M \<nu>"
assumes v: "\<And>x. \<lbrakk> x \<in> space M ; \<mu> {x} = 0 \<rbrakk> \<Longrightarrow> \<nu> {x} = 0"
shows "absolutely_continuous \<nu>"
proof (unfold absolutely_continuous_def sets_eq_Pow, safe)
fix N assume "\<mu> N = 0" "N \<subseteq> space M"
interpret v: finite_measure_space M \<nu> by fact
have "\<nu> N = \<nu> (\<Union>x\<in>N. {x})" by simp
also have "\<dots> = (\<Sum>x\<in>N. \<nu> {x})"
proof (rule v.measure_finitely_additive''[symmetric])
show "finite N" using `N \<subseteq> space M` finite_space by (auto intro: finite_subset)
show "disjoint_family_on (\<lambda>i. {i}) N" unfolding disjoint_family_on_def by auto
fix x assume "x \<in> N" thus "{x} \<in> sets M" using `N \<subseteq> space M` sets_eq_Pow by auto
qed
also have "\<dots> = 0"
proof (safe intro!: setsum_0')
fix x assume "x \<in> N"
hence "\<mu> {x} \<le> \<mu> N" using sets_eq_Pow `N \<subseteq> space M` by (auto intro!: measure_mono)
hence "\<mu> {x} = 0" using `\<mu> N = 0` by simp
thus "\<nu> {x} = 0" using v[of x] `x \<in> N` `N \<subseteq> space M` by auto
qed
finally show "\<nu> N = 0" .
qed
lemma (in finite_measure) Radon_Nikodym_aux_epsilon:
fixes e :: real assumes "0 < e"
assumes "finite_measure M s"
shows "\<exists>A\<in>sets M. real (\<mu> (space M)) - real (s (space M)) \<le>
real (\<mu> A) - real (s A) \<and>
(\<forall>B\<in>sets M. B \<subseteq> A \<longrightarrow> - e < real (\<mu> B) - real (s B))"
proof -
let "?d A" = "real (\<mu> A) - real (s A)"
interpret M': finite_measure M s by fact
let "?A A" = "if (\<forall>B\<in>sets M. B \<subseteq> space M - A \<longrightarrow> -e < ?d B)
then {}
else (SOME B. B \<in> sets M \<and> B \<subseteq> space M - A \<and> ?d B \<le> -e)"
def A \<equiv> "\<lambda>n. ((\<lambda>B. B \<union> ?A B) ^^ n) {}"
have A_simps[simp]:
"A 0 = {}"
"\<And>n. A (Suc n) = (A n \<union> ?A (A n))" unfolding A_def by simp_all
{ fix A assume "A \<in> sets M"
have "?A A \<in> sets M"
by (auto intro!: someI2[of _ _ "\<lambda>A. A \<in> sets M"] simp: not_less) }
note A'_in_sets = this
{ fix n have "A n \<in> sets M"
proof (induct n)
case (Suc n) thus "A (Suc n) \<in> sets M"
using A'_in_sets[of "A n"] by (auto split: split_if_asm)
qed (simp add: A_def) }
note A_in_sets = this
hence "range A \<subseteq> sets M" by auto
{ fix n B
assume Ex: "\<exists>B. B \<in> sets M \<and> B \<subseteq> space M - A n \<and> ?d B \<le> -e"
hence False: "\<not> (\<forall>B\<in>sets M. B \<subseteq> space M - A n \<longrightarrow> -e < ?d B)" by (auto simp: not_less)
have "?d (A (Suc n)) \<le> ?d (A n) - e" unfolding A_simps if_not_P[OF False]
proof (rule someI2_ex[OF Ex])
fix B assume "B \<in> sets M \<and> B \<subseteq> space M - A n \<and> ?d B \<le> - e"
hence "A n \<inter> B = {}" "B \<in> sets M" and dB: "?d B \<le> -e" by auto
hence "?d (A n \<union> B) = ?d (A n) + ?d B"
using `A n \<in> sets M` real_finite_measure_Union M'.real_finite_measure_Union by simp
also have "\<dots> \<le> ?d (A n) - e" using dB by simp
finally show "?d (A n \<union> B) \<le> ?d (A n) - e" .
qed }
note dA_epsilon = this
{ fix n have "?d (A (Suc n)) \<le> ?d (A n)"
proof (cases "\<exists>B. B\<in>sets M \<and> B \<subseteq> space M - A n \<and> ?d B \<le> - e")
case True from dA_epsilon[OF this] show ?thesis using `0 < e` by simp
next
case False
hence "\<forall>B\<in>sets M. B \<subseteq> space M - A n \<longrightarrow> -e < ?d B" by (auto simp: not_le)
thus ?thesis by simp
qed }
note dA_mono = this
show ?thesis
proof (cases "\<exists>n. \<forall>B\<in>sets M. B \<subseteq> space M - A n \<longrightarrow> -e < ?d B")
case True then obtain n where B: "\<And>B. \<lbrakk> B \<in> sets M; B \<subseteq> space M - A n\<rbrakk> \<Longrightarrow> -e < ?d B" by blast
show ?thesis
proof (safe intro!: bexI[of _ "space M - A n"])
fix B assume "B \<in> sets M" "B \<subseteq> space M - A n"
from B[OF this] show "-e < ?d B" .
next
show "space M - A n \<in> sets M" by (rule compl_sets) fact
next
show "?d (space M) \<le> ?d (space M - A n)"
proof (induct n)
fix n assume "?d (space M) \<le> ?d (space M - A n)"
also have "\<dots> \<le> ?d (space M - A (Suc n))"
using A_in_sets sets_into_space dA_mono[of n]
real_finite_measure_Diff[of "space M"]
real_finite_measure_Diff[of "space M"]
M'.real_finite_measure_Diff[of "space M"]
M'.real_finite_measure_Diff[of "space M"]
by (simp del: A_simps)
finally show "?d (space M) \<le> ?d (space M - A (Suc n))" .
qed simp
qed
next
case False hence B: "\<And>n. \<exists>B. B\<in>sets M \<and> B \<subseteq> space M - A n \<and> ?d B \<le> - e"
by (auto simp add: not_less)
{ fix n have "?d (A n) \<le> - real n * e"
proof (induct n)
case (Suc n) with dA_epsilon[of n, OF B] show ?case by (simp del: A_simps add: real_of_nat_Suc field_simps)
qed simp } note dA_less = this
have decseq: "decseq (\<lambda>n. ?d (A n))" unfolding decseq_eq_incseq
proof (rule incseq_SucI)
fix n show "- ?d (A n) \<le> - ?d (A (Suc n))" using dA_mono[of n] by auto
qed
from real_finite_continuity_from_below[of A] `range A \<subseteq> sets M`
M'.real_finite_continuity_from_below[of A]
have convergent: "(\<lambda>i. ?d (A i)) ----> ?d (\<Union>i. A i)"
by (auto intro!: LIMSEQ_diff)
obtain n :: nat where "- ?d (\<Union>i. A i) / e < real n" using reals_Archimedean2 by auto
moreover from order_trans[OF decseq_le[OF decseq convergent] dA_less]
have "real n \<le> - ?d (\<Union>i. A i) / e" using `0<e` by (simp add: field_simps)
ultimately show ?thesis by auto
qed
qed
lemma (in finite_measure) Radon_Nikodym_aux:
assumes "finite_measure M s"
shows "\<exists>A\<in>sets M. real (\<mu> (space M)) - real (s (space M)) \<le>
real (\<mu> A) - real (s A) \<and>
(\<forall>B\<in>sets M. B \<subseteq> A \<longrightarrow> 0 \<le> real (\<mu> B) - real (s B))"
proof -
let "?d A" = "real (\<mu> A) - real (s A)"
let "?P A B n" = "A \<in> sets M \<and> A \<subseteq> B \<and> ?d B \<le> ?d A \<and> (\<forall>C\<in>sets M. C \<subseteq> A \<longrightarrow> - 1 / real (Suc n) < ?d C)"
interpret M': finite_measure M s by fact
let "?r S" = "restricted_space S"
{ fix S n
assume S: "S \<in> sets M"
hence **: "\<And>X. X \<in> op \<inter> S ` sets M \<longleftrightarrow> X \<in> sets M \<and> X \<subseteq> S" by auto
from M'.restricted_finite_measure[of S] restricted_finite_measure[of S] S
have "finite_measure (?r S) \<mu>" "0 < 1 / real (Suc n)"
"finite_measure (?r S) s" by auto
from finite_measure.Radon_Nikodym_aux_epsilon[OF this] guess X ..
hence "?P X S n"
proof (simp add: **, safe)
fix C assume C: "C \<in> sets M" "C \<subseteq> X" "X \<subseteq> S" and
*: "\<forall>B\<in>sets M. S \<inter> B \<subseteq> X \<longrightarrow> - (1 / real (Suc n)) < ?d (S \<inter> B)"
hence "C \<subseteq> S" "C \<subseteq> X" "S \<inter> C = C" by auto
with *[THEN bspec, OF `C \<in> sets M`]
show "- (1 / real (Suc n)) < ?d C" by auto
qed
hence "\<exists>A. ?P A S n" by auto }
note Ex_P = this
def A \<equiv> "nat_rec (space M) (\<lambda>n A. SOME B. ?P B A n)"
have A_Suc: "\<And>n. A (Suc n) = (SOME B. ?P B (A n) n)" by (simp add: A_def)
have A_0[simp]: "A 0 = space M" unfolding A_def by simp
{ fix i have "A i \<in> sets M" unfolding A_def
proof (induct i)
case (Suc i)
from Ex_P[OF this, of i] show ?case unfolding nat_rec_Suc
by (rule someI2_ex) simp
qed simp }
note A_in_sets = this
{ fix n have "?P (A (Suc n)) (A n) n"
using Ex_P[OF A_in_sets] unfolding A_Suc
by (rule someI2_ex) simp }
note P_A = this
have "range A \<subseteq> sets M" using A_in_sets by auto
have A_mono: "\<And>i. A (Suc i) \<subseteq> A i" using P_A by simp
have mono_dA: "mono (\<lambda>i. ?d (A i))" using P_A by (simp add: mono_iff_le_Suc)
have epsilon: "\<And>C i. \<lbrakk> C \<in> sets M; C \<subseteq> A (Suc i) \<rbrakk> \<Longrightarrow> - 1 / real (Suc i) < ?d C"
using P_A by auto
show ?thesis
proof (safe intro!: bexI[of _ "\<Inter>i. A i"])
show "(\<Inter>i. A i) \<in> sets M" using A_in_sets by auto
from `range A \<subseteq> sets M` A_mono
real_finite_continuity_from_above[of A]
M'.real_finite_continuity_from_above[of A]
have "(\<lambda>i. ?d (A i)) ----> ?d (\<Inter>i. A i)" by (auto intro!: LIMSEQ_diff)
thus "?d (space M) \<le> ?d (\<Inter>i. A i)" using mono_dA[THEN monoD, of 0 _]
by (rule_tac LIMSEQ_le_const) (auto intro!: exI)
next
fix B assume B: "B \<in> sets M" "B \<subseteq> (\<Inter>i. A i)"
show "0 \<le> ?d B"
proof (rule ccontr)
assume "\<not> 0 \<le> ?d B"
hence "0 < - ?d B" by auto
from ex_inverse_of_nat_Suc_less[OF this]
obtain n where *: "?d B < - 1 / real (Suc n)"
by (auto simp: real_eq_of_nat inverse_eq_divide field_simps)
have "B \<subseteq> A (Suc n)" using B by (auto simp del: nat_rec_Suc)
from epsilon[OF B(1) this] *
show False by auto
qed
qed
qed
lemma (in finite_measure) Radon_Nikodym_finite_measure:
assumes "finite_measure M \<nu>"
assumes "absolutely_continuous \<nu>"
shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
proof -
interpret M': finite_measure M \<nu> using assms(1) .
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}"
have "(\<lambda>x. 0) \<in> G" unfolding G_def by auto
hence "G \<noteq> {}" by auto
{ fix f g assume f: "f \<in> G" and g: "g \<in> G"
have "(\<lambda>x. max (g x) (f x)) \<in> G" (is "?max \<in> G") unfolding G_def
proof safe
show "?max \<in> borel_measurable M" using f g unfolding G_def by auto
let ?A = "{x \<in> space M. f x \<le> g x}"
have "?A \<in> sets M" using f g unfolding G_def by auto
fix A assume "A \<in> sets M"
hence sets: "?A \<inter> A \<in> sets M" "(space M - ?A) \<inter> A \<in> sets M" using `?A \<in> sets M` by auto
have union: "((?A \<inter> A) \<union> ((space M - ?A) \<inter> A)) = A"
using sets_into_space[OF `A \<in> sets M`] by auto
have "\<And>x. x \<in> space M \<Longrightarrow> max (g x) (f x) * indicator A x =
g x * indicator (?A \<inter> A) x + f x * indicator ((space M - ?A) \<inter> A) x"
by (auto simp: indicator_def max_def)
hence "positive_integral (\<lambda>x. max (g x) (f x) * indicator A x) =
positive_integral (\<lambda>x. g x * indicator (?A \<inter> A) x) +
positive_integral (\<lambda>x. f x * indicator ((space M - ?A) \<inter> A) x)"
using f g sets unfolding G_def
by (auto cong: positive_integral_cong intro!: positive_integral_add borel_measurable_indicator)
also have "\<dots> \<le> \<nu> (?A \<inter> A) + \<nu> ((space M - ?A) \<inter> A)"
using f g sets unfolding G_def by (auto intro!: add_mono)
also have "\<dots> = \<nu> A"
using M'.measure_additive[OF sets] union by auto
finally show "positive_integral (\<lambda>x. max (g x) (f x) * indicator A x) \<le> \<nu> A" .
qed }
note max_in_G = this
{ fix f g assume "f \<up> g" and f: "\<And>i. f i \<in> G"
have "g \<in> G" unfolding G_def
proof safe
from `f \<up> g` have [simp]: "g = (SUP i. f i)" unfolding isoton_def by simp
have f_borel: "\<And>i. f i \<in> borel_measurable M" using f unfolding G_def by simp
thus "g \<in> borel_measurable M" by (auto intro!: borel_measurable_SUP)
fix A assume "A \<in> sets M"
hence "\<And>i. (\<lambda>x. f i x * indicator A x) \<in> borel_measurable M"
using f_borel by (auto intro!: borel_measurable_indicator)
from positive_integral_isoton[OF isoton_indicator[OF `f \<up> g`] this]
have SUP: "positive_integral (\<lambda>x. g x * indicator A x) =
(SUP i. positive_integral (\<lambda>x. f i x * indicator A x))"
unfolding isoton_def by simp
show "positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A" unfolding SUP
using f `A \<in> sets M` unfolding G_def by (auto intro!: SUP_leI)
qed }
note SUP_in_G = this
let ?y = "SUP g : G. positive_integral g"
have "?y \<le> \<nu> (space M)" unfolding G_def
proof (safe intro!: SUP_leI)
fix g assume "\<forall>A\<in>sets M. positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A"
from this[THEN bspec, OF top] show "positive_integral g \<le> \<nu> (space M)"
by (simp cong: positive_integral_cong)
qed
hence "?y \<noteq> \<omega>" using M'.finite_measure_of_space by auto
from SUPR_countable_SUPR[OF this `G \<noteq> {}`] guess ys .. note ys = this
hence "\<forall>n. \<exists>g. g\<in>G \<and> positive_integral g = ys n"
proof safe
fix n assume "range ys \<subseteq> positive_integral ` G"
hence "ys n \<in> positive_integral ` G" by auto
thus "\<exists>g. g\<in>G \<and> positive_integral g = ys n" by auto
qed
from choice[OF this] obtain gs where "\<And>i. gs i \<in> G" "\<And>n. positive_integral (gs n) = ys n" by auto
hence y_eq: "?y = (SUP i. positive_integral (gs i))" using ys by auto
let "?g i x" = "Max ((\<lambda>n. gs n x) ` {..i})"
def f \<equiv> "SUP i. ?g i"
have gs_not_empty: "\<And>i. (\<lambda>n. gs n x) ` {..i} \<noteq> {}" by auto
{ fix i have "?g i \<in> G"
proof (induct i)
case 0 thus ?case by simp fact
next
case (Suc i)
with Suc gs_not_empty `gs (Suc i) \<in> G` show ?case
by (auto simp add: atMost_Suc intro!: max_in_G)
qed }
note g_in_G = this
have "\<And>x. \<forall>i. ?g i x \<le> ?g (Suc i) x"
using gs_not_empty by (simp add: atMost_Suc)
hence isoton_g: "?g \<up> f" by (simp add: isoton_def le_fun_def f_def)
from SUP_in_G[OF this g_in_G] have "f \<in> G" .
hence [simp, intro]: "f \<in> borel_measurable M" unfolding G_def by auto
have "(\<lambda>i. positive_integral (?g i)) \<up> positive_integral f"
using isoton_g g_in_G by (auto intro!: positive_integral_isoton simp: G_def f_def)
hence "positive_integral f = (SUP i. positive_integral (?g i))"
unfolding isoton_def by simp
also have "\<dots> = ?y"
proof (rule antisym)
show "(SUP i. positive_integral (?g i)) \<le> ?y"
using g_in_G by (auto intro!: exI Sup_mono simp: SUPR_def)
show "?y \<le> (SUP i. positive_integral (?g i))" unfolding y_eq
by (auto intro!: SUP_mono positive_integral_mono Max_ge)
qed
finally have int_f_eq_y: "positive_integral f = ?y" .
let "?t A" = "\<nu> A - positive_integral (\<lambda>x. f x * indicator A x)"
have "finite_measure M ?t"
proof
show "?t {} = 0" by simp
show "?t (space M) \<noteq> \<omega>" using M'.finite_measure by simp
show "countably_additive M ?t" unfolding countably_additive_def
proof safe
fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets M" "disjoint_family A"
have "(\<Sum>\<^isub>\<infinity> n. positive_integral (\<lambda>x. f x * indicator (A n) x))
= positive_integral (\<lambda>x. (\<Sum>\<^isub>\<infinity>n. f x * indicator (A n) x))"
using `range A \<subseteq> sets M`
by (rule_tac positive_integral_psuminf[symmetric]) (auto intro!: borel_measurable_indicator)
also have "\<dots> = positive_integral (\<lambda>x. f x * indicator (\<Union>n. A n) x)"
apply (rule positive_integral_cong)
apply (subst psuminf_cmult_right)
unfolding psuminf_indicator[OF `disjoint_family A`] ..
finally have "(\<Sum>\<^isub>\<infinity> n. positive_integral (\<lambda>x. f x * indicator (A n) x))
= positive_integral (\<lambda>x. f x * indicator (\<Union>n. A n) x)" .
moreover have "(\<Sum>\<^isub>\<infinity>n. \<nu> (A n)) = \<nu> (\<Union>n. A n)"
using M'.measure_countably_additive A by (simp add: comp_def)
moreover have "\<And>i. positive_integral (\<lambda>x. f x * indicator (A i) x) \<le> \<nu> (A i)"
using A `f \<in> G` unfolding G_def by auto
moreover have v_fin: "\<nu> (\<Union>i. A i) \<noteq> \<omega>" using M'.finite_measure A by (simp add: countable_UN)
moreover {
have "positive_integral (\<lambda>x. f x * indicator (\<Union>i. A i) x) \<le> \<nu> (\<Union>i. A i)"
using A `f \<in> G` unfolding G_def by (auto simp: countable_UN)
also have "\<nu> (\<Union>i. A i) < \<omega>" using v_fin by (simp add: pinfreal_less_\<omega>)
finally have "positive_integral (\<lambda>x. f x * indicator (\<Union>i. A i) x) \<noteq> \<omega>"
by (simp add: pinfreal_less_\<omega>) }
ultimately
show "(\<Sum>\<^isub>\<infinity> n. ?t (A n)) = ?t (\<Union>i. A i)"
apply (subst psuminf_minus) by simp_all
qed
qed
then interpret M: finite_measure M ?t .
have ac: "absolutely_continuous ?t" using `absolutely_continuous \<nu>` unfolding absolutely_continuous_def by auto
have upper_bound: "\<forall>A\<in>sets M. ?t A \<le> 0"
proof (rule ccontr)
assume "\<not> ?thesis"
then obtain A where A: "A \<in> sets M" and pos: "0 < ?t A"
by (auto simp: not_le)
note pos
also have "?t A \<le> ?t (space M)"
using M.measure_mono[of A "space M"] A sets_into_space by simp
finally have pos_t: "0 < ?t (space M)" by simp
moreover
hence pos_M: "0 < \<mu> (space M)"
using ac top unfolding absolutely_continuous_def by auto
moreover
have "positive_integral (\<lambda>x. f x * indicator (space M) x) \<le> \<nu> (space M)"
using `f \<in> G` unfolding G_def by auto
hence "positive_integral (\<lambda>x. f x * indicator (space M) x) \<noteq> \<omega>"
using M'.finite_measure_of_space by auto
moreover
def b \<equiv> "?t (space M) / \<mu> (space M) / 2"
ultimately have b: "b \<noteq> 0" "b \<noteq> \<omega>"
using M'.finite_measure_of_space
by (auto simp: pinfreal_inverse_eq_0 finite_measure_of_space)
have "finite_measure M (\<lambda>A. b * \<mu> A)" (is "finite_measure M ?b")
proof
show "?b {} = 0" by simp
show "?b (space M) \<noteq> \<omega>" using finite_measure_of_space b by auto
show "countably_additive M ?b"
unfolding countably_additive_def psuminf_cmult_right
using measure_countably_additive by auto
qed
from M.Radon_Nikodym_aux[OF this]
obtain A0 where "A0 \<in> sets M" and
space_less_A0: "real (?t (space M)) - real (b * \<mu> (space M)) \<le> real (?t A0) - real (b * \<mu> A0)" and
*: "\<And>B. \<lbrakk> B \<in> sets M ; B \<subseteq> A0 \<rbrakk> \<Longrightarrow> 0 \<le> real (?t B) - real (b * \<mu> B)" by auto
{ fix B assume "B \<in> sets M" "B \<subseteq> A0"
with *[OF this] have "b * \<mu> B \<le> ?t B"
using M'.finite_measure b finite_measure
by (cases "b * \<mu> B", cases "?t B") (auto simp: field_simps) }
note bM_le_t = this
let "?f0 x" = "f x + b * indicator A0 x"
{ fix A assume A: "A \<in> sets M"
hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
have "positive_integral (\<lambda>x. ?f0 x * indicator A x) =
positive_integral (\<lambda>x. f x * indicator A x + b * indicator (A \<inter> A0) x)"
by (auto intro!: positive_integral_cong simp: field_simps indicator_inter_arith)
hence "positive_integral (\<lambda>x. ?f0 x * indicator A x) =
positive_integral (\<lambda>x. f x * indicator A x) + b * \<mu> (A \<inter> A0)"
using `A0 \<in> sets M` `A \<inter> A0 \<in> sets M` A
by (simp add: borel_measurable_indicator positive_integral_add positive_integral_cmult_indicator) }
note f0_eq = this
{ fix A assume A: "A \<in> sets M"
hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
have f_le_v: "positive_integral (\<lambda>x. f x * indicator A x) \<le> \<nu> A"
using `f \<in> G` A unfolding G_def by auto
note f0_eq[OF A]
also have "positive_integral (\<lambda>x. f x * indicator A x) + b * \<mu> (A \<inter> A0) \<le>
positive_integral (\<lambda>x. f x * indicator A x) + ?t (A \<inter> A0)"
using bM_le_t[OF `A \<inter> A0 \<in> sets M`] `A \<in> sets M` `A0 \<in> sets M`
by (auto intro!: add_left_mono)
also have "\<dots> \<le> positive_integral (\<lambda>x. f x * indicator A x) + ?t A"
using M.measure_mono[simplified, OF _ `A \<inter> A0 \<in> sets M` `A \<in> sets M`]
by (auto intro!: add_left_mono)
also have "\<dots> \<le> \<nu> A"
using f_le_v M'.finite_measure[simplified, OF `A \<in> sets M`]
by (cases "positive_integral (\<lambda>x. f x * indicator A x)", cases "\<nu> A", auto)
finally have "positive_integral (\<lambda>x. ?f0 x * indicator A x) \<le> \<nu> A" . }
hence "?f0 \<in> G" using `A0 \<in> sets M` unfolding G_def
by (auto intro!: borel_measurable_indicator borel_measurable_pinfreal_add borel_measurable_pinfreal_times)
have real: "?t (space M) \<noteq> \<omega>" "?t A0 \<noteq> \<omega>"
"b * \<mu> (space M) \<noteq> \<omega>" "b * \<mu> A0 \<noteq> \<omega>"
using `A0 \<in> sets M` b
finite_measure[of A0] M.finite_measure[of A0]
finite_measure_of_space M.finite_measure_of_space
by auto
have int_f_finite: "positive_integral f \<noteq> \<omega>"
using M'.finite_measure_of_space pos_t unfolding pinfreal_zero_less_diff_iff
by (auto cong: positive_integral_cong)
have "?t (space M) > b * \<mu> (space M)" unfolding b_def
apply (simp add: field_simps)
apply (subst mult_assoc[symmetric])
apply (subst pinfreal_mult_inverse)
using finite_measure_of_space M'.finite_measure_of_space pos_t pos_M
using pinfreal_mult_strict_right_mono[of "Real (1/2)" 1 "?t (space M)"]
by simp_all
hence "0 < ?t (space M) - b * \<mu> (space M)"
by (simp add: pinfreal_zero_less_diff_iff)
also have "\<dots> \<le> ?t A0 - b * \<mu> A0"
using space_less_A0 pos_M pos_t b real[unfolded pinfreal_noteq_omega_Ex] by auto
finally have "b * \<mu> A0 < ?t A0" unfolding pinfreal_zero_less_diff_iff .
hence "0 < ?t A0" by auto
hence "0 < \<mu> A0" using ac unfolding absolutely_continuous_def
using `A0 \<in> sets M` by auto
hence "0 < b * \<mu> A0" using b by auto
from int_f_finite this
have "?y + 0 < positive_integral f + b * \<mu> A0" unfolding int_f_eq_y
by (rule pinfreal_less_add)
also have "\<dots> = positive_integral ?f0" using f0_eq[OF top] `A0 \<in> sets M` sets_into_space
by (simp cong: positive_integral_cong)
finally have "?y < positive_integral ?f0" by simp
moreover from `?f0 \<in> G` have "positive_integral ?f0 \<le> ?y" by (auto intro!: le_SUPI)
ultimately show False by auto
qed
show ?thesis
proof (safe intro!: bexI[of _ f])
fix A assume "A\<in>sets M"
show "\<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
proof (rule antisym)
show "positive_integral (\<lambda>x. f x * indicator A x) \<le> \<nu> A"
using `f \<in> G` `A \<in> sets M` unfolding G_def by auto
show "\<nu> A \<le> positive_integral (\<lambda>x. f x * indicator A x)"
using upper_bound[THEN bspec, OF `A \<in> sets M`]
by (simp add: pinfreal_zero_le_diff)
qed
qed simp
qed
lemma (in finite_measure) split_space_into_finite_sets_and_rest:
assumes "measure_space M \<nu>"
assumes ac: "absolutely_continuous \<nu>"
shows "\<exists>\<Omega>0\<in>sets M. \<exists>\<Omega>::nat\<Rightarrow>'a set. disjoint_family \<Omega> \<and> range \<Omega> \<subseteq> sets M \<and> \<Omega>0 = space M - (\<Union>i. \<Omega> i) \<and>
(\<forall>A\<in>sets M. A \<subseteq> \<Omega>0 \<longrightarrow> (\<mu> A = 0 \<and> \<nu> A = 0) \<or> (\<mu> A > 0 \<and> \<nu> A = \<omega>)) \<and>
(\<forall>i. \<nu> (\<Omega> i) \<noteq> \<omega>)"
proof -
interpret v: measure_space M \<nu> by fact
let ?Q = "{Q\<in>sets M. \<nu> Q \<noteq> \<omega>}"
let ?a = "SUP Q:?Q. \<mu> Q"
have "{} \<in> ?Q" using v.empty_measure by auto
then have Q_not_empty: "?Q \<noteq> {}" by blast
have "?a \<le> \<mu> (space M)" using sets_into_space
by (auto intro!: SUP_leI measure_mono top)
then have "?a \<noteq> \<omega>" using finite_measure_of_space
by auto
from SUPR_countable_SUPR[OF this Q_not_empty]
obtain Q'' where "range Q'' \<subseteq> \<mu> ` ?Q" and a: "?a = (SUP i::nat. Q'' i)"
by auto
then have "\<forall>i. \<exists>Q'. Q'' i = \<mu> Q' \<and> Q' \<in> ?Q" by auto
from choice[OF this] obtain Q' where Q': "\<And>i. Q'' i = \<mu> (Q' i)" "\<And>i. Q' i \<in> ?Q"
by auto
then have a_Lim: "?a = (SUP i::nat. \<mu> (Q' i))" using a by simp
let "?O n" = "\<Union>i\<le>n. Q' i"
have Union: "(SUP i. \<mu> (?O i)) = \<mu> (\<Union>i. ?O i)"
proof (rule continuity_from_below[of ?O])
show "range ?O \<subseteq> sets M" using Q' by (auto intro!: finite_UN)
show "\<And>i. ?O i \<subseteq> ?O (Suc i)" by fastsimp
qed
have Q'_sets: "\<And>i. Q' i \<in> sets M" using Q' by auto
have O_sets: "\<And>i. ?O i \<in> sets M"
using Q' by (auto intro!: finite_UN Un)
then have O_in_G: "\<And>i. ?O i \<in> ?Q"
proof (safe del: notI)
fix i have "Q' ` {..i} \<subseteq> sets M"
using Q' by (auto intro: finite_UN)
with v.measure_finitely_subadditive[of "{.. i}" Q']
have "\<nu> (?O i) \<le> (\<Sum>i\<le>i. \<nu> (Q' i))" by auto
also have "\<dots> < \<omega>" unfolding setsum_\<omega> pinfreal_less_\<omega> using Q' by auto
finally show "\<nu> (?O i) \<noteq> \<omega>" unfolding pinfreal_less_\<omega> by auto
qed auto
have O_mono: "\<And>n. ?O n \<subseteq> ?O (Suc n)" by fastsimp
have a_eq: "?a = \<mu> (\<Union>i. ?O i)" unfolding Union[symmetric]
proof (rule antisym)
show "?a \<le> (SUP i. \<mu> (?O i))" unfolding a_Lim
using Q' by (auto intro!: SUP_mono measure_mono finite_UN)
show "(SUP i. \<mu> (?O i)) \<le> ?a" unfolding SUPR_def
proof (safe intro!: Sup_mono, unfold bex_simps)
fix i
have *: "(\<Union>Q' ` {..i}) = ?O i" by auto
then show "\<exists>x. (x \<in> sets M \<and> \<nu> x \<noteq> \<omega>) \<and>
\<mu> (\<Union>Q' ` {..i}) \<le> \<mu> x"
using O_in_G[of i] by (auto intro!: exI[of _ "?O i"])
qed
qed
let "?O_0" = "(\<Union>i. ?O i)"
have "?O_0 \<in> sets M" using Q' by auto
def Q \<equiv> "\<lambda>i. case i of 0 \<Rightarrow> Q' 0 | Suc n \<Rightarrow> ?O (Suc n) - ?O n"
{ fix i have "Q i \<in> sets M" unfolding Q_def using Q'[of 0] by (cases i) (auto intro: O_sets) }
note Q_sets = this
show ?thesis
proof (intro bexI exI conjI ballI impI allI)
show "disjoint_family Q"
by (fastsimp simp: disjoint_family_on_def Q_def
split: nat.split_asm)
show "range Q \<subseteq> sets M"
using Q_sets by auto
{ fix A assume A: "A \<in> sets M" "A \<subseteq> space M - ?O_0"
show "\<mu> A = 0 \<and> \<nu> A = 0 \<or> 0 < \<mu> A \<and> \<nu> A = \<omega>"
proof (rule disjCI, simp)
assume *: "0 < \<mu> A \<longrightarrow> \<nu> A \<noteq> \<omega>"
show "\<mu> A = 0 \<and> \<nu> A = 0"
proof cases
assume "\<mu> A = 0" moreover with ac A have "\<nu> A = 0"
unfolding absolutely_continuous_def by auto
ultimately show ?thesis by simp
next
assume "\<mu> A \<noteq> 0" with * have "\<nu> A \<noteq> \<omega>" by auto
with A have "\<mu> ?O_0 + \<mu> A = \<mu> (?O_0 \<union> A)"
using Q' by (auto intro!: measure_additive countable_UN)
also have "\<dots> = (SUP i. \<mu> (?O i \<union> A))"
proof (rule continuity_from_below[of "\<lambda>i. ?O i \<union> A", symmetric, simplified])
show "range (\<lambda>i. ?O i \<union> A) \<subseteq> sets M"
using `\<nu> A \<noteq> \<omega>` O_sets A by auto
qed fastsimp
also have "\<dots> \<le> ?a"
proof (safe intro!: SUPR_bound)
fix i have "?O i \<union> A \<in> ?Q"
proof (safe del: notI)
show "?O i \<union> A \<in> sets M" using O_sets A by auto
from O_in_G[of i]
moreover have "\<nu> (?O i \<union> A) \<le> \<nu> (?O i) + \<nu> A"
using v.measure_subadditive[of "?O i" A] A O_sets by auto
ultimately show "\<nu> (?O i \<union> A) \<noteq> \<omega>"
using `\<nu> A \<noteq> \<omega>` by auto
qed
then show "\<mu> (?O i \<union> A) \<le> ?a" by (rule le_SUPI)
qed
finally have "\<mu> A = 0" unfolding a_eq using finite_measure[OF `?O_0 \<in> sets M`]
by (cases "\<mu> A") (auto simp: pinfreal_noteq_omega_Ex)
with `\<mu> A \<noteq> 0` show ?thesis by auto
qed
qed }
{ fix i show "\<nu> (Q i) \<noteq> \<omega>"
proof (cases i)
case 0 then show ?thesis
unfolding Q_def using Q'[of 0] by simp
next
case (Suc n)
then show ?thesis unfolding Q_def
using `?O n \<in> ?Q` `?O (Suc n) \<in> ?Q` O_mono
using v.measure_Diff[of "?O n" "?O (Suc n)"] by auto
qed }
show "space M - ?O_0 \<in> sets M" using Q'_sets by auto
{ fix j have "(\<Union>i\<le>j. ?O i) = (\<Union>i\<le>j. Q i)"
proof (induct j)
case 0 then show ?case by (simp add: Q_def)
next
case (Suc j)
have eq: "\<And>j. (\<Union>i\<le>j. ?O i) = (\<Union>i\<le>j. Q' i)" by fastsimp
have "{..j} \<union> {..Suc j} = {..Suc j}" by auto
then have "(\<Union>i\<le>Suc j. Q' i) = (\<Union>i\<le>j. Q' i) \<union> Q (Suc j)"
by (simp add: UN_Un[symmetric] Q_def del: UN_Un)
then show ?case using Suc by (auto simp add: eq atMost_Suc)
qed }
then have "(\<Union>j. (\<Union>i\<le>j. ?O i)) = (\<Union>j. (\<Union>i\<le>j. Q i))" by simp
then show "space M - ?O_0 = space M - (\<Union>i. Q i)" by fastsimp
qed
qed
lemma (in finite_measure) Radon_Nikodym_finite_measure_infinite:
assumes "measure_space M \<nu>"
assumes "absolutely_continuous \<nu>"
shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
proof -
interpret v: measure_space M \<nu> by fact
from split_space_into_finite_sets_and_rest[OF assms]
obtain Q0 and Q :: "nat \<Rightarrow> 'a set"
where Q: "disjoint_family Q" "range Q \<subseteq> sets M"
and Q0: "Q0 \<in> sets M" "Q0 = space M - (\<Union>i. Q i)"
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>"
and Q_fin: "\<And>i. \<nu> (Q i) \<noteq> \<omega>" by force
from Q have Q_sets: "\<And>i. Q i \<in> sets M" by auto
have "\<forall>i. \<exists>f. f\<in>borel_measurable M \<and> (\<forall>A\<in>sets M.
\<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f x * indicator (Q i \<inter> A) x))"
proof
fix i
have indicator_eq: "\<And>f x A. (f x :: pinfreal) * indicator (Q i \<inter> A) x * indicator (Q i) x
= (f x * indicator (Q i) x) * indicator A x"
unfolding indicator_def by auto
have fm: "finite_measure (restricted_space (Q i)) \<mu>"
(is "finite_measure ?R \<mu>") by (rule restricted_finite_measure[OF Q_sets[of i]])
then interpret R: finite_measure ?R .
have fmv: "finite_measure ?R \<nu>"
unfolding finite_measure_def finite_measure_axioms_def
proof
show "measure_space ?R \<nu>"
using v.restricted_measure_space Q_sets[of i] by auto
show "\<nu> (space ?R) \<noteq> \<omega>"
using Q_fin by simp
qed
have "R.absolutely_continuous \<nu>"
using `absolutely_continuous \<nu>` `Q i \<in> sets M`
by (auto simp: R.absolutely_continuous_def absolutely_continuous_def)
from finite_measure.Radon_Nikodym_finite_measure[OF fm fmv this]
obtain f where f: "(\<lambda>x. f x * indicator (Q i) x) \<in> borel_measurable M"
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)"
unfolding Bex_def borel_measurable_restricted[OF `Q i \<in> sets M`]
positive_integral_restricted[OF `Q i \<in> sets M`] by (auto simp: indicator_eq)
then show "\<exists>f. f\<in>borel_measurable M \<and> (\<forall>A\<in>sets M.
\<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f x * indicator (Q i \<inter> A) x))"
by (fastsimp intro!: exI[of _ "\<lambda>x. f x * indicator (Q i) x"] positive_integral_cong
simp: indicator_def)
qed
from choice[OF this] obtain f where borel: "\<And>i. f i \<in> borel_measurable M"
and f: "\<And>A i. A \<in> sets M \<Longrightarrow>
\<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f i x * indicator (Q i \<inter> A) x)"
by auto
let "?f x" =
"(\<Sum>\<^isub>\<infinity> i. f i x * indicator (Q i) x) + \<omega> * indicator Q0 x"
show ?thesis
proof (safe intro!: bexI[of _ ?f])
show "?f \<in> borel_measurable M"
by (safe intro!: borel_measurable_psuminf borel_measurable_pinfreal_times
borel_measurable_pinfreal_add borel_measurable_indicator
borel_measurable_const borel Q_sets Q0 Diff countable_UN)
fix A assume "A \<in> sets M"
have *:
"\<And>x i. indicator A x * (f i x * indicator (Q i) x) =
f i x * indicator (Q i \<inter> A) x"
"\<And>x i. (indicator A x * indicator Q0 x :: pinfreal) =
indicator (Q0 \<inter> A) x" by (auto simp: indicator_def)
have "positive_integral (\<lambda>x. ?f x * indicator A x) =
(\<Sum>\<^isub>\<infinity> i. \<nu> (Q i \<inter> A)) + \<omega> * \<mu> (Q0 \<inter> A)"
unfolding f[OF `A \<in> sets M`]
apply (simp del: pinfreal_times(2) add: field_simps *)
apply (subst positive_integral_add)
apply (fastsimp intro: Q0 `A \<in> sets M`)
apply (fastsimp intro: Q_sets `A \<in> sets M` borel_measurable_psuminf borel)
apply (subst positive_integral_cmult_indicator)
apply (fastsimp intro: Q0 `A \<in> sets M`)
unfolding psuminf_cmult_right[symmetric]
apply (subst positive_integral_psuminf)
apply (fastsimp intro: `A \<in> sets M` Q_sets borel)
apply (simp add: *)
done
moreover have "(\<Sum>\<^isub>\<infinity>i. \<nu> (Q i \<inter> A)) = \<nu> ((\<Union>i. Q i) \<inter> A)"
using Q Q_sets `A \<in> sets M`
by (intro v.measure_countably_additive[of "\<lambda>i. Q i \<inter> A", unfolded comp_def, simplified])
(auto simp: disjoint_family_on_def)
moreover have "\<omega> * \<mu> (Q0 \<inter> A) = \<nu> (Q0 \<inter> A)"
proof -
have "Q0 \<inter> A \<in> sets M" using Q0(1) `A \<in> sets M` by blast
from in_Q0[OF this] show ?thesis by auto
qed
moreover have "Q0 \<inter> A \<in> sets M" "((\<Union>i. Q i) \<inter> A) \<in> sets M"
using Q_sets `A \<in> sets M` Q0(1) by (auto intro!: countable_UN)
moreover have "((\<Union>i. Q i) \<inter> A) \<union> (Q0 \<inter> A) = A" "((\<Union>i. Q i) \<inter> A) \<inter> (Q0 \<inter> A) = {}"
using `A \<in> sets M` sets_into_space Q0 by auto
ultimately show "\<nu> A = positive_integral (\<lambda>x. ?f x * indicator A x)"
using v.measure_additive[simplified, of "(\<Union>i. Q i) \<inter> A" "Q0 \<inter> A"]
by simp
qed
qed
lemma (in sigma_finite_measure) Radon_Nikodym:
assumes "measure_space M \<nu>"
assumes "absolutely_continuous \<nu>"
shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
proof -
from Ex_finite_integrable_function
obtain h where finite: "positive_integral h \<noteq> \<omega>" and
borel: "h \<in> borel_measurable M" and
pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x" and
"\<And>x. x \<in> space M \<Longrightarrow> h x < \<omega>" by auto
let "?T A" = "positive_integral (\<lambda>x. h x * indicator A x)"
from measure_space_density[OF borel] finite
interpret T: finite_measure M ?T
unfolding finite_measure_def finite_measure_axioms_def
by (simp cong: positive_integral_cong)
have "\<And>N. N \<in> sets M \<Longrightarrow> {x \<in> space M. h x \<noteq> 0 \<and> indicator N x \<noteq> (0::pinfreal)} = N"
using sets_into_space pos by (force simp: indicator_def)
then have "T.absolutely_continuous \<nu>" using assms(2) borel
unfolding T.absolutely_continuous_def absolutely_continuous_def
by (fastsimp simp: borel_measurable_indicator positive_integral_0_iff)
from T.Radon_Nikodym_finite_measure_infinite[simplified, OF assms(1) this]
obtain f where f_borel: "f \<in> borel_measurable M" and
fT: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = T.positive_integral (\<lambda>x. f x * indicator A x)" by auto
show ?thesis
proof (safe intro!: bexI[of _ "\<lambda>x. h x * f x"])
show "(\<lambda>x. h x * f x) \<in> borel_measurable M"
using borel f_borel by (auto intro: borel_measurable_pinfreal_times)
fix A assume "A \<in> sets M"
then have "(\<lambda>x. f x * indicator A x) \<in> borel_measurable M"
using f_borel by (auto intro: borel_measurable_pinfreal_times borel_measurable_indicator)
from positive_integral_translated_density[OF borel this]
show "\<nu> A = positive_integral (\<lambda>x. h x * f x * indicator A x)"
unfolding fT[OF `A \<in> sets M`] by (simp add: field_simps)
qed
qed
section "Uniqueness of densities"
lemma (in measure_space) density_is_absolutely_continuous:
assumes "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
shows "absolutely_continuous \<nu>"
using assms unfolding absolutely_continuous_def
by (simp add: positive_integral_null_set)
lemma (in measure_space) finite_density_unique:
assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
and fin: "positive_integral f < \<omega>"
shows "(\<forall>A\<in>sets M. positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. g x * indicator A x))
\<longleftrightarrow> (AE x. f x = g x)"
(is "(\<forall>A\<in>sets M. ?P f A = ?P g A) \<longleftrightarrow> _")
proof (intro iffI ballI)
fix A assume eq: "AE x. f x = g x"
show "?P f A = ?P g A"
by (rule positive_integral_cong_AE[OF AE_mp[OF eq]]) simp
next
assume eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
from this[THEN bspec, OF top] fin
have g_fin: "positive_integral g < \<omega>" by (simp cong: positive_integral_cong)
{ fix f g assume borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
and g_fin: "positive_integral g < \<omega>" and eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
let ?N = "{x\<in>space M. g x < f x}"
have N: "?N \<in> sets M" using borel by simp
have "?P (\<lambda>x. (f x - g x)) ?N = positive_integral (\<lambda>x. f x * indicator ?N x - g x * indicator ?N x)"
by (auto intro!: positive_integral_cong simp: indicator_def)
also have "\<dots> = ?P f ?N - ?P g ?N"
proof (rule positive_integral_diff)
show "(\<lambda>x. f x * indicator ?N x) \<in> borel_measurable M" "(\<lambda>x. g x * indicator ?N x) \<in> borel_measurable M"
using borel N by auto
have "?P g ?N \<le> positive_integral g"
by (auto intro!: positive_integral_mono simp: indicator_def)
then show "?P g ?N \<noteq> \<omega>" using g_fin by auto
fix x assume "x \<in> space M"
show "g x * indicator ?N x \<le> f x * indicator ?N x"
by (auto simp: indicator_def)
qed
also have "\<dots> = 0"
using eq[THEN bspec, OF N] by simp
finally have "\<mu> {x\<in>space M. (f x - g x) * indicator ?N x \<noteq> 0} = 0"
using borel N by (subst (asm) positive_integral_0_iff) auto
moreover have "{x\<in>space M. (f x - g x) * indicator ?N x \<noteq> 0} = ?N"
by (auto simp: pinfreal_zero_le_diff)
ultimately have "?N \<in> null_sets" using N by simp }
from this[OF borel g_fin eq] this[OF borel(2,1) fin]
have "{x\<in>space M. g x < f x} \<union> {x\<in>space M. f x < g x} \<in> null_sets"
using eq by (intro null_sets_Un) auto
also have "{x\<in>space M. g x < f x} \<union> {x\<in>space M. f x < g x} = {x\<in>space M. f x \<noteq> g x}"
by auto
finally show "AE x. f x = g x"
unfolding almost_everywhere_def by auto
qed
lemma (in finite_measure) density_unique_finite_measure:
assumes borel: "f \<in> borel_measurable M" "f' \<in> borel_measurable M"
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)"
(is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A")
shows "AE x. f x = f' x"
proof -
let "?\<nu> A" = "?P f A" and "?\<nu>' A" = "?P f' A"
let "?f A x" = "f x * indicator A x" and "?f' A x" = "f' x * indicator A x"
interpret M: measure_space M ?\<nu>
using borel(1) by (rule measure_space_density)
have ac: "absolutely_continuous ?\<nu>"
using f by (rule density_is_absolutely_continuous)
from split_space_into_finite_sets_and_rest[OF `measure_space M ?\<nu>` ac]
obtain Q0 and Q :: "nat \<Rightarrow> 'a set"
where Q: "disjoint_family Q" "range Q \<subseteq> sets M"
and Q0: "Q0 \<in> sets M" "Q0 = space M - (\<Union>i. Q i)"
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>"
and Q_fin: "\<And>i. ?\<nu> (Q i) \<noteq> \<omega>" by force
from Q have Q_sets: "\<And>i. Q i \<in> sets M" by auto
let ?N = "{x\<in>space M. f x \<noteq> f' x}"
have "?N \<in> sets M" using borel by auto
have *: "\<And>i x A. \<And>y::pinfreal. y * indicator (Q i) x * indicator A x = y * indicator (Q i \<inter> A) x"
unfolding indicator_def by auto
have 1: "\<forall>i. AE x. ?f (Q i) x = ?f' (Q i) x"
using borel Q_fin Q
by (intro finite_density_unique[THEN iffD1] allI)
(auto intro!: borel_measurable_pinfreal_times f Int simp: *)
have 2: "AE x. ?f Q0 x = ?f' Q0 x"
proof (rule AE_I')
{ fix f :: "'a \<Rightarrow> pinfreal" assume borel: "f \<in> borel_measurable M"
and eq: "\<And>A. A \<in> sets M \<Longrightarrow> ?\<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
let "?A i" = "Q0 \<inter> {x \<in> space M. f x < of_nat i}"
have "(\<Union>i. ?A i) \<in> null_sets"
proof (rule null_sets_UN)
fix i have "?A i \<in> sets M"
using borel Q0(1) by auto
have "?\<nu> (?A i) \<le> positive_integral (\<lambda>x. of_nat i * indicator (?A i) x)"
unfolding eq[OF `?A i \<in> sets M`]
by (auto intro!: positive_integral_mono simp: indicator_def)
also have "\<dots> = of_nat i * \<mu> (?A i)"
using `?A i \<in> sets M` by (auto intro!: positive_integral_cmult_indicator)
also have "\<dots> < \<omega>"
using `?A i \<in> sets M`[THEN finite_measure] by auto
finally have "?\<nu> (?A i) \<noteq> \<omega>" by simp
then show "?A i \<in> null_sets" using in_Q0[OF `?A i \<in> sets M`] `?A i \<in> sets M` by auto
qed
also have "(\<Union>i. ?A i) = Q0 \<inter> {x\<in>space M. f x < \<omega>}"
by (auto simp: less_\<omega>_Ex_of_nat)
finally have "Q0 \<inter> {x\<in>space M. f x \<noteq> \<omega>} \<in> null_sets" by (simp add: pinfreal_less_\<omega>) }
from this[OF borel(1) refl] this[OF borel(2) f]
have "Q0 \<inter> {x\<in>space M. f x \<noteq> \<omega>} \<in> null_sets" "Q0 \<inter> {x\<in>space M. f' x \<noteq> \<omega>} \<in> null_sets" by simp_all
then show "(Q0 \<inter> {x\<in>space M. f x \<noteq> \<omega>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<omega>}) \<in> null_sets" by (rule null_sets_Un)
show "{x \<in> space M. ?f Q0 x \<noteq> ?f' Q0 x} \<subseteq>
(Q0 \<inter> {x\<in>space M. f x \<noteq> \<omega>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<omega>})" by (auto simp: indicator_def)
qed
have **: "\<And>x. (?f Q0 x = ?f' Q0 x) \<longrightarrow> (\<forall>i. ?f (Q i) x = ?f' (Q i) x) \<longrightarrow>
?f (space M) x = ?f' (space M) x"
by (auto simp: indicator_def Q0)
have 3: "AE x. ?f (space M) x = ?f' (space M) x"
by (rule AE_mp[OF 1[unfolded all_AE_countable] AE_mp[OF 2]]) (simp add: **)
then show "AE x. f x = f' x"
by (rule AE_mp) (auto intro!: AE_cong simp: indicator_def)
qed
lemma (in sigma_finite_measure) density_unique:
assumes borel: "f \<in> borel_measurable M" "f' \<in> borel_measurable M"
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)"
(is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A")
shows "AE x. f x = f' x"
proof -
obtain h where h_borel: "h \<in> borel_measurable M"
and fin: "positive_integral h \<noteq> \<omega>" and pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<omega>"
using Ex_finite_integrable_function by auto
interpret h: measure_space M "\<lambda>A. positive_integral (\<lambda>x. h x * indicator A x)"
using h_borel by (rule measure_space_density)
interpret h: finite_measure M "\<lambda>A. positive_integral (\<lambda>x. h x * indicator A x)"
by default (simp cong: positive_integral_cong add: fin)
interpret f: measure_space M "\<lambda>A. positive_integral (\<lambda>x. f x * indicator A x)"
using borel(1) by (rule measure_space_density)
interpret f': measure_space M "\<lambda>A. positive_integral (\<lambda>x. f' x * indicator A x)"
using borel(2) by (rule measure_space_density)
{ fix A assume "A \<in> sets M"
then have " {x \<in> space M. h x \<noteq> 0 \<and> indicator A x \<noteq> (0::pinfreal)} = A"
using pos sets_into_space by (force simp: indicator_def)
then have "positive_integral (\<lambda>xa. h xa * indicator A xa) = 0 \<longleftrightarrow> A \<in> null_sets"
using h_borel `A \<in> sets M` by (simp add: positive_integral_0_iff) }
note h_null_sets = this
{ fix A assume "A \<in> sets M"
have "positive_integral (\<lambda>x. h x * (f x * indicator A x)) =
f.positive_integral (\<lambda>x. h x * indicator A x)"
using `A \<in> sets M` h_borel borel
by (simp add: positive_integral_translated_density ac_simps cong: positive_integral_cong)
also have "\<dots> = f'.positive_integral (\<lambda>x. h x * indicator A x)"
by (rule f'.positive_integral_cong_measure) (rule f)
also have "\<dots> = positive_integral (\<lambda>x. h x * (f' x * indicator A x))"
using `A \<in> sets M` h_borel borel
by (simp add: positive_integral_translated_density ac_simps cong: positive_integral_cong)
finally have "positive_integral (\<lambda>x. h x * (f x * indicator A x)) = positive_integral (\<lambda>x. h x * (f' x * indicator A x))" . }
then have "h.almost_everywhere (\<lambda>x. f x = f' x)"
using h_borel borel
by (intro h.density_unique_finite_measure[OF borel])
(simp add: positive_integral_translated_density)
then show "AE x. f x = f' x"
unfolding h.almost_everywhere_def almost_everywhere_def
by (auto simp add: h_null_sets)
qed
lemma (in sigma_finite_measure) sigma_finite_iff_density_finite:
assumes \<nu>: "measure_space M \<nu>" and f: "f \<in> borel_measurable M"
and eq: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
shows "sigma_finite_measure M \<nu> \<longleftrightarrow> (AE x. f x \<noteq> \<omega>)"
proof
assume "sigma_finite_measure M \<nu>"
then interpret \<nu>: sigma_finite_measure M \<nu> .
from \<nu>.Ex_finite_integrable_function obtain h where
h: "h \<in> borel_measurable M" "\<nu>.positive_integral h \<noteq> \<omega>"
and fin: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<omega>" by auto
have "AE x. f x * h x \<noteq> \<omega>"
proof (rule AE_I')
have "\<nu>.positive_integral h = positive_integral (\<lambda>x. f x * h x)"
by (simp add: \<nu>.positive_integral_cong_measure[symmetric, OF eq[symmetric]])
(intro positive_integral_translated_density f h)
then have "positive_integral (\<lambda>x. f x * h x) \<noteq> \<omega>"
using h(2) by simp
then show "(\<lambda>x. f x * h x) -` {\<omega>} \<inter> space M \<in> null_sets"
using f h(1) by (auto intro!: positive_integral_omega borel_measurable_vimage)
qed auto
then show "AE x. f x \<noteq> \<omega>"
proof (rule AE_mp, intro AE_cong)
fix x assume "x \<in> space M" from this[THEN fin]
show "f x * h x \<noteq> \<omega> \<longrightarrow> f x \<noteq> \<omega>" by auto
qed
next
assume AE: "AE x. f x \<noteq> \<omega>"
from sigma_finite guess Q .. note Q = this
interpret \<nu>: measure_space M \<nu> by fact
def A \<equiv> "\<lambda>i. f -` (case i of 0 \<Rightarrow> {\<omega>} | Suc n \<Rightarrow> {.. of_nat (Suc n)}) \<inter> space M"
{ fix i j have "A i \<inter> Q j \<in> sets M"
unfolding A_def using f Q
apply (rule_tac Int)
by (cases i) (auto intro: measurable_sets[OF f]) }
note A_in_sets = this
let "?A n" = "case prod_decode n of (i,j) \<Rightarrow> A i \<inter> Q j"
show "sigma_finite_measure M \<nu>"
proof (default, intro exI conjI subsetI allI)
fix x assume "x \<in> range ?A"
then obtain n where n: "x = ?A n" by auto
then show "x \<in> sets M" using A_in_sets by (cases "prod_decode n") auto
next
have "(\<Union>i. ?A i) = (\<Union>i j. A i \<inter> Q j)"
proof safe
fix x i j assume "x \<in> A i" "x \<in> Q j"
then show "x \<in> (\<Union>i. case prod_decode i of (i, j) \<Rightarrow> A i \<inter> Q j)"
by (intro UN_I[of "prod_encode (i,j)"]) auto
qed auto
also have "\<dots> = (\<Union>i. A i) \<inter> space M" using Q by auto
also have "(\<Union>i. A i) = space M"
proof safe
fix x assume x: "x \<in> space M"
show "x \<in> (\<Union>i. A i)"
proof (cases "f x")
case infinite then show ?thesis using x unfolding A_def by (auto intro: exI[of _ 0])
next
case (preal r)
with less_\<omega>_Ex_of_nat[of "f x"] obtain n where "f x < of_nat n" by auto
then show ?thesis using x preal unfolding A_def by (auto intro!: exI[of _ "Suc n"])
qed
qed (auto simp: A_def)
finally show "(\<Union>i. ?A i) = space M" by simp
next
fix n obtain i j where
[simp]: "prod_decode n = (i, j)" by (cases "prod_decode n") auto
have "positive_integral (\<lambda>x. f x * indicator (A i \<inter> Q j) x) \<noteq> \<omega>"
proof (cases i)
case 0
have "AE x. f x * indicator (A i \<inter> Q j) x = 0"
using AE by (rule AE_mp) (auto intro!: AE_cong simp: A_def `i = 0`)
then have "positive_integral (\<lambda>x. f x * indicator (A i \<inter> Q j) x) = 0"
using A_in_sets f
apply (subst positive_integral_0_iff)
apply fast
apply (subst (asm) AE_iff_null_set)
apply (intro borel_measurable_pinfreal_neq_const)
apply fast
by simp
then show ?thesis by simp
next
case (Suc n)
then have "positive_integral (\<lambda>x. f x * indicator (A i \<inter> Q j) x) \<le>
positive_integral (\<lambda>x. of_nat (Suc n) * indicator (Q j) x)"
by (auto intro!: positive_integral_mono simp: indicator_def A_def)
also have "\<dots> = of_nat (Suc n) * \<mu> (Q j)"
using Q by (auto intro!: positive_integral_cmult_indicator)
also have "\<dots> < \<omega>"
using Q by auto
finally show ?thesis by simp
qed
then show "\<nu> (?A n) \<noteq> \<omega>"
using A_in_sets Q eq by auto
qed
qed
section "Radon Nikodym derivative"
definition (in sigma_finite_measure)
"RN_deriv \<nu> \<equiv> SOME f. f \<in> borel_measurable M \<and>
(\<forall>A \<in> sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x))"
lemma (in sigma_finite_measure) RN_deriv_cong:
assumes cong: "\<And>A. A \<in> sets M \<Longrightarrow> \<mu>' A = \<mu> A" "\<And>A. A \<in> sets M \<Longrightarrow> \<nu>' A = \<nu> A"
shows "sigma_finite_measure.RN_deriv M \<mu>' \<nu>' x = RN_deriv \<nu> x"
proof -
interpret \<mu>': sigma_finite_measure M \<mu>'
using cong(1) by (rule sigma_finite_measure_cong)
show ?thesis
unfolding RN_deriv_def \<mu>'.RN_deriv_def
by (simp add: cong positive_integral_cong_measure[OF cong(1)])
qed
lemma (in sigma_finite_measure) RN_deriv:
assumes "measure_space M \<nu>"
assumes "absolutely_continuous \<nu>"
shows "RN_deriv \<nu> \<in> borel_measurable M" (is ?borel)
and "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)"
(is "\<And>A. _ \<Longrightarrow> ?int A")
proof -
note Ex = Radon_Nikodym[OF assms, unfolded Bex_def]
thus ?borel unfolding RN_deriv_def by (rule someI2_ex) auto
fix A assume "A \<in> sets M"
from Ex show "?int A" unfolding RN_deriv_def
by (rule someI2_ex) (simp add: `A \<in> sets M`)
qed
lemma (in sigma_finite_measure) RN_deriv_positive_integral:
assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
and f: "f \<in> borel_measurable M"
shows "measure_space.positive_integral M \<nu> f = positive_integral (\<lambda>x. RN_deriv \<nu> x * f x)"
proof -
interpret \<nu>: measure_space M \<nu> by fact
have "\<nu>.positive_integral f =
measure_space.positive_integral M (\<lambda>A. positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)) f"
by (intro \<nu>.positive_integral_cong_measure[symmetric] RN_deriv(2)[OF \<nu>, symmetric])
also have "\<dots> = positive_integral (\<lambda>x. RN_deriv \<nu> x * f x)"
by (intro positive_integral_translated_density RN_deriv[OF \<nu>] f)
finally show ?thesis .
qed
lemma (in sigma_finite_measure) RN_deriv_unique:
assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
and f: "f \<in> borel_measurable M"
and eq: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
shows "AE x. f x = RN_deriv \<nu> x"
proof (rule density_unique[OF f RN_deriv(1)[OF \<nu>]])
fix A assume A: "A \<in> sets M"
show "positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)"
unfolding eq[OF A, symmetric] RN_deriv(2)[OF \<nu> A, symmetric] ..
qed
lemma the_inv_into_in:
assumes "inj_on f A" and x: "x \<in> f`A"
shows "the_inv_into A f x \<in> A"
using assms by (auto simp: the_inv_into_f_f)
lemma (in sigma_finite_measure) RN_deriv_vimage:
fixes f :: "'b \<Rightarrow> 'a"
assumes f: "bij_betw f S (space M)"
assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
shows "AE x.
sigma_finite_measure.RN_deriv (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>A. \<nu> (f ` A)) (the_inv_into S f x) = RN_deriv \<nu> x"
proof (rule RN_deriv_unique[OF \<nu>])
interpret sf: sigma_finite_measure "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
using f by (rule sigma_finite_measure_isomorphic)
interpret \<nu>: measure_space M \<nu> using \<nu>(1) .
have \<nu>': "measure_space (vimage_algebra S f) (\<lambda>A. \<nu> (f ` A))"
using f by (rule \<nu>.measure_space_isomorphic)
{ fix A assume "A \<in> sets M" then have "f ` (f -` A \<inter> S) = A"
using sets_into_space f[unfolded bij_betw_def]
by (intro image_vimage_inter_eq[where T="space M"]) auto }
note A_f = this
then have ac: "sf.absolutely_continuous (\<lambda>A. \<nu> (f ` A))"
using \<nu>(2) by (auto simp: sf.absolutely_continuous_def absolutely_continuous_def)
show "(\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (the_inv_into S f x)) \<in> borel_measurable M"
using sf.RN_deriv(1)[OF \<nu>' ac]
unfolding measurable_vimage_iff_inv[OF f] comp_def .
fix A assume "A \<in> sets M"
then have *: "\<And>x. x \<in> space M \<Longrightarrow> indicator (f -` A \<inter> S) (the_inv_into S f x) = (indicator A x :: pinfreal)"
using f[unfolded bij_betw_def]
unfolding indicator_def by (auto simp: f_the_inv_into_f the_inv_into_in)
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)"
using `A \<in> sets M` by (force intro!: sf.RN_deriv(2)[OF \<nu>' ac])
also have "\<dots> = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (the_inv_into S f x) * indicator A x)"
unfolding positive_integral_vimage_inv[OF f]
by (simp add: * cong: positive_integral_cong)
finally show "\<nu> A = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (the_inv_into S f x) * indicator A x)"
unfolding A_f[OF `A \<in> sets M`] .
qed
lemma (in sigma_finite_measure) RN_deriv_finite:
assumes sfm: "sigma_finite_measure M \<nu>" and ac: "absolutely_continuous \<nu>"
shows "AE x. RN_deriv \<nu> x \<noteq> \<omega>"
proof -
interpret \<nu>: sigma_finite_measure M \<nu> by fact
have \<nu>: "measure_space M \<nu>" by default
from sfm show ?thesis
using sigma_finite_iff_density_finite[OF \<nu> RN_deriv[OF \<nu> ac]] by simp
qed
lemma (in sigma_finite_measure)
assumes \<nu>: "sigma_finite_measure M \<nu>" "absolutely_continuous \<nu>"
and f: "f \<in> borel_measurable M"
shows RN_deriv_integral: "measure_space.integral M \<nu> f = integral (\<lambda>x. real (RN_deriv \<nu> x) * f x)" (is ?integral)
and RN_deriv_integrable: "measure_space.integrable M \<nu> f \<longleftrightarrow> integrable (\<lambda>x. real (RN_deriv \<nu> x) * f x)" (is ?integrable)
proof -
interpret \<nu>: sigma_finite_measure M \<nu> by fact
have ms: "measure_space M \<nu>" by default
have minus_cong: "\<And>A B A' B'::pinfreal. A = A' \<Longrightarrow> B = B' \<Longrightarrow> real A - real B = real A' - real B'" by simp
have f': "(\<lambda>x. - f x) \<in> borel_measurable M" using f by auto
{ fix f :: "'a \<Rightarrow> real" assume "f \<in> borel_measurable M"
{ fix x assume *: "RN_deriv \<nu> x \<noteq> \<omega>"
have "Real (real (RN_deriv \<nu> x)) * Real (f x) = Real (real (RN_deriv \<nu> x) * f x)"
by (simp add: mult_le_0_iff)
then have "RN_deriv \<nu> x * Real (f x) = Real (real (RN_deriv \<nu> x) * f x)"
using * by (simp add: Real_real) }
note * = this
have "positive_integral (\<lambda>x. RN_deriv \<nu> x * Real (f x)) = positive_integral (\<lambda>x. Real (real (RN_deriv \<nu> x) * f x))"
apply (rule positive_integral_cong_AE)
apply (rule AE_mp[OF RN_deriv_finite[OF \<nu>]])
by (auto intro!: AE_cong simp: *) }
with this[OF f] this[OF f'] f f'
show ?integral ?integrable
unfolding \<nu>.integral_def integral_def \<nu>.integrable_def integrable_def
by (auto intro!: RN_deriv(1)[OF ms \<nu>(2)] minus_cong simp: RN_deriv_positive_integral[OF ms \<nu>(2)])
qed
lemma (in sigma_finite_measure) RN_deriv_singleton:
assumes "measure_space M \<nu>"
and ac: "absolutely_continuous \<nu>"
and "{x} \<in> sets M"
shows "\<nu> {x} = RN_deriv \<nu> x * \<mu> {x}"
proof -
note deriv = RN_deriv[OF assms(1, 2)]
from deriv(2)[OF `{x} \<in> sets M`]
have "\<nu> {x} = positive_integral (\<lambda>w. RN_deriv \<nu> x * indicator {x} w)"
by (auto simp: indicator_def intro!: positive_integral_cong)
thus ?thesis using positive_integral_cmult_indicator[OF `{x} \<in> sets M`]
by auto
qed
theorem (in finite_measure_space) RN_deriv_finite_measure:
assumes "measure_space M \<nu>"
and ac: "absolutely_continuous \<nu>"
and "x \<in> space M"
shows "\<nu> {x} = RN_deriv \<nu> x * \<mu> {x}"
proof -
have "{x} \<in> sets M" using sets_eq_Pow `x \<in> space M` by auto
from RN_deriv_singleton[OF assms(1,2) this] show ?thesis .
qed
end