From e6ca69750e260ceeb4a582002ba13f8fbae1742a Mon Sep 17 00:00:00 2001 From: ndslusarz Date: Fri, 15 Nov 2024 17:46:52 +0000 Subject: [PATCH] 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].