From Stdlib Require Export ArithRing.

From Stdlib Require Import Rdefinitions Raxioms RIneq.
From Stdlib Require Export Rpow_def.
From Stdlib Require Export R_Ifp.
From Stdlib Require Export Rbasic_fun.
From Stdlib Require Export R_sqr.
From Stdlib Require Export SplitAbsolu.
From Stdlib Require Export SplitRmult.
From Stdlib Require Export ArithProp.
From Stdlib Require Import Zpower.
From Stdlib Require Import Znat.
From Stdlib Require Import Arith.Factorial.
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).