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).