Library Coq.Reals.Ranalysis1
Require Import Rbase.
Require Import Rfunctions.
Require Export Rlimit.
Require Export Rderiv.
Open Local Scope R_scope.
Implicit Type f :
R ->
R.
Basic operations on functions
Definition plus_fct f1 f2 (
x:R) :
R :=
f1 x +
f2 x.
Definition opp_fct f (
x:R) :
R := -
f x.
Definition mult_fct f1 f2 (
x:R) :
R :=
f1 x *
f2 x.
Definition mult_real_fct (
a:R)
f (
x:R) :
R :=
a *
f x.
Definition minus_fct f1 f2 (
x:R) :
R :=
f1 x -
f2 x.
Definition div_fct f1 f2 (
x:R) :
R :=
f1 x /
f2 x.
Definition div_real_fct (
a:R)
f (
x:R) :
R :=
a /
f x.
Definition comp f1 f2 (
x:R) :
R :=
f1 (
f2 x).
Definition inv_fct f (
x:R) :
R := /
f x.
Delimit Scope Rfun_scope with F.
Infix "+" :=
plus_fct :
Rfun_scope.
Notation "- x" := (
opp_fct x) :
Rfun_scope.
Infix "*" :=
mult_fct :
Rfun_scope.
Infix "-" :=
minus_fct :
Rfun_scope.
Infix "/" :=
div_fct :
Rfun_scope.
Notation Local "f1 'o' f2" := (
comp f1 f2)
(
at level 20,
right associativity) :
Rfun_scope.
Notation "/ x" := (
inv_fct x) :
Rfun_scope.
Definition fct_cte (
a x:R) :
R :=
a.
Definition id (
x:R) :=
x.
Definition increasing f :
Prop :=
forall x y:R,
x <=
y ->
f x <=
f y.
Definition decreasing f :
Prop :=
forall x y:R,
x <=
y ->
f y <=
f x.
Definition strict_increasing f :
Prop :=
forall x y:R,
x <
y ->
f x <
f y.
Definition strict_decreasing f :
Prop :=
forall x y:R,
x <
y ->
f y <
f x.
Definition constant f :
Prop :=
forall x y:R,
f x =
f y.
Definition no_cond (
x:R) :
Prop :=
True.
Definition constant_D_eq f (
D:R ->
Prop) (
c:R) :
Prop :=
forall x:R,
D x ->
f x =
c.
Definition of continuity as a limit
Definition continuity_pt f (
x0:R) :
Prop :=
continue_in f no_cond x0.
Definition continuity f :
Prop :=
forall x:R,
continuity_pt f x.
Lemma continuity_pt_plus :
forall f1 f2 (
x0:R),
continuity_pt f1 x0 ->
continuity_pt f2 x0 ->
continuity_pt (
f1 +
f2)
x0.
Lemma continuity_pt_opp :
forall f (
x0:R),
continuity_pt f x0 ->
continuity_pt (-
f)
x0.
Lemma continuity_pt_minus :
forall f1 f2 (
x0:R),
continuity_pt f1 x0 ->
continuity_pt f2 x0 ->
continuity_pt (
f1 -
f2)
x0.
Lemma continuity_pt_mult :
forall f1 f2 (
x0:R),
continuity_pt f1 x0 ->
continuity_pt f2 x0 ->
continuity_pt (
f1 *
f2)
x0.
Lemma continuity_pt_const :
forall f (
x0:R),
constant f ->
continuity_pt f x0.
Lemma continuity_pt_scal :
forall f (
a x0:R),
continuity_pt f x0 ->
continuity_pt (
mult_real_fct a f)
x0.
Lemma continuity_pt_inv :
forall f (
x0:R),
continuity_pt f x0 ->
f x0 <> 0 ->
continuity_pt (/
f)
x0.
Lemma div_eq_inv :
forall f1 f2, (
f1 /
f2)%F = (
f1 * /
f2)%F.
Lemma continuity_pt_div :
forall f1 f2 (
x0:R),
continuity_pt f1 x0 ->
continuity_pt f2 x0 ->
f2 x0 <> 0 ->
continuity_pt (
f1 /
f2)
x0.
Lemma continuity_pt_comp :
forall f1 f2 (
x:R),
continuity_pt f1 x ->
continuity_pt f2 (
f1 x) ->
continuity_pt (
f2 o f1)
x.
Lemma continuity_plus :
forall f1 f2,
continuity f1 ->
continuity f2 ->
continuity (
f1 +
f2).
Lemma continuity_opp :
forall f,
continuity f ->
continuity (-
f).
Lemma continuity_minus :
forall f1 f2,
continuity f1 ->
continuity f2 ->
continuity (
f1 -
f2).
Lemma continuity_mult :
forall f1 f2,
continuity f1 ->
continuity f2 ->
continuity (
f1 *
f2).
Lemma continuity_const :
forall f,
constant f ->
continuity f.
Lemma continuity_scal :
forall f (
a:R),
continuity f ->
continuity (
mult_real_fct a f).
Lemma continuity_inv :
forall f,
continuity f -> (
forall x:R,
f x <> 0) ->
continuity (/
f).
Lemma continuity_div :
forall f1 f2,
continuity f1 ->
continuity f2 -> (
forall x:R,
f2 x <> 0) ->
continuity (
f1 /
f2).
Lemma continuity_comp :
forall f1 f2,
continuity f1 ->
continuity f2 ->
continuity (
f2 o f1).
Derivative's definition using Landau's kernel
Class of differential functions
Equivalence of this definition with the one using limit concept
derivability -> continuity
Lemma derivable_pt_lim_plus :
forall f1 f2 (
x l1 l2:R),
derivable_pt_lim f1 x l1 ->
derivable_pt_lim f2 x l2 ->
derivable_pt_lim (
f1 +
f2)
x (
l1 +
l2).
Lemma derivable_pt_lim_opp :
forall f (
x l:R),
derivable_pt_lim f x l ->
derivable_pt_lim (-
f)
x (-
l).
Lemma derivable_pt_lim_minus :
forall f1 f2 (
x l1 l2:R),
derivable_pt_lim f1 x l1 ->
derivable_pt_lim f2 x l2 ->
derivable_pt_lim (
f1 -
f2)
x (
l1 -
l2).
Lemma derivable_pt_lim_mult :
forall f1 f2 (
x l1 l2:R),
derivable_pt_lim f1 x l1 ->
derivable_pt_lim f2 x l2 ->
derivable_pt_lim (
f1 *
f2)
x (
l1 *
f2 x +
f1 x *
l2).
Lemma derivable_pt_lim_const :
forall a x:R,
derivable_pt_lim (
fct_cte a)
x 0.
Lemma derivable_pt_lim_scal :
forall f (
a x l:R),
derivable_pt_lim f x l ->
derivable_pt_lim (
mult_real_fct a f)
x (
a *
l).
Lemma derivable_pt_lim_id :
forall x:R,
derivable_pt_lim id x 1.
Lemma derivable_pt_lim_Rsqr :
forall x:R,
derivable_pt_lim Rsqr x (2 *
x).
Lemma derivable_pt_lim_comp :
forall f1 f2 (
x l1 l2:R),
derivable_pt_lim f1 x l1 ->
derivable_pt_lim f2 (
f1 x)
l2 ->
derivable_pt_lim (
f2 o f1)
x (
l2 *
l1).
Lemma derivable_pt_plus :
forall f1 f2 (
x:R),
derivable_pt f1 x ->
derivable_pt f2 x ->
derivable_pt (
f1 +
f2)
x.
Lemma derivable_pt_opp :
forall f (
x:R),
derivable_pt f x ->
derivable_pt (-
f)
x.
Lemma derivable_pt_minus :
forall f1 f2 (
x:R),
derivable_pt f1 x ->
derivable_pt f2 x ->
derivable_pt (
f1 -
f2)
x.
Lemma derivable_pt_mult :
forall f1 f2 (
x:R),
derivable_pt f1 x ->
derivable_pt f2 x ->
derivable_pt (
f1 *
f2)
x.
Lemma derivable_pt_const :
forall a x:R,
derivable_pt (
fct_cte a)
x.
Lemma derivable_pt_scal :
forall f (
a x:R),
derivable_pt f x ->
derivable_pt (
mult_real_fct a f)
x.
Lemma derivable_pt_id :
forall x:R,
derivable_pt id x.
Lemma derivable_pt_Rsqr :
forall x:R,
derivable_pt Rsqr x.
Lemma derivable_pt_comp :
forall f1 f2 (
x:R),
derivable_pt f1 x ->
derivable_pt f2 (
f1 x) ->
derivable_pt (
f2 o f1)
x.
Lemma derivable_plus :
forall f1 f2,
derivable f1 ->
derivable f2 ->
derivable (
f1 +
f2).
Lemma derivable_opp :
forall f,
derivable f ->
derivable (-
f).
Lemma derivable_minus :
forall f1 f2,
derivable f1 ->
derivable f2 ->
derivable (
f1 -
f2).
Lemma derivable_mult :
forall f1 f2,
derivable f1 ->
derivable f2 ->
derivable (
f1 *
f2).
Lemma derivable_const :
forall a:R,
derivable (
fct_cte a).
Lemma derivable_scal :
forall f (
a:R),
derivable f ->
derivable (
mult_real_fct a f).
Lemma derivable_id :
derivable id.
Lemma derivable_Rsqr :
derivable Rsqr.
Lemma derivable_comp :
forall f1 f2,
derivable f1 ->
derivable f2 ->
derivable (
f2 o f1).
Lemma derive_pt_plus :
forall f1 f2 (
x:R) (
pr1:derivable_pt
f1 x) (
pr2:derivable_pt
f2 x),
derive_pt (
f1 +
f2)
x (
derivable_pt_plus _ _ _ pr1 pr2) =
derive_pt f1 x pr1 +
derive_pt f2 x pr2.
Lemma derive_pt_opp :
forall f (
x:R) (
pr1:derivable_pt
f x),
derive_pt (-
f)
x (
derivable_pt_opp _ _ pr1) = -
derive_pt f x pr1.
Lemma derive_pt_minus :
forall f1 f2 (
x:R) (
pr1:derivable_pt
f1 x) (
pr2:derivable_pt
f2 x),
derive_pt (
f1 -
f2)
x (
derivable_pt_minus _ _ _ pr1 pr2) =
derive_pt f1 x pr1 -
derive_pt f2 x pr2.
Lemma derive_pt_mult :
forall f1 f2 (
x:R) (
pr1:derivable_pt
f1 x) (
pr2:derivable_pt
f2 x),
derive_pt (
f1 *
f2)
x (
derivable_pt_mult _ _ _ pr1 pr2) =
derive_pt f1 x pr1 *
f2 x +
f1 x *
derive_pt f2 x pr2.
Lemma derive_pt_const :
forall a x:R,
derive_pt (
fct_cte a)
x (
derivable_pt_const a x) = 0.
Lemma derive_pt_scal :
forall f (
a x:R) (
pr:derivable_pt
f x),
derive_pt (
mult_real_fct a f)
x (
derivable_pt_scal _ _ _ pr) =
a *
derive_pt f x pr.
Lemma derive_pt_id :
forall x:R,
derive_pt id x (
derivable_pt_id _) = 1.
Lemma derive_pt_Rsqr :
forall x:R,
derive_pt Rsqr x (
derivable_pt_Rsqr _) = 2 *
x.
Lemma derive_pt_comp :
forall f1 f2 (
x:R) (
pr1:derivable_pt
f1 x) (
pr2:derivable_pt
f2 (
f1 x)),
derive_pt (
f2 o f1)
x (
derivable_pt_comp _ _ _ pr1 pr2) =
derive_pt f2 (
f1 x)
pr2 *
derive_pt f1 x pr1.
Definition pow_fct (
n:nat) (
y:R) :
R :=
y ^
n.
Lemma derivable_pt_lim_pow_pos :
forall (
x:R) (
n:nat),
(0 <
n)%nat ->
derivable_pt_lim (
fun y:R =>
y ^
n)
x (
INR n *
x ^
pred n).
Lemma derivable_pt_lim_pow :
forall (
x:R) (
n:nat),
derivable_pt_lim (
fun y:R =>
y ^
n)
x (
INR n *
x ^
pred n).
Lemma derivable_pt_pow :
forall (
n:nat) (
x:R),
derivable_pt (
fun y:R =>
y ^
n)
x.
Lemma derivable_pow :
forall n:nat,
derivable (
fun y:R =>
y ^
n).
Lemma derive_pt_pow :
forall (
n:nat) (
x:R),
derive_pt (
fun y:R =>
y ^
n)
x (
derivable_pt_pow n x) =
INR n *
x ^
pred n.
Lemma pr_nu :
forall f (
x:R) (
pr1 pr2:derivable_pt
f x),
derive_pt f x pr1 =
derive_pt f x pr2.
Local extremum's condition
Theorem deriv_maximum :
forall f (
a b c:R) (
pr:derivable_pt
f c),
a <
c ->
c <
b ->
(
forall x:R,
a <
x ->
x <
b ->
f x <=
f c) ->
derive_pt f c pr = 0.
Theorem deriv_minimum :
forall f (
a b c:R) (
pr:derivable_pt
f c),
a <
c ->
c <
b ->
(
forall x:R,
a <
x ->
x <
b ->
f c <=
f x) ->
derive_pt f c pr = 0.
Theorem deriv_constant2 :
forall f (
a b c:R) (
pr:derivable_pt
f c),
a <
c ->
c <
b -> (
forall x:R,
a <
x ->
x <
b ->
f x =
f c) ->
derive_pt f c pr = 0.
Lemma nonneg_derivative_0 :
forall f (
pr:derivable
f),
increasing f ->
forall x:R, 0 <=
derive_pt f x (
pr x).