FexpDiv.v

(****************************************************************************                                                                                         IEEE754  :  FexpDiv                                                                                                                                                    Sylvie Boldo                                                                                                                          ***************************************************************************** *)
Require Import Arith.
Require Import Reals.
Require Export Faux.
Require Export sTactic.
Section Div.
Variables wi, wi1, qi, D, N, qi1, wi2, ai, bi, eps1, eps2, eps3, ep:R.
Hypothesis Hw:<R> wi==(Rminus wi1 (Rmult qi D)).
Hypothesis Ha:(Rle (Rabsolu (Rmult (Rinv wi1) (Rminus ai wi1))) eps1).
Hypothesis Hb:(Rle (Rabsolu (Rmult (Rinv D) (Rminus bi D))) eps2).
Hypothesis Hq:
           (Rle
              (Rabsolu
                 (Rmult
                    (Rinv (Rmult (Rinv bi) ai)) (Rminus qi (Rmult (Rinv bi) ai))))
              eps3).
Hypothesis NZwi:~ wi1==R0.
Hypothesis NZD:~ D==R0.
Hypothesis NZbi:~ bi==R0.
Hypothesis NZai:~ ai==R0.
Hypothesis PosEps1:(Rle R0 eps1).
Hypothesis PosEps2:(Rle R0 eps2).
Hypothesis PosEps3:(Rle R0 eps3).
Hypothesis LeEps1:(Rlt eps1 R1).
Hypothesis LeEps2:(Rlt eps2 R1).
Hypothesis LeEps3:(Rlt eps3 R1).
Hypothesis Hep:<R> ep==(Rmax (Rmax eps1 eps2) eps3).

Theorem InegAbsInf:
  (x, y, eps:R) ~ x==R0 -> (Rle (Rabsolu (Rmult (Rinv x) (Rminus y x))) eps) ->
  (Rle (Rabsolu y) (Rmult (Rplus R1 eps) (Rabsolu x))).

Theorem InegAbsSup:
  (x, y, eps:R) ~ x==R0 -> (Rle (Rabsolu (Rmult (Rinv x) (Rminus y x))) eps) ->
  (Rle (Rmult (Rminus R1 eps) (Rabsolu x)) (Rabsolu y)).

Theorem DivFirstCase:
  (Rle
     (Rmult (Rminus (Rabsolu wi1) (Rabsolu (Rmult qi D))) (Rinv (Rabsolu wi1)))
     (Rminus
        R1
        (Rmult (Rmult (Rminus R1 eps3) (Rminus R1 eps1)) (Rinv (Rplus R1 eps2))))).

Theorem DivSecondCase:
  (Rle
     (Rmult (Rminus (Rabsolu (Rmult qi D)) (Rabsolu wi1)) (Rinv (Rabsolu wi1)))
     (Rminus
        (Rmult (Rmult (Rplus R1 eps3) (Rplus R1 eps1)) (Rinv (Rminus R1 eps2)))
        R1)).

Definition dsd := [x, y:R](Rle R0 x) /\ (Rle R0 y) \/ (Rle x R0) /\ (Rle y R0).

Theorem dsdAbs:
  (x, y:R) (dsd x y) ->
  (Rabsolu (Rminus x y))==(Rabsolu (Rminus (Rabsolu x) (Rabsolu y))).

Theorem dsdsym: (x, y:R) (dsd x y) ->(dsd y x).

Theorem Inegdsd:
  (x, y, eps:R)
  ~ x==R0 ->
  (Rlt eps R1) -> (Rle (Rabsolu (Rmult (Rinv x) (Rminus y x))) eps) ->(dsd x y).

Theorem dsdtrans: (x, y, z:R) (dsd x y) -> (dsd y z) -> ~ y==R0 ->(dsd x z).

Theorem dsdinv: (x, y:R) (dsd x y) -> ~ y==R0 ->(dsd x (Rinv y)).

Theorem dsdmult: (x, y, r:R) (dsd x y) ->(dsd (Rmult r x) (Rmult r y)).

Theorem dsdwi1qiD: (dsd wi1 (Rmult qi D)).

Theorem Maxwiwi1:
  (Rle
     (Rmult (Rabsolu wi) (Rinv (Rabsolu wi1)))
     (Rmax
        (Rminus
           R1
           (Rmult
              (Rmult (Rminus R1 eps3) (Rminus R1 eps1)) (Rinv (Rplus R1 eps2))))
        (Rminus
           (Rmult
              (Rmult (Rplus R1 eps3) (Rplus R1 eps1)) (Rinv (Rminus R1 eps2)))
           R1))).

Theorem Rmax_simpl1: (p, q:R) (Rle p q) ->(Rmax p q)==q.

Theorem RmaxProp: (P:R ->Prop) (x, y:R) (P x) -> (P y) ->(P (Rmax x y)).

Theorem ep_aux:
  ((Rle R0 ep) /\ (Rlt ep R1)) /\
  ((Rle eps1 ep) /\ ((Rle eps2 ep) /\ (Rle eps3 ep))).

Theorem ConvDiv:
  (Rle
     (Rmult (Rabsolu wi) (Rinv (Rabsolu wi1)))
     (Rmult
        (Rplus ep (Rplus ep (Rplus ep (Rmult ep ep)))) (Rinv (Rminus R1 ep)))).
End Div.

30/05/01, 17:53