Library Coq.Reals.MVT
Require Import Rbase.
Require Import Rfunctions.
Require Import Ranalysis1.
Require Import Rtopology.
Open Local 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).