Library Coquelicot.Series

This file is part of the Coquelicot formalization of real analysis in Coq: http://coquelicot.saclay.inria.fr/
Copyright (C) 2011-2015 Sylvie Boldo
Copyright (C) 2011-2015 Catherine Lelay
Copyright (C) 2011-2015 Guillaume Melquiond
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Require Import Reals Omega Ssreflect.ssreflect.
Require Import Rcomplements.
Require Import Lim_seq Rbar Hierarchy.

This file gives definitions and properties about series defined on a normed module. An equivalence with the standard library and several convergence criteria are provided.

Section Definitions.

Definitions


Context {K : AbsRing} {V : NormedModule K}.

Definition is_series (a : natV) (l : V) :=
   filterlim (sum_n a) (eventually) (locally l).

Definition ex_series (a : natV) :=
    l : V, is_series a l.

Definition Cauchy_series (a : natV) :=
   eps : posreal,
     N : nat, n m : nat,
      (N n)%nat → (N m)%nat
      norm (sum_n_m a n m) < eps.

End Definitions.

Definition Series (a : natR) : R :=
   real (Lim_seq (sum_n a)).

Lemma ex_series_dec (a : natR) :
  {ex_series a} + {¬ ex_series a}.

Lemma is_series_unique (a : natR) (l : R) :
  is_series a lSeries a = l.
Lemma Series_correct (a : natR) :
  ex_series ais_series a (Series a).

Lemma is_series_Reals (a : natR) (l : R) :
  is_series a l infinite_sum a l.

Lemma ex_series_Reals_0 (a : natR) :
  ex_series a{ l:R | Un_cv (fun N:natsum_f_R0 a N) l }.

Lemma ex_series_Reals_1 (a : natR) :
  { l:R | Un_cv (fun N:natsum_f_R0 a N) l }ex_series a.

Cauchy

Lemma Cauchy_ex_series {K : AbsRing} {V : CompleteNormedModule K}
  (a : natV) :
  ex_series aCauchy_series a.

Lemma ex_series_Cauchy {K : AbsRing} {V : CompleteNormedModule K}
  (a : natV) :
  Cauchy_series aex_series a.

Section Properties1.

Context {K : AbsRing} {V : NormedModule K}.

Extensionality

Lemma is_series_ext (a b : natV) (l : V) :
  ( n, a n = b n) → (is_series a l)
    → is_series b l.
Lemma ex_series_ext (a b : natV) :
  ( n, a n = b n) → ex_series a
    → ex_series b.
Lemma Series_ext (a b : natR) :
  ( n, a n = b n) → Series a = Series b.

Index offset

Lemma is_series_incr_1 (a : natV) (l : V) :
  is_series a (plus l (a O))
    → is_series (fun ka (S k)%nat) l.

Lemma is_series_incr_n (a : natV) (n : nat) (l : V) :
  (0 < n)%natis_series a (plus l (sum_n a (pred n)))
    → is_series (fun ka (n + k)%nat) l.

Lemma is_series_decr_1 (a : natV) (l : V) :
  is_series (fun ka (S k)%nat) (plus l (opp (a O))) → is_series a l.

Lemma is_series_decr_n (a : natV) (n : nat) (l : V) :
  (0 < n)%natis_series (fun ka (n + k)%nat) (plus l (opp (sum_n a (pred n))))
    → is_series a l.

Lemma ex_series_incr_1 (a : natV) :
  ex_series a ex_series (fun ka (S k)%nat).

Lemma ex_series_incr_n (a : natV) (n : nat) :
  ex_series a ex_series (fun ka (n + k)%nat).

End Properties1.

Lemma Series_incr_1 (a : natR) :
  ex_series aSeries a = a O + Series (fun ka (S k)).

Lemma Series_incr_n (a : natR) (n : nat) :
  (0 < n)%natex_series a
    → Series a = sum_f_R0 a (pred n) + Series (fun ka (n + k)%nat).

Lemma Series_incr_1_aux (a : natR) :
  a O = 0 → Series a = Series (fun ka (S k)).
Lemma Series_incr_n_aux (a : natR) (n : nat) :
   ( k, (k < n)%nata k = 0)
     → Series a = Series (fun ka (n + k)%nat).

Convergence theorems


Lemma Cauchy_series_Reals (a : natR) :
  Cauchy_series a Cauchy_crit_series a.

Lemma ex_series_lim_0 (a : natR) :
  ex_series ais_lim_seq a 0.

Lemma ex_series_Rabs (a : natR) :
  ex_series (fun nRabs (a n)) → ex_series a.

Lemma Series_Rabs (a : natR) :
  ex_series (fun nRabs (a n)) →
    Rabs (Series a) Series (fun nRabs (a n)).

Comparison

Lemma ex_series_le {K : AbsRing} {V : CompleteNormedModule K}
  (a : natV) (b : natR) :
   ( n : nat, norm (a n) b n) →
   ex_series bex_series a.

Lemma Series_le (a b : natR) :
  ( n : nat, 0 a n b n) →
   ex_series bSeries a Series b.

Operations

Additive operators

Section Properties2.

Context {K : AbsRing} {V : NormedModule K}.

Lemma is_series_opp (a : natV) (la : V) :
  is_series a la
    → is_series (fun nopp (a n)) (opp la).

Lemma ex_series_opp (a : natV) :
  ex_series a
    → ex_series (fun nopp (a n)).
Lemma Series_opp (a : natR) :
  Series (fun n- a n) = - Series a.

Lemma is_series_plus (a b : natV) (la lb : V) :
  is_series a lais_series b lb
    → is_series (fun nplus (a n) (b n)) (plus la lb).
Lemma ex_series_plus (a b : natV) :
  ex_series aex_series b
    → ex_series (fun nplus (a n) (b n)).

Lemma is_series_minus (a b : natV) (la lb : V) :
  is_series a lais_series b lb
    → is_series (fun nplus (a n) (opp (b n))) (plus la (opp lb)).
Lemma ex_series_minus (a b : natV) :
  ex_series aex_series b
    → ex_series (fun nplus (a n) (opp (b n))).

End Properties2.

Lemma Series_plus (a b : natR) :
  ex_series aex_series b
    → Series (fun na n + b n) = Series a + Series b.

Lemma Series_minus (a b : natR) :
  ex_series aex_series b
    → Series (fun na n - b n) = Series a - Series b.

Multiplication by a scalar

Section Properties3.

Context {K : AbsRing} {V : NormedModule K}.

Lemma is_series_scal (c : K) (a : natV) (l : V) :
  is_series a lis_series (fun nscal c (a n)) (scal c l).
Lemma is_series_scal_l : (c : K) (a : natV) (l : V),
  is_series a lis_series (fun nscal c (a n)) (scal c l).

Lemma ex_series_scal (c : K) (a : natV) :
  ex_series aex_series (fun nscal c (a n)).

Lemma ex_series_scal_l : (c : K) (a : natV),
  ex_series aex_series (fun nscal c (a n)).

End Properties3.

Lemma Series_scal_l (c : R) (a : natR) :
  Series (fun nc × a n) = c × Series a.

Lemma is_series_scal_r (c : R) (a : natR) (l : R) :
  is_series a lis_series (fun n(a n) × c) (l × c).
Lemma ex_series_scal_r (c : R) (a : natR) :
  ex_series aex_series (fun na n × c).

Lemma Series_scal_r (c : R) (a : natR) :
  Series (fun na n × c) = Series a × c.

Lemma is_series_mult_pos (a b : natR) (la lb : R) :
  is_series a lais_series b lb
  ( n, 0 a n) → ( n, 0 b n)
  → is_series (fun nsum_f_R0 (fun ka k × b (n - k)%nat) n) (la × lb).

Lemma is_series_mult (a b : natR) (la lb : R) :
  is_series a lais_series b lb
  → ex_series (fun nRabs (a n)) → ex_series (fun nRabs (b n))
  → is_series (fun nsum_f_R0 (fun ka k × b (n - k)%nat) n) (la × lb).

D'Alembert criterion


Lemma ex_series_DAlembert (a : natR) (k : R) :
  k < 1 → ( n, a n 0)
    → is_lim_seq (fun nRabs (a (S n) / a n)) k
      → ex_series (fun nRabs (a n)).

Lemma not_ex_series_DAlembert (a : natR) (l : R) :
  l > 1 → ( n, a n 0)
    → is_lim_seq (fun nRabs (a (S n) / a n)) l
      → ¬ is_lim_seq a 0.

Lemma partial_summation_R (a b : natR) :
  ( M, n, norm (sum_n b n) M)
  → filterlim a eventually (locally 0)
  → ex_series (fun nnorm (minus (a (S n)) (a n)))
  → ex_series (fun nscal (a n) (b n)).

Geometric series


Lemma is_series_geom (q : R) :
  Rabs q < 1 → is_series (fun nq ^ n) (/ (1-q)).
Lemma ex_series_geom (q : R) :
  Rabs q < 1 → ex_series (fun nq ^ n).
Lemma Series_geom (q : R) :
  Rabs q < 1 → Series (fun nq ^ n) = / (1-q).