Library Coq.Reals.Rderiv
Definition of the derivative,continuity
Require Import Rbase.
Require Import Rfunctions.
Require Import Rlimit.
Require Import Fourier.
Require Import Omega.
Local Open 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.