generalization of FTC2 (#1446)

* generalization of FTC2

- for continuous function on unbounded intervals

---------

Co-authored-by: IshiguroYoshihiro <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -99,6 +99,17 @@
 
 - in `normedtype.v`:
   + lemmas `ninfty`, `cvgy_compNP`
+- 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`
 
 - new file `measurable_realfun.v`
   + with as contents the first half of the file `lebesgue_measure.v`

Makefile.common

@@ -138,15 +138,14 @@ coq2html:
 	gsed -i 's/Analysis_stdlib/mathcomp\.analysis_stdlib/' depend.dot
 	gsed -i 's/\//\./g' depend.dot
 	../coq2html/tools/generate-hierarchy-graph.sh
-	../coq2html/coq2html \
+	find . -not -path '*/.*' -name "*.v" -or -name "*.glob" | xargs ../coq2html/coq2html \
   -hierarchy-graph hierarchy-graph.dot \
   -dependency-graph depend.dot \
   -title "Mathcomp Analysis" \
   -d html/ -base mathcomp -Q theories analysis \
   -coqlib https://coq.inria.fr/doc/V8.19.2/stdlib/ \
   -external https://math-comp.github.io/htmldoc/ mathcomp.ssreflect \
-  -external https://math-comp.github.io/htmldoc/ mathcomp.algebra \
-  $(find . -not -path '*/.*' -name "*.v" -or -name "*.glob")
+  -external https://math-comp.github.io/htmldoc/ mathcomp.algebra
 
 coq2html-clean:
 	rm -f */*.glob

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,20 +5,39 @@ 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                *)
+(* # Fundamental Theorem of Calculus and Consequences                         *)
 (*                                                                            *)
-(* NB: See CONTRIBUTING.md for an introduction to HB concepts and commands.   *)
+(* This file provides lemmas about derivation and integration. It contains in *)
+(* particular a proof of the first fundamental theorem of calculus for the    *)
+(* Lebesgue integral and its consequences, in particular a corollary to       *)
+(* compute the integral of continuous functions, integration by parts, by     *)
+(* substitution, etc.                                                         *)
 (*                                                                            *)
-(* This file provides a proof of the first fundamental theorem of calculus    *)
-(* for the Lebesgue integral. We derive from this theorem a corollary to      *)
-(* compute the definite integral of continuous functions.                     *)
+(* Reference:                                                                 *)
+(* - R. Affeldt, Z. Stone. A Comprehensive Overview of the Lebesgue           *)
+(*   Differentiation Theorem in Coq. ITP 2024                                 *)
 (*                                                                            *)
+(* Examples of lemmas (with `F` and `G` antiderivatives of `f` and `g`):      *)
+(* - `continuous_FTC2`: $\int_a^b f(x)dx = F(b) - F(a)$                       *)
+(* - `{ge0,le0}_continuous_FTC2y`: $\int_a^\infty f(x)dx = \ell - F(a)$ with  *)
+(*   $\lim_{x\to\infty}F(x)=\ell$ and $f$ non-negative or non-positive        *)
+(* - `integration_by_parts`:                                                  *)
+(*   $\int_a^b F(x)g(x)dx = F(b)G(b) - F(a)G(a) - \int_a^b f(x)G(x)dx$        *)
+(* - `integration_by_substitution_{decreasing,increasing}`:                   *)
+(*   $\int_{F(b)}^{F(a)} G(x)dx = \int_a^b -G(F(x))f(x)dx$                    *)
+(*   with $F$ decreasing,                                                     *)
+(*   $\int_{F(a)}^{F(b)} G(x)dx = \int_a^b G(F(x))f(x)dx$                     *)
+(*   with $F$ increasing                                                      *)
+(*                                                                            *)
+(* Detailed documentation:                                                    *)
+(* ```                                                                        *)
 (*                   partial1of2 f == first partial derivative of f           *)
 (*                                    f has type R -> T -> R for R : realType *)
 (* parameterized_integral mu a x f := \int[mu]_(t \in `[a, x] f t)            *)
+(* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)
 
@@ -771,6 +790,143 @@ rewrite -EFinB -cE -GbFbc /G /Rintegral/= fineK//.
 exact: integral_fune_fin_num.
 Unshelve. all: by end_near. Qed.
 
+Lemma ge0_continuous_FTC2y (f F : R -> R) a (l : R) :
+  (forall x, a <= x -> 0 <= f x)%R ->
+  {within `[a, +oo[, continuous f} ->
+  F x @[x --> +oo%R] --> l ->
+  (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 cf Fxl dF Fa dFE.
+have mf : measurable_fun `]a, +oo[ f.
+  apply: open_continuous_measurable_fun => //.
+  by move: cf => /continuous_within_itvcyP[/in_continuous_mksetP 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 ->
+  {within `[a, +oo[, continuous f} ->
+  F x @[x --> +oo%R] --> l ->
+  (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 cf Fxl dF Fa dFE.
+by rewrite /Rintegral (ge0_continuous_FTC2y f_ge0 cf Fxl dF Fa dFE) -EFinD.
+Qed.
+
+Lemma le0_continuous_FTC2y (f F : R -> R) a (l : R) :
+  (forall x, a <= x -> f x <= 0)%R ->
+  {within `[a, +oo[, continuous f} ->
+  F x @[x --> +oo%R] --> l ->
+  (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 cf Fl 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.
+- move: cf => /continuous_within_itvcyP[cf fa].
+  rewrite continuous_within_itvcyP; split; last exact: cvgN.
+  by move=> x ax; exact/continuousN/cf.
+- exact: cvgN.
+- by move=> x ax; exact/derivableN/dF.
+- exact: cvgN.
+- move=> x ax; rewrite derive1E deriveN.
+    by rewrite -derive1E dFE.
+  by apply: dF; move: ax; rewrite in_itv/= andbT.
+Qed.
+
 End corollary_FTC1.
 
 Section integration_by_parts.

theories/normedtype.v

@@ -1294,6 +1294,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.
@@ -1461,6 +1475,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.