diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index dc8fdf7201..8983c96269 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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` ### Changed diff --git a/Makefile.common b/Makefile.common index cf974a9017..360f0162c2 100644 --- a/Makefile.common +++ b/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 diff --git a/theories/convex.v b/theories/convex.v index fbd28dd43d..eb668edad5 100644 --- a/theories/convex.v +++ b/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. diff --git a/theories/ftc.v b/theories/ftc.v index d75df24299..69e0931e3a 100644 --- a/theories/ftc.v +++ b/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 `]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. diff --git a/theories/normedtype.v b/theories/normedtype.v index a36ac85f25..5db598078d 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -1298,6 +1298,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. diff --git a/theories/sequences.v b/theories/sequences.v index eead6b72b7..7c31e06f00 100644 --- a/theories/sequences.v +++ b/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 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 n /=; apply: big_nat_widenl. Qed.