ae corollary of FTC1

CHANGELOG_UNRELEASED.md

@@ -23,6 +23,9 @@
   + definition `completed_algebra_gen`
   + lemmas `g_sigma_completed_algebra_genE`, `negligible_sub_caratheodory`,
     `completed_caratheodory_measurable`
+- in `ftc.v`:
+  + lemma `FTC1` (specialization of the previous `FTC1` lemma, now renamed to `FTC1_lebesgue_pt`)
+  + lemma `FTC1Ny`
 
 ### Changed
 
@@ -52,6 +55,9 @@
   + `lee_ndivr_mulr` -> `lee_ndivrMr`
   + `eqe_pdivr_mull` -> `eqe_pdivrMl`
 
+- in `ftc.v`:
+  + `FTC1` -> `FTC1_lebesgue_pt`
+
 ### Generalized
 
 ### Deprecated

theories/ftc.v

@@ -23,7 +23,7 @@ Local Open Scope ring_scope.
 
 Section FTC.
 Context {R : realType}.
-Notation mu := lebesgue_measure.
+Notation mu := (@lebesgue_measure R).
 Local Open Scope ereal_scope.
 Implicit Types (f : R -> R) (a : itv_bound R).
 
@@ -179,7 +179,7 @@ apply: cvg_at_right_left_dnbhs.
 Unshelve. all: by end_near. Qed.
 
 (* NB: right-closed interval *)
-Lemma FTC1 f a : mu.-integrable setT (EFin \o f) ->
+Lemma FTC1_lebesgue_pt f a : mu.-integrable setT (EFin \o f) ->
   let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in
   forall x, a < BRight x -> lebesgue_pt f x ->
   derivable F x 1 /\ F^`() x = f x.
@@ -191,26 +191,41 @@ have /= := FTC0 intf ax fx.
 set g := (f in f n @[n --> _] --> _ -> _).
 set h := (f in _ -> f n @[n --> _] --> _).
 suff : g = h by move=> <-.
-by apply/funext => y;rewrite /g /h /= [X in F (X + _)](mulr1).
+by apply/funext => y;rewrite /g /h /= [X in F (X + _)]mulr1.
+Qed.
+
+Corollary FTC1 f a : mu.-integrable setT (EFin \o f) ->
+  let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in
+  {ae mu, forall x, a < BRight x -> derivable F x 1 /\ F^`() x = f x}.
+Proof.
+move=> intf F.
+have /lebesgue_differentiation : locally_integrable setT f.
+  by apply: integrable_locally => //; exact: openT.
+apply: filterS; first exact: (ae_filter_ringOfSetsType mu).
+by move=> i fi ai; apply: FTC1_lebesgue_pt => //; rewrite ltNyr.
+Qed.
+
+Corollary FTC1Ny f : mu.-integrable setT (EFin \o f) ->
+  let F x := (\int[mu]_(t in [set` `]-oo, x]]) (f t))%R in
+  {ae mu, forall x, derivable F x 1 /\ F^`() x = f x}.
+Proof.
+move=> intf F; have := FTC1 -oo%O intf.
+apply: filterS; first exact: (ae_filter_ringOfSetsType mu).
+by move=> r /=; apply; rewrite ltNyr.
 Qed.
 
 Corollary continuous_FTC1 f a : mu.-integrable setT (EFin \o f) ->
   let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) (f t))%R in
   forall x, a < BRight x -> {for x, continuous f} ->
   derivable F x 1 /\ F^`() x = f x.
 Proof.
-move=> fi F x ax fx.
-have lfx : lebesgue_pt f x.
-  near (0%R:R)^'+ => e.
-  apply: (@continuous_lebesgue_pt _ _ _ (ball x e)).
+move=> fi F x ax fx; have lfx : lebesgue_pt f x.
+  near (0%R:R)^'+ => e; apply: (@continuous_lebesgue_pt _ _ _ (ball x e)).
   - exact: ball_open_nbhs.
   - exact: measurable_ball.
-  - case/integrableP : fi => + _.
-    by move/EFin_measurable_fun; exact: measurable_funS.
+  - by apply/measurable_funTS/EFin_measurable_fun; exact: measurable_int fi.
   - exact: fx.
-have lif : locally_integrable setT f.
-  by apply: integrable_locally => //; exact: openT.
-have /= /(_ ax lfx)/= [dfx f'xE] := @FTC1 f a fi x.
+have /= /(_ ax lfx)/= [dfx f'xE] := @FTC1_lebesgue_pt f a fi x.
 by split; [exact: dfx|rewrite f'xE].
 Unshelve. all: by end_near. Qed.