proposition: Lemma measurable_fun_xsection A : measurable A -> measurable_fun setT (phi A).
proof: Proof. move: A; suff : measurable `<=` B by move=> + A => /[apply] -[]. have /sigma_finiteP [F [F_T F_nd F_oo]] := sigma_finiteT m2 => X mX. have -> : X = \bigcup_n (X `&` (setT `*` F n)). by rewrite -setI_bigcupr -setM_bigcupr -F_T setMTT setIT. apply: xsection_ndseq_closed. move=> m n mn; apply/subsetPset; apply: setIS; apply: setSM => //. exact/subsetPset/F_nd. move=> n; rewrite -/B; have [? ?] := F_oo n. pose m2Fn := mrestr m2 (F_oo n).1. have m2Fn_bounded : exists M, forall X, measurable X -> (m2Fn X < M%:E)%E. exists (fine (m2Fn (F n)) + 1) => Y mY. rewrite [in ltRHS]EFinD lte_spadder// fineK; last first. by rewrite ge0_fin_numE ?measure_ge0//= /m2Fn /mrestr setIid. by rewrite /m2Fn /mrestr/= setIid le_measure// inE//; exact: measurableI. pose phi' A := m2Fn \o xsection A. pose B' := [set A | measurable A /\ measurable_fun setT (phi' A)]. have subset_B' : measurable `<=` B' by exact: measurable_prod_subset_xsection. split=> [|_ Y mY]; first by apply: measurableI => //; exact: measurableM. have [_ /(_ measurableT Y mY)] := subset_B' X mX. have ->// : phi' X = m2 \o xsection (X `&` setT `*` F n). by apply/funext => x/=; rewrite /phi' setTM xsectionI xsection_preimage_snd. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun