proposition: Lemma emeasurable_fin_num : measurable (D `&` [set x | f x \is a fin_num]).
proof: Proof. rewrite [X in measurable X](_ : _ = \bigcup_k (D `&` ([set x | - k%:R%:E <= f x] `&` [set x | f x <= k%:R%:E]))). apply: bigcupT_measurable => k; rewrite -(setIid D) setIACA. by apply: measurableI; [exact: emeasurable_fun_c_infty| exact: emeasurable_fun_infty_c]. rewrite predeqE => t; split => [/= [Dt ft]|]. have [ft0|ft0] := leP 0%R (fine (f t)). exists `|ceil (fine (f t))|%N => //=; split => //; split. by rewrite -{2}(fineK ft)// lee_fin (le_trans _ ft0)// lerNl oppr0. by rewrite natr_absz ger0_norm ?ceil_ge0// -(fineK ft) lee_fin ceil_ge. exists `|floor (fine (f t))|%N => //=; split => //; split. rewrite natr_absz ltr0_norm ?floor_lt0// EFinN. by rewrite -{2}(fineK ft) lee_fin mulrNz opprK floor_le. by rewrite -(fineK ft)// lee_fin (le_trans (ltW ft0)). move=> [n _] [/= Dt [nft fnt]]; split => //; rewrite fin_numElt. by rewrite (lt_le_trans _ nft) ?ltNyr//= (le_lt_trans fnt)// ltry. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology numfun normedtype HB(structures) sequences esum measure real_interval realfun exp lebesgue_stieltjes_measure