proposition: Lemma radon_nikodym_sigma_finite : nu `<< mu -> exists f : T -> \bar R, [/\ forall x, f x >= 0, forall x, f x \is a fin_num, mu.-integrable [set: T] f & forall A, measurable A -> nu A = \int[mu]_(x in A) f x].
proof: Proof. move=> nu_mu; have [F TF /all_and2[mF muFoo]] := sigma_finiteT mu. pose E := seqDU F. have mE k : measurable (E k). by apply: measurableD => //; exact: bigsetU_measurable. have muEoo k : mu (E k) < +oo. by rewrite (le_lt_trans _ (muFoo k))// le_measure ?inE//; exact: subDsetl. have UET : \bigcup_i E i = [set: T] by rewrite TF [RHS]seqDU_bigcup_eq. have tE := trivIset_seqDU F. pose mu_ j : {finite_measure set T -> \bar R} := [the {finite_measure set _ -> \bar _} of mfrestr (mE j) (muEoo j)]. have nuEoo i : nu (E i) < +oo by rewrite ltey_eq fin_num_measure. pose nu_ j : {finite_measure set T -> \bar R} := [the {finite_measure set _ -> \bar _} of mfrestr (mE j) (nuEoo j)]. have nu_mu_ k : nu_ k `<< mu_ k. by move=> S mS mu_kS0; apply: nu_mu => //; exact: measurableI. have [g_] := choice (fun j => radon_nikodym_finite (nu_mu_ j)). move=> /all_and3[g_ge0 ig_ int_gE]. pose f_ j x := if x \in E j then g_ j x else 0. have f_ge0 k x : 0 <= f_ k x by rewrite /f_; case: ifP. have mf_ k : measurable_fun setT (f_ k). apply: measurable_fun_if => //. - by apply: (measurable_fun_bool true); rewrite preimage_mem_true. - rewrite preimage_mem_true. by apply: measurable_funTS => //; have /integrableP[] := ig_ k. have if_T k : integrable mu setT (f_ k). apply/integrableP; split => //. under eq_integral do rewrite gee0_abs//. rewrite -(setUv (E k)) integral_setU //; last 3 first. - exact: measurableC. - by rewrite setUv. - exact/disj_set2P/subsets_disjoint. rewrite /f_; under eq_integral do rewrite ifT//. rewrite (@eq_measure_integral _ _ _ (E k) (mu_ k)); last first. by move=> A mA AEj; rewrite /mu_ /= /mfrestr /mrestr setIidl. rewrite -int_gE ?inE//. under eq_integral. move=> x /[!inE] /= Ekx; rewrite ifF; last by rewrite memNset. over. by rewrite integral0 ?adde0 ltey_eq fin_num_measure. have int_f_E j S : measurable S -> \int[mu]_(x in S) f_ j x = nu (S `&` E j). move=> mS. have mSIEj := measurableI _ _ mS (mE j). have mSDEj := measurableD mS (mE j). rewrite -{1}(setUIDK S (E j)) (integral_setU _ mSIEj mSDEj)//; last 2 first. - by rewrite setUIDK; exact: (measurable_funS measurableT). - by apply/disj_set2P; rewrite setDE setIACA setICr setI0. rewrite /f_ -(eq_integral _ (g_ j)); last first. by move=> x /[!inE] SIEjx; rewrite /f_ ifT// inE; exact: (@subIsetr _ S). rewrite (@eq_measure_integral _ _ _ (S `&` E j) (mu_ j)); last first. move=> A mA; rewrite subsetI => -[_ ?]; rewrite /mu_ /=. by rewrite /mfrestr /mrestr setIidl. rewrite -int_gE; last exact: measurableI. under eq_integral. move=> x; rewrite inE setDE /= => -[_ Ejx]. rewrite ifF; last by rewrite memNset. over. by rewrite integral0 adde0 /nu_/= /mfrestr /mrestr -setIA setIid. pose f x : \bar R := \sum_(j <oo) f_ j x. have int_f_nuT : \int[mu]_x f x = nu setT. rewrite integral_nneseries//. transitivity (\sum_(n <oo) nu (E n)). by apply: eq_eseriesr => i _; rewrite int_f_E// setTI. rewrite -UET measure_bigcup//. by apply: eq_eseriesl => // x; rewrite in_setT. have mf : measurable_fun setT f by exact: ge0_emeasurable_fun_sum. have fi : mu.-integrable setT f. apply/integrableP; split => //. under eq_integral do (rewrite gee0_abs; last exact: nneseries_ge0). by rewrite int_f_nuT ltey_eq fin_num_measure. have ae_f := integrable_ae measurableT fi. pose f' x := if f x \is a fin_num then f x else 0. have ff' : ae_eq mu setT f f'. case: ae_f => N [mN N0 fN]; exists N; split => //. apply: subset_trans fN; apply: subsetC => z/= /(_ I) fz _. by rewrite /f' fz. have mf' : measurable_fun setT f'. apply: measurable_fun_ifT => //; apply: (measurable_fun_bool true) => /=. by have := emeasurable_fin_num measurableT mf; rewrite setTI. exists f'; split. - by move=> t; rewrite /f'; case: ifPn => // ?; exact: nneseries_ge0. - by move=> t; rewrite /f'; case: ifPn. - apply/integrableP; split => //; apply/abse_integralP => //. move/ae_eq_integral : (ff') => /(_ measurableT mf) <-//. by apply/abse_integralP => //; move/integrableP : fi => []. have nuf A : d.-measurable A -> nu A = \int[mu]_(x in A) f x. move=> mA; rewrite integral_nneseries//; last first. by move=> n; exact: measurable_funTS. rewrite nneseries_esum; last by move=> m _; rewrite integral_ge0. under eq_esum do rewrite int_f_E//. rewrite -nneseries_esum; last first. by move=> n; rewrite measure_ge0//; exact: measurableI. rewrite (@eq_eseriesl _ _ (fun x => x \in [set: nat])); last first. by move=> x; rewrite in_setT. rewrite -measure_bigcup//. - by rewrite -setI_bigcupr UET setIT. - by move=> i _; exact: measurableI. - exact: trivIset_setIl. move=> A mA; rewrite nuf ?inE//; apply: ae_eq_integral => //. - exact/measurable_funTS. - exact/measurable_funTS. - exact: ae_eq_subset ff'. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets cardinality) mathcomp(functions fsbigop set_interval) HB(structures) reals ereal signed topology numfun normedtype sequences esum measure realfun lebesgue_measure lebesgue_integral