proposition: Lemma epsRN_ex : {eps : {posnum R} | \int[mu]_(x in A) (fRN x + eps%:num%:E) < nu A}.
proof: Proof. have [muA0|] := eqVneq (mu A) 0. exists (PosNum ltr01). under eq_integral. move=> x _; rewrite -(@gee0_abs _ (_ + _)); last first. by rewrite adde_ge0// fRN_ge0. over. rewrite (@integral_abs_eq0 _ _ _ _ setT)//. by rewrite (le_lt_trans _ h)// integral_ge0// => x Ax; exact: fRN_ge0. by apply: emeasurable_funD => //; exact: measurable_fun_fRN. rewrite neq_lt ltNge measure_ge0//= => muA_gt0. pose mid := ((fine (nu A) - fine (\int[mu]_(x in A) fRN x)) / 2)%R. pose e := (mid / fine (mu A))%R. have ? : \int[mu]_(x in A) fRN x \is a fin_num. rewrite ge0_fin_numE// ?(lt_le_trans h)// ?leey// integral_ge0//. by move=> x Ax; exact: fRN_ge0. have e_gt0 : (0 < e)%R. rewrite /e divr_gt0//; last first. by rewrite fine_gt0// muA_gt0/= ltey_eq fin_num_measure. by rewrite divr_gt0// subr_gt0// fine_lt// fin_num_measure. exists (PosNum e_gt0); rewrite ge0_integralD//; last 2 first. by move=> x Ax; exact: fRN_ge0. exact: measurable_funS measurable_fun_fRN. rewrite integral_cst// -lte_subr_addr//; last first. by rewrite fin_numM// fin_num_measure. rewrite -[X in _ * X](@fineK _ (mu A)) ?fin_num_measure//. rewrite -EFinM -mulrA mulVr ?mulr1; last first. by rewrite unitfE gt_eqF// fine_gt0// muA_gt0/= ltey_eq fin_num_measure. rewrite lte_subr_addl// addeC -lte_subr_addl//; last first. rewrite -(@fineK _ (nu A))// ?fin_num_measure// -[X in _ - X](@fineK _)//. rewrite -EFinB lte_fin /mid ltr_pdivrMr// ltr_pMr// ?ltr1n// subr_gt0. by rewrite fine_lt// fin_num_measure. 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