proposition: Lemma 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 -> (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 finA fptwsg epspos; pose h q (z : T) : R := `|f_ q z - g z|%R. have mfunh q : measurable_fun A (h q). by apply: measurableT_comp; [exact: measurable_normr |exact: measurable_funB]. pose E k n := \bigcup_(i in [set j | n <= j]%N) (A `&` [set x | h i x >= k.+1%:R^-1]%R). have Einc k : nonincreasing_seq (E k). move=> n m nm; apply/asboolP => z [i] /= /(leq_trans _) mi [? ?]. by exists i => //; apply: mi. have mE k n : measurable (E k n). apply: bigcup_measurable => q /= ?. have -> : [set x | h q x >= k.+1%:R^-1]%R = h q @^-1` `[k.+1%:R^-1, +oo[. by rewrite eqEsubset; split => z; rewrite /= in_itv /= andbT. exact: mfunh. have nEcvg x k : exists n, A x -> (~` (E k n)) x. have [Ax|?] := pselect (A x); last by exists point. have [] := fptwsg _ Ax (interior (ball (g x) k.+1%:R^-1)). by apply: open_nbhs_nbhs; split; [exact: open_interior|exact: nbhsx_ballx]. move=> N _ Nk; exists N.+1 => _; rewrite /E setC_bigcup => i /= /ltnW Ni. apply/not_andP; right; apply/negP; rewrite /h -real_ltNge // distrC. by case: (Nk _ Ni) => _/posnumP[?]; apply; exact: ball_norm_center. have Ek0 k : \bigcap_n (E k n) = set0. rewrite eqEsubset; split => // z /=; suff : (~` \bigcap_n E k n) z by []. rewrite setC_bigcap; have [Az | nAz] := pselect (A z). by have [N /(_ Az) ?] := nEcvg z k; exists N. by exists O; rewrite // /E setC_bigcup => n ? []. have badn' k : exists n, mu (E k n) < ((eps/2) / (2 ^ k.+1)%:R)%:E. pose ek :R := eps/2 / (2 ^ k.+1)%:R. have : mu \o E k @ \oo --> mu set0. rewrite -(Ek0 k); apply: nonincreasing_cvg_mu => //. - by rewrite (le_lt_trans _ finA)// le_measure// ?inE// => ? [? _ []]. - exact: bigcap_measurable. rewrite measure0; case/fine_cvg/(_ (interior (ball 0 ek))%R). apply: open_nbhs_nbhs; split; first exact: open_interior. by apply: nbhsx_ballx; rewrite !divr_gt0. move=> N _ /(_ N (leqnn _))/interior_subset muEN; exists N; move: muEN. rewrite /ball /= distrC subr0 ger0_norm // -[x in x < _]fineK ?ge0_fin_numE//. by rewrite (le_lt_trans _ finA)// le_measure// ?inE// => ? [? _ []]. pose badn k := projT1 (cid (badn' k)); exists (\bigcup_k (E k (badn k))); split. - exact: bigcup_measurable. - apply: (@le_lt_trans _ _ (eps/2)%R%:E); first last. by rewrite lte_fin ltr_pdivrMr // ltr_pMr // Rint_ltr_addr1 // ?Rint1. apply: le_trans. apply: (measure_sigma_sub_additive _ (fun k => mE k (badn k)) _ _) => //. exact: bigcup_measurable. apply: le_trans; first last. by apply: (@epsilon_trick0 R _ xpredT); rewrite divr_ge0 //; exact: ltW. by rewrite lee_nneseries // => n _; exact/ltW/(projT2 (cid (badn' _))). apply/uniform_restrict_cvg => /= U /=; rewrite !uniform_nbhsT. case/nbhs_ex => del /= ballU; apply: filterS; first by move=> ?; exact: ballU. have [N _ /(_ N)/(_ (leqnn _)) Ndel] := near_infty_natSinv_lt del. exists (badn N) => // r badNr x. rewrite /patch; case: ifPn => // /set_mem xAB; apply: (lt_trans _ Ndel). move: xAB; rewrite setDE => -[Ax]; rewrite setC_bigcup => /(_ N I). rewrite /E setC_bigcup => /(_ r) /=; rewrite /h => /(_ badNr) /not_andP[]//. by move/negP; rewrite ltNge // distrC. 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