# Library Coq.Reals.MVT

Require Import Rbase.
Require Import Rfunctions.
Require Import Ranalysis1.
Require Import Rtopology.
Local Open Scope R_scope.

Theorem MVT :
forall (f g:R -> R) (a b:R) (pr1:forall c:R, a < c < b -> derivable_pt f c)
(pr2:forall c:R, a < c < b -> derivable_pt g c),
a < b ->
(forall c:R, a <= c <= b -> continuity_pt f c) ->
(forall c:R, a <= c <= b -> continuity_pt g c) ->
exists c : R,
(exists P : a < c < b,
(g b - g a) * derive_pt f c (pr1 c P) =
(f b - f a) * derive_pt g c (pr2 c P)).

Lemma MVT_cor1 :
forall (f:R -> R) (a b:R) (pr:derivable f),
a < b ->
exists c : R, f b - f a = derive_pt f c (pr c) * (b - a) /\ a < c < b.

Theorem MVT_cor2 :
forall (f f':R -> R) (a b:R),
a < b ->
(forall c:R, a <= c <= b -> derivable_pt_lim f c (f' c)) ->
exists c : R, f b - f a = f' c * (b - a) /\ a < c < b.

Lemma MVT_cor3 :
forall (f f':R -> R) (a b:R),
a < b ->
(forall x:R, a <= x -> x <= b -> derivable_pt_lim f x (f' x)) ->
exists c : R, a <= c /\ c <= b /\ f b = f a + f' c * (b - a).

Lemma Rolle :
forall (f:R -> R) (a b:R) (pr:forall x:R, a < x < b -> derivable_pt f x),
(forall x:R, a <= x <= b -> continuity_pt f x) ->
a < b ->
f a = f b ->
exists c : R, (exists P : a < c < b, derive_pt f c (pr c P) = 0).

Lemma nonneg_derivative_1 :
forall (f:R -> R) (pr:derivable f),
(forall x:R, 0 <= derive_pt f x (pr x)) -> increasing f.

Lemma nonpos_derivative_0 :
forall (f:R -> R) (pr:derivable f),
decreasing f -> forall x:R, derive_pt f x (pr x) <= 0.

Lemma increasing_decreasing_opp :
forall f:R -> R, increasing f -> decreasing (- f)%F.

Lemma nonpos_derivative_1 :
forall (f:R -> R) (pr:derivable f),
(forall x:R, derive_pt f x (pr x) <= 0) -> decreasing f.

Lemma positive_derivative :
forall (f:R -> R) (pr:derivable f),
(forall x:R, 0 < derive_pt f x (pr x)) -> strict_increasing f.

Lemma strictincreasing_strictdecreasing_opp :
forall f:R -> R, strict_increasing f -> strict_decreasing (- f)%F.

Lemma negative_derivative :
forall (f:R -> R) (pr:derivable f),
(forall x:R, derive_pt f x (pr x) < 0) -> strict_decreasing f.

Lemma null_derivative_0 :
forall (f:R -> R) (pr:derivable f),
constant f -> forall x:R, derive_pt f x (pr x) = 0.

Lemma increasing_decreasing :
forall f:R -> R, increasing f -> decreasing f -> constant f.

Lemma null_derivative_1 :
forall (f:R -> R) (pr:derivable f),
(forall x:R, derive_pt f x (pr x) = 0) -> constant f.

Lemma derive_increasing_interv_ax :
forall (a b:R) (f:R -> R) (pr:derivable f),
a < b ->
((forall t:R, a < t < b -> 0 < derive_pt f t (pr t)) ->
forall x y:R, a <= x <= b -> a <= y <= b -> x < y -> f x < f y) /\
((forall t:R, a < t < b -> 0 <= derive_pt f t (pr t)) ->
forall x y:R, a <= x <= b -> a <= y <= b -> x < y -> f x <= f y).

Lemma derive_increasing_interv :
forall (a b:R) (f:R -> R) (pr:derivable f),
a < b ->
(forall t:R, a < t < b -> 0 < derive_pt f t (pr t)) ->
forall x y:R, a <= x <= b -> a <= y <= b -> x < y -> f x < f y.

Lemma derive_increasing_interv_var :
forall (a b:R) (f:R -> R) (pr:derivable f),
a < b ->
(forall t:R, a < t < b -> 0 <= derive_pt f t (pr t)) ->
forall x y:R, a <= x <= b -> a <= y <= b -> x < y -> f x <= f y.

Theorem IAF :
forall (f:R -> R) (a b k:R) (pr:derivable f),
a <= b ->
(forall c:R, a <= c <= b -> derive_pt f c (pr c) <= k) ->
f b - f a <= k * (b - a).

Lemma IAF_var :
forall (f g:R -> R) (a b:R) (pr1:derivable f) (pr2:derivable g),
a <= b ->
(forall c:R, a <= c <= b -> derive_pt g c (pr2 c) <= derive_pt f c (pr1 c)) ->
g b - g a <= f b - f a.

Lemma null_derivative_loc :
forall (f:R -> R) (a b:R) (pr:forall x:R, a < x < b -> derivable_pt f x),
(forall x:R, a <= x <= b -> continuity_pt f x) ->
(forall (x:R) (P:a < x < b), derive_pt f x (pr x P) = 0) ->
constant_D_eq f (fun x:R => a <= x <= b) (f a).

Lemma antiderivative_Ucte :
forall (f g1 g2:R -> R) (a b:R),
antiderivative f g1 a b ->
antiderivative f g2 a b ->
exists c : R, (forall x:R, a <= x <= b -> g1 x = g2 x + c).

Lemma MVT_abs :
forall (f f' : R -> R) (a b : R),
(forall c : R, Rmin a b <= c <= Rmax a b ->
derivable_pt_lim f c (f' c)) ->
exists c : R, Rabs (f b - f a) = Rabs (f' c) * Rabs (b - a) /\
Rmin a b <= c <= Rmax a b.