Require Export ArithRing.

Require Import Rdefinitions Raxioms RIneq.
Require Export Rpow_def.
Require Export R_Ifp.
Require Export Rbasic_fun.
Require Export R_sqr.
Require Export SplitAbsolu.
Require Export SplitRmult.
Require Export ArithProp.
Require Import Zpower.
Require Import Ztac.
Local Open Scope nat_scope.
Local Open Scope R_scope.

Lemma INR_fact_neq_0 : forall n:nat, INR (fact n) <> 0.

Lemma fact_simpl : forall n:nat, fact (S n) = (S n * fact n)%nat.

Lemma simpl_fact :
  forall n:nat, / INR (fact (S n)) * / / INR (fact n) = / INR (S n).

Infix "^" := pow : R_scope.

Lemma pow_O : forall x:R, x ^ 0 = 1.

Lemma pow_1 : forall x:R, x ^ 1 = x.

Lemma pow_add : forall (x:R) (n m:nat), x ^ (n + m) = x ^ n * x ^ m.

Lemma Rpow_mult_distr : forall (x y:R) (n:nat), (x * y) ^ n = x^n * y^n.

Lemma pow_nonzero : forall (x:R) (n:nat), x <> 0 -> x ^ n <> 0.

#[global]
Hint Resolve pow_O pow_1 pow_add pow_nonzero: real.

Lemma pow_RN_plus :
  forall (x:R) (n m:nat), x <> 0 -> x ^ n = x ^ (n + m) * / x ^ m.

Lemma pow_lt : forall (x:R) (n:nat), 0 < x -> 0 < x ^ n.
#[global]
Hint Resolve pow_lt: real.

Lemma Rlt_pow_R1 : forall (x:R) (n:nat), 1 < x -> (0 < n)%nat -> 1 < x ^ n.
#[global]
Hint Resolve Rlt_pow_R1: real.

Lemma Rlt_pow : forall (x:R) (n m:nat), 1 < x -> (n < m)%nat -> x ^ n < x ^ m.
#[global]
Hint Resolve Rlt_pow: real.

Lemma tech_pow_Rmult : forall (x:R) (n:nat), x * x ^ n = x ^ S n.

Lemma tech_pow_Rplus :
  forall (x:R) (a n:nat), x ^ a + INR n * x ^ a = INR (S n) * x ^ a.

Lemma poly : forall (n:nat) (x:R), 0 < x -> 1 + INR n * x <= (1 + x) ^ n.

Lemma Power_monotonic :
  forall (x:R) (m n:nat),
    Rabs x > 1 -> (m <= n)%nat -> Rabs (x ^ m) <= Rabs (x ^ n).

Lemma RPow_abs : forall (x:R) (n:nat), Rabs x ^ n = Rabs (x ^ n).

Lemma Pow_x_infinity :
  forall x:R,
    Rabs x > 1 ->
    forall b:R,
    exists N : nat, (forall n:nat, (n >= N)%nat -> Rabs (x ^ n) >= b).

Lemma pow_ne_zero : forall n:nat, n <> 0%nat -> 0 ^ n = 0.

Lemma pow_inv x n : (/ x)^n = / x^n.

Lemma Rinv_pow_depr : forall (x:R) (n:nat), x <> 0 -> / x ^ n = (/ x) ^ n.

#[deprecated(since="8.16",note="Use pow_inv.")]
Notation Rinv_pow := Rinv_pow_depr.

Lemma pow_lt_1_zero :
  forall x:R,
    Rabs x < 1 ->
    forall y:R,
      0 < y ->
      exists N : nat, (forall n:nat, (n >= N)%nat -> Rabs (x ^ n) < y).

Lemma pow_R1 : forall (r:R) (n:nat), r ^ n = 1 -> Rabs r = 1 \/ n = 0%nat.

Lemma pow_Rsqr : forall (x:R) (n:nat), x ^ (2 * n) = Rsqr x ^ n.

Lemma pow_le : forall (a:R) (n:nat), 0 <= a -> 0 <= a ^ n.

Lemma pow_1_even : forall n:nat, (-1) ^ (2 * n) = 1.

Lemma pow_1_odd : forall n:nat, (-1) ^ S (2 * n) = -1.

Lemma pow_1_abs : forall n:nat, Rabs ((-1) ^ n) = 1.

Lemma pow_mult : forall (x:R) (n1 n2:nat), x ^ (n1 * n2) = (x ^ n1) ^ n2.

Lemma pow_incr : forall (x y:R) (n:nat), 0 <= x <= y -> x ^ n <= y ^ n.

Lemma pow_R1_Rle : forall (x:R) (k:nat), 1 <= x -> 1 <= x ^ k.

Lemma Rle_pow :
  forall (x:R) (m n:nat), 1 <= x -> (m <= n)%nat -> x ^ m <= x ^ n.

Lemma pow1 : forall n:nat, 1 ^ n = 1.

Lemma pow_Rabs : forall (x:R) (n:nat), x ^ n <= Rabs x ^ n.

Lemma pow_maj_Rabs : forall (x y:R) (n:nat), Rabs y <= x -> y ^ n <= x ^ n.

Lemma Rsqr_pow2 : forall x, Rsqr x = x ^ 2.

Section PowerRZ.

Local Coercion Z_of_nat : nat >-> Z.

Section Z_compl.

Local Open Scope Z_scope.

Inductive Z_spec (x : Z) : Z -> Type :=
| ZintNull : x = 0 -> Z_spec x 0
| ZintPos (n : nat) : x = n -> Z_spec x n
| ZintNeg (n : nat) : x = - n -> Z_spec x (- n).

Lemma intP (x : Z) : Z_spec x x.

End Z_compl.

Definition powerRZ (x:R) (n:Z) :=
  match n with
    | Z0 => 1
    | Zpos p => x ^ Pos.to_nat p
    | Zneg p => / x ^ Pos.to_nat p
  end.

Local Infix "^Z" := powerRZ (at level 30, right associativity) : R_scope.

Lemma Zpower_NR0 :
  forall (x:Z) (n:nat), (0 <= x)%Z -> (0 <= Zpower_nat x n)%Z.

Lemma powerRZ_O : forall x:R, x ^Z 0 = 1.

Lemma powerRZ_1 : forall x:R, x ^Z Z.succ 0 = x.

Lemma powerRZ_NOR : forall (x:R) (z:Z), x <> 0 -> x ^Z z <> 0.

Lemma powerRZ_pos_sub (x:R) (n m:positive) : x <> 0 ->
   x ^Z (Z.pos_sub n m) = x ^ Pos.to_nat n * / x ^ Pos.to_nat m.

Lemma powerRZ_add :
  forall (x:R) (n m:Z), x <> 0 -> x ^Z (n + m) = x ^Z n * x ^Z m.
#[local]
Hint Resolve powerRZ_O powerRZ_1 powerRZ_NOR powerRZ_add: real.

Lemma Zpower_nat_powerRZ :
  forall n m:nat, IZR (Zpower_nat (Z.of_nat n) m) = INR n ^Z Z.of_nat m.

Lemma Zpower_pos_powerRZ :
  forall n m, IZR (Z.pow_pos n m) = IZR n ^Z Zpos m.

Lemma powerRZ_lt : forall (x:R) (z:Z), 0 < x -> 0 < x ^Z z.
#[local]
Hint Resolve powerRZ_lt: real.

Lemma powerRZ_le : forall (x:R) (z:Z), 0 < x -> 0 <= x ^Z z.
#[local]
Hint Resolve powerRZ_le: real.

Lemma Zpower_nat_powerRZ_absolu :
  forall n m:Z, (0 <= m)%Z -> IZR (Zpower_nat n (Z.abs_nat m)) = IZR n ^Z m.

Lemma powerRZ_R1 : forall n:Z, 1 ^Z n = 1.

Local Open Scope Z_scope.

Lemma pow_powerRZ (r : R) (n : nat) :
  (r ^ n)%R = powerRZ r (Z_of_nat n).

Lemma powerRZ_ind (P : Z -> R -> R -> Prop) :
  (forall x, P 0 x 1%R) ->
  (forall x n, P (Z.of_nat n) x (x ^ n)%R) ->
  (forall x n, P ((-(Z.of_nat n))%Z) x (Rinv (x ^ n))) ->
  forall x (m : Z), P m x (powerRZ x m)%R.

Lemma powerRZ_inv' x alpha : powerRZ (/ x) alpha = Rinv (powerRZ x alpha).

Lemma powerRZ_inv_depr x alpha : (x <> 0)%R -> powerRZ (/ x) alpha = Rinv (powerRZ x alpha).

Lemma powerRZ_neg' x : forall alpha, powerRZ x (- alpha) = Rinv (powerRZ x alpha).

Lemma powerRZ_neg_depr x : forall alpha, x <> R0 -> powerRZ x (- alpha) = powerRZ (/ x) alpha.

Lemma powerRZ_mult m x y : (powerRZ (x*y) m = powerRZ x m * powerRZ y m)%R.

Lemma powerRZ_mult_distr_depr :
  forall m x y, ((0 <= m)%Z \/ (x * y <> 0)%R) ->
           (powerRZ (x*y) m = powerRZ x m * powerRZ y m)%R.

End PowerRZ.

#[deprecated(since="8.16",note="Use powerRZ_inv'.")]
Notation powerRZ_inv := powerRZ_inv_depr.

#[deprecated(since="8.16",note="Use powerRZ_neg' and powerRZ_inv'.")]
Notation powerRZ_neg := powerRZ_neg_depr.

#[deprecated(since="8.16",note="Use powerRZ_mult.")]
Notation powerRZ_mult_distr := powerRZ_mult_distr_depr.

Local Infix "^Z" := powerRZ (at level 30, right associativity) : R_scope.


Definition decimal_exp (r:R) (z:Z) : R := (r * 10 ^Z z).

Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) : nat :=
  match n with
    | O => f 0%nat
    | S n' => (sum_nat_f_O f n' + f (S n'))%nat
  end.

Definition sum_nat_f (s n:nat) (f:nat -> nat) : nat :=
  sum_nat_f_O (fun x:nat => f (x + s)%nat) (n - s).

Definition sum_nat_O (n:nat) : nat := sum_nat_f_O (fun x:nat => x) n.

Definition sum_nat (s n:nat) : nat := sum_nat_f s n (fun x:nat => x).

Fixpoint sum_f_R0 (f:nat -> R) (N:nat) : R :=
  match N with
    | O => f 0%nat
    | S i => sum_f_R0 f i + f (S i)
  end.

Definition sum_f (s n:nat) (f:nat -> R) : R :=
  sum_f_R0 (fun x:nat => f (x + s)%nat) (n - s).

Lemma GP_finite :
  forall (x:R) (n:nat),
    sum_f_R0 (fun n:nat => x ^ n) n * (x - 1) = x ^ (n + 1) - 1.

Lemma sum_f_R0_triangle :
  forall (x:nat -> R) (n:nat),
    Rabs (sum_f_R0 x n) <= sum_f_R0 (fun i:nat => Rabs (x i)) n.

Definition Rdist (x y:R) : R := Rabs (x - y).

Lemma Rdist_pos : forall x y:R, Rdist x y >= 0.

Lemma Rdist_sym : forall x y:R, Rdist x y = Rdist y x.

Lemma Rdist_refl : forall x y:R, Rdist x y = 0 <-> x = y.

Lemma Rdist_eq : forall x:R, Rdist x x = 0.

Lemma Rdist_tri : forall x y z:R, Rdist x y <= Rdist x z + Rdist z y.

Lemma Rdist_plus :
  forall a b c d:R, Rdist (a + c) (b + d) <= Rdist a b + Rdist c d.

Lemma Rdist_mult_l : forall a b c,
  Rdist (a * b) (a * c) = Rabs a * Rdist b c.

Notation R_dist := Rdist (only parsing).
Notation R_dist_pos := Rdist_pos (only parsing).
Notation R_dist_sym := Rdist_sym (only parsing).
Notation R_dist_refl := Rdist_refl (only parsing).
Notation R_dist_eq := Rdist_eq (only parsing).
Notation R_dist_tri := Rdist_tri (only parsing).
Notation R_dist_plus := Rdist_plus (only parsing).
Notation R_dist_mult_l := Rdist_mult_l (only parsing).

Definition infinite_sum (s:nat -> R) (l:R) : Prop :=
  forall eps:R,
    eps > 0 ->
    exists N : nat,
      (forall n:nat, (n >= N)%nat -> Rdist (sum_f_R0 s n) l < eps).

Notation infinit_sum := infinite_sum (only parsing).