proposition: Lemma MVT (R : realType) (f df : R -> R) (a b : R) : a < b -> (forall x, x \in `]a, b[%R -> is_derive x 1 f (df x)) -> {within `[a, b], continuous f} -> exists2 c, c \in `]a, b[%R & f b - f a = df c * (b - a).
proof: Proof. move=> altb fdrvbl fcont. set g := f + (- ( *:%R^~ ((f b - f a) / (b - a)) : R -> R)). have gdrvbl x : x \in `]a, b[%R -> derivable g x 1. by move=> /fdrvbl dfx; apply: derivableB => //; exact/derivable1_diffP. have gcont : {within `[a, b], continuous g}. move=> x; apply: continuousD _ ; first by move=>?; exact: fcont. by apply/continuousN/continuous_subspaceT=> ?; exact: scalel_continuous. have gaegb : g a = g b. rewrite /g -![(_ - _ : _ -> _) _]/(_ - _). apply/eqP; rewrite -subr_eq /= opprK addrAC -addrA -scalerBl. rewrite [_ *: _]mulrA mulrC mulrA mulVf. by rewrite mul1r addrCA subrr addr0. by apply: lt0r_neq0; rewrite subr_gt0. have [c cab dgc0] := Rolle altb gdrvbl gcont gaegb. exists c; first exact: cab. have /fdrvbl dfc := cab; move/@derive_val: dgc0; rewrite deriveB //; last first. exact/derivable1_diffP. move/eqP; rewrite [X in _ - X]deriveE // derive_val diff_val scale1r subr_eq0. move/eqP->; rewrite -mulrA mulVf ?mulr1 //; apply: lt0r_neq0. by rewrite subr_gt0. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix interval) mathcomp(mathcomp_extra boolp classical_sets functions) reals signed topology prodnormedzmodule normedtype landau forms