tentative generalization of FTC2

- for continuous function on unbounded intervals

Co-authored-by: IshiguroYoshihiro <jb.15r.1213@s.thers.ac.jp>

CHANGELOG_UNRELEASED.md

@@ -30,6 +30,18 @@
 - in `classical_sets.v`:
   + lemmas `xsectionE`, `ysectionE`
 
+- in `normedtype.v`
+  + global hint to automatically apply `interval_open`
+
+- in `sequences.v`:
+  + lemma `seqDUE`
+  + lemma `nondecreasing_telescope_sumey`
+
+- in `ftc.v`:
+  + lemma `ge0_continuous_FTC2y`
+  + lemma `Rintegral_ge0_continuous_FTC2y`
+  + lemma `le0_continuous_FTC2y`
+
 ### Changed
 
 - in `lebesgue_integrale.v`

theories/convex.v

@@ -213,7 +213,7 @@ have [c2 Ic2 Hc2] : exists2 c2, x < c2 < b & (f b - f x) / (b - x) = 'D_1 f c2.
   have [|z zxb fbfx] := MVT xb derivef.
     apply/(derivable_oo_continuous_bnd_within (And3 xbf _ cvg_left))/cvg_at_right_filter.
     have := derivable_within_continuous HDf.
-    rewrite continuous_open_subspace//; last exact: interval_open.
+    rewrite continuous_open_subspace//.
     by apply; rewrite inE/= in_itv/= ax.
   by exists z => //; rewrite fbfx -mulrA divff ?mulr1// subr_eq0 gt_eqF.
 have [c1 Ic1 Hc1] : exists2 c1, a < c1 < x & (f x - f a) / (x - a) = 'D_1 f c1.
@@ -224,11 +224,10 @@ have [c1 Ic1 Hc1] : exists2 c1, a < c1 < x & (f x - f a) / (x - a) = 'D_1 f c1.
   have [|z zax fxfa] := MVT ax derivef.
     apply/(derivable_oo_continuous_bnd_within (And3 axf cvg_right _))/cvg_at_left_filter.
     have := derivable_within_continuous HDf.
-    rewrite continuous_open_subspace//; last exact: interval_open.
+    rewrite continuous_open_subspace//.
     by apply; rewrite inE/= in_itv/= ax.
   exists z; first by [].
-  rewrite fxfa -mulrA divff; first exact: mulr1.
-  by rewrite subr_eq0 gt_eqF.
+  by rewrite fxfa -mulrA divff ?mulr1// subr_eq0 gt_eqF.
 have c1c2 : c1 < c2.
   by move: Ic2 Ic1 => /andP[+ _] => /[swap] /andP[_] /lt_trans; apply.
 have [d Id h] :
@@ -242,10 +241,10 @@ have [d Id h] :
   have [|z zc1c2 {}h] := MVT c1c2 derivef.
     apply: (derivable_oo_continuous_bnd_within (And3 h _ _)).
     + apply: cvg_at_right_filter.
-      move: cDf; rewrite continuous_open_subspace//; last exact: interval_open.
+      move: cDf; rewrite continuous_open_subspace//.
       by apply; rewrite inE/= in_itv/= (andP Ic1).1 (lt_trans _ (andP Ic2).2).
     + apply: cvg_at_left_filter.
-      move: cDf; rewrite continuous_open_subspace//; last exact: interval_open.
+      move: cDf; rewrite continuous_open_subspace//.
       by apply; rewrite inE/= in_itv/= (andP Ic2).2 (lt_trans (andP Ic1).1).
   exists z; first by [].
   rewrite h -mulrA divff; first exact: mulr1.

theories/ftc.v

@@ -5,7 +5,7 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import cardinality fsbigop signed reals ereal.
 From mathcomp Require Import topology tvs normedtype sequences real_interval.
 From mathcomp Require Import esum measure lebesgue_measure numfun realfun.
-From mathcomp Require Import lebesgue_integral derive charge.
+From mathcomp Require Import itv real_interval lebesgue_integral derive charge.
 
 (**md**************************************************************************)
 (* # Fundamental Theorem of Calculus for the Lebesgue Integral                *)
@@ -594,6 +594,152 @@ rewrite -EFinB -cE -GbFbc /G /Rintegral/= fineK//.
 exact: integral_fune_fin_num.
 Unshelve. all: by end_near. Qed.
 
+(* TODO: move? *)
+Let in_continuous_mkseP {T : realFieldType} {U : realFieldType}
+    (i : interval T) (f : T -> U) :
+  {in i, continuous f} <-> {in [set` i], continuous f}.
+Proof.
+split=> [fi x|fi x xi]; first by rewrite inE/=; exact: fi.
+by apply: fi; rewrite inE.
+Qed.
+
+Lemma ge0_continuous_FTC2y (f F : R -> R) a (l : R) :
+  (forall x, a <= x -> 0 <= f x)%R ->
+  F x @[x --> +oo%R] --> l ->
+  {within `[a, +oo[, continuous f} ->
+  (forall x, a < x -> derivable F x 1)%R -> F x @[x --> a^'+] --> F a ->
+  {in `]a, +oo[, F^`() =1 f} ->
+  (\int[mu]_(x in `[a, +oo[) (f x)%:E = l%:E - (F a)%:E)%E.
+Proof.
+move=> f_ge0 Fxl cf dF Fa dFE.
+have mf : measurable_fun `]a, +oo[ f.
+  apply: open_continuous_measurable_fun => //.
+  by move: cf => /continuous_within_itvcyP[/in_continuous_mkseP cf _].
+rewrite -integral_itv_obnd_cbnd// itv_bnd_infty_bigcup seqDU_bigcup_eq.
+rewrite ge0_integral_bigcup//=; last 3 first.
+- by move=> k; apply: measurableD => //; exact: bigsetU_measurable.
+- by rewrite -seqDU_bigcup_eq -itv_bnd_infty_bigcup; exact: measurableT_comp.
+- move=> x/=; rewrite -seqDU_bigcup_eq -itv_bnd_infty_bigcup/=.
+  by rewrite /= in_itv/= => /andP[/ltW + _]; rewrite lee_fin; exact: f_ge0.
+have dFEn n : {in `]a + n%:R, a + n.+1%:R[, F^`() =1 f}.
+  apply: in1_subset_itv dFE.
+  apply: subset_trans (subset_itvl _) (subset_itvr _) => //=.
+  by rewrite bnd_simp lerDl.
+have liml : limn (EFin \o (fun k => F (a + k%:R))) = l%:E.
+  apply/cvg_lim => //.
+  apply: cvg_EFin; first exact: nearW.
+  apply/((cvg_pinftyP F l).1 Fxl)/cvgryPge => r.
+  by near do rewrite -lerBlDl; exact: nbhs_infty_ger.
+transitivity (\sum_(0 <= i <oo) ((F (a + i.+1%:R))%:E - (F (a + i%:R))%:E)).
+  transitivity (\sum_(0 <= i <oo)
+      \int[mu]_(x in seqDU (fun k => `]a, (a + k%:R)]%classic) i.+1) (f x)%:E).
+    apply/cvg_lim => //; rewrite -cvg_shiftS/=.
+    under eq_cvg.
+      move=> k /=; rewrite big_nat_recl//.
+      rewrite /seqDU addr0 set_itvoc0// set0D integral_set0 add0r.
+      over.
+    apply: cvg_toP => //; apply: is_cvg_nneseries => n _.
+    rewrite integral_ge0//= => x []; rewrite in_itv/= => /andP[/ltW + _] _.
+    by rewrite lee_fin; exact: f_ge0.
+  apply: eq_eseriesr => n _.
+  rewrite seqDUE/= integral_itv_obnd_cbnd; last first.
+    apply: (@measurable_fun_itv_oc _ _ _ false true).
+    apply: open_continuous_measurable_fun => //.
+    move: cf => /continuous_within_itvcyP[cf _] x.
+    rewrite inE/= in_itv/= => /andP[anx _].
+    by apply: cf; rewrite in_itv/= andbT (le_lt_trans _ anx)// lerDl.
+  apply: continuous_FTC2 (dFEn n).
+  - by rewrite ltrD2l ltr_nat.
+  - have : {within `[a, +oo[, continuous f}.
+      apply/continuous_within_itvcyP => //.
+      by move: cf => /continuous_within_itvcyP[].
+    apply: continuous_subspaceW.
+    apply: subset_trans (subset_itvl _) (subset_itvr _) => //=.
+    by rewrite bnd_simp lerDl.
+  - split => /=.
+    + move=> x; rewrite in_itv/= => /andP[anx _].
+      by apply/dF; rewrite (le_lt_trans _ anx)// lerDl.
+    + move: n => [|n]; first by rewrite addr0.
+      have : {within `[a + n.+1%:R, a + n.+2%:R], continuous F}.
+        apply: derivable_within_continuous => /= x.
+        rewrite in_itv/= => /andP[aSn _].
+        by apply: dF; rewrite (lt_le_trans _ aSn)// ltrDl.
+      move/continuous_within_itvP.
+      by rewrite ltrD2l ltr_nat ltnS => /(_ (ltnSn _))[].
+  - have : {within `[a + n%:R + 2^-1, a + n.+1%:R], continuous F}.
+      apply: derivable_within_continuous => x.
+      rewrite in_itv/= => /andP[aSn _].
+      by apply: dF; rewrite (lt_le_trans _ aSn)// -addrA ltrDl ltr_wpDl.
+    move/continuous_within_itvP.
+    suff: (a + n%:R + 2^-1 < a + n.+1%:R)%R by move=> /[swap] /[apply] => -[].
+    by rewrite -[in ltRHS]natr1 addrA ltrD2l invf_lt1// ltr1n.
+rewrite nondecreasing_telescope_sumey.
+- by rewrite addr0 EFinN; congr (_ - _).
+- by rewrite liml.
+- apply/nondecreasing_seqP => n; rewrite -subr_ge0.
+  have isdF (x : R) : x \in `]a + n%:R, a + n.+1%:R[ -> is_derive x 1%R F (f x).
+    rewrite in_itv/= => /andP[anx _].
+    rewrite -dFE; last by rewrite in_itv/= andbT (le_lt_trans _ anx)// lerDl.
+    rewrite derive1E.
+    by apply/derivableP/dF; rewrite (le_lt_trans _ anx)// lerDl.
+  have [| |r ranaSn ->] := MVT _ isdF.
+  + by rewrite ltrD2l ltr_nat.
+  + move : n isdF => [_ |n _].
+    + have : {within `[a, +oo[, continuous F}.
+        apply/continuous_within_itvcyP; split => // x.
+        rewrite in_itv/= andbT => ax.
+        by apply: differentiable_continuous; exact/derivable1_diffP/dF.
+      by apply: continuous_subspaceW; rewrite addr0; exact: subset_itvl.
+    + apply: @derivable_within_continuous => x.
+      rewrite in_itv/= => /andP[aSnx _].
+      by apply: dF; rewrite (lt_le_trans _ aSnx)// ltrDl.
+  + move: ranaSn; rewrite in_itv/= => /andP[/ltW anr _].
+    rewrite mulr_ge0//; last by rewrite subr_ge0 lerD2l ler_nat.
+    by rewrite f_ge0// (le_trans _ anr)// lerDl.
+Unshelve. end_near. Qed.
+
+Lemma Rintegral_ge0_continuous_FTC2y (f F : R -> R) a (l : R) :
+  (forall x, a <= x -> 0 <= f x)%R ->
+  F x @[x --> +oo%R] --> l ->
+  {within `[a, +oo[, continuous f} ->
+  (forall x, a < x -> derivable F x 1)%R -> F x @[x --> a^'+] --> F a ->
+  {in `]a, +oo[, F^`() =1 f} ->
+  (\int[mu]_(x in `[a, +oo[) (f x) = l - F a)%R.
+Proof.
+move=> f_ge0 Fxl cf dF Fa dFE.
+by rewrite /Rintegral (ge0_continuous_FTC2y f_ge0 Fxl cf dF Fa dFE) -EFinD.
+Qed.
+
+Lemma le0_continuous_FTC2y (f F : R -> R) a (l : R) :
+  (forall x, a <= x -> f x <= 0)%R ->
+  F x @[x --> +oo%R] --> l ->
+  {within `[a, +oo[, continuous f} ->
+  (F x @[x --> a^'+] --> F a) ->
+  (forall x, (a < x)%R -> derivable F x 1) ->
+  {in `]a, +oo[, F^`() =1 f} ->
+  \int[mu]_(x in `[a, +oo[) (f x)%:E = l%:E - (F a)%:E.
+Proof.
+move=> f_ge0 Fl cf Fa dF dFE; rewrite -[LHS]oppeK -integralN/=; last first.
+  rewrite adde_defN ge0_adde_def => //=; rewrite inE.
+    rewrite oppe_ge0 le_eqVlt; apply/predU1P; left.
+    apply: integral0_eq => /= x; rewrite in_itv/= => /andP[ax _].
+    by rewrite funeposE -EFin_max; congr EFin; exact/max_idPr/f_ge0.
+  apply: integral_ge0 => /= x; rewrite in_itv/= => /andP[ax _].
+  by rewrite funenegE -fine_max// lee_fin le_max lexx orbT.
+rewrite (@ge0_continuous_FTC2y (- f)%R (- F)%R _ (- l)%R).
+- by rewrite oppeB// EFinN oppeK.
+- by move=> x ax; rewrite oppr_ge0 f_ge0.
+- exact: cvgN.
+- move: cf => /continuous_within_itvcyP[cf fa].
+  rewrite continuous_within_itvcyP; split; last exact: cvgN.
+  by move=> x ax; exact/continuousN/cf.
+- by move=> x ax; exact/derivableN/dF.
+- exact: cvgN.
+- move=> x ax; rewrite derive1E deriveN; last first.
+    by apply: dF; move: ax; rewrite in_itv/= andbT.
+  by rewrite -derive1E dFE.
+Qed.
+
 End corollary_FTC1.
 
 Section integration_by_parts.

theories/normedtype.v

@@ -1290,6 +1290,7 @@ End open_closed_sets.
 #[global] Hint Extern 0 (closed _) => now apply: closed_ge : core.
 #[global] Hint Extern 0 (closed _) => now apply: closed_le : core.
 #[global] Hint Extern 0 (closed _) => now apply: closed_eq : core.
+#[global] Hint Extern 0 (open _) => now apply: interval_open : core.
 
 Section at_left_right.
 Variable R : numFieldType.

theories/sequences.v

@@ -364,6 +364,20 @@ End seqD.
 #[deprecated(since="mathcomp-analysis 1.2.0", note="renamed to `nondecreasing_bigsetU_seqD`")]
 Notation eq_bigsetU_seqD := nondecreasing_bigsetU_seqD (only parsing).
 
+Lemma seqDUE {R : realDomainType} n (r : R) :
+  (seqDU (fun n => `]r, r + n%:R]) n = `]r + n.-1%:R, r + n%:R])%classic.
+Proof.
+rewrite seqDU_seqD; last first.
+  apply/nondecreasing_seqP => k; apply/subsetPset/subset_itvl.
+  by rewrite bnd_simp lerD2l ler_nat.
+move: n => [/=|n]; first by rewrite addr0.
+rewrite eqEsubset; split => x /= /[!in_itv] /=.
+- by move=> [] /andP[-> ->] /[!andbT] /= /negP; rewrite -ltNge.
+- move=> /andP[rnx ->].
+  rewrite andbT; split; first by rewrite (le_lt_trans _ rnx)// lerDl.
+  by apply/negP; rewrite negb_and -ltNge rnx orbT.
+Qed.
+
 (** Convergence of patched sequences *)
 
 Section sequences_patched.
@@ -1554,6 +1568,32 @@ Lemma congr_lim (R : numFieldType) (f g : nat -> \bar R) :
   f = g -> limn f = limn g.
 Proof. by move=> ->. Qed.
 
+Lemma nondecreasing_telescope_sumey (R : realType) n (f : nat -> R) :
+  limn (EFin \o f) \is a fin_num ->
+  {homo f : x y / (x <= y)%N >-> (x <= y)%R} ->
+  \sum_(n <= k <oo) ((f k.+1)%:E - (f k)%:E) = limn (EFin \o f) - (f n)%:E.
+Proof.
+move=> fin_limf ndf.
+have nd_sumf : {homo (fun i => \sum_(n <= k < i) ((f k.+1)%:E - (f k)%:E)) :
+    k m / (k <= m)%N >-> k <= m}.
+  apply/nondecreasing_seqP => m; apply: lee_sum_nneg_natr => // k _ _.
+  by rewrite -EFinB lee_fin subr_ge0 ndf.
+transitivity
+    (ereal_sup (range (fun m => \sum_(n <= k < m) ((f k.+1)%:E - (f k)%:E)%E))).
+  by apply/cvg_lim => //; exact: ereal_nondecreasing_cvgn.
+transitivity (limn ((EFin \o f) \- cst (f n)%:E)); last first.
+  apply/cvg_lim => //; apply: cvgeB.
+  - exact: fin_num_adde_defl.
+  - by apply: ereal_nondecreasing_is_cvgn => x y xy; rewrite lee_fin ndf.
+  - exact: cvg_cst.
+have := @ereal_nondecreasing_cvgn _ _ nd_sumf.
+rewrite -(cvg_restrict n (EFin \o f \- cst (f n)%:E)) => /cvg_lim <-//.
+apply: congr_lim; apply/funext => k/=.
+case: ifPn => //; rewrite -ltnNge => nk.
+under eq_bigr do rewrite EFinN.
+by rewrite telescope_sume// ltnW.
+Qed.
+
 Lemma eseries_cond {R : numFieldType} (f : (\bar R)^nat) P N :
   \sum_(N <= i <oo | P i) f i = \sum_(i <oo | P i && (N <= i)%N) f i.
 Proof. by apply/congr_lim/eq_fun => n /=; apply: big_nat_widenl. Qed.