From 071cfb78c6597f306d0934fe854e08a6a53017af Mon Sep 17 00:00:00 2001 From: mkerjean Date: Sat, 5 Oct 2024 11:24:10 +0200 Subject: [PATCH] R^o --- theories/ftc.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/ftc.v b/theories/ftc.v index 005270857..018f9f814 100644 --- a/theories/ftc.v +++ b/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.