R^o

theories/ftc.v

@@ -188,9 +188,9 @@ Unshelve. all: by end_near. Qed.
 
 Let FTC0_restrict f a x (u : R) : (x < u)%R ->
   mu.-integrable [set` Interval a (BRight u)] (EFin \o f) ->
-  let F y := (\int[mu]_(t in [set` Interval a (BRight y)]) f t)%R in
+  let F y : R^o := (\int[mu]_(t in [set` Interval a (BRight y)]) f t)%R in
   a < BRight x -> lebesgue_pt f x ->
-  h^-1 *: (F (h + x) - F x) @[h --> 0%R^'] --> f x.
+  h^-1 *: (F (h + x) - F x) @[h --> ((0:R^o)%R^')] --> f x.
 Proof.
 move=> xu + F ax fx.
 rewrite integrable_mkcond//= (restrict_EFin f) => intf.
@@ -204,7 +204,7 @@ apply: cvg_trans; apply: near_eq_cvg; near=> r; congr (_ *: (_ - _)).
   move: yaxr; rewrite /= !in_itv/= inE/= in_itv/= => /andP[->/=].
   move=> /le_trans; apply; rewrite -lerBrDr.
   have [r0|r0] := leP r 0%R; first by rewrite (le_trans r0)// subr_ge0 ltW.
-  by rewrite -(gtr0_norm r0); near: r; apply: dnbhs0_le; rewrite subr_gt0.
+  by rewrite -(gtr0_norm r0); near: r; apply: nbhs0_le; rewrite subr_gt0.
 - apply: eq_Rintegral => y yaxr; rewrite patchE mem_set//=.
   move: yaxr => /=; rewrite !in_itv/= inE/= in_itv/= => /andP[->/=].
   by move=> /le_trans; apply; exact/ltW.