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.
Copyright (C) 2011-2015 Catherine Lelay
Copyright (C) 2011-2015 Guillaume Melquiond
From Coq Require Import Reals Psatz ssreflect.
Require Import Rcomplements Lim_seq Rbar Hierarchy.
Local Tactic Notation "intuition" := (intuition auto with arith zarith real).
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.
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).
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.
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).
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)).