fix

theories/ftc.v

@@ -615,7 +615,7 @@ Lemma integration_by_parts F G f g a b : (a < b)%R ->
 Proof.
 move=> ab cf Fab Ff cg Gab Gg.
 have cfg : {within `[a, b], continuous (f * G + F * g)%R}.
-apply/subspace_continuousP => x abx; apply: cvgD.
+  apply/subspace_continuousP => x abx; apply: cvgD.
   - apply: cvgM.
     + by move/subspace_continuousP : cf; exact.
     + have := derivable_oo_continuous_bnd_within Gab.

theories/lebesgue_measure.v

@@ -912,8 +912,6 @@ move=> /= _ [_ [a ->]] <-; apply: measurableI => //; apply: open_measurable.
 by rewrite preimage_itv_o_infty; move/lower_semicontinuousP : scif; exact.
 Qed.
 
-Import numFieldNormedType.Exports.
-
 Section standard_measurable_fun.
 Variable R : realType.
 Implicit Types D : set R.
@@ -1630,6 +1628,100 @@ Qed.
 
 End open_itv_cover.
 
+Section egorov.
+Context d {R : realType} {T : measurableType d}.
+Context (mu : {measure set T -> \bar R}).
+
+Local Open Scope ereal_scope.
+
+(*TODO : this generalizes to any metric space with a borel measure*)
+Lemma pointwise_almost_uniform
+    (f : (T -> R)^nat) (g : T -> R) (A : set T) (eps : R) :
+  (forall n, measurable_fun A (f n)) ->
+  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.
+move=> mf mA finA fptwsg epspos; pose h q (z : T) : R := `|f q z - g z|%R.
+have mfunh q : measurable_fun A (h q).
+  apply: measurableT_comp => //; apply: measurable_funB => //.
+  exact: measurable_fun_cvg.
+pose E k n := \bigcup_(i >= 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 => //; exact: 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 0%N => //; rewrite 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 R^o (ball 0%R ek))).
+    apply/open_nbhs_nbhs/(open_nbhs_ball _ (@PosNum _ ek _)).
+    by 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)%:E); first last.
+    by rewrite lte_fin ltr_pdivrMr // ltr_pMr // Rint_ltr_addr1 // Rint1.
+  apply: le_trans.
+    apply: (measure_sigma_subadditive _ (fun k => mE k (badn k)) _ _) => //.
+    exact: bigcup_measurable.
+  apply: le_trans; first last.
+    by apply: (epsilon_trick0 xpredT); rewrite divr_ge0// 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.
+
+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.
+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: measurableI => //; exact: measurableC.
+  - by rewrite (le_lt_trans _ Afin)// le_measure// inE//; exact: measurableD.
+  - 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.
+
+End egorov.
 
 (* This module contains a direct construction of the Lebesgue measure that is
    kept here for archival purpose. The Lebesgue measure is actually defined as
@@ -2461,101 +2553,6 @@ Qed.
 
 End negligible_outer_measure.
 
-Section egorov.
-Context d {R : realType} {T : measurableType d}.
-Context (mu : {measure set T -> \bar R}).
-
-Local Open Scope ereal_scope.
-
-(*TODO : this generalizes to any metric space with a borel measure*)
-Lemma pointwise_almost_uniform
-    (f : (T -> R)^nat) (g : T -> R) (A : set T) (eps : R) :
-  (forall n, measurable_fun A (f n)) ->
-  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.
-move=> mf mA finA fptwsg epspos; pose h q (z : T) : R := `|f q z - g z|%R.
-have mfunh q : measurable_fun A (h q).
-  apply: measurableT_comp => //; apply: measurable_funB => //.
-  exact: measurable_fun_cvg.
-pose E k n := \bigcup_(i >= 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 => //; exact: 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 0%N => //; rewrite 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 R^o (ball 0%R ek))).
-    apply/open_nbhs_nbhs/(open_nbhs_ball _ (@PosNum _ ek _)).
-    by 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)%:E); first last.
-    by rewrite lte_fin ltr_pdivrMr // ltr_pMr // Rint_ltr_addr1 // Rint1.
-  apply: le_trans.
-    apply: (measure_sigma_subadditive _ (fun k => mE k (badn k)) _ _) => //.
-    exact: bigcup_measurable.
-  apply: le_trans; first last.
-    by apply: (epsilon_trick0 xpredT); rewrite divr_ge0// 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.
-
-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.
-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: measurableI => //; exact: measurableC.
-  - by rewrite (le_lt_trans _ Afin)// le_measure// inE//; exact: measurableD.
-  - 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.
-
-End egorov.
-
 Section lebesgue_regularity.
 Local Open Scope ereal_scope.
 Context {R : realType}.
@@ -3017,7 +3014,7 @@ End vitali_theorem.
 Section vitali_theorem_corollary.
 Context {R : realType} (A : set R) (B : nat -> set R).
 
-Lemma vitali_coverS (F : set nat) (O : set R^o) : open O -> A `<=` O ->
+Lemma vitali_coverS (F : set nat) (O : set R) : open O -> A `<=` O ->
   vitali_cover A B F -> vitali_cover A B (F `&` [set k | B k `<=` O]).
 Proof.
 move=> oO AO [Bball ABF]; split => // x Ax r r0.
@@ -3119,7 +3116,7 @@ have [c Hc] : exists c : {posnum R},
       rewrite -measure_bigcup -?ge0_fin_numE//=.
       by move=> i _; exact: vitali_cover_mclosure ABF.
     by move/(@nneseries_tail_cvg _ _ (mem G)); exact.
-  move/fine_cvgP => [_] /(@cvgrPdist_lt _ R^o) /(_ _ e0)[n _ /=] nGe.
+  move/fine_cvgP => [_] /cvgrPdist_lt /(_ _ e0)[n _ /=] nGe.
   have [c nc] : exists c : {posnum R}, forall k,
       (c%:num > (radius (B k))%:num)%R -> (k >= n)%N.
     pose x := (\big[minr/(radius (B 0))%:num]_(i < n.+1) (radius (B i))%:num)%R.