Library Coq.Reals.Rderiv
Definition of the derivative,continuity
Require Import Rbase.
Require Import Rfunctions.
Require Import Rlimit.
Require Import Fourier.
Require Import Classical_Prop.
Require Import Classical_Pred_Type.
Require Import Omega.
Open Local Scope R_scope.
Definition D_x (
D:R ->
Prop) (
y x:R) :
Prop :=
D x /\
y <>
x.
Definition continue_in (
f:R ->
R) (
D:R ->
Prop) (
x0:R) :
Prop :=
limit1_in f (
D_x D x0) (
f x0)
x0.
Definition D_in (
f d:R ->
R) (
D:R ->
Prop) (
x0:R) :
Prop :=
limit1_in (
fun x:R => (
f x -
f x0) / (
x -
x0)) (
D_x D x0) (
d x0)
x0.
Lemma cont_deriv :
forall (
f d:R ->
R) (
D:R ->
Prop) (
x0:R),
D_in f d D x0 ->
continue_in f D x0.
Lemma Dconst :
forall (
D:R ->
Prop) (
y x0:R),
D_in (
fun x:R =>
y) (
fun x:R => 0)
D x0.
Lemma Dx :
forall (
D:R ->
Prop) (
x0:R),
D_in (
fun x:R =>
x) (
fun x:R => 1)
D x0.
Lemma Dadd :
forall (
D:R ->
Prop) (
df dg f g:R ->
R) (
x0:R),
D_in f df D x0 ->
D_in g dg D x0 ->
D_in (
fun x:R =>
f x +
g x) (
fun x:R =>
df x +
dg x)
D x0.
Lemma Dmult :
forall (
D:R ->
Prop) (
df dg f g:R ->
R) (
x0:R),
D_in f df D x0 ->
D_in g dg D x0 ->
D_in (
fun x:R =>
f x *
g x) (
fun x:R =>
df x *
g x +
f x *
dg x)
D x0.
Lemma Dmult_const :
forall (
D:R ->
Prop) (
f df:R ->
R) (
x0 a:R),
D_in f df D x0 ->
D_in (
fun x:R =>
a *
f x) (
fun x:R =>
a *
df x)
D x0.
Lemma Dopp :
forall (
D:R ->
Prop) (
f df:R ->
R) (
x0:R),
D_in f df D x0 ->
D_in (
fun x:R => -
f x) (
fun x:R => -
df x)
D x0.
Lemma Dminus :
forall (
D:R ->
Prop) (
df dg f g:R ->
R) (
x0:R),
D_in f df D x0 ->
D_in g dg D x0 ->
D_in (
fun x:R =>
f x -
g x) (
fun x:R =>
df x -
dg x)
D x0.
Lemma Dx_pow_n :
forall (
n:nat) (
D:R ->
Prop) (
x0:R),
D_in (
fun x:R =>
x ^
n) (
fun x:R =>
INR n *
x ^ (
n - 1))
D x0.
Lemma Dcomp :
forall (
Df Dg:R ->
Prop) (
df dg f g:R ->
R) (
x0:R),
D_in f df Df x0 ->
D_in g dg Dg (
f x0) ->
D_in (
fun x:R =>
g (
f x)) (
fun x:R =>
df x *
dg (
f x)) (
Dgf Df Dg f)
x0.
Lemma D_pow_n :
forall (
n:nat) (
D:R ->
Prop) (
x0:R) (
expr dexpr:R ->
R),
D_in expr dexpr D x0 ->
D_in (
fun x:R =>
expr x ^
n)
(
fun x:R =>
INR n *
expr x ^ (
n - 1) *
dexpr x) (
Dgf D D expr)
x0.