imports Bochner_Integration

section

imports Bochner_Integration
begin

definition diff_measure ::
where

lemma
shows space_diff_measure[simp]:
and sets_diff_measure[simp]:
by (auto simp: diff_measure_def)

lemma emeasure_diff_measure:
assumes fin:   and sets_eq:
assumes pos:  and A:
shows  (is )
unfolding diff_measure_def
proof (rule emeasure_measure_of_sigma)
show  ..
show
using pos by (simp add: positive_def)
show
fix A ::   assume A:  and
then have suminf:

with A have
using fin pos[of ]
by (intro ennreal_suminf_minus)
(auto simp: sets_eq finite_measure.emeasure_eq_measure suminf_emeasure)
then show
qed
qed fact

text

lemma (in sigma_finite_measure) obtain_positive_integrable_function:
obtains f:: where

proof -
obtain A ::  where
using sigma_finite by auto
then have [measurable]: for n by auto
define g where
have [measurable]:  unfolding g_def by auto
have *:  for x
apply (rule summable_comparison_test'[of  0])
using power_half_series summable_def by (auto simp add: indicator_def divide_simps)
have  for x unfolding g_def
apply (rule suminf_le) using * power_half_series summable_def by (auto simp add: indicator_def divide_simps)
then have g_le_1:  for x using power_half_series sums_unique by fastforce

have g_pos:  if  for x
unfolding g_def proof (subst suminf_pos_iff[OF *[of x]], auto)
obtain i where  using   by auto
then have
unfolding indicator_def apply (auto simp add: divide_simps) using measure_nonneg[of M ]
by (auto, meson add_nonneg_nonneg linorder_not_le mult_nonneg_nonneg zero_le_numeral zero_le_one zero_le_power)
then show
by auto
qed

have
unfolding g_def proof (rule integrable_suminf)
fix n
show
using
by (auto intro!: integrable_mult_right integrable_divide_zero integrable_real_indicator simp add: top.not_eq_extremum)
next
show
using * by auto
show
apply (rule summable_comparison_test'[of  0], auto)
using power_half_series summable_def apply auto[1]
apply (auto simp add: divide_simps) using measure_nonneg[of M] not_less by fastforce
qed

define f where
have  for x unfolding f_def using g_pos by auto
moreover have  for x unfolding f_def using g_le_1 by auto
moreover have [measurable]:  unfolding f_def by auto
moreover have
apply (subst integrable_cong[of _ _ _ g]) unfolding f_def using  by auto
ultimately show
by (meson that)
qed

lemma (in sigma_finite_measure) Ex_finite_integrable_function:

proof -
obtain A ::  where
range[measurable]:  and
space:  and
measure:  and
disjoint:
using sigma_finite_disjoint by blast
let ?B =
have [measurable]:
using range by fastforce+
have
proof
fix i show
using measure[of i]
by (auto intro!: dense simp: ennreal_inverse_positive ennreal_mult_eq_top_iff power_eq_top_ennreal)
qed
from choice[OF this] obtain n where n:
by auto
{ fix i have  using n(1)[of i] by auto } note pos = this
let ?h =
show ?thesis
proof (safe intro!: bexI[of _ ?h] del: notI)
have  using pos
also have
proof (intro suminf_le allI)
fix N
have
using n[of N] by (intro mult_right_mono) auto
also have
using measure[of N]
by (simp add: ennreal_inverse_power divide_ennreal_def ennreal_inverse_mult
power_eq_top_ennreal less_top[symmetric] mult_ac
del: power_Suc)
also have
using measure[of N]
by (cases ; cases )
(auto simp: inverse_ennreal ennreal_mult[symmetric] divide_ennreal_def simp del: power_Suc)
also have
by (subst ennreal_power[symmetric], simp) (simp add: inverse_ennreal)
finally show
by simp
qed auto
also have
unfolding less_top[symmetric]
by (rule ennreal_suminf_neq_top)
(auto simp: summable_geometric summable_Suc_iff simp del: power_Suc)
finally show
by (auto simp: top_unique)
next
{ fix x assume
then obtain i where  using space[symmetric] by auto
with disjoint n have
by (auto intro!: suminf_cmult_indicator intro: less_imp_le)
then show  and  using n[of i] by (auto simp: less_top[symmetric]) }
note pos = this
qed measurable
qed

subsection

definition absolutely_continuous ::  where

lemma absolutely_continuousI_count_space:
unfolding absolutely_continuous_def by (auto simp: null_sets_count_space)

lemma absolutely_continuousI_density:

by (force simp add: absolutely_continuous_def null_sets_density_iff dest: AE_not_in)

lemma absolutely_continuousI_point_measure_finite:

unfolding absolutely_continuous_def by (force simp: null_sets_point_measure_iff)

lemma absolutely_continuousD:

by (auto simp: absolutely_continuous_def null_sets_def)

lemma absolutely_continuous_AE:
assumes sets_eq:
and
shows
proof -
from  obtain N where N:
unfolding eventually_ae_filter by auto
show
proof (rule AE_I')
show  using sets_eq_imp_space_eq[OF sets_eq] N(2) by simp
from  show
using N unfolding absolutely_continuous_def sets_eq null_sets_def by auto
qed
qed

subsection

assumes  and sets_eq[simp]:
assumes
shows
proof -
interpret N: finite_measure N by fact
define G where
have [measurable_dest]:
and G_D:  for f
by (auto simp: G_def)
note this[measurable_dest]
have  unfolding G_def by auto
hence  by auto
{ fix f g assume f[measurable]:  and g[measurable]:
have  (is ) unfolding G_def
proof safe
let ?A =
have  using f g unfolding G_def by auto
fix A assume [measurable]:
have union:
using sets.sets_into_space[OF ] by auto
have
by (auto simp: indicator_def max_def)
hence
by (auto cong: nn_integral_cong intro!: nn_integral_add)
also have
using f g unfolding G_def by (auto intro!: add_mono)
also have
using union by (subst plus_emeasure) auto
finally show  .
qed auto }
note max_in_G = this
{ fix f assume   and f:
then have [measurable]:  by (auto simp: G_def)
have  unfolding G_def
proof safe
show  by measurable
next
fix A assume
have
by (intro nn_integral_cong) (simp split: split_indicator)
also have
using  f
by (intro nn_integral_monotone_convergence_SUP)
(auto simp: G_def incseq_Suc_iff le_fun_def split: split_indicator)
finally show
using f  by (auto intro!: SUP_least simp: G_D)
qed }
note SUP_in_G = this
let ?y =
have y_le:  unfolding G_def
proof (safe intro!: SUP_least)
fix g assume
from this[THEN bspec, OF sets.top] show
by (simp cong: nn_integral_cong)
qed
from ennreal_SUP_countable_SUP [OF , of ] guess ys .. note ys = this
then have
proof safe
fix n assume
hence  by auto
thus  by auto
qed
from choice[OF this] obtain gs where   by auto
hence y_eq:  using ys by auto
let ?g =
define f where [abs_def]:  for x
let ?F =
have gs_not_empty:  by auto
{ fix i have
proof (induct i)
case 0 thus ?case by simp fact
next
case (Suc i)
with Suc gs_not_empty  show ?case
by (auto simp add: atMost_Suc intro!: max_in_G)
qed }
note g_in_G = this
have  using gs_not_empty
by (auto intro!: incseq_SucI le_funI simp add: atMost_Suc)

from SUP_in_G[OF this g_in_G] have [measurable]:  unfolding f_def .
then have [measurable]:  unfolding G_def by auto

have  unfolding f_def
using g_in_G  by (auto intro!: nn_integral_monotone_convergence_SUP simp: G_def)
also have
proof (rule antisym)
show
using g_in_G by (auto intro: SUP_mono)
show  unfolding y_eq
by (auto intro!: SUP_mono nn_integral_mono Max_ge)
qed
finally have int_f_eq_y:  .

have upper_bound:
proof (rule ccontr)
assume
then obtain A where A[measurable]:  and f_less_N:
by (auto simp: not_le)
then have pos_A:
using [THEN absolutely_continuousD, OF A]
by (auto simp: zero_less_iff_neq_zero)

define b where
with f_less_N pos_A have
by (auto intro!: diff_gr0_ennreal simp: zero_less_iff_neq_zero diff_eq_0_iff_ennreal ennreal_divide_eq_top_iff)

let ?f =
have
using [THEN G_D, of ] by (auto simp: top_unique cong: nn_integral_cong)
with  interpret Mf: finite_measure
by (intro finite_measureI)
(auto simp: field_simps mult_indicator_subset ennreal_mult_eq_top_iff
cong: nn_integral_cong)

from unsigned_Hahn_decomposition[of  N A]
obtain Y where [measurable]:  and [simp]:
and Y1:
and Y2:
by auto

let ?f' =
have
proof
assume
then have
using [THEN absolutely_continuousD, of Y] by auto
then have
by (subst emeasure_Diff) auto
also have
by (rule Y2) auto
also have
by (subst emeasure_Diff) auto
also have
by (intro ennreal_minus_mono) auto
also have
also have
using f_less_N pos_A
by (cases ; cases ; cases )
(auto simp: b_def ennreal_less_iff ennreal_minus divide_ennreal ennreal_numeral[symmetric]
ennreal_plus[symmetric] ennreal_mult[symmetric] field_simps
simp del: ennreal_numeral ennreal_plus)
finally show False
by simp
qed
then have
using
moreover
have
unfolding G_def
proof safe
fix X assume [measurable]:
have
also have
using G_D[OF ] by (intro add_mono Y1) (auto simp: emeasure_density)
also have
by (subst plus_emeasure) (auto intro!: arg_cong2[where f=emeasure])
finally show  .
qed simp
then have
by (rule SUP_upper)
ultimately show False
qed
show ?thesis
proof (intro bexI[of _ f] measure_eqI conjI antisym)
fix A assume  then show
by (auto simp: emeasure_density intro!: G_D[OF ])
next
fix A assume A:  then show
using upper_bound by auto
qed auto
qed

lemma (in finite_measure) split_space_into_finite_sets_and_rest:
assumes ac:  and sets_eq[simp]:
shows
proof -
let ?Q =
let ?a =
have  by auto
then have Q_not_empty:  by blast
have  using sets.sets_into_space
by (auto intro!: SUP_least emeasure_mono)
then have
using finite_emeasure_space
by (auto simp: less_top[symmetric] top_unique simp del: SUP_eq_top_iff Sup_eq_top_iff)
from ennreal_SUP_countable_SUP [OF Q_not_empty, of ]
obtain Q'' where  and a:
by auto
then have  by auto
from choice[OF this] obtain Q' where Q':
by auto
then have a_Lim:  using a by simp
let ?O =
have Union:
proof (rule SUP_emeasure_incseq[of ?O])
show  using Q' by auto
show  by (fastforce intro!: incseq_SucI)
qed
have Q'_sets[measurable]:  using Q' by auto
have O_sets:  using Q' by auto
then have O_in_G:
proof (safe del: notI)
fix i have  using Q' by auto
then have
also have  using Q' by (simp add: less_top)
finally show  by simp
qed auto
have O_mono:  by fastforce
have a_eq:  unfolding Union[symmetric]
proof (rule antisym)
show  unfolding a_Lim
using Q' by (auto intro!: SUP_mono emeasure_mono)
show
proof (safe intro!: Sup_mono, unfold bex_simps)
fix i
have *:  by auto
then show
using O_in_G[of i] by (auto intro!: exI[of _ ])
qed
qed
let ?O_0 =
have  using Q' by auto
have  for i
using sets.range_disjointed_sets[of Q' M] using Q'_sets by (auto simp: subset_eq)
note Q_sets = this
show ?thesis
proof (intro bexI exI conjI ballI impI allI)
show
by (rule disjoint_family_disjointed)
show
using Q'_sets by (intro sets.range_disjointed_sets) auto
{ fix A assume A:
then have A1:
unfolding UN_disjointed_eq by auto
show
proof (rule disjCI, simp)
assume *:
show
proof (cases )
case True
with ac A have
unfolding absolutely_continuous_def by auto
with True show ?thesis by simp
next
case False
with * have  by auto
with A have
using Q' A1 by (auto intro!: plus_emeasure simp: set_eq_iff)
also have
proof (rule SUP_emeasure_incseq[of , symmetric, simplified])
show
using  O_sets A by auto
qed (fastforce intro!: incseq_SucI)
also have
proof (safe intro!: SUP_least)
fix i have
proof (safe del: notI)
show  using O_sets A by auto
from O_in_G[of i] have
using emeasure_subadditive[of  N A] A O_sets by auto
with O_in_G[of i] show
using  by (auto simp: top_unique)
qed
then show  by (rule SUP_upper)
qed
finally have
unfolding a_eq using measure_nonneg[of M A] by (simp add: emeasure_eq_measure)
with  show ?thesis by auto
qed
qed }
{ fix i
have
by (auto intro!: emeasure_mono simp: disjointed_def)
then show
using Q'(2)[of i] by (auto simp: top_unique) }
qed
qed

assumes  and sets_eq:
shows
proof -
from split_space_into_finite_sets_and_rest[OF assms]
obtain Q ::
where Q:
and in_Q0:
and Q_fin:  by force
from Q have Q_sets:  by auto
let ?N =  and ?M =
have
fix i
from Q show
by (auto intro!: finite_measureI cong: nn_integral_cong
from Q have
by (simp add: sets_eq[symmetric] emeasure_density subset_eq cong: nn_integral_cong)
with Q_fin show
by (auto intro!: finite_measureI)
have [measurable]:  by (simp add: sets_eq)
show
using
by (auto simp: absolutely_continuous_def null_sets_density_iff sets_eq
intro!: absolutely_continuous_AE[OF sets_eq])
qed
from choice[OF this[unfolded Bex_def]]
obtain f where borel:
and f_density:
by force
{ fix A i assume A:
with Q borel have
by (auto simp add: emeasure_density nn_integral_density subset_eq
intro!: nn_integral_cong split: split_indicator)
also have
using A Q by (simp add: f_density emeasure_restricted subset_eq sets_eq)
finally have  .. }
note integral_eq = this
let ?f =
show ?thesis
proof (safe intro!: bexI[of _ ?f])
show  using borel Q_sets
by (auto intro!: measurable_If)
show
proof (rule measure_eqI)
fix A assume
then have  by simp
have Qi:  using Q by auto
have [intro,simp]:

using borel Qi  by auto
have
using borel by (intro nn_integral_cong) (auto simp: indicator_def)
also have
using borel Qi
(auto simp add: nn_integral_cmult_indicator sets.Int intro!: suminf_0_le)
also have
by (subst integral_eq[OF ], subst nn_integral_suminf) auto
finally have  .
moreover have
using Q Q_sets
by (subst suminf_emeasure) (auto simp: disjoint_family_on_def sets_eq)
moreover
have
by auto
then have
using in_Q0[of ]  Q by (auto simp: ennreal_top_mult)
moreover have
using Q_sets  by auto
moreover have
using  sets.sets_into_space by auto
ultimately have
using plus_emeasure[of  N ] by (simp add: sets_eq)
with  borel Q show
by (auto simp: subset_eq emeasure_density)
qed
qed

assumes ac:  assumes sets_eq:
shows
proof -
from Ex_finite_integrable_function
obtain h where finite:  and
borel:  and
nn:  and
pos:  and
by auto
let ?T =
let ?MT =
from borel finite nn interpret T: finite_measure ?MT
by (auto intro!: finite_measureI cong: nn_integral_cong simp: emeasure_density)
have
proof (unfold absolutely_continuous_def, safe)
fix A assume
with borel have
with pos sets.sets_into_space have
by (elim eventually_mono) (auto simp: not_le[symmetric])
then have
with ac show
by (auto simp: absolutely_continuous_def)
obtain f where f_borel:   by auto
with nn borel show ?thesis
by (auto intro!: bexI[of _ ] simp: density_density_eq)
qed

subsection

lemma finite_density_unique:
assumes borel:
assumes pos:
and fin:
shows
proof (intro iffI ballI)
fix A assume eq:
with borel show
by (auto intro: density_cong)
next
let ?P =
assume
with borel have eq:
from this[THEN bspec, OF sets.top] fin
have g_fin:  by (simp cong: nn_integral_cong)
{ fix f g assume borel:
and pos:
and g_fin:  and eq:
let ?N =
have N:  using borel by simp
have  using pos
by (intro nn_integral_mono_AE) (auto split: split_indicator)
then have Pg_fin:  using g_fin by (auto simp: top_unique)
have
by (auto intro!: nn_integral_cong simp: indicator_def)
also have
proof (rule nn_integral_diff)
show
using borel N by auto
show
using pos by (auto split: split_indicator)
qed fact
also have
unfolding eq[THEN bspec, OF N] using Pg_fin by auto
finally have
using pos borel nn_integral_PInf_AE[OF borel(2) g_fin]
by (subst (asm) nn_integral_0_iff_AE)
(auto split: split_indicator simp: not_less ennreal_minus_eq_0) }
from this[OF borel pos g_fin eq] this[OF borel(2,1) pos(2,1) fin] eq
show  by auto
qed

lemma (in finite_measure) density_unique_finite_measure:
assumes borel:
assumes pos:
assumes f:
(is )
shows
proof -
let ?D =
let ?N =  and ?N' =
let ?f =  and ?f' =

have ac:
using borel by (auto intro!: absolutely_continuousI_density)
from split_space_into_finite_sets_and_rest[OF this]
obtain Q ::
where Q:
and in_Q0:
and Q_fin:  by force
with borel pos have in_Q0:
and Q_fin:  by (auto simp: emeasure_density subset_eq)

from Q have Q_sets[measurable]:  by auto
let ?D =
have  using borel by auto
have *:
unfolding indicator_def by auto
have  using borel Q_fin Q pos
by (intro finite_density_unique[THEN iffD1] allI)
(auto intro!: f measure_eqI simp: emeasure_density * subset_eq)
moreover have
proof (rule AE_I')
{ fix f ::  assume borel:
and eq:
let ?A =
have
proof (rule null_sets_UN)
fix i ::nat have
using borel by auto
have
unfolding eq[OF ]
by (auto intro!: nn_integral_mono simp: indicator_def)
also have
using  by (auto intro!: nn_integral_cmult_indicator)
also have  using emeasure_real[of ] by (auto simp: ennreal_mult_less_top of_nat_less_top)
finally have  by simp
then show  using in_Q0[OF ]  by auto
qed
also have
by (auto simp: ennreal_Ex_less_of_nat less_top[symmetric])
finally have  by simp }
from this[OF borel(1) refl] this[OF borel(2) f]
have   by simp_all
then show  by (rule null_sets.Un)
show  by (auto simp: indicator_def)
qed
moreover have
by (auto simp: indicator_def)
ultimately have
unfolding AE_all_countable[symmetric]
by eventually_elim (auto split: if_split_asm simp: indicator_def)
then show  by auto
qed

lemma (in sigma_finite_measure) density_unique:
assumes f:
assumes f':
assumes density_eq:
shows
proof -
obtain h where h_borel:
and fin:  and pos:
using Ex_finite_integrable_function by auto
then have h_nn:  by auto
let ?H =
interpret h: finite_measure ?H
using fin h_borel pos
by (intro finite_measureI) (simp cong: nn_integral_cong emeasure_density add: fin)
let ?fM =
let ?f'M =
{ fix A assume
then have
using pos(1) sets.sets_into_space by (force simp: indicator_def)
then have
using h_borel  h_nn by (subst nn_integral_0_iff) auto }
note h_null_sets = this
{ fix A assume
have
using  h_borel h_nn f f'
by (intro nn_integral_density[symmetric]) auto
also have
also have
using  h_borel h_nn f f'
by (intro nn_integral_density) auto
finally have
then have
using  h_borel h_nn f f'
by (subst (asm) (1 2) nn_integral_density[symmetric]) auto }
then have  using h_borel h_nn f f'
by (intro h.density_unique_finite_measure absolutely_continuous_AE[of M]) auto
with AE_space[of M] pos show
unfolding AE_density[OF h_borel] by auto
qed

lemma (in sigma_finite_measure) density_unique_iff:
assumes f:  and f':
shows
using density_unique[OF assms] density_cong[OF f f'] by auto

lemma sigma_finite_density_unique:
assumes borel:
and fin:
shows
proof
assume  with borel show
by (auto intro: density_cong)
next
assume eq:
interpret f: sigma_finite_measure  by fact
from f.sigma_finite_incseq guess A . note cover = this

have
unfolding AE_all_countable
proof
fix i
have
unfolding eq ..
moreover have
using cover(1) cover(3)[of i] borel by (auto simp: emeasure_density subset_eq)
ultimately have
using borel cover(1)
by (intro finite_density_unique[THEN iffD1]) (auto simp: density_density_eq subset_eq)
then show
by auto
qed
with AE_space show
apply eventually_elim
using cover(2)[symmetric]
apply auto
done
qed

lemma (in sigma_finite_measure) sigma_finite_iff_density_finite':
assumes f:
shows
(is )
proof
assume
then interpret N: sigma_finite_measure ?N .
from N.Ex_finite_integrable_function obtain h where
h:   and
fin:
by auto
have
proof (rule AE_I')
have
using f h by (auto intro!: nn_integral_density)
then have
using h(2) by simp
then show
using f h(1) by (auto intro!: nn_integral_PInf[unfolded infinity_ennreal_def] borel_measurable_vimage)
qed auto
then show
using fin by (auto elim!: AE_Ball_mp simp: less_top ennreal_mult_less_top)
next
assume AE:
from sigma_finite guess Q . note Q = this
define A where  for i
{ fix i j have
unfolding A_def using f Q
apply (rule_tac sets.Int)
by (cases i) (auto intro: measurable_sets[OF f(1)]) }
note A_in_sets = this

show
proof (standard, intro exI conjI ballI)
show
by auto
show
using A_in_sets by auto
next
have
by auto
also have  using Q by auto
also have
proof safe
fix x assume x:
show
proof (cases  rule: ennreal_cases)
case top with x show ?thesis unfolding A_def by (auto intro: exI[of _ 0])
next
case (real r)
with ennreal_Ex_less_of_nat[of ] obtain n :: nat where
by auto
also have
by simp
finally show ?thesis
using x real by (auto simp: A_def ennreal_of_nat_eq_real_of_nat intro!: exI[of _ ])
qed
qed (auto simp: A_def)
finally show  by simp
next
fix X assume
then obtain i j where [simp]: by auto
have
proof (cases i)
case 0
have
using AE by (auto simp: A_def )
from nn_integral_cong_AE[OF this] show ?thesis by simp
next
case (Suc n)
then have
by (auto intro!: nn_integral_mono simp: indicator_def A_def ennreal_of_nat_eq_real_of_nat)
also have
using Q by (auto intro!: nn_integral_cmult_indicator)
also have
using Q by (auto simp: ennreal_mult_less_top less_top of_nat_less_top)
finally show ?thesis by simp
qed
then show
using A_in_sets Q f by (auto simp: emeasure_density)
qed
qed

lemma (in sigma_finite_measure) sigma_finite_iff_density_finite:

by (subst sigma_finite_iff_density_finite')
(auto simp: max_def intro!: measurable_If)

subsection

definition RN_deriv ::  where

lemma RN_derivI:
assumes
shows
proof -
have *:
using assms by auto
then have
by (rule someI2_ex) auto
with * show ?thesis
by (auto simp: RN_deriv_def)
qed

lemma borel_measurable_RN_deriv[measurable]:
proof -
{ assume ex:
have 1:
using ex by (rule someI2_ex) auto }
from this show ?thesis
by (auto simp: RN_deriv_def)
qed

lemma density_RN_deriv_density:
assumes f:
shows
by (rule RN_derivI[OF f]) simp

lemma (in sigma_finite_measure) density_RN_deriv:

lemma (in sigma_finite_measure) RN_deriv_nn_integral:
assumes N:
and f:
shows
proof -
have
using N by (simp add: density_RN_deriv)
also have
using f by (simp add: nn_integral_density)
finally show ?thesis by simp
qed

lemma (in sigma_finite_measure) RN_deriv_unique:
assumes f:
and eq:
shows
unfolding eq[symmetric]
by (intro density_unique_iff[THEN iffD1] f borel_measurable_RN_deriv
density_RN_deriv_density[symmetric])

lemma RN_deriv_unique_sigma_finite:
assumes f:
and eq:  and fin:
shows
using fin unfolding eq[symmetric]
by (intro sigma_finite_density_unique[THEN iffD1] f borel_measurable_RN_deriv
density_RN_deriv_density[symmetric])

lemma (in sigma_finite_measure) RN_deriv_distr:
fixes T ::
assumes T:  and T':
and inv:
and ac[simp]:
and N:
shows
proof (rule RN_deriv_unique)
have [simp]:  by fact
note sets_eq_imp_space_eq[OF N, simp]
have measurable_N[simp]:  by (auto simp: measurable_def)
{ fix A assume
with inv T T' sets.sets_into_space[OF this]
have
by (auto simp: measurable_def) }
note eq = this[simp]
{ fix A assume
with inv T T' sets.sets_into_space[OF this]
have
by (auto simp: measurable_def) }
note eq2 = this[simp]
let ?M' =  and ?N' =
interpret M': sigma_finite_measure ?M'
proof
from sigma_finite_countable guess F .. note F = this
show
proof (intro exI conjI ballI)
show *:
using F T' by (auto simp: measurable_def)
show
using F T'[THEN measurable_space] by (auto simp: set_eq_iff)
next
fix X assume
then obtain A where [simp]:  and  by auto
have  using F T'  by auto
moreover
have Fi:  using F  by auto
ultimately show
using F T T'  by (simp add: emeasure_distr)
qed (insert F, auto)
qed
have
using T ac by measurable
then show

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

lemma (in sigma_finite_measure) RN_deriv_finite:
assumes N:  and ac:
shows
proof -
interpret N: sigma_finite_measure N by fact
from N show ?thesis
using sigma_finite_iff_density_finite[OF borel_measurable_RN_deriv, of N] density_RN_deriv[OF ac]
by simp
qed

lemma (in sigma_finite_measure)
assumes N:  and ac:
and f:
shows RN_deriv_integrable:  (is ?integrable)
and RN_deriv_integral:  (is ?integral)
proof -
note ac(2)[simp] and sets_eq_imp_space_eq[OF ac(2), simp]
interpret N: sigma_finite_measure N by fact

have eq:
proof (rule density_cong)
from RN_deriv_finite[OF assms(1,2,3)]
show
by eventually_elim (auto simp: less_top)
qed (insert ac, auto)

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

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

lemma (in sigma_finite_measure) real_RN_deriv:
assumes
assumes ac:
obtains D where
and
and
and
proof
interpret N: finite_measure N by fact

note RN = borel_measurable_RN_deriv density_RN_deriv[OF ac]

let ?RN =

show
using RN by auto

have
using RN(1) by (subst RN(2)[symmetric]) (auto simp: emeasure_density)
also have
by (intro nn_integral_cong) (auto simp: indicator_def)
also have
using RN by (intro nn_integral_cmult_indicator) auto
finally have eq:  .
moreover
have
proof (rule ccontr)
assume
then have
by (auto simp: zero_less_iff_neq_zero)
with eq have  by (simp add: ennreal_mult_eq_top_iff)
with N.emeasure_finite[of ] RN show False by auto
qed
ultimately have
using RN by (intro AE_iff_measurable[THEN iffD2]) (auto simp: less_top[symmetric])
then show
by auto
then have eq:
using ac absolutely_continuous_AE by auto

have
by (subst RN(2)[symmetric]) (auto simp: emeasure_density)
also have
by (intro nn_integral_cong) (auto simp: indicator_def)
finally have
using RN by (subst AE_iff_measurable[OF _ refl]) (auto simp: ac cong: sets_eq_imp_space_eq)
with eq show
by (auto simp: enn2real_positive_iff less_top[symmetric] zero_less_iff_neq_zero)
qed (rule enn2real_nonneg)

lemma (in sigma_finite_measure) RN_deriv_singleton:
assumes ac:
and x:
shows
proof -
from
have
by (auto simp: indicator_def emeasure_density intro!: nn_integral_cong)
with x density_RN_deriv[OF ac] show ?thesis
by (auto simp: max_def)
qed

end