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.