proposition: Lemma ae_pointwise_almost_uniform (f_ : (T -> R)^nat) (g : T -> R) (A : set T) (eps : R): (forall n, measurable_fun A (f_ n)) -> measurable_fun A g -> measurable A -> mu A < +oo -> {ae mu, (forall x, A x -> f_ ^~ x @\oo --> g x)} -> (0 < eps)%R -> exists B, [/\ measurable B, mu B < eps%:E & {uniform A `\` B, f_ @\oo --> g}].
proof: Proof. move=> mf mg mA Afin [C [mC C0 nC] epspos]. have [B [mB Beps Bunif]] : exists B, [/\ d.-measurable B, mu B < eps%:E & {uniform (A `\` C) `\` B, f_ @\oo --> g}]. apply: pointwise_almost_uniform => //. - by move=> n; apply : (measurable_funS mA _ (mf n)) => ? []. - by apply : (measurable_funS mA _ (mg)) => ? []. - by apply: measurableI => //; exact: measurableC. - apply: (le_lt_trans _ Afin); apply: le_measure; rewrite ?inE //. by apply: measurableI => //; exact: measurableC. - by move=> x; rewrite setDE; case => Ax /(subsetC nC); rewrite setCK; exact. exists (B `|` C); split. - exact: measurableU. - by apply: (le_lt_trans _ Beps); rewrite measureU0. - by rewrite setUC -setDDl. 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