proposition: Lemma radon_nikodym_finite : nu `<< mu -> exists f : T -> \bar R, [/\ forall x, f x >= 0, mu.-integrable [set: T] f & forall E, measurable E -> nu E = \int[mu]_(x in E) f x].
proof: Proof. move=> nu_mu; exists f; split. - by move=> x; exact: f_ge0. - by apply/integrableP; split; [exact: mf|exact: int_fRN_lty]. move=> // A mA. apply/eqP; rewrite eq_le int_fRN_ub// andbT leNgt; apply/negP => abs. pose sigma : {charge set T -> \bar R} := [the {charge set T -> \bar R} of sigmaRN mA abs]. have [P [N [[mP posP] [mN negN] PNX PN0]]] := Hahn_decomposition sigma. pose AP := A `&` P. have mAP : measurable AP by exact: measurableI. have muAP_gt0 : 0 < mu AP. rewrite lt0e measure_ge0// andbT. apply/eqP/(contra_not (nu_mu _ mAP))/eqP; rewrite gt_eqF//. rewrite (@lt_le_trans _ _ (sigma AP))//. rewrite (@lt_le_trans _ _ (sigma A))//; last first. rewrite (charge_partition _ _ mP mN)// gee_addl//. by apply: negN => //; exact: measurableI. by rewrite sube_gt0// (proj2_sig (epsRN_ex mA abs)). rewrite /sigma/= /sigmaRN lee_subel_addl ?fin_num_measure//. by rewrite lee_paddl// integral_ge0// => x _; rewrite adde_ge0//; exact: f_ge0. pose h x := if x \in AP then f x + (epsRN mA abs)%:num%:E else f x. have mh : measurable_fun setT h. apply: measurable_fun_if => //. - by apply: (measurable_fun_bool true); rewrite preimage_mem_true. - by apply: measurable_funTS; apply: emeasurable_funD => //; exact: mf. - by apply: measurable_funTS; exact: mf. have hge0 x : 0 <= h x. by rewrite /h; case: ifPn => [_|?]; [rewrite adde_ge0// f_ge0|exact: f_ge0]. have hnuP S : measurable S -> S `<=` AP -> \int[mu]_(x in S) h x <= nu S. move=> mS SAP. have : 0 <= sigma S. by apply: posP => //; apply: (subset_trans SAP); exact: subIsetr. rewrite sube_ge0; last by rewrite fin_num_measure// orbT. apply: le_trans; rewrite le_eqVlt; apply/orP; left; apply/eqP. rewrite -{1}(setIid S) integral_mkcondr; apply/eq_integral => x /[!inE] Sx. by rewrite /restrict /h !ifT// inE//; exact: SAP. have hnuN S : measurable S -> S `<=` ~` AP -> \int[mu]_(x in S) h x <= nu S. move=> mS ScAP; rewrite /h; under eq_integral. move=> x xS; rewrite ifF; last first. by apply/negbTE; rewrite notin_set; apply: ScAP; apply: set_mem. over. exact: int_fRN_ub. have hnu S : measurable S -> \int[mu]_(x in S) h x <= nu S. move=> mS. rewrite -(setD0 S) -(setDv AP) setDDr. have mSIAP : measurable (S `&` AP) by exact: measurableI. have mSDAP : measurable (S `\` AP) by exact: measurableD. rewrite integral_setU //. - rewrite measureU//. by apply: leeD; [exact: hnuN|exact: hnuP]. by rewrite setDE setIACA setICl setI0. - exact: measurable_funTS. - by rewrite disj_set2E setDE setIACA setICl setI0. have int_h_M : \int[mu]_x h x > M. have mCAP := measurableC mAP. have disj_AP : [disjoint AP & ~` AP] by exact/disj_set2P/setICr. rewrite -(setUv AP) integral_setU ?setUv// /h. under eq_integral do rewrite ifT//. under [X in _ < _ + X]eq_integral. by move=> x; rewrite inE /= => xE0p; rewrite memNset//; over. rewrite ge0_integralD//; last 2 first. - by move=> x _; exact: f_ge0. - by apply: measurable_funTS; exact: mf. rewrite integral_cst // addeAC -integral_setU//; last 2 first. by rewrite setUv//; exact: mf. by move=> x _; exact: f_ge0. rewrite setUv int_fRNE -lte_subel_addl; last first. rewrite ge0_fin_numE// ?sup_int_approxRN_lty//. exact: approxRN_seq.sup_int_approxRN_lty. exact: sup_int_approxRN_ge0. by rewrite /M subee ?mule_gt0// approxRN_seq.sup_int_approxRN_fin_num. have Gh : G h. split=> //; apply/integrableP; split => //. under eq_integral do rewrite gee0_abs//. by rewrite (le_lt_trans (hnu _ measurableT))// ltey_eq fin_num_measure. have : \int[mu]_x h x <= M. rewrite -(ereal_sup1 (\int[mu]_x h x)). rewrite (@le_ereal_sup _ [set \int[mu]_x h x] (int_approxRN mu nu))//. by rewrite sub1set inE; exists h. by rewrite leNgt int_h_M. 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