proposition: Lemma measurable_fun_ysection 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 m1 => X mX. have -> : X = \bigcup_n (X `&` (F n `*` setT)). by rewrite -setI_bigcupr -setM_bigcupl -F_T setMTT setIT. apply: ysection_ndseq_closed. move=> m n mn; apply/subsetPset; apply: setIS; apply: setSM => //. exact/subsetPset/F_nd. move=> n; have [? ?] := F_oo n; rewrite -/B. pose m1Fn := mrestr m1 (F_oo n).1. have m1Fn_bounded : exists M, forall X, measurable X -> (m1Fn X < M%:E)%E. exists (fine (m1Fn (F n)) + 1) => Y mY. rewrite [in ltRHS]EFinD lte_spadder// fineK; last first. by rewrite ge0_fin_numE ?measure_ge0// /m1Fn/= /mrestr setIid. by rewrite /m1Fn/= /mrestr setIid le_measure// inE//=; exact: measurableI. pose psi' A := m1Fn \o ysection A. pose B' := [set A | measurable A /\ measurable_fun setT (psi' A)]. have subset_B' : measurable `<=` B' by exact: measurable_prod_subset_ysection. split=> [|_ Y mY]; first by apply: measurableI => //; exact: measurableM. have [_ /(_ measurableT Y mY)] := subset_B' X mX. have ->// : psi' X = m1 \o (ysection (X `&` F n `*` setT)). by apply/funext => y/=; rewrite /psi' setMT ysectionI// ysection_preimage_fst. 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