From c8df1b0ff4ec565e081ec38adafa3833abb5e458 Mon Sep 17 00:00:00 2001 From: ndslusarz Date: Mon, 28 Oct 2024 11:43:28 +0000 Subject: [PATCH 1/9] lhopital + cauchy mvt --- theories/realfun.v | 231 ++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 230 insertions(+), 1 deletion(-) diff --git a/theories/realfun.v b/theories/realfun.v index bb902bfa2..9763955b3 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -63,7 +63,7 @@ Notation "'nonincreasing_fun' f" := ({homo f : n m / (n <= m)%O >-> (n >= m)%O}) Notation "'increasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n <= m)%O}) (at level 10). Notation "'decreasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n >= m)%O}) - (at level 10). + (at level 10). Lemma nondecreasing_funN {R : realType} a b (f : R -> R) : {in `[a, b] &, nondecreasing_fun f} <-> @@ -2544,3 +2544,232 @@ apply/continuous_within_itvP => //; split. Qed. End variation_continuity. + +Section Cauchy_MVT. +Context {R : realType}. +Variables (f df g dg : R -> R) (a b c : R). +Hypothesis ab : a < b. +Hypotheses (cf : {within `[a, b], continuous f}) + (cg : {within `[a, b], continuous g}). +Hypotheses (fdf : forall x, x \in `]a, b[%R -> is_derive x 1 f (df x)) + (gdg : forall x, x \in `]a, b[%R -> is_derive x 1 g (dg x)). +Hypotheses (dg0 : forall x, x \in `]a, b[%R -> dg x != 0). + +Lemma cauchy_MVT : + exists2 c, c \in `]a, b[%R & df c / dg c = (f b - f a) / (g b - g a). +Proof. +have [r] := MVT ab gdg cg; rewrite in_itv/= => /andP[ar rb] dgg. +have gba0 : g b - g a != 0. + by rewrite dgg mulf_neq0 ?dg0 ?in_itv/= ?ar// subr_eq0 gt_eqF. +pose h (x : R) := f x - ((f b - f a) / (g b - g a)) * g x. +have hder x : x \in `]a, b[%R -> derivable h x 1. + move=> xab; apply: derivableB => /=. + exact: (@ex_derive _ _ _ _ _ _ _ (fdf xab)). + by apply: derivableM => //; exact: (@ex_derive _ _ _ _ _ _ _ (gdg xab)). +have ch : {within `[a, b], continuous h}. + rewrite continuous_subspace_in => x xab. + by apply: cvgB; [exact: cf|apply: cvgM; [exact: cvg_cst|exact: cg]]. +have /(Rolle ab hder ch)[x xab derh] : h a = h b. + rewrite /h; apply/eqP; rewrite subr_eq eq_sym -addrA eq_sym addrC -subr_eq. + rewrite -mulrN -mulrDr -(addrC (g a)) -[X in _ * X]opprB mulrN -mulrA. + by rewrite mulVf// mulr1 opprB. +pose dh (x : R) := df x - (f b - f a) / (g b - g a) * dg x. +have his_der y : y \in `]a, b[%R -> is_derive x 1 h (dh x). + by move=> yab; apply: is_deriveB; [exact: fdf|apply: is_deriveZ; exact: gdg]. +exists x => //. +have := @derive_val _ R _ _ _ _ _ (his_der _ xab). +have -> := @derive_val _ R _ _ _ _ _ derh. +move=> /eqP; rewrite eq_sym subr_eq add0r => /eqP ->. +by rewrite -mulrA divff ?mulr1//; exact: dg0. +Qed. + +End Cauchy_MVT. + +Section lhopital. +Context {R : realType}. +Variables (f df g dg : R -> R) (a : R) (U : set R) (Ua : nbhs a U). +Hypotheses (fdf : forall x, x \in U -> is_derive x 1 f (df x)) + (gdg : forall x, x \in U -> is_derive x 1 g (dg x)). +Hypotheses (fa0 : f a = 0) (ga0 : g a = 0) + (cdg : \forall x \near a^', dg x != 0). + +Lemma lhopital_right (l : R) : + df x / dg x @[x --> a^'+] --> l -> f x / g x @[x --> a^'+] --> l. +Proof. +case: cdg => r/= r0 cdg'. +move: Ua; rewrite filter_of_nearI => -[D /= D0 aDU]. +near a^'+ => b. +have abf x : x \in `]a, b[%R -> {within `[a, x], continuous f}. + rewrite in_itv/= => /andP[ax xb]. + apply: derivable_within_continuous => y; rewrite in_itv/= => /andP[ay yx]. + apply: ex_derive. + apply: fdf. + rewrite inE; apply: aDU => /=. + rewrite ler0_norm? subr_le0//. + rewrite opprD opprK addrC ltrBlDr (le_lt_trans yx)// (lt_trans xb)//. + near: b; apply: nbhs_right_lt. + by rewrite ltrDr. +have abg x : x \in `]a, b[%R -> {within `[a, x], continuous g}. + rewrite in_itv/= => /andP[ax xb]. + apply: derivable_within_continuous => y; rewrite in_itv/= => /andP[ay yx]. + apply: ex_derive. + apply: gdg. + rewrite inE; apply: aDU => /=. + rewrite ler0_norm? subr_le0//. + rewrite opprD opprK addrC ltrBlDr (le_lt_trans yx)// (lt_trans xb)//. + near: b; apply: nbhs_right_lt. + by rewrite ltrDr. +have fdf' y : y \in `]a, b[%R -> is_derive y 1 f (df y). + rewrite in_itv/= => /andP[ay yb]; apply: fdf. + rewrite inE; apply: aDU => /=. + rewrite ltr0_norm ?subr_lt0//. + rewrite opprD opprK addrC ltrBlDr (lt_le_trans yb)//. + near: b; apply: nbhs_right_le. + by rewrite ltrDr. +have gdg' y : y \in `]a, b[%R -> is_derive y 1 g (dg y). + rewrite in_itv/= => /andP[ay yb]; apply: gdg. + rewrite inE; apply: aDU => /=. + rewrite ltr0_norm ?subr_lt0//. + rewrite opprD opprK addrC ltrBlDr (lt_le_trans yb)//. + near: b; apply: nbhs_right_le. + by rewrite ltrDr. +have {}dg0 y : y \in `]a, b[%R -> dg y != 0. + rewrite in_itv/= => /andP[ay yb]. + apply: (cdg' y) => /=; last by rewrite gt_eqF. + rewrite ltr0_norm; last by rewrite subr_lt0. + rewrite opprB ltrBlDl (lt_trans yb)//. + near: b; apply: nbhs_right_lt. + by rewrite ltrDl. +move=> fgal. +have L : \forall x \near a^'+, + exists2 c, c \in `]a, x[%R & df c / dg c = f x / g x. + near=> x. + have /andP[ax xb] : a < x < b by exact/andP. + have {}fdf' y : y \in `]a, x[%R -> is_derive y 1 f (df y). + rewrite !in_itv/= => /andP[ay yx]. + by apply: fdf'; rewrite in_itv/= ay/= (lt_trans yx). + have {}gdg' y : y \in `]a, x[%R -> is_derive y 1 g (dg y). + rewrite !in_itv/= => /andP[ay yx]. + by apply: gdg'; rewrite in_itv/= ay/= (lt_trans yx). + have {}dg0 y : y \in `]a, x[%R -> dg y != 0. + rewrite in_itv/= => /andP[ya yx]. + by apply: dg0; rewrite in_itv/= ya/= (lt_trans yx). + have {}axf : {within `[a, x], continuous f}. + rewrite continuous_subspace_in => y; rewrite inE/= in_itv/= => /andP[ay yx]. + by apply: abf; rewrite in_itv/= xb andbT. + have {}axg : {within `[a, x], continuous g}. + rewrite continuous_subspace_in => y; rewrite inE/= in_itv/= => /andP[ay yx]. + by apply: abg; rewrite in_itv/= xb andbT. + have := @cauchy_MVT _ f df g dg _ _ ax axf axg fdf' gdg' dg0. + by rewrite fa0 ga0 2!subr0. +apply/cvgrPdist_le => /= e e0. +move/cvgrPdist_le : fgal. +move=> /(_ _ e0)[r'/= r'0 fagl]. +case: L => d /= d0 L. +near=> t. +have /= := L t. +have atd : `|a - t| < d. + rewrite ltr0_norm; last by rewrite subr_lt0. + rewrite opprB ltrBlDl. + near: t; apply: nbhs_right_lt. + by rewrite ltrDl. +have at_ : a < t by []. +move=> /(_ atd)/(_ at_)[c]; rewrite in_itv/= => /andP[ac ct <-]. +apply: fagl => //=. +rewrite ltr0_norm; last by rewrite subr_lt0. +rewrite opprB ltrBlDl (lt_trans ct)//. +near: t; apply: nbhs_right_lt. +by rewrite ltrDl. +Unshelve. all: by end_near. Qed. + +Lemma lhopital_left (l : R) : + df x / dg x @[x --> a^'-] --> l -> f x / g x @[x --> a^'-] --> l. +Proof. +case: cdg => r/= r0 cdg'. +move: Ua; rewrite filter_of_nearI => -[D /= D0 aDU]. +near a^'- => b. +have baf x : x \in `]b, a[%R -> {within `[x, a], continuous f}. + rewrite in_itv/= => /andP[bx xa]. + apply: derivable_within_continuous => y; rewrite in_itv/= => /andP[xy ya]. + apply: ex_derive. + apply: fdf. + rewrite inE; apply: aDU => /=. + rewrite ger0_norm ?subr_ge0//. + rewrite ltrBlDr -ltrBlDl (lt_le_trans _ xy)// (le_lt_trans _ bx)//. + near: b; apply: nbhs_left_ge. + by rewrite ltrBlDl ltrDr. +have bag x : x \in `]b, a[%R -> {within `[x, a], continuous g}. + rewrite in_itv/= => /andP[bx xa]. + apply: derivable_within_continuous => y; rewrite in_itv/= => /andP[xy ya]. + apply: ex_derive. + apply: gdg. + rewrite inE; apply: aDU => /=. + rewrite ger0_norm ?subr_ge0//. + rewrite ltrBlDr -ltrBlDl (lt_le_trans _ xy)// (lt_trans _ bx)//. + near: b; apply: nbhs_left_gt. + by rewrite ltrBlDl ltrDr. +have fdf' y : y \in `]b, a[%R -> is_derive y 1 f (df y). + rewrite in_itv/= => /andP[by_ ya]; apply: fdf. + rewrite inE. + apply: aDU => /=. + rewrite gtr0_norm ?subr_gt0//. + rewrite ltrBlDl -ltrBlDr (le_lt_trans _ by_)//. + near: b; apply: nbhs_left_ge. + by rewrite ltrBlDr ltrDl. +have gdg' y : y \in `]b, a[%R -> is_derive y 1 g (dg y). + rewrite in_itv/= => /andP[by_ ya]; apply: gdg. + rewrite inE; apply: aDU => /=. + rewrite gtr0_norm ?subr_gt0//. + rewrite ltrBlDl -ltrBlDr (le_lt_trans _ by_)//. + near: b; apply: nbhs_left_ge. + by rewrite ltrBlDr ltrDl. +have {}dg0 y : y \in `]b, a[%R -> dg y != 0. + rewrite in_itv/= => /andP[by_ ya]. + apply: (cdg' y) => /=; last by rewrite lt_eqF. + rewrite gtr0_norm; last by rewrite subr_gt0. + rewrite ltrBlDr -ltrBlDl (lt_trans _ by_)//. + near: b; apply: nbhs_left_gt. + by rewrite ltrBlDl ltrDr. +move=> fgal. +have L : \forall x \near a^'-, + exists2 c, c \in `]x, a[%R & df c / dg c = f x / g x. + near=> x. + have /andP[bx xa] : b < x < a by exact/andP. + have {}fdf' y : y \in `]x, a[%R -> is_derive y 1 f (df y). + rewrite in_itv/= => /andP[xy ya]. + by apply: fdf'; rewrite in_itv/= ya andbT (lt_trans bx). + have {}gdg' y : y \in `]x, a[%R -> is_derive y 1 g (dg y). + rewrite in_itv/= => /andP[xy ya]. + by apply: gdg'; rewrite in_itv/= ya andbT (lt_trans _ xy). + have {}dg0 y : y \in `]x, a[%R -> dg y != 0. + rewrite in_itv/= => /andP[xy ya]. + by apply: dg0; rewrite in_itv/= ya andbT (lt_trans bx). + have {}xaf : {within `[x, a], continuous f}. + rewrite continuous_subspace_in => y; rewrite inE/= in_itv/= => /andP[xy ya]. + by apply: baf; rewrite in_itv/= bx. + have {}xag : {within `[x, a], continuous g}. + rewrite continuous_subspace_in => y; rewrite inE/= in_itv/= => /andP[xy ya]. + by apply: bag; rewrite in_itv/= bx. + have := @cauchy_MVT _ f df g dg _ _ xa xaf xag fdf' gdg' dg0. + by rewrite fa0 ga0 !sub0r divrN mulNr opprK. +apply/cvgrPdist_le => /= e e0. +move/cvgrPdist_le : fgal. +move=> /(_ _ e0)[r'/= r'0 fagl]. +case: L => d /= d0 L. +near=> t. +have /= := L t. +have atd : `|a - t| < d. + rewrite gtr0_norm; last by rewrite subr_gt0. + rewrite ltrBlDr -ltrBlDl. + near: t; apply: nbhs_left_gt. + by rewrite ltrBlDl ltrDr. +have ta : t < a by []. +move=> /(_ atd)/(_ ta)[c]; rewrite in_itv/= => /andP[tc ca <-]. +apply: fagl => //=. +rewrite gtr0_norm; last by rewrite subr_gt0. +rewrite ltrBlDr -ltrBlDl (lt_trans _ tc)//. +near: t; apply: nbhs_left_gt. +by rewrite ltrBlDl ltrDr. +Unshelve. all: by end_near. Qed. + +End lhopital. From 5e0b0dbd0d44b26053b42edac523ad09eeed49d1 Mon Sep 17 00:00:00 2001 From: ndslusarz Date: Mon, 28 Oct 2024 23:54:56 +0000 Subject: [PATCH 2/9] headings --- theories/realfun.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/theories/realfun.v b/theories/realfun.v index 9763955b3..39465ec35 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -41,6 +41,9 @@ From HB Require Import structures. (* lime_sup f a/lime_inf f a == limit sup/inferior of the extended real- *) (* valued function f at point a *) (* ``` *) +(* cauchy_MVT == Cauchy's mean value theorem *) +(* lhopital_right == L'Hopital rule (limit taken on the right) *) +(* lhopital_left == L'Hopital rule (limit taken on the left) *) (* *) (******************************************************************************) @@ -63,7 +66,7 @@ Notation "'nonincreasing_fun' f" := ({homo f : n m / (n <= m)%O >-> (n >= m)%O}) Notation "'increasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n <= m)%O}) (at level 10). Notation "'decreasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n >= m)%O}) - (at level 10). + (at level 10). Lemma nondecreasing_funN {R : realType} a b (f : R -> R) : {in `[a, b] &, nondecreasing_fun f} <-> From 6835511ce06b709219d0bfc101b320ec2fdcad86 Mon Sep 17 00:00:00 2001 From: ndslusarz Date: Tue, 29 Oct 2024 00:03:48 +0000 Subject: [PATCH 3/9] updated changelog --- CHANGELOG_UNRELEASED.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 03c90f7b0..73c076eaf 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -57,6 +57,11 @@ `locally_compact_completely_regular`, and `completely_regular_regular`. +- in file `realfun.v`, + + new lemmas `cauchy_MVT`, + `lhopital_right`, and + `lhopital_left`. + ### Changed - in file `normedtype.v`, From e6ca69750e260ceeb4a582002ba13f8fbae1742a Mon Sep 17 00:00:00 2001 From: ndslusarz Date: Fri, 15 Nov 2024 17:46:52 +0000 Subject: [PATCH 4/9] deduplicating into lemma --- theories/realfun.v | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/theories/realfun.v b/theories/realfun.v index 39465ec35..804726610 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -2558,12 +2558,17 @@ Hypotheses (fdf : forall x, x \in `]a, b[%R -> is_derive x 1 f (df x)) (gdg : forall x, x \in `]a, b[%R -> is_derive x 1 g (dg x)). Hypotheses (dg0 : forall x, x \in `]a, b[%R -> dg x != 0). +Lemma differentiable_subr_neq0 : + g b - g a != 0. +Proof. +have [r] := MVT ab gdg cg; rewrite in_itv/= => /andP[ar rb] dgg. +by rewrite dgg mulf_neq0 ?dg0 ?in_itv/= ?ar//; rewrite subr_eq0 gt_eqF. +Qed. + Lemma cauchy_MVT : exists2 c, c \in `]a, b[%R & df c / dg c = (f b - f a) / (g b - g a). Proof. have [r] := MVT ab gdg cg; rewrite in_itv/= => /andP[ar rb] dgg. -have gba0 : g b - g a != 0. - by rewrite dgg mulf_neq0 ?dg0 ?in_itv/= ?ar// subr_eq0 gt_eqF. pose h (x : R) := f x - ((f b - f a) / (g b - g a)) * g x. have hder x : x \in `]a, b[%R -> derivable h x 1. move=> xab; apply: derivableB => /=. @@ -2575,7 +2580,9 @@ have ch : {within `[a, b], continuous h}. have /(Rolle ab hder ch)[x xab derh] : h a = h b. rewrite /h; apply/eqP; rewrite subr_eq eq_sym -addrA eq_sym addrC -subr_eq. rewrite -mulrN -mulrDr -(addrC (g a)) -[X in _ * X]opprB mulrN -mulrA. - by rewrite mulVf// mulr1 opprB. + rewrite mulVf//. + by rewrite mulr1 opprB. + by rewrite differentiable_subr_neq0. pose dh (x : R) := df x - (f b - f a) / (g b - g a) * dg x. have his_der y : y \in `]a, b[%R -> is_derive x 1 h (dh x). by move=> yab; apply: is_deriveB; [exact: fdf|apply: is_deriveZ; exact: gdg]. From 0129b38f5260c5bf646b8b58a0d97900f25cd170 Mon Sep 17 00:00:00 2001 From: ndslusarz Date: Mon, 28 Oct 2024 11:43:28 +0000 Subject: [PATCH 5/9] lhopital + cauchy mvt --- theories/realfun.v | 231 ++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 230 insertions(+), 1 deletion(-) diff --git a/theories/realfun.v b/theories/realfun.v index 235f87458..e3b06dcd2 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -63,7 +63,7 @@ Notation "'nonincreasing_fun' f" := ({homo f : n m / (n <= m)%O >-> (n >= m)%O}) Notation "'increasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n <= m)%O}) (at level 10). Notation "'decreasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n >= m)%O}) - (at level 10). + (at level 10). Lemma nondecreasing_funN {R : realType} a b (f : R -> R) : {in `[a, b] &, nondecreasing_fun f} <-> @@ -2586,3 +2586,232 @@ apply/continuous_within_itvP => //; split. Qed. End variation_continuity. + +Section Cauchy_MVT. +Context {R : realType}. +Variables (f df g dg : R -> R) (a b c : R). +Hypothesis ab : a < b. +Hypotheses (cf : {within `[a, b], continuous f}) + (cg : {within `[a, b], continuous g}). +Hypotheses (fdf : forall x, x \in `]a, b[%R -> is_derive x 1 f (df x)) + (gdg : forall x, x \in `]a, b[%R -> is_derive x 1 g (dg x)). +Hypotheses (dg0 : forall x, x \in `]a, b[%R -> dg x != 0). + +Lemma cauchy_MVT : + exists2 c, c \in `]a, b[%R & df c / dg c = (f b - f a) / (g b - g a). +Proof. +have [r] := MVT ab gdg cg; rewrite in_itv/= => /andP[ar rb] dgg. +have gba0 : g b - g a != 0. + by rewrite dgg mulf_neq0 ?dg0 ?in_itv/= ?ar// subr_eq0 gt_eqF. +pose h (x : R) := f x - ((f b - f a) / (g b - g a)) * g x. +have hder x : x \in `]a, b[%R -> derivable h x 1. + move=> xab; apply: derivableB => /=. + exact: (@ex_derive _ _ _ _ _ _ _ (fdf xab)). + by apply: derivableM => //; exact: (@ex_derive _ _ _ _ _ _ _ (gdg xab)). +have ch : {within `[a, b], continuous h}. + rewrite continuous_subspace_in => x xab. + by apply: cvgB; [exact: cf|apply: cvgM; [exact: cvg_cst|exact: cg]]. +have /(Rolle ab hder ch)[x xab derh] : h a = h b. + rewrite /h; apply/eqP; rewrite subr_eq eq_sym -addrA eq_sym addrC -subr_eq. + rewrite -mulrN -mulrDr -(addrC (g a)) -[X in _ * X]opprB mulrN -mulrA. + by rewrite mulVf// mulr1 opprB. +pose dh (x : R) := df x - (f b - f a) / (g b - g a) * dg x. +have his_der y : y \in `]a, b[%R -> is_derive x 1 h (dh x). + by move=> yab; apply: is_deriveB; [exact: fdf|apply: is_deriveZ; exact: gdg]. +exists x => //. +have := @derive_val _ R _ _ _ _ _ (his_der _ xab). +have -> := @derive_val _ R _ _ _ _ _ derh. +move=> /eqP; rewrite eq_sym subr_eq add0r => /eqP ->. +by rewrite -mulrA divff ?mulr1//; exact: dg0. +Qed. + +End Cauchy_MVT. + +Section lhopital. +Context {R : realType}. +Variables (f df g dg : R -> R) (a : R) (U : set R) (Ua : nbhs a U). +Hypotheses (fdf : forall x, x \in U -> is_derive x 1 f (df x)) + (gdg : forall x, x \in U -> is_derive x 1 g (dg x)). +Hypotheses (fa0 : f a = 0) (ga0 : g a = 0) + (cdg : \forall x \near a^', dg x != 0). + +Lemma lhopital_right (l : R) : + df x / dg x @[x --> a^'+] --> l -> f x / g x @[x --> a^'+] --> l. +Proof. +case: cdg => r/= r0 cdg'. +move: Ua; rewrite filter_of_nearI => -[D /= D0 aDU]. +near a^'+ => b. +have abf x : x \in `]a, b[%R -> {within `[a, x], continuous f}. + rewrite in_itv/= => /andP[ax xb]. + apply: derivable_within_continuous => y; rewrite in_itv/= => /andP[ay yx]. + apply: ex_derive. + apply: fdf. + rewrite inE; apply: aDU => /=. + rewrite ler0_norm? subr_le0//. + rewrite opprD opprK addrC ltrBlDr (le_lt_trans yx)// (lt_trans xb)//. + near: b; apply: nbhs_right_lt. + by rewrite ltrDr. +have abg x : x \in `]a, b[%R -> {within `[a, x], continuous g}. + rewrite in_itv/= => /andP[ax xb]. + apply: derivable_within_continuous => y; rewrite in_itv/= => /andP[ay yx]. + apply: ex_derive. + apply: gdg. + rewrite inE; apply: aDU => /=. + rewrite ler0_norm? subr_le0//. + rewrite opprD opprK addrC ltrBlDr (le_lt_trans yx)// (lt_trans xb)//. + near: b; apply: nbhs_right_lt. + by rewrite ltrDr. +have fdf' y : y \in `]a, b[%R -> is_derive y 1 f (df y). + rewrite in_itv/= => /andP[ay yb]; apply: fdf. + rewrite inE; apply: aDU => /=. + rewrite ltr0_norm ?subr_lt0//. + rewrite opprD opprK addrC ltrBlDr (lt_le_trans yb)//. + near: b; apply: nbhs_right_le. + by rewrite ltrDr. +have gdg' y : y \in `]a, b[%R -> is_derive y 1 g (dg y). + rewrite in_itv/= => /andP[ay yb]; apply: gdg. + rewrite inE; apply: aDU => /=. + rewrite ltr0_norm ?subr_lt0//. + rewrite opprD opprK addrC ltrBlDr (lt_le_trans yb)//. + near: b; apply: nbhs_right_le. + by rewrite ltrDr. +have {}dg0 y : y \in `]a, b[%R -> dg y != 0. + rewrite in_itv/= => /andP[ay yb]. + apply: (cdg' y) => /=; last by rewrite gt_eqF. + rewrite ltr0_norm; last by rewrite subr_lt0. + rewrite opprB ltrBlDl (lt_trans yb)//. + near: b; apply: nbhs_right_lt. + by rewrite ltrDl. +move=> fgal. +have L : \forall x \near a^'+, + exists2 c, c \in `]a, x[%R & df c / dg c = f x / g x. + near=> x. + have /andP[ax xb] : a < x < b by exact/andP. + have {}fdf' y : y \in `]a, x[%R -> is_derive y 1 f (df y). + rewrite !in_itv/= => /andP[ay yx]. + by apply: fdf'; rewrite in_itv/= ay/= (lt_trans yx). + have {}gdg' y : y \in `]a, x[%R -> is_derive y 1 g (dg y). + rewrite !in_itv/= => /andP[ay yx]. + by apply: gdg'; rewrite in_itv/= ay/= (lt_trans yx). + have {}dg0 y : y \in `]a, x[%R -> dg y != 0. + rewrite in_itv/= => /andP[ya yx]. + by apply: dg0; rewrite in_itv/= ya/= (lt_trans yx). + have {}axf : {within `[a, x], continuous f}. + rewrite continuous_subspace_in => y; rewrite inE/= in_itv/= => /andP[ay yx]. + by apply: abf; rewrite in_itv/= xb andbT. + have {}axg : {within `[a, x], continuous g}. + rewrite continuous_subspace_in => y; rewrite inE/= in_itv/= => /andP[ay yx]. + by apply: abg; rewrite in_itv/= xb andbT. + have := @cauchy_MVT _ f df g dg _ _ ax axf axg fdf' gdg' dg0. + by rewrite fa0 ga0 2!subr0. +apply/cvgrPdist_le => /= e e0. +move/cvgrPdist_le : fgal. +move=> /(_ _ e0)[r'/= r'0 fagl]. +case: L => d /= d0 L. +near=> t. +have /= := L t. +have atd : `|a - t| < d. + rewrite ltr0_norm; last by rewrite subr_lt0. + rewrite opprB ltrBlDl. + near: t; apply: nbhs_right_lt. + by rewrite ltrDl. +have at_ : a < t by []. +move=> /(_ atd)/(_ at_)[c]; rewrite in_itv/= => /andP[ac ct <-]. +apply: fagl => //=. +rewrite ltr0_norm; last by rewrite subr_lt0. +rewrite opprB ltrBlDl (lt_trans ct)//. +near: t; apply: nbhs_right_lt. +by rewrite ltrDl. +Unshelve. all: by end_near. Qed. + +Lemma lhopital_left (l : R) : + df x / dg x @[x --> a^'-] --> l -> f x / g x @[x --> a^'-] --> l. +Proof. +case: cdg => r/= r0 cdg'. +move: Ua; rewrite filter_of_nearI => -[D /= D0 aDU]. +near a^'- => b. +have baf x : x \in `]b, a[%R -> {within `[x, a], continuous f}. + rewrite in_itv/= => /andP[bx xa]. + apply: derivable_within_continuous => y; rewrite in_itv/= => /andP[xy ya]. + apply: ex_derive. + apply: fdf. + rewrite inE; apply: aDU => /=. + rewrite ger0_norm ?subr_ge0//. + rewrite ltrBlDr -ltrBlDl (lt_le_trans _ xy)// (le_lt_trans _ bx)//. + near: b; apply: nbhs_left_ge. + by rewrite ltrBlDl ltrDr. +have bag x : x \in `]b, a[%R -> {within `[x, a], continuous g}. + rewrite in_itv/= => /andP[bx xa]. + apply: derivable_within_continuous => y; rewrite in_itv/= => /andP[xy ya]. + apply: ex_derive. + apply: gdg. + rewrite inE; apply: aDU => /=. + rewrite ger0_norm ?subr_ge0//. + rewrite ltrBlDr -ltrBlDl (lt_le_trans _ xy)// (lt_trans _ bx)//. + near: b; apply: nbhs_left_gt. + by rewrite ltrBlDl ltrDr. +have fdf' y : y \in `]b, a[%R -> is_derive y 1 f (df y). + rewrite in_itv/= => /andP[by_ ya]; apply: fdf. + rewrite inE. + apply: aDU => /=. + rewrite gtr0_norm ?subr_gt0//. + rewrite ltrBlDl -ltrBlDr (le_lt_trans _ by_)//. + near: b; apply: nbhs_left_ge. + by rewrite ltrBlDr ltrDl. +have gdg' y : y \in `]b, a[%R -> is_derive y 1 g (dg y). + rewrite in_itv/= => /andP[by_ ya]; apply: gdg. + rewrite inE; apply: aDU => /=. + rewrite gtr0_norm ?subr_gt0//. + rewrite ltrBlDl -ltrBlDr (le_lt_trans _ by_)//. + near: b; apply: nbhs_left_ge. + by rewrite ltrBlDr ltrDl. +have {}dg0 y : y \in `]b, a[%R -> dg y != 0. + rewrite in_itv/= => /andP[by_ ya]. + apply: (cdg' y) => /=; last by rewrite lt_eqF. + rewrite gtr0_norm; last by rewrite subr_gt0. + rewrite ltrBlDr -ltrBlDl (lt_trans _ by_)//. + near: b; apply: nbhs_left_gt. + by rewrite ltrBlDl ltrDr. +move=> fgal. +have L : \forall x \near a^'-, + exists2 c, c \in `]x, a[%R & df c / dg c = f x / g x. + near=> x. + have /andP[bx xa] : b < x < a by exact/andP. + have {}fdf' y : y \in `]x, a[%R -> is_derive y 1 f (df y). + rewrite in_itv/= => /andP[xy ya]. + by apply: fdf'; rewrite in_itv/= ya andbT (lt_trans bx). + have {}gdg' y : y \in `]x, a[%R -> is_derive y 1 g (dg y). + rewrite in_itv/= => /andP[xy ya]. + by apply: gdg'; rewrite in_itv/= ya andbT (lt_trans _ xy). + have {}dg0 y : y \in `]x, a[%R -> dg y != 0. + rewrite in_itv/= => /andP[xy ya]. + by apply: dg0; rewrite in_itv/= ya andbT (lt_trans bx). + have {}xaf : {within `[x, a], continuous f}. + rewrite continuous_subspace_in => y; rewrite inE/= in_itv/= => /andP[xy ya]. + by apply: baf; rewrite in_itv/= bx. + have {}xag : {within `[x, a], continuous g}. + rewrite continuous_subspace_in => y; rewrite inE/= in_itv/= => /andP[xy ya]. + by apply: bag; rewrite in_itv/= bx. + have := @cauchy_MVT _ f df g dg _ _ xa xaf xag fdf' gdg' dg0. + by rewrite fa0 ga0 !sub0r divrN mulNr opprK. +apply/cvgrPdist_le => /= e e0. +move/cvgrPdist_le : fgal. +move=> /(_ _ e0)[r'/= r'0 fagl]. +case: L => d /= d0 L. +near=> t. +have /= := L t. +have atd : `|a - t| < d. + rewrite gtr0_norm; last by rewrite subr_gt0. + rewrite ltrBlDr -ltrBlDl. + near: t; apply: nbhs_left_gt. + by rewrite ltrBlDl ltrDr. +have ta : t < a by []. +move=> /(_ atd)/(_ ta)[c]; rewrite in_itv/= => /andP[tc ca <-]. +apply: fagl => //=. +rewrite gtr0_norm; last by rewrite subr_gt0. +rewrite ltrBlDr -ltrBlDl (lt_trans _ tc)//. +near: t; apply: nbhs_left_gt. +by rewrite ltrBlDl ltrDr. +Unshelve. all: by end_near. Qed. + +End lhopital. From 4c97c535dd3d7ad7d691d6d35da5d70be3945699 Mon Sep 17 00:00:00 2001 From: ndslusarz Date: Mon, 28 Oct 2024 23:54:56 +0000 Subject: [PATCH 6/9] headings --- theories/realfun.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/theories/realfun.v b/theories/realfun.v index e3b06dcd2..45612db02 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -41,6 +41,9 @@ From mathcomp Require Import sequences real_interval. (* lime_sup f a/lime_inf f a == limit sup/inferior of the extended real- *) (* valued function f at point a *) (* ``` *) +(* cauchy_MVT == Cauchy's mean value theorem *) +(* lhopital_right == L'Hopital rule (limit taken on the right) *) +(* lhopital_left == L'Hopital rule (limit taken on the left) *) (* *) (******************************************************************************) @@ -63,7 +66,7 @@ Notation "'nonincreasing_fun' f" := ({homo f : n m / (n <= m)%O >-> (n >= m)%O}) Notation "'increasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n <= m)%O}) (at level 10). Notation "'decreasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n >= m)%O}) - (at level 10). + (at level 10). Lemma nondecreasing_funN {R : realType} a b (f : R -> R) : {in `[a, b] &, nondecreasing_fun f} <-> From 285dcd799bca3854a46d571675b6c18aabfa5c00 Mon Sep 17 00:00:00 2001 From: ndslusarz Date: Tue, 29 Oct 2024 00:03:48 +0000 Subject: [PATCH 7/9] updated changelog --- CHANGELOG_UNRELEASED.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1ed83e6d9..e95210190 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -30,6 +30,11 @@ - in `classical_sets.v`: + lemmas `xsectionE`, `ysectionE` +- in file `realfun.v`, + + new lemmas `cauchy_MVT`, + `lhopital_right`, and + `lhopital_left`. + ### Changed - in `lebesgue_integrale.v` From 7e816dcf2e2f4afb0323658fc515cbf439453d9b Mon Sep 17 00:00:00 2001 From: ndslusarz Date: Fri, 15 Nov 2024 17:46:52 +0000 Subject: [PATCH 8/9] deduplicating into lemma --- theories/realfun.v | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/theories/realfun.v b/theories/realfun.v index 45612db02..9c5ef86d4 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -2600,12 +2600,17 @@ Hypotheses (fdf : forall x, x \in `]a, b[%R -> is_derive x 1 f (df x)) (gdg : forall x, x \in `]a, b[%R -> is_derive x 1 g (dg x)). Hypotheses (dg0 : forall x, x \in `]a, b[%R -> dg x != 0). +Lemma differentiable_subr_neq0 : + g b - g a != 0. +Proof. +have [r] := MVT ab gdg cg; rewrite in_itv/= => /andP[ar rb] dgg. +by rewrite dgg mulf_neq0 ?dg0 ?in_itv/= ?ar//; rewrite subr_eq0 gt_eqF. +Qed. + Lemma cauchy_MVT : exists2 c, c \in `]a, b[%R & df c / dg c = (f b - f a) / (g b - g a). Proof. have [r] := MVT ab gdg cg; rewrite in_itv/= => /andP[ar rb] dgg. -have gba0 : g b - g a != 0. - by rewrite dgg mulf_neq0 ?dg0 ?in_itv/= ?ar// subr_eq0 gt_eqF. pose h (x : R) := f x - ((f b - f a) / (g b - g a)) * g x. have hder x : x \in `]a, b[%R -> derivable h x 1. move=> xab; apply: derivableB => /=. @@ -2617,7 +2622,9 @@ have ch : {within `[a, b], continuous h}. have /(Rolle ab hder ch)[x xab derh] : h a = h b. rewrite /h; apply/eqP; rewrite subr_eq eq_sym -addrA eq_sym addrC -subr_eq. rewrite -mulrN -mulrDr -(addrC (g a)) -[X in _ * X]opprB mulrN -mulrA. - by rewrite mulVf// mulr1 opprB. + rewrite mulVf//. + by rewrite mulr1 opprB. + by rewrite differentiable_subr_neq0. pose dh (x : R) := df x - (f b - f a) / (g b - g a) * dg x. have his_der y : y \in `]a, b[%R -> is_derive x 1 h (dh x). by move=> yab; apply: is_deriveB; [exact: fdf|apply: is_deriveZ; exact: gdg]. From d2fecced53d005364601feafd62df8d2784df3cf Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 9 Jan 2025 17:02:59 +0900 Subject: [PATCH 9/9] mv lemmas to derive --- CHANGELOG_UNRELEASED.md | 7 +- theories/derive.v | 234 ++++++++++++++++++++++++++++++++++++++- theories/realfun.v | 240 ---------------------------------------- 3 files changed, 236 insertions(+), 245 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index e95210190..fc1862439 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -30,10 +30,9 @@ - in `classical_sets.v`: + lemmas `xsectionE`, `ysectionE` -- in file `realfun.v`, - + new lemmas `cauchy_MVT`, - `lhopital_right`, and - `lhopital_left`. +- in `derive.v`: + + lemmas `differentiable_subr_neq0`, `cauchy_MVT`, + `lhopital_right`, `lhopital_left` ### Changed diff --git a/theories/derive.v b/theories/derive.v index 9cd9384f8..cd4147993 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -11,7 +11,8 @@ From mathcomp Require Import normedtype landau forms poly. (* This file provides a theory of differentiation. It includes the standard *) (* rules of differentiation (differential of a sum, of a product, of *) (* exponentiation, of the inverse, etc.) as well as standard theorems (the *) -(* Extreme Value Theorem, Rolle's theorem, the Mean Value Theorem). *) +(* Extreme Value Theorem, Rolle's theorem, the Mean Value Theorem, Cauchy's *) +(* mean value theorem, L'Hopital's rule). *) (* *) (* Parsable notations (in all of the following, f is not supposed to be *) (* differentiable): *) @@ -1602,6 +1603,237 @@ have [c cab D] := MVT altb fdrvbl fcont. by exists c => //; rewrite in_itv /= ltW (itvP cab). Qed. +Section Cauchy_MVT. +Context {R : realType}. +Variables (f df g dg : R -> R) (a b c : R). +Hypothesis ab : a < b. +Hypotheses (cf : {within `[a, b], continuous f}) + (cg : {within `[a, b], continuous g}). +Hypotheses (fdf : forall x, x \in `]a, b[%R -> is_derive x 1 f (df x)) + (gdg : forall x, x \in `]a, b[%R -> is_derive x 1 g (dg x)). +Hypotheses (dg0 : forall x, x \in `]a, b[%R -> dg x != 0). + +Lemma differentiable_subr_neq0 : g b - g a != 0. +Proof. +have [r] := MVT ab gdg cg; rewrite in_itv/= => /andP[ar rb] dgg. +by rewrite dgg mulf_neq0 ?dg0 ?in_itv/= ?ar//; rewrite subr_eq0 gt_eqF. +Qed. + +Lemma cauchy_MVT : + exists2 c, c \in `]a, b[%R & df c / dg c = (f b - f a) / (g b - g a). +Proof. +pose h x := f x - ((f b - f a) / (g b - g a)) * g x. +have hder x : x \in `]a, b[%R -> derivable h x 1. + move=> xab; apply: derivableB => /=. + exact: (@ex_derive _ _ _ _ _ _ _ (fdf xab)). + by apply: derivableM => //; exact: (@ex_derive _ _ _ _ _ _ _ (gdg xab)). +have ch : {within `[a, b], continuous h}. + rewrite continuous_subspace_in => x xab. + by apply: cvgB; [exact: cf|apply: cvgM; [exact: cvg_cst|exact: cg]]. +have /(Rolle ab hder ch)[x xab derh] : h a = h b. + rewrite /h; apply/eqP; rewrite subr_eq eq_sym -addrA eq_sym addrC -subr_eq. + rewrite -mulrN -mulrDr -(addrC (g a)) -[X in _ * X]opprB mulrN -mulrA. + by rewrite mulVf ?differentiable_subr_neq0// mulr1 opprB. +pose dh x := df x - (f b - f a) / (g b - g a) * dg x. +have his_der y : y \in `]a, b[%R -> is_derive x 1 h (dh x). + by move=> yab; apply: is_deriveB; [exact: fdf|apply: is_deriveZ; exact: gdg]. +exists x => //. +have := @derive_val _ R _ _ _ _ _ (his_der _ xab). +rewrite (@derive_val _ R _ _ _ _ _ derh) => /esym/eqP. +by rewrite subr_eq add0r => /eqP ->; rewrite -mulrA divff ?mulr1//; exact: dg0. +Qed. + +End Cauchy_MVT. + +Section lhopital. +Context {R : realType}. +Variables (f df g dg : R -> R) (a : R) (U : set R) (Ua : nbhs a U). +Hypotheses (fdf : forall x, x \in U -> is_derive x 1 f (df x)) + (gdg : forall x, x \in U -> is_derive x 1 g (dg x)). +Hypotheses (fa0 : f a = 0) (ga0 : g a = 0) + (cdg : \forall x \near a^', dg x != 0). + +Lemma lhopital_right (l : R) : + df x / dg x @[x --> a^'+] --> l -> f x / g x @[x --> a^'+] --> l. +Proof. +case: cdg => r/= r0 cdg'. +move: Ua; rewrite filter_of_nearI => -[D /= D0 aDU]. +near a^'+ => b. +have abf x : x \in `]a, b[%R -> {within `[a, x], continuous f}. + rewrite in_itv/= => /andP[ax xb]. + apply: derivable_within_continuous => y; rewrite in_itv/= => /andP[ay yx]. + apply: ex_derive. + apply: fdf. + rewrite inE; apply: aDU => /=. + rewrite ler0_norm? subr_le0//. + rewrite opprD opprK addrC ltrBlDr (le_lt_trans yx)// (lt_trans xb)//. + near: b; apply: nbhs_right_lt. + by rewrite ltrDr. +have abg x : x \in `]a, b[%R -> {within `[a, x], continuous g}. + rewrite in_itv/= => /andP[ax xb]. + apply: derivable_within_continuous => y; rewrite in_itv/= => /andP[ay yx]. + apply: ex_derive. + apply: gdg. + rewrite inE; apply: aDU => /=. + rewrite ler0_norm? subr_le0//. + rewrite opprD opprK addrC ltrBlDr (le_lt_trans yx)// (lt_trans xb)//. + near: b; apply: nbhs_right_lt. + by rewrite ltrDr. +have fdf' y : y \in `]a, b[%R -> is_derive y 1 f (df y). + rewrite in_itv/= => /andP[ay yb]; apply: fdf. + rewrite inE; apply: aDU => /=. + rewrite ltr0_norm ?subr_lt0//. + rewrite opprD opprK addrC ltrBlDr (lt_le_trans yb)//. + near: b; apply: nbhs_right_le. + by rewrite ltrDr. +have gdg' y : y \in `]a, b[%R -> is_derive y 1 g (dg y). + rewrite in_itv/= => /andP[ay yb]; apply: gdg. + rewrite inE; apply: aDU => /=. + rewrite ltr0_norm ?subr_lt0//. + rewrite opprD opprK addrC ltrBlDr (lt_le_trans yb)//. + near: b; apply: nbhs_right_le. + by rewrite ltrDr. +have {}dg0 y : y \in `]a, b[%R -> dg y != 0. + rewrite in_itv/= => /andP[ay yb]. + apply: (cdg' y) => /=; last by rewrite gt_eqF. + rewrite ltr0_norm; last by rewrite subr_lt0. + rewrite opprB ltrBlDl (lt_trans yb)//. + near: b; apply: nbhs_right_lt. + by rewrite ltrDl. +move=> fgal. +have L : \forall x \near a^'+, + exists2 c, c \in `]a, x[%R & df c / dg c = f x / g x. + near=> x. + have /andP[ax xb] : a < x < b by exact/andP. + have {}fdf' y : y \in `]a, x[%R -> is_derive y 1 f (df y). + rewrite !in_itv/= => /andP[ay yx]. + by apply: fdf'; rewrite in_itv/= ay/= (lt_trans yx). + have {}gdg' y : y \in `]a, x[%R -> is_derive y 1 g (dg y). + rewrite !in_itv/= => /andP[ay yx]. + by apply: gdg'; rewrite in_itv/= ay/= (lt_trans yx). + have {}dg0 y : y \in `]a, x[%R -> dg y != 0. + rewrite in_itv/= => /andP[ya yx]. + by apply: dg0; rewrite in_itv/= ya/= (lt_trans yx). + have {}axf : {within `[a, x], continuous f}. + rewrite continuous_subspace_in => y; rewrite inE/= in_itv/= => /andP[ay yx]. + by apply: abf; rewrite in_itv/= xb andbT. + have {}axg : {within `[a, x], continuous g}. + rewrite continuous_subspace_in => y; rewrite inE/= in_itv/= => /andP[ay yx]. + by apply: abg; rewrite in_itv/= xb andbT. + have := @cauchy_MVT _ f df g dg _ _ ax axf axg fdf' gdg' dg0. + by rewrite fa0 ga0 2!subr0. +apply/cvgrPdist_le => /= e e0. +move/cvgrPdist_le : fgal. +move=> /(_ _ e0)[r'/= r'0 fagl]. +case: L => d /= d0 L. +near=> t. +have /= := L t. +have atd : `|a - t| < d. + rewrite ltr0_norm; last by rewrite subr_lt0. + rewrite opprB ltrBlDl. + near: t; apply: nbhs_right_lt. + by rewrite ltrDl. +have at_ : a < t by []. +move=> /(_ atd)/(_ at_)[c]; rewrite in_itv/= => /andP[ac ct <-]. +apply: fagl => //=. +rewrite ltr0_norm; last by rewrite subr_lt0. +rewrite opprB ltrBlDl (lt_trans ct)//. +near: t; apply: nbhs_right_lt. +by rewrite ltrDl. +Unshelve. all: by end_near. Qed. + +Lemma lhopital_left (l : R) : + df x / dg x @[x --> a^'-] --> l -> f x / g x @[x --> a^'-] --> l. +Proof. +case: cdg => r/= r0 cdg'. +move: Ua; rewrite filter_of_nearI => -[D /= D0 aDU]. +near a^'- => b. +have baf x : x \in `]b, a[%R -> {within `[x, a], continuous f}. + rewrite in_itv/= => /andP[bx xa]. + apply: derivable_within_continuous => y; rewrite in_itv/= => /andP[xy ya]. + apply: ex_derive. + apply: fdf. + rewrite inE; apply: aDU => /=. + rewrite ger0_norm ?subr_ge0//. + rewrite ltrBlDr -ltrBlDl (lt_le_trans _ xy)// (le_lt_trans _ bx)//. + near: b; apply: nbhs_left_ge. + by rewrite ltrBlDl ltrDr. +have bag x : x \in `]b, a[%R -> {within `[x, a], continuous g}. + rewrite in_itv/= => /andP[bx xa]. + apply: derivable_within_continuous => y; rewrite in_itv/= => /andP[xy ya]. + apply: ex_derive. + apply: gdg. + rewrite inE; apply: aDU => /=. + rewrite ger0_norm ?subr_ge0//. + rewrite ltrBlDr -ltrBlDl (lt_le_trans _ xy)// (lt_trans _ bx)//. + near: b; apply: nbhs_left_gt. + by rewrite ltrBlDl ltrDr. +have fdf' y : y \in `]b, a[%R -> is_derive y 1 f (df y). + rewrite in_itv/= => /andP[by_ ya]; apply: fdf. + rewrite inE. + apply: aDU => /=. + rewrite gtr0_norm ?subr_gt0//. + rewrite ltrBlDl -ltrBlDr (le_lt_trans _ by_)//. + near: b; apply: nbhs_left_ge. + by rewrite ltrBlDr ltrDl. +have gdg' y : y \in `]b, a[%R -> is_derive y 1 g (dg y). + rewrite in_itv/= => /andP[by_ ya]; apply: gdg. + rewrite inE; apply: aDU => /=. + rewrite gtr0_norm ?subr_gt0//. + rewrite ltrBlDl -ltrBlDr (le_lt_trans _ by_)//. + near: b; apply: nbhs_left_ge. + by rewrite ltrBlDr ltrDl. +have {}dg0 y : y \in `]b, a[%R -> dg y != 0. + rewrite in_itv/= => /andP[by_ ya]. + apply: (cdg' y) => /=; last by rewrite lt_eqF. + rewrite gtr0_norm; last by rewrite subr_gt0. + rewrite ltrBlDr -ltrBlDl (lt_trans _ by_)//. + near: b; apply: nbhs_left_gt. + by rewrite ltrBlDl ltrDr. +move=> fgal. +have L : \forall x \near a^'-, + exists2 c, c \in `]x, a[%R & df c / dg c = f x / g x. + near=> x. + have /andP[bx xa] : b < x < a by exact/andP. + have {}fdf' y : y \in `]x, a[%R -> is_derive y 1 f (df y). + rewrite in_itv/= => /andP[xy ya]. + by apply: fdf'; rewrite in_itv/= ya andbT (lt_trans bx). + have {}gdg' y : y \in `]x, a[%R -> is_derive y 1 g (dg y). + rewrite in_itv/= => /andP[xy ya]. + by apply: gdg'; rewrite in_itv/= ya andbT (lt_trans _ xy). + have {}dg0 y : y \in `]x, a[%R -> dg y != 0. + rewrite in_itv/= => /andP[xy ya]. + by apply: dg0; rewrite in_itv/= ya andbT (lt_trans bx). + have {}xaf : {within `[x, a], continuous f}. + rewrite continuous_subspace_in => y; rewrite inE/= in_itv/= => /andP[xy ya]. + by apply: baf; rewrite in_itv/= bx. + have {}xag : {within `[x, a], continuous g}. + rewrite continuous_subspace_in => y; rewrite inE/= in_itv/= => /andP[xy ya]. + by apply: bag; rewrite in_itv/= bx. + have := @cauchy_MVT _ f df g dg _ _ xa xaf xag fdf' gdg' dg0. + by rewrite fa0 ga0 !sub0r divrN mulNr opprK. +apply/cvgrPdist_le => /= e e0. +move/cvgrPdist_le : fgal. +move=> /(_ _ e0)[r'/= r'0 fagl]. +case: L => d /= d0 L. +near=> t. +have /= := L t. +have atd : `|a - t| < d. + rewrite gtr0_norm; last by rewrite subr_gt0. + rewrite ltrBlDr -ltrBlDl. + near: t; apply: nbhs_left_gt. + by rewrite ltrBlDl ltrDr. +have ta : t < a by []. +move=> /(_ atd)/(_ ta)[c]; rewrite in_itv/= => /andP[tc ca <-]. +apply: fagl => //=. +rewrite gtr0_norm; last by rewrite subr_gt0. +rewrite ltrBlDr -ltrBlDl (lt_trans _ tc)//. +near: t; apply: nbhs_left_gt. +by rewrite ltrBlDl ltrDr. +Unshelve. all: by end_near. Qed. + +End lhopital. + Lemma ler0_derive1_nincr (R : realType) (f : R -> R) (a b : R) : (forall x, x \in `]a, b[%R -> derivable f x 1) -> (forall x, x \in `]a, b[%R -> f^`() x <= 0) -> diff --git a/theories/realfun.v b/theories/realfun.v index 9c5ef86d4..610ed1ed5 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -41,10 +41,6 @@ From mathcomp Require Import sequences real_interval. (* lime_sup f a/lime_inf f a == limit sup/inferior of the extended real- *) (* valued function f at point a *) (* ``` *) -(* cauchy_MVT == Cauchy's mean value theorem *) -(* lhopital_right == L'Hopital rule (limit taken on the right) *) -(* lhopital_left == L'Hopital rule (limit taken on the left) *) -(* *) (******************************************************************************) Set Implicit Arguments. @@ -2589,239 +2585,3 @@ apply/continuous_within_itvP => //; split. Qed. End variation_continuity. - -Section Cauchy_MVT. -Context {R : realType}. -Variables (f df g dg : R -> R) (a b c : R). -Hypothesis ab : a < b. -Hypotheses (cf : {within `[a, b], continuous f}) - (cg : {within `[a, b], continuous g}). -Hypotheses (fdf : forall x, x \in `]a, b[%R -> is_derive x 1 f (df x)) - (gdg : forall x, x \in `]a, b[%R -> is_derive x 1 g (dg x)). -Hypotheses (dg0 : forall x, x \in `]a, b[%R -> dg x != 0). - -Lemma differentiable_subr_neq0 : - g b - g a != 0. -Proof. -have [r] := MVT ab gdg cg; rewrite in_itv/= => /andP[ar rb] dgg. -by rewrite dgg mulf_neq0 ?dg0 ?in_itv/= ?ar//; rewrite subr_eq0 gt_eqF. -Qed. - -Lemma cauchy_MVT : - exists2 c, c \in `]a, b[%R & df c / dg c = (f b - f a) / (g b - g a). -Proof. -have [r] := MVT ab gdg cg; rewrite in_itv/= => /andP[ar rb] dgg. -pose h (x : R) := f x - ((f b - f a) / (g b - g a)) * g x. -have hder x : x \in `]a, b[%R -> derivable h x 1. - move=> xab; apply: derivableB => /=. - exact: (@ex_derive _ _ _ _ _ _ _ (fdf xab)). - by apply: derivableM => //; exact: (@ex_derive _ _ _ _ _ _ _ (gdg xab)). -have ch : {within `[a, b], continuous h}. - rewrite continuous_subspace_in => x xab. - by apply: cvgB; [exact: cf|apply: cvgM; [exact: cvg_cst|exact: cg]]. -have /(Rolle ab hder ch)[x xab derh] : h a = h b. - rewrite /h; apply/eqP; rewrite subr_eq eq_sym -addrA eq_sym addrC -subr_eq. - rewrite -mulrN -mulrDr -(addrC (g a)) -[X in _ * X]opprB mulrN -mulrA. - rewrite mulVf//. - by rewrite mulr1 opprB. - by rewrite differentiable_subr_neq0. -pose dh (x : R) := df x - (f b - f a) / (g b - g a) * dg x. -have his_der y : y \in `]a, b[%R -> is_derive x 1 h (dh x). - by move=> yab; apply: is_deriveB; [exact: fdf|apply: is_deriveZ; exact: gdg]. -exists x => //. -have := @derive_val _ R _ _ _ _ _ (his_der _ xab). -have -> := @derive_val _ R _ _ _ _ _ derh. -move=> /eqP; rewrite eq_sym subr_eq add0r => /eqP ->. -by rewrite -mulrA divff ?mulr1//; exact: dg0. -Qed. - -End Cauchy_MVT. - -Section lhopital. -Context {R : realType}. -Variables (f df g dg : R -> R) (a : R) (U : set R) (Ua : nbhs a U). -Hypotheses (fdf : forall x, x \in U -> is_derive x 1 f (df x)) - (gdg : forall x, x \in U -> is_derive x 1 g (dg x)). -Hypotheses (fa0 : f a = 0) (ga0 : g a = 0) - (cdg : \forall x \near a^', dg x != 0). - -Lemma lhopital_right (l : R) : - df x / dg x @[x --> a^'+] --> l -> f x / g x @[x --> a^'+] --> l. -Proof. -case: cdg => r/= r0 cdg'. -move: Ua; rewrite filter_of_nearI => -[D /= D0 aDU]. -near a^'+ => b. -have abf x : x \in `]a, b[%R -> {within `[a, x], continuous f}. - rewrite in_itv/= => /andP[ax xb]. - apply: derivable_within_continuous => y; rewrite in_itv/= => /andP[ay yx]. - apply: ex_derive. - apply: fdf. - rewrite inE; apply: aDU => /=. - rewrite ler0_norm? subr_le0//. - rewrite opprD opprK addrC ltrBlDr (le_lt_trans yx)// (lt_trans xb)//. - near: b; apply: nbhs_right_lt. - by rewrite ltrDr. -have abg x : x \in `]a, b[%R -> {within `[a, x], continuous g}. - rewrite in_itv/= => /andP[ax xb]. - apply: derivable_within_continuous => y; rewrite in_itv/= => /andP[ay yx]. - apply: ex_derive. - apply: gdg. - rewrite inE; apply: aDU => /=. - rewrite ler0_norm? subr_le0//. - rewrite opprD opprK addrC ltrBlDr (le_lt_trans yx)// (lt_trans xb)//. - near: b; apply: nbhs_right_lt. - by rewrite ltrDr. -have fdf' y : y \in `]a, b[%R -> is_derive y 1 f (df y). - rewrite in_itv/= => /andP[ay yb]; apply: fdf. - rewrite inE; apply: aDU => /=. - rewrite ltr0_norm ?subr_lt0//. - rewrite opprD opprK addrC ltrBlDr (lt_le_trans yb)//. - near: b; apply: nbhs_right_le. - by rewrite ltrDr. -have gdg' y : y \in `]a, b[%R -> is_derive y 1 g (dg y). - rewrite in_itv/= => /andP[ay yb]; apply: gdg. - rewrite inE; apply: aDU => /=. - rewrite ltr0_norm ?subr_lt0//. - rewrite opprD opprK addrC ltrBlDr (lt_le_trans yb)//. - near: b; apply: nbhs_right_le. - by rewrite ltrDr. -have {}dg0 y : y \in `]a, b[%R -> dg y != 0. - rewrite in_itv/= => /andP[ay yb]. - apply: (cdg' y) => /=; last by rewrite gt_eqF. - rewrite ltr0_norm; last by rewrite subr_lt0. - rewrite opprB ltrBlDl (lt_trans yb)//. - near: b; apply: nbhs_right_lt. - by rewrite ltrDl. -move=> fgal. -have L : \forall x \near a^'+, - exists2 c, c \in `]a, x[%R & df c / dg c = f x / g x. - near=> x. - have /andP[ax xb] : a < x < b by exact/andP. - have {}fdf' y : y \in `]a, x[%R -> is_derive y 1 f (df y). - rewrite !in_itv/= => /andP[ay yx]. - by apply: fdf'; rewrite in_itv/= ay/= (lt_trans yx). - have {}gdg' y : y \in `]a, x[%R -> is_derive y 1 g (dg y). - rewrite !in_itv/= => /andP[ay yx]. - by apply: gdg'; rewrite in_itv/= ay/= (lt_trans yx). - have {}dg0 y : y \in `]a, x[%R -> dg y != 0. - rewrite in_itv/= => /andP[ya yx]. - by apply: dg0; rewrite in_itv/= ya/= (lt_trans yx). - have {}axf : {within `[a, x], continuous f}. - rewrite continuous_subspace_in => y; rewrite inE/= in_itv/= => /andP[ay yx]. - by apply: abf; rewrite in_itv/= xb andbT. - have {}axg : {within `[a, x], continuous g}. - rewrite continuous_subspace_in => y; rewrite inE/= in_itv/= => /andP[ay yx]. - by apply: abg; rewrite in_itv/= xb andbT. - have := @cauchy_MVT _ f df g dg _ _ ax axf axg fdf' gdg' dg0. - by rewrite fa0 ga0 2!subr0. -apply/cvgrPdist_le => /= e e0. -move/cvgrPdist_le : fgal. -move=> /(_ _ e0)[r'/= r'0 fagl]. -case: L => d /= d0 L. -near=> t. -have /= := L t. -have atd : `|a - t| < d. - rewrite ltr0_norm; last by rewrite subr_lt0. - rewrite opprB ltrBlDl. - near: t; apply: nbhs_right_lt. - by rewrite ltrDl. -have at_ : a < t by []. -move=> /(_ atd)/(_ at_)[c]; rewrite in_itv/= => /andP[ac ct <-]. -apply: fagl => //=. -rewrite ltr0_norm; last by rewrite subr_lt0. -rewrite opprB ltrBlDl (lt_trans ct)//. -near: t; apply: nbhs_right_lt. -by rewrite ltrDl. -Unshelve. all: by end_near. Qed. - -Lemma lhopital_left (l : R) : - df x / dg x @[x --> a^'-] --> l -> f x / g x @[x --> a^'-] --> l. -Proof. -case: cdg => r/= r0 cdg'. -move: Ua; rewrite filter_of_nearI => -[D /= D0 aDU]. -near a^'- => b. -have baf x : x \in `]b, a[%R -> {within `[x, a], continuous f}. - rewrite in_itv/= => /andP[bx xa]. - apply: derivable_within_continuous => y; rewrite in_itv/= => /andP[xy ya]. - apply: ex_derive. - apply: fdf. - rewrite inE; apply: aDU => /=. - rewrite ger0_norm ?subr_ge0//. - rewrite ltrBlDr -ltrBlDl (lt_le_trans _ xy)// (le_lt_trans _ bx)//. - near: b; apply: nbhs_left_ge. - by rewrite ltrBlDl ltrDr. -have bag x : x \in `]b, a[%R -> {within `[x, a], continuous g}. - rewrite in_itv/= => /andP[bx xa]. - apply: derivable_within_continuous => y; rewrite in_itv/= => /andP[xy ya]. - apply: ex_derive. - apply: gdg. - rewrite inE; apply: aDU => /=. - rewrite ger0_norm ?subr_ge0//. - rewrite ltrBlDr -ltrBlDl (lt_le_trans _ xy)// (lt_trans _ bx)//. - near: b; apply: nbhs_left_gt. - by rewrite ltrBlDl ltrDr. -have fdf' y : y \in `]b, a[%R -> is_derive y 1 f (df y). - rewrite in_itv/= => /andP[by_ ya]; apply: fdf. - rewrite inE. - apply: aDU => /=. - rewrite gtr0_norm ?subr_gt0//. - rewrite ltrBlDl -ltrBlDr (le_lt_trans _ by_)//. - near: b; apply: nbhs_left_ge. - by rewrite ltrBlDr ltrDl. -have gdg' y : y \in `]b, a[%R -> is_derive y 1 g (dg y). - rewrite in_itv/= => /andP[by_ ya]; apply: gdg. - rewrite inE; apply: aDU => /=. - rewrite gtr0_norm ?subr_gt0//. - rewrite ltrBlDl -ltrBlDr (le_lt_trans _ by_)//. - near: b; apply: nbhs_left_ge. - by rewrite ltrBlDr ltrDl. -have {}dg0 y : y \in `]b, a[%R -> dg y != 0. - rewrite in_itv/= => /andP[by_ ya]. - apply: (cdg' y) => /=; last by rewrite lt_eqF. - rewrite gtr0_norm; last by rewrite subr_gt0. - rewrite ltrBlDr -ltrBlDl (lt_trans _ by_)//. - near: b; apply: nbhs_left_gt. - by rewrite ltrBlDl ltrDr. -move=> fgal. -have L : \forall x \near a^'-, - exists2 c, c \in `]x, a[%R & df c / dg c = f x / g x. - near=> x. - have /andP[bx xa] : b < x < a by exact/andP. - have {}fdf' y : y \in `]x, a[%R -> is_derive y 1 f (df y). - rewrite in_itv/= => /andP[xy ya]. - by apply: fdf'; rewrite in_itv/= ya andbT (lt_trans bx). - have {}gdg' y : y \in `]x, a[%R -> is_derive y 1 g (dg y). - rewrite in_itv/= => /andP[xy ya]. - by apply: gdg'; rewrite in_itv/= ya andbT (lt_trans _ xy). - have {}dg0 y : y \in `]x, a[%R -> dg y != 0. - rewrite in_itv/= => /andP[xy ya]. - by apply: dg0; rewrite in_itv/= ya andbT (lt_trans bx). - have {}xaf : {within `[x, a], continuous f}. - rewrite continuous_subspace_in => y; rewrite inE/= in_itv/= => /andP[xy ya]. - by apply: baf; rewrite in_itv/= bx. - have {}xag : {within `[x, a], continuous g}. - rewrite continuous_subspace_in => y; rewrite inE/= in_itv/= => /andP[xy ya]. - by apply: bag; rewrite in_itv/= bx. - have := @cauchy_MVT _ f df g dg _ _ xa xaf xag fdf' gdg' dg0. - by rewrite fa0 ga0 !sub0r divrN mulNr opprK. -apply/cvgrPdist_le => /= e e0. -move/cvgrPdist_le : fgal. -move=> /(_ _ e0)[r'/= r'0 fagl]. -case: L => d /= d0 L. -near=> t. -have /= := L t. -have atd : `|a - t| < d. - rewrite gtr0_norm; last by rewrite subr_gt0. - rewrite ltrBlDr -ltrBlDl. - near: t; apply: nbhs_left_gt. - by rewrite ltrBlDl ltrDr. -have ta : t < a by []. -move=> /(_ atd)/(_ ta)[c]; rewrite in_itv/= => /andP[tc ca <-]. -apply: fagl => //=. -rewrite gtr0_norm; last by rewrite subr_gt0. -rewrite ltrBlDr -ltrBlDl (lt_trans _ tc)//. -near: t; apply: nbhs_left_gt. -by rewrite ltrBlDl ltrDr. -Unshelve. all: by end_near. Qed. - -End lhopital.