Library Coq.Reals.Ranalysis2
Require Import Rbase.
Require Import Rfunctions.
Require Import Ranalysis1.
Local Open 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 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 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
).