proposition: Lemma MVT_gen (f : R -> R) (a b : R) (df : R -> R) : let a0 := Rmin a b in let b0 := Rmax a b in (forall x, a0 < x < b0 -> is_derive f x (df x)) -> (forall x, a0 <= x <= b0 -> continuity_pt f x) -> exists c, a0 <= c <= b0 /\ f b - f a = df c * (b - a).
proof: Proof. move => a0 b0 Hd Hf. case: (Req_dec a0 b0) => Hab. exists a0 ; split. split ; by apply Req_le. replace b with a. ring. move: Hab ; rewrite /a0 /b0 /Rmin /Rmax ; by case: Rle_dec => Hab. have pr1 : forall c:R, a0 < c < b0 -> derivable_pt f c. move => x Hx ; exists (df x). by apply is_derive_Reals, Hd. have pr2 : forall c:R, a0 < c < b0 -> derivable_pt id c. move => x Hx ; exists 1. by apply derivable_pt_lim_id. case: (MVT f id a0 b0 pr1 pr2). apply Rnot_le_lt ; contradict Hab ; apply Rle_antisym. by apply Rcomplements.Rmin_Rmax. by apply Hab. by apply Hf. move => x Hx ; apply derivable_continuous, derivable_id. move => /= c [Hc H]. exists c ; split. split ; by apply Rlt_le, Hc. replace (df c) with (derive_pt f c (pr1 c Hc)). move: H ; rewrite {1 2}/id /a0 /b0 /Rmin /Rmax ; case: Rle_dec => Hab0 H. rewrite Rmult_comm H -(pr_nu _ _ (derivable_pt_id _)) derive_pt_id. ring. replace (derive_pt f c (pr1 c Hc) * (b - a)) with (-((a - b) * derive_pt f c (pr1 c Hc))) by ring. rewrite H -(pr_nu _ _ (derivable_pt_id _)) derive_pt_id. ring. case: (pr1 c Hc) => /= l Hl. transitivity (Derive f c). apply sym_eq, is_derive_unique, is_derive_Reals, Hl. by apply is_derive_unique, Hd. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv