Library Coq.Reals.MVT

Require Import Rbase.
Require Import Rfunctions.
Require Import Ranalysis1.
Require Import Rtopology.
Require Import Lra.
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.