Library Stdlib.Reals.Abstract.ConstructiveLimits

From Stdlib Require Import PeanoNat QArith Qabs.
From Stdlib Require Import ConstructiveReals.
From Stdlib Require Import ConstructiveAbs.

Local Open Scope ConstructiveReals.

Lemma CR_cv_extens
  : forall {R : ConstructiveReals} (xn yn : nat -> CRcarrier R) (l : CRcarrier R),
    (forall n:nat, xn n == yn n)
    -> CR_cv R xn l
    -> CR_cv R yn l.

Lemma CR_cv_opp : forall {R : ConstructiveReals} (xn : nat -> CRcarrier R) (l : CRcarrier R),
    CR_cv R xn l
    -> CR_cv R (fun n => - xn n) (- l).

Lemma CR_cv_plus : forall {R : ConstructiveReals} (xn yn : nat -> CRcarrier R) (a b : CRcarrier R),
    CR_cv R xn a
    -> CR_cv R yn b
    -> CR_cv R (fun n => xn n + yn n) (a + b).

Lemma CR_cv_unique : forall {R : ConstructiveReals} (xn : nat -> CRcarrier R)
                       (a b : CRcarrier R),
    CR_cv R xn a
    -> CR_cv R xn b
    -> a == b.

Lemma CR_cv_eq : forall {R : ConstructiveReals}
                   (v u : nat -> CRcarrier R) (s : CRcarrier R),
    (forall n:nat, u n == v n)
    -> CR_cv R u s
    -> CR_cv R v s.

Lemma CR_cauchy_eq : forall {R : ConstructiveReals}
                       (un vn : nat -> CRcarrier R),
    (forall n:nat, un n == vn n)
    -> CR_cauchy R un
    -> CR_cauchy R vn.

Lemma CR_cv_proper : forall {R : ConstructiveReals}
                       (un : nat -> CRcarrier R) (a b : CRcarrier R),
    CR_cv R un a
    -> a == b
    -> CR_cv R un b.

#[global]
Instance CR_cv_morph
  : forall {R : ConstructiveReals} (un : nat -> CRcarrier R), CMorphisms.Proper
      (CMorphisms.respectful (CReq R) CRelationClasses.iffT) (CR_cv R un).

Lemma Un_cv_nat_real : forall {R : ConstructiveReals}
                         (un : nat -> CRcarrier R) (l : CRcarrier R),
    CR_cv R un l
    -> forall eps : CRcarrier R,
      0 < eps
      -> { p : nat & forall i:nat, le p i -> CRabs R (un i - l) < eps }.

Lemma Un_cv_real_nat : forall {R : ConstructiveReals}
                         (un : nat -> CRcarrier R) (l : CRcarrier R),
    (forall eps : CRcarrier R,
      0 < eps
      -> { p : nat & forall i:nat, le p i -> CRabs R (un i - l) < eps })
    -> CR_cv R un l.

Lemma CR_cv_minus :
  forall {R : ConstructiveReals}
    (An Bn:nat -> CRcarrier R) (l1 l2:CRcarrier R),
    CR_cv R An l1 -> CR_cv R Bn l2
    -> CR_cv R (fun i:nat => An i - Bn i) (l1 - l2).

Lemma CR_cv_nonneg :
  forall {R : ConstructiveReals} (An:nat -> CRcarrier R) (l:CRcarrier R),
    CR_cv R An l
    -> (forall n:nat, 0 <= An n)
    -> 0 <= l.

Lemma CR_cv_scale : forall {R : ConstructiveReals} (u : nat -> CRcarrier R)
                      (a : CRcarrier R) (s : CRcarrier R),
    CR_cv R u s -> CR_cv R (fun n => u n * a) (s * a).

Lemma CR_cv_const : forall {R : ConstructiveReals} (a : CRcarrier R),
    CR_cv R (fun n => a) a.

Lemma Rcv_cauchy_mod : forall {R : ConstructiveReals}
                         (un : nat -> CRcarrier R) (l : CRcarrier R),
    CR_cv R un l -> CR_cauchy R un.

Lemma CR_growing_transit : forall {R : ConstructiveReals} (un : nat -> CRcarrier R),
    (forall n:nat, un n <= un (S n))
    -> forall n p : nat, le n p -> un n <= un p.

Lemma growing_ineq :
  forall {R : ConstructiveReals} (Un:nat -> CRcarrier R) (l:CRcarrier R),
    (forall n:nat, Un n <= Un (S n))
    -> CR_cv R Un l -> forall n:nat, Un n <= l.

Lemma CR_cv_open_below
  : forall {R : ConstructiveReals}
      (un : nat -> CRcarrier R) (m l : CRcarrier R),
    CR_cv R un l
    -> m < l
    -> { n : nat & forall i:nat, le n i -> m < un i }.

Lemma CR_cv_open_above
  : forall {R : ConstructiveReals}
      (un : nat -> CRcarrier R) (m l : CRcarrier R),
    CR_cv R un l
    -> l < m
    -> { n : nat & forall i:nat, le n i -> un i < m }.

Lemma CR_cv_bound_down : forall {R : ConstructiveReals}
                           (u : nat -> CRcarrier R) (A l : CRcarrier R) (N : nat),
    (forall n:nat, le N n -> A <= u n)
    -> CR_cv R u l
    -> A <= l.

Lemma CR_cv_bound_up : forall {R : ConstructiveReals}
                         (u : nat -> CRcarrier R) (A l : CRcarrier R) (N : nat),
    (forall n:nat, le N n -> u n <= A)
    -> CR_cv R u l
    -> l <= A.

Lemma CR_cv_le : forall {R : ConstructiveReals}
                   (u v : nat -> CRcarrier R) (a b : CRcarrier R),
    (forall n:nat, u n <= v n)
    -> CR_cv R u a
    -> CR_cv R v b
    -> a <= b.

Lemma CR_cv_abs_cont : forall {R : ConstructiveReals}
                         (u : nat -> CRcarrier R) (s : CRcarrier R),
    CR_cv R u s
    -> CR_cv R (fun n => CRabs R (u n)) (CRabs R s).

Lemma CR_cv_dist_cont : forall {R : ConstructiveReals}
                          (u : nat -> CRcarrier R) (a s : CRcarrier R),
    CR_cv R u s
    -> CR_cv R (fun n => CRabs R (a - u n)) (CRabs R (a - s)).

Lemma CR_cv_shift :
  forall {R : ConstructiveReals} f k l,
    CR_cv R (fun n => f (n + k)%nat) l -> CR_cv R f l.

Lemma CR_cv_shift' :
  forall {R : ConstructiveReals} f k l,
    CR_cv R f l -> CR_cv R (fun n => f (n + k)%nat) l.