specialized lemma

math-comp · Jul 3, 2024 · 130a44f · 130a44f
1 parent 2b875af
commit 130a44f
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 0 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -25,6 +25,7 @@
     `completed_caratheodory_measurable`
 - in `ftc.v`:
   + lemma `FTC1` (specialization of the previous `FTC1` lemma, now renamed to `FTC1_lebesgue_pt`)
+  + lemma `FTC1Ny`
 
 ### Changed
 

diff --git a/theories/ftc.v b/theories/ftc.v
@@ -205,6 +205,15 @@ 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} ->