Rpower.v

(****************************************************************************                                                                                         IEEE754  :  Rpower                                                                                                                                          Laurent Thery                                                                                                                                     ***************************************************************************** Definition of an exponential function over relative numbers *)
Require Import Omega.
Require Import Reals.
Require Import Zpower.
Require Import fast_integer.
Require Import Digit.
Require Import Faux.
Require Import sTactic.
(* We have already an exponential over natural number,    we prove some basic properties for this function *)

Theorem pow_O: (e:R)(pow e O)==R1.

Theorem pow_1: (e:R)(pow e (1))==e.

Theorem pow_NR0: (e:R) (n:nat) ~ e==R0 ->~ (pow e n)==R0.

Theorem pow_add:
  (e:R) (n, m:nat)(pow e (plus n m))==(Rmult (pow e n) (pow e m)).

Theorem pow_is_exp_on_nat: (n, m:nat)(pow (INR n) m)==(INR (exp n m)).

Theorem pow_RN_plus:
  (e:R) (n, m:nat) ~ e==R0 ->
  (pow e n)==(Rmult (pow e (plus n m)) (Rinv (pow e m))).

Theorem pow_lt: (e:R) (n:nat) (Rlt R0 e) ->(Rlt R0 (pow e n)).

Theorem Rlt_pow_R1: (e:R) (n:nat) (Rlt R1 e) -> (lt O n) ->(Rlt R1 (pow e n)).

Theorem Rlt_pow:
  (e:R) (n, m:nat) (Rlt R1 e) -> (lt n m) ->(Rlt (pow e n) (pow e m)).

Theorem pow_abs: (r:R) (n:nat)(Rabsolu (pow r n))==(pow (Rabsolu r) n).

Theorem pow_inv: (r:R) (n:nat) ~ r==R0 ->(Rinv (pow r n))==(pow (Rinv r) n).

Theorem pow_R1: (r:R) (n:nat) (pow r n)==R1 ->(Rabsolu r)==R1 \/ n=O.

Theorem Zpower_NR0: (e:Z) (n:nat) (Zle ZERO e) ->(Zle ZERO (Zpower_nat e n)).

(* To define exponential over relative number, we simply do    a case analysis on the sign of the number *)

Definition powerRZ :=
   [e:R] [n:Z]
      Cases n of
          ZERO => R1
         | (POS p) => (pow e (convert p))
         | (NEG p) => (Rinv (pow e (convert p)))
      end.
(* we now prove some basic properties of our exponential *)

Theorem powerRZ_O: (e:R)(powerRZ e ZERO)==R1.

Theorem powerRZ_1: (e:R)(powerRZ e (Zs ZERO))==e.

Theorem powerRZ_NOR: (e:R) (z:Z) ~ e==R0 ->~ (powerRZ e z)==R0.

Theorem powerRZ_add:
  (e:R) (n, m:Z) ~ e==R0 ->
  (powerRZ e (Zplus n m))==(Rmult (powerRZ e n) (powerRZ e m)).

Theorem powerRZ_Zs:
  (e:R) (n:Z) ~ e==R0 ->(powerRZ e (Zs n))==(Rmult e (powerRZ e n)).
(* Conversion theorem between relative numbers and reals *)

Theorem Zpower_nat_powerRZ:
  (n, m:nat)
  (IZR (Zpower_nat (inject_nat n) m))==(powerRZ (INR n) (inject_nat m)).

Theorem powerRZ_lt: (e:R) (z:Z) (Rlt R0 e) ->(Rlt R0 (powerRZ e z)).

Theorem powerRZ_le: (e:R) (z:Z) (Rlt R0 e) ->(Rle R0 (powerRZ e z)).

Theorem Rlt_powerRZ:
  (e:R) (n, m:Z) (Rlt R1 e) -> (Zlt n m) ->(Rlt (powerRZ e n) (powerRZ e m)).

Theorem Rpow_R1:
  (r:R) (z:Z) ~ r==R0 -> (powerRZ r z)==R1 ->(Rabsolu r)==R1 \/ z=ZERO.

Theorem Rpow_eq_inv:
  (r:R) (p, q:Z) ~ r==R0 -> ~ (Rabsolu r)==R1 -> (powerRZ r p)==(powerRZ r q) ->
  p=q.

Theorem Zpower_nat_powerRZ_absolu:
  (n, m:Z) (Zle ZERO m) ->(IZR (Zpower_nat n (absolu m)))==(powerRZ (IZR n) m).

Theorem absolu_comp_Rpower:
  (p:Z) (n:nat)(absolu (Zpower_nat p n))=(exp (absolu p) n).

Theorem powerRZ_R1: (n:Z)(powerRZ R1 n)==R1.

Theorem Rle_powerRZ:
  (e:R) (n, m:Z) (Rle R1 e) -> (Zle n m) ->(Rle (powerRZ e n) (powerRZ e m)).

Theorem Zlt_powerRZ:
  (e:R) (n, m:Z) (Rle R1 e) -> (Rlt (powerRZ e n) (powerRZ e m)) ->(Zlt n m).

Theorem Zle_powerRZ:
  (e:R) (n, m:Z) (Rlt R1 e) -> (Rle (powerRZ e n) (powerRZ e m)) ->(Zle n m).
(* Conversion theorem between natural numbers and reals *)

Theorem powerRZ_is_exp:
  (m, n:nat) (lt O m) ->(powerRZ (INR m) (INZ n))==(INR (exp m n)).

30/05/01, 18:27