Library Coq.Reals.Ranalysis2
Require Import Rbase.
Require Import Rfunctions.
Require Import Ranalysis1.
Open Local Scope R_scope.
Lemma formule :
forall (
x h l1 l2:R) (
f1 f2:R ->
R),
h <> 0 ->
f2 x <> 0 ->
f2 (
x +
h) <> 0 ->
(
f1 (
x +
h) /
f2 (
x +
h) -
f1 x /
f2 x) /
h -
(
l1 *
f2 x -
l2 *
f1 x) /
Rsqr (
f2 x) =
/
f2 (
x +
h) * ((
f1 (
x +
h) -
f1 x) /
h -
l1) +
l1 / (
f2 x *
f2 (
x +
h)) * (
f2 x -
f2 (
x +
h)) -
f1 x / (
f2 x *
f2 (
x +
h)) * ((
f2 (
x +
h) -
f2 x) /
h -
l2) +
l2 *
f1 x / (
Rsqr (
f2 x) *
f2 (
x +
h)) * (
f2 (
x +
h) -
f2 x).
Lemma Rmin_pos :
forall x y:R, 0 <
x -> 0 <
y -> 0 <
Rmin x y.
Lemma maj_term1 :
forall (
x h eps l1 alp_f2:R) (
eps_f2 alp_f1d:posreal)
(
f1 f2:R ->
R),
0 <
eps ->
f2 x <> 0 ->
f2 (
x +
h) <> 0 ->
(
forall h:R,
h <> 0 ->
Rabs h <
alp_f1d ->
Rabs ((
f1 (
x +
h) -
f1 x) /
h -
l1) <
Rabs (
eps *
f2 x / 8)) ->
(
forall a:R,
Rabs a <
Rmin eps_f2 alp_f2 -> /
Rabs (
f2 (
x +
a)) < 2 /
Rabs (
f2 x)) ->
h <> 0 ->
Rabs h <
alp_f1d ->
Rabs h <
Rmin eps_f2 alp_f2 ->
Rabs (/
f2 (
x +
h) * ((
f1 (
x +
h) -
f1 x) /
h -
l1)) <
eps / 4.
Lemma maj_term2 :
forall (
x h eps l1 alp_f2 alp_f2t2:R) (
eps_f2:posreal)
(
f2:R ->
R),
0 <
eps ->
f2 x <> 0 ->
f2 (
x +
h) <> 0 ->
(
forall a:R,
Rabs a <
alp_f2t2 ->
Rabs (
f2 (
x +
a) -
f2 x) <
Rabs (
eps *
Rsqr (
f2 x) / (8 *
l1))) ->
(
forall a:R,
Rabs a <
Rmin eps_f2 alp_f2 -> /
Rabs (
f2 (
x +
a)) < 2 /
Rabs (
f2 x)) ->
h <> 0 ->
Rabs h <
alp_f2t2 ->
Rabs h <
Rmin eps_f2 alp_f2 ->
l1 <> 0 ->
Rabs (
l1 / (
f2 x *
f2 (
x +
h)) * (
f2 x -
f2 (
x +
h))) <
eps / 4.
Lemma maj_term3 :
forall (
x h eps l2 alp_f2:R) (
eps_f2 alp_f2d:posreal)
(
f1 f2:R ->
R),
0 <
eps ->
f2 x <> 0 ->
f2 (
x +
h) <> 0 ->
(
forall h:R,
h <> 0 ->
Rabs h <
alp_f2d ->
Rabs ((
f2 (
x +
h) -
f2 x) /
h -
l2) <
Rabs (
Rsqr (
f2 x) *
eps / (8 *
f1 x))) ->
(
forall a:R,
Rabs a <
Rmin eps_f2 alp_f2 -> /
Rabs (
f2 (
x +
a)) < 2 /
Rabs (
f2 x)) ->
h <> 0 ->
Rabs h <
alp_f2d ->
Rabs h <
Rmin eps_f2 alp_f2 ->
f1 x <> 0 ->
Rabs (
f1 x / (
f2 x *
f2 (
x +
h)) * ((
f2 (
x +
h) -
f2 x) /
h -
l2)) <
eps / 4.
Lemma maj_term4 :
forall (
x h eps l2 alp_f2 alp_f2c:R) (
eps_f2:posreal)
(
f1 f2:R ->
R),
0 <
eps ->
f2 x <> 0 ->
f2 (
x +
h) <> 0 ->
(
forall a:R,
Rabs a <
alp_f2c ->
Rabs (
f2 (
x +
a) -
f2 x) <
Rabs (
Rsqr (
f2 x) *
f2 x *
eps / (8 *
f1 x *
l2))) ->
(
forall a:R,
Rabs a <
Rmin eps_f2 alp_f2 -> /
Rabs (
f2 (
x +
a)) < 2 /
Rabs (
f2 x)) ->
h <> 0 ->
Rabs h <
alp_f2c ->
Rabs h <
Rmin eps_f2 alp_f2 ->
f1 x <> 0 ->
l2 <> 0 ->
Rabs (
l2 *
f1 x / (
Rsqr (
f2 x) *
f2 (
x +
h)) * (
f2 (
x +
h) -
f2 x)) <
eps / 4.
Lemma D_x_no_cond :
forall x a:R,
a <> 0 ->
D_x no_cond x (
x +
a).
Lemma Rabs_4 :
forall a b c d:R,
Rabs (
a +
b +
c +
d) <=
Rabs a +
Rabs b +
Rabs c +
Rabs d.
Lemma Rlt_4 :
forall a b c d e f g h:R,
a <
b ->
c <
d ->
e <
f ->
g <
h ->
a +
c +
e +
g <
b +
d +
f +
h.
Lemma Rmin_2 :
forall a b c:R,
a <
b ->
a <
c ->
a <
Rmin b c.
Lemma quadruple :
forall x:R, 4 *
x =
x +
x +
x +
x.
Lemma quadruple_var :
forall x:R,
x =
x / 4 +
x / 4 +
x / 4 +
x / 4.
Lemma continuous_neq_0 :
forall (
f:R ->
R) (
x0:R),
continuity_pt f x0 ->
f x0 <> 0 ->
exists eps :
posreal, (
forall h:R,
Rabs h <
eps ->
f (
x0 +
h) <> 0).