Library Coq.Reals.Abstract.ConstructiveSum


Require Import QArith Qabs.
Require Import ConstructiveReals.
Require Import ConstructiveRealsMorphisms.
Require Import ConstructiveAbs.
Require Import ConstructiveLimits.

Local Open Scope ConstructiveReals.

Definition and properties of finite sums and powers.
WARNING: this file is experimental and likely to change in future releases.

Fixpoint CRsum {R : ConstructiveReals}
         (f:nat -> CRcarrier R) (N:nat) : CRcarrier R :=
  match N with
    | O => f 0%nat
    | S i => CRsum f i + f (S i)
  end.

Lemma CRsum_eq :
  forall {R : ConstructiveReals} (An Bn:nat -> CRcarrier R) (N:nat),
    (forall i:nat, (i <= N)%nat -> An i == Bn i) ->
    CRsum An N == CRsum Bn N.

Lemma sum_eq_R0 : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (n : nat),
    (forall k:nat, un k == 0)
    -> CRsum un n == 0.

Definition INR {R : ConstructiveReals} (n : nat) : CRcarrier R
  := CR_of_Q R (Z.of_nat n # 1).

Lemma sum_const : forall {R : ConstructiveReals} (a : CRcarrier R) (n : nat),
    CRsum (fun _ => a) n == a * INR (S n).

Lemma multiTriangleIneg : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (n : nat),
    CRabs R (CRsum u n) <= CRsum (fun k => CRabs R (u k)) n.

Lemma sum_assoc : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (n p : nat),
    CRsum u (S n + p)
    == CRsum u n + CRsum (fun k => u (S n + k)%nat) p.

Lemma sum_Rle : forall {R : ConstructiveReals} (un vn : nat -> CRcarrier R) (n : nat),
    (forall k, le k n -> un k <= vn k)
    -> CRsum un n <= CRsum vn n.

Lemma Abs_sum_maj : forall {R : ConstructiveReals} (un vn : nat -> CRcarrier R),
    (forall n:nat, CRabs R (un n) <= (vn n))
    -> forall n p:nat, (CRabs R (CRsum un n - CRsum un p) <=
              CRsum vn (Init.Nat.max n p) - CRsum vn (Init.Nat.min n p)).

Lemma cond_pos_sum : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (n : nat),
    (forall k, 0 <= un k)
    -> 0 <= CRsum un n.

Lemma pos_sum_more : forall {R : ConstructiveReals} (u : nat -> CRcarrier R)
                       (n p : nat),
    (forall k:nat, 0 <= u k)
    -> le n p -> CRsum u n <= CRsum u p.

Lemma sum_opp : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (n : nat),
    CRsum (fun k => - un k) n == - CRsum un n.

Lemma sum_scale : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (a : CRcarrier R) (n : nat),
    CRsum (fun k : nat => u k * a) n == CRsum u n * a.

Lemma sum_plus : forall {R : ConstructiveReals} (u v : nat -> CRcarrier R) (n : nat),
    CRsum (fun n0 : nat => u n0 + v n0) n == CRsum u n + CRsum v n.

Lemma decomp_sum :
  forall {R : ConstructiveReals} (An:nat -> CRcarrier R) (N:nat),
    (0 < N)%nat ->
    CRsum An N == An 0%nat + CRsum (fun i:nat => An (S i)) (pred N).

Lemma reverse_sum : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (n : nat),
    CRsum u n == CRsum (fun k => u (n-k)%nat) n.

Lemma Rplus_le_pos : forall {R : ConstructiveReals} (a b : CRcarrier R),
    0 <= b -> a <= a + b.

Lemma selectOneInSum : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (n i : nat),
    le i n
    -> (forall k:nat, 0 <= u k)
    -> u i <= CRsum u n.

Lemma splitSum : forall {R : ConstructiveReals} (un : nat -> CRcarrier R)
                        (filter : nat -> bool) (n : nat),
    CRsum un n
    == CRsum (fun i => if filter i then un i else 0) n
       + CRsum (fun i => if filter i then 0 else un i) n.

Definition series_cv {R : ConstructiveReals}
           (un : nat -> CRcarrier R) (s : CRcarrier R) : Set
  := CR_cv R (CRsum un) s.

Definition series_cv_lim_lt {R : ConstructiveReals}
           (un : nat -> CRcarrier R) (x : CRcarrier R) : Set
  := { l : CRcarrier R & prod (series_cv un l) (l < x) }.

Definition series_cv_le_lim {R : ConstructiveReals}
           (x : CRcarrier R) (un : nat -> CRcarrier R) : Set
  := { l : CRcarrier R & prod (series_cv un l) (x <= l) }.

Lemma series_cv_maj : forall {R : ConstructiveReals}
                        (un vn : nat -> CRcarrier R) (s : CRcarrier R),
    (forall n:nat, CRabs R (un n) <= vn n)
    -> series_cv vn s
    -> { l : CRcarrier R & prod (series_cv un l) (l <= s) }.

Lemma series_cv_abs_lt
  : forall {R : ConstructiveReals} (un vn : nat -> CRcarrier R) (l : CRcarrier R),
    (forall n:nat, CRabs R (un n) <= vn n)
    -> series_cv_lim_lt vn l
    -> series_cv_lim_lt un l.

Definition series_cv_abs {R : ConstructiveReals} (u : nat -> CRcarrier R)
  : CR_cauchy R (CRsum (fun n => CRabs R (u n)))
    -> { l : CRcarrier R & series_cv u l }.

Lemma series_cv_unique :
  forall {R : ConstructiveReals} (Un:nat -> CRcarrier R) (l1 l2:CRcarrier R),
    series_cv Un l1 -> series_cv Un l2 -> l1 == l2.

Lemma series_cv_abs_eq
  : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (a : CRcarrier R)
           (cau : CR_cauchy R (CRsum (fun n => CRabs R (u n)))),
    series_cv u a
    -> (a == (let (l,_):= series_cv_abs u cau in l))%ConstructiveReals.

Lemma series_cv_abs_cv
  : forall {R : ConstructiveReals} (u : nat -> CRcarrier R)
           (cau : CR_cauchy R (CRsum (fun n => CRabs R (u n)))),
    series_cv u (let (l,_):= series_cv_abs u cau in l).

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

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

Lemma series_cv_plus : forall {R : ConstructiveReals}
                         (u v : nat -> CRcarrier R) (s t : CRcarrier R),
    series_cv u s
    -> series_cv v t
    -> series_cv (fun n => u n + v n) (s + t).

Lemma series_cv_minus : forall {R : ConstructiveReals}
                          (u v : nat -> CRcarrier R) (s t : CRcarrier R),
    series_cv u s
    -> series_cv v t
    -> series_cv (fun n => u n - v n) (s - t).

Lemma series_cv_nonneg : forall {R : ConstructiveReals}
                           (u : nat -> CRcarrier R) (s : CRcarrier R),
    (forall n:nat, 0 <= u n) -> series_cv u s -> 0 <= s.

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

Lemma series_cv_remainder_maj : forall {R : ConstructiveReals} (u : nat -> CRcarrier R)
                                  (s eps : CRcarrier R)
                                  (N : nat),
    series_cv u s
    -> 0 < eps
    -> (forall n:nat, 0 <= u n)
    -> CRabs R (CRsum u N - s) <= eps
    -> forall n:nat, CRsum (fun k=> u (N + S k)%nat) n <= eps.

Lemma series_cv_abs_remainder : forall {R : ConstructiveReals} (u : nat -> CRcarrier R)
                                  (s sAbs : CRcarrier R)
                                  (n : nat),
    series_cv u s
    -> series_cv (fun n => CRabs R (u n)) sAbs
    -> CRabs R (CRsum u n - s)
      <= sAbs - CRsum (fun n => CRabs R (u n)) n.

Lemma series_cv_triangle : forall {R : ConstructiveReals}
                             (u : nat -> CRcarrier R) (s sAbs : CRcarrier R),
    series_cv u s
    -> series_cv (fun n => CRabs R (u n)) sAbs
    -> CRabs R s <= sAbs.

Lemma series_cv_shift :
  forall {R : ConstructiveReals} (f : nat -> CRcarrier R) k l,
    series_cv (fun n => f (S k + n)%nat) l
    -> series_cv f (l + CRsum f k).

Lemma series_cv_shift' : forall {R : ConstructiveReals}
                           (un : nat -> CRcarrier R) (s : CRcarrier R) (shift : nat),
    series_cv un s
    -> series_cv (fun n => un (n+shift)%nat)
                       (s - match shift with
                            | O => 0
                            | S p => CRsum un p
                            end).

Lemma CRmorph_sum : forall {R1 R2 : ConstructiveReals}
                      (f : @ConstructiveRealsMorphism R1 R2)
                      (un : nat -> CRcarrier R1) (n : nat),
  CRmorph f (CRsum un n) ==
  CRsum (fun n0 : nat => CRmorph f (un n0)) n.

Lemma CRmorph_INR : forall {R1 R2 : ConstructiveReals}
                      (f : @ConstructiveRealsMorphism R1 R2)
                      (n : nat),
  CRmorph f (INR n) == INR n.

Lemma CRmorph_series_cv : forall {R1 R2 : ConstructiveReals}
                     (f : @ConstructiveRealsMorphism R1 R2)
                     (un : nat -> CRcarrier R1)
                     (l : CRcarrier R1),
    series_cv un l
    -> series_cv (fun n => CRmorph f (un n)) (CRmorph f l).