Library Coq.Reals.Ranalysis1
Basic operations on functions
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_locally_ext :
forall f g a x, 0
< a -> (forall y,
R_dist y x < a -> f y = g y) ->
continuity_pt f x -> continuity_pt g 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
Main rules
Rules for derivable_pt_lim (value of the derivative at a point)
Lemma derivable_pt_lim_id :
forall x:
R,
derivable_pt_lim id x 1.
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_lim_opp :
forall f (
x l:
R),
derivable_pt_lim f x l -> derivable_pt_lim (
- f)
x (
- l).
Lemma derivable_pt_lim_opp_fwd :
forall f (
x l:
R),
derivable_pt_lim f x (
- l)
-> derivable_pt_lim (
- f)
x l.
Lemma derivable_pt_lim_opp_rev :
forall f (
x l:
R),
derivable_pt_lim (
- f)
x (
- l)
-> derivable_pt_lim f x l.
Lemma derivable_pt_lim_mirr_fwd :
forall f (
x l:
R),
derivable_pt_lim f (
- x) (
- l)
-> derivable_pt_lim (
mirr_fct f)
x l.
Lemma derivable_pt_lim_mirr_rev :
forall f (
x l:
R),
derivable_pt_lim (
mirr_fct f) (
- x) (
- l)
-> derivable_pt_lim f x l.
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_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_div_scal :
forall f x l a,
derivable_pt_lim f x l ->
derivable_pt_lim (
fun y =>
f y / a)
x (
l / a).
Lemma derivable_pt_lim_scal_right :
forall f x l a,
derivable_pt_lim f x l ->
derivable_pt_lim (
fun y =>
f y * a)
x (
l * a).
Lemma derivable_pt_lim_Rsqr :
forall x:
R,
derivable_pt_lim Rsqr x (2
* x).
Rules for derivable_pt (derivability at a point)
Lemma derivable_pt_id :
forall x:
R,
derivable_pt id 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_pt_xeq:
forall (
f :
R -> R) (
x1 x2 :
R),
x1=x2 -> derivable_pt f x1 -> derivable_pt f x2.
Lemma derivable_pt_opp :
forall (
f :
R -> R) (
x:
R),
derivable_pt f x -> derivable_pt (
- f)
x.
Lemma derivable_pt_opp_rev:
forall (
f :
R -> R) (
x :
R),
derivable_pt (
- f)
x -> derivable_pt f x.
Lemma derivable_pt_mirr:
forall (
f :
R -> R) (
x :
R),
derivable_pt f (
-x)
-> derivable_pt (
mirr_fct f)
x.
Lemma derivable_pt_mirr_rev:
forall (
f :
R -> R) (
x :
R),
derivable_pt (
mirr_fct f) (
- x)
-> derivable_pt f x.
Lemma derivable_pt_mirr_prem:
forall (
f :
R -> R) (
x :
R),
derivable_pt (
mirr_fct f)
x -> derivable_pt f (
-x).
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_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_Rsqr :
forall x:
R,
derivable_pt Rsqr x.
Rules for derivable (derivability on whole domain)
Rules for derive_pt (derivative function on whole domain)
Lemma derive_pt_id :
forall x:
R,
derive_pt id x (
derivable_pt_id _)
= 1.
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.
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_opp_rev :
forall f (
x:
R) (
pr1:
derivable_pt (
- f)
x),
derive_pt (
- f)
x pr1 = - derive_pt f x (
derivable_pt_opp_rev _ _ pr1).
Lemma derive_pt_mirr :
forall f (
x:
R) (
pr1:
derivable_pt f (
-x)),
derive_pt (
mirr_fct f)
x (
derivable_pt_mirr _ _ pr1)
= - derive_pt f (
-x)
pr1.
Lemma derive_pt_mirr_rev :
forall f (
x:
R) (
pr1:
derivable_pt (
mirr_fct f)
x),
derive_pt (
mirr_fct f)
x pr1 = - derive_pt f (
-x) (
derivable_pt_mirr_prem f x pr1).
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_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_Rsqr :
forall x:
R,
derive_pt Rsqr x (
derivable_pt_Rsqr _)
= 2
* x.
Definition and derivative of power function with natural number exponent
Irrelevance of derivability proof for derivative
In dependently typed environments it is sometimes hard to rewrite.
Having pr_nu for separate x with a proof that they are equal helps.
Local extremum's condition