Library Coquelicot.Series

This file is part of the Coquelicot formalization of real analysis in Coq: http://coquelicot.saclay.inria.fr/

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 Psatz.
Require Import mathcomp.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 : nat → V) (l : V) :=
   filterlim (sum_n a) (eventually) (locally l).

Definition ex_series (a : nat → V) :=
   ∃ l : V , is_series a l.

Definition Cauchy_series (a : nat → V) :=
  ∀ 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 : nat → R) : R :=
   real (Lim_seq (sum_n a)).

Lemma ex_series_dec (a : nat → R) :
  {ex_series a } + {¬ ex_series a }.

Lemma is_series_unique (a : nat → R) (l : R) :
  is_series a l → Series a = l.
Lemma Series_correct (a : nat → R) :
  ex_series a → is_series a (Series a).

Lemma is_series_Reals (a : nat → R) (l : R) :
  is_series a l ↔ infinite_sum a l.

Lemma ex_series_Reals_0 (a : nat → R) :
  ex_series a → { l:R | Un_cv (fun N:nat ⇒ sum_f_R0 a N) l }.

Lemma ex_series_Reals_1 (a : nat → R) :
  { l:R | Un_cv (fun N:nat ⇒ sum_f_R0 a N) l } → ex_series a.

Cauchy

Lemma Cauchy_ex_series {K : AbsRing} {V : CompleteNormedModule K}
  (a : nat → V) :
  ex_series a → Cauchy_series a.

Lemma ex_series_Cauchy {K : AbsRing} {V : CompleteNormedModule K}
  (a : nat → V) :
  Cauchy_series a → ex_series a.

Section Properties1.

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

Extensionality

Lemma is_series_ext (a b : nat → V) (l : V) :
  (∀ n, a n = b n ) → (is_series a l )
    → is_series b l.
Lemma ex_series_ext (a b : nat → V) :
  (∀ n, a n = b n ) → ex_series a
    → ex_series b.
Lemma Series_ext (a b : nat → R) :
  (∀ n, a n = b n ) → Series a = Series b.

Index offset

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

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

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

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

Lemma ex_series_incr_1 (a : nat → V) :
  ex_series a ↔ ex_series (fun k ⇒ a (S k)%nat).

Lemma ex_series_incr_n (a : nat → V) (n : nat) :
  ex_series a ↔ ex_series (fun k ⇒ a (n + k)%nat).

End Properties1.

Lemma Series_incr_1 (a : nat → R) :
  ex_series a → Series a = a O + Series (fun k ⇒ a (S k)).

Lemma Series_incr_n (a : nat → R) (n : nat) :
  (0 < n)%nat → ex_series a
    → Series a = sum_f_R0 a (pred n) + Series (fun k ⇒ a (n + k)%nat).

Lemma Series_incr_1_aux (a : nat → R) :
  a O = 0 → Series a = Series (fun k ⇒ a (S k)).
Lemma Series_incr_n_aux (a : nat → R) (n : nat) :
   (∀ k, (k < n)%nat → a k = 0)
     → Series a = Series (fun k ⇒ a (n + k)%nat).

Convergence theorems

Lemma Cauchy_series_Reals (a : nat → R) :
  Cauchy_series a ↔ Cauchy_crit_series a.

Lemma ex_series_lim_0 (a : nat → R) :
  ex_series a → is_lim_seq a 0.

Lemma ex_series_Rabs (a : nat → R) :
  ex_series (fun n ⇒ Rabs (a n)) → ex_series a.

Lemma Series_Rabs (a : nat → R) :
  ex_series (fun n ⇒ Rabs (a n)) →
    Rabs (Series a) ≤ Series (fun n ⇒ Rabs (a n)).

Comparison

Lemma ex_series_le {K : AbsRing} {V : CompleteNormedModule K}
  (a : nat → V) (b : nat → R) :
   (∀ n : nat, norm (a n) ≤ b n ) →
   ex_series b → ex_series a.

Lemma Series_le (a b : nat → R) :
  (∀ n : nat, 0 ≤ a n ≤ b n ) →
   ex_series b → Series a ≤ Series b.

Operations

Additive operators

Section Properties2.

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

Lemma is_series_opp (a : nat → V) (la : V) :
  is_series a la
    → is_series (fun n ⇒ opp (a n)) (opp la).

Lemma ex_series_opp (a : nat → V) :
  ex_series a
    → ex_series (fun n ⇒ opp (a n)).
Lemma Series_opp (a : nat → R) :
  Series (fun n ⇒ - a n) = - Series a.

Lemma is_series_plus (a b : nat → V) (la lb : V) :
  is_series a la → is_series b lb
    → is_series (fun n ⇒ plus (a n) (b n)) (plus la lb).
Lemma ex_series_plus (a b : nat → V) :
  ex_series a → ex_series b
    → ex_series (fun n ⇒ plus (a n) (b n)).

Lemma is_series_minus (a b : nat → V) (la lb : V) :
  is_series a la → is_series b lb
    → is_series (fun n ⇒ plus (a n) (opp (b n))) (plus la (opp lb)).
Lemma ex_series_minus (a b : nat → V) :
  ex_series a → ex_series b
    → ex_series (fun n ⇒ plus (a n) (opp (b n))).

End Properties2.

Lemma Series_plus (a b : nat → R) :
  ex_series a → ex_series b
    → Series (fun n ⇒ a n + b n) = Series a + Series b.

Lemma Series_minus (a b : nat → R) :
  ex_series a → ex_series b
    → Series (fun n ⇒ a 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 : nat → V) (l : V) :
  is_series a l → is_series (fun n ⇒ scal c (a n)) (scal c l).
Lemma is_series_scal_l : ∀ (c : K) (a : nat → V) (l : V),
  is_series a l → is_series (fun n ⇒ scal c (a n)) (scal c l).

Lemma ex_series_scal (c : K) (a : nat → V) :
  ex_series a → ex_series (fun n ⇒ scal c (a n)).

Lemma ex_series_scal_l : ∀ (c : K) (a : nat → V),
  ex_series a → ex_series (fun n ⇒ scal c (a n)).

End Properties3.

Lemma Series_scal_l (c : R) (a : nat → R) :
  Series (fun n ⇒ c × a n) = c × Series a.

Lemma is_series_scal_r (c : R) (a : nat → R) (l : R) :
  is_series a l → is_series (fun n ⇒ (a n ) × c) (l × c).
Lemma ex_series_scal_r (c : R) (a : nat → R) :
  ex_series a → ex_series (fun n ⇒ a n × c).

Lemma Series_scal_r (c : R) (a : nat → R) :
  Series (fun n ⇒ a n × c) = Series a × c.

Lemma is_series_mult_pos (a b : nat → R) (la lb : R) :
  is_series a la → is_series b lb →
  (∀ n, 0 ≤ a n ) → (∀ n, 0 ≤ b n )
  → is_series (fun n ⇒ sum_f_R0 (fun k ⇒ a k × b (n - k)%nat) n) (la × lb).

Lemma is_series_mult (a b : nat → R) (la lb : R) :
  is_series a la → is_series b lb
  → ex_series (fun n ⇒ Rabs (a n)) → ex_series (fun n ⇒ Rabs (b n))
  → is_series (fun n ⇒ sum_f_R0 (fun k ⇒ a k × b (n - k)%nat) n) (la × lb).

D'Alembert criterion

Lemma ex_series_DAlembert (a : nat → R) (k : R) :
  k < 1 → (∀ n, a n ≠ 0)
    → is_lim_seq (fun n ⇒ Rabs (a (S n) / a n)) k
      → ex_series (fun n ⇒ Rabs (a n)).

Lemma not_ex_series_DAlembert (a : nat → R) (l : R) :
  l > 1 → (∀ n, a n ≠ 0)
    → is_lim_seq (fun n ⇒ Rabs (a (S n) / a n)) l
      → ¬ is_lim_seq a 0.

Lemma partial_summation_R (a b : nat → R) :
  (∃ M, ∀ n, norm (sum_n b n) ≤ M )
  → filterlim a eventually (locally 0)
  → ex_series (fun n ⇒ norm (minus (a (S n)) (a n)))
  → ex_series (fun n ⇒ scal (a n) (b n)).

Geometric series

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