Library Coquelicot.PSeries

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 Even Div2 Omega Psatz.
Require Import mathcomp.ssreflect.ssreflect.
Require Import Rcomplements Rbar Lim_seq Lub Hierarchy.
Require Import Continuity Derive Seq_fct Series.

This file describes power series: Σ ak xk. It contains definition, equivalence with the standard library, differentiability, integrability, and many results about the convergence circle.

Section Definitions.

Definition


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

Definition is_pseries (a : nat → V) (x:K) (l : V) :=
  is_series (fun k ⇒ scal (pow_n x k) (a k)) l.

Definition ex_pseries (a : nat → V) (x : K) :=
  ex_series (fun k ⇒ scal (pow_n x k) (a k)).

End Definitions.

Definition PSeries (a : nat → R) (x : R) : R :=
  Series (fun k ⇒ a k × x ^ k).

Lemma ex_pseries_dec {V : NormedModule R_AbsRing} (a : nat → R) (x : R) :
  {ex_pseries a x} + {¬ ex_pseries a x}.

Lemma is_pseries_R (a : nat → R) (x l : R) :
  is_pseries a x l ↔ is_series (fun n : nat ⇒ a n × x ^ n) l.

Lemma ex_pseries_R (a : nat → R) (x : R) :
  ex_pseries a x ↔ ex_series (fun n : nat ⇒ a n × x ^ n).

Lemma PSeries_eq (a : nat → R) (x : R) :
  PSeries a x = Series (fun k ⇒ scal (pow_n x k) (a k)).

Lemma PSeries_1 (a : nat → R) :
  PSeries a 1 = Series a.
Lemma ex_pseries_1 (a : nat → R) :
  ex_pseries a 1 ↔ ex_series a.

Lemma is_pseries_unique (a : nat → R) (x l : R) :
  is_pseries a x l → PSeries a x = l.
Lemma PSeries_correct (a : nat → R) (x : R) :
  ex_pseries a x → is_pseries a x (PSeries a x).

Equivalence with standard library Reals

Lemma is_pseries_Reals (a : nat → R) (x l : R) :
  is_pseries a x l ↔ Pser a x l.

Extensionality

Section Extensionality.

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

Lemma is_pseries_ext (a b : nat → V) (x : K) (l:V) :
  (∀ n, a n = b n) → (is_pseries a x l)
    → is_pseries b x l.

Lemma ex_pseries_ext (a b : nat → V) (x : K) :
  (∀ n, a n = b n) → ex_pseries a x
    → ex_pseries b x.

End Extensionality.

Lemma PSeries_ext (a b : nat → R) (x : R) :
  (∀ n, a n = b n) → PSeries a x = PSeries b x.

Convergence circle

A power series is always defined at 0

Section ConvergenceCircle.

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

Lemma is_pseries_0 (a : nat → V) :
  is_pseries a zero (a O).

Lemma ex_pseries_0 (a : nat → V) :
  ex_pseries a zero.

End ConvergenceCircle.

Lemma PSeries_0 (a : nat → R) :
  PSeries a 0 = a O.

Convergence disk
Definition CV_disk (a : nat → R) (r : R) :=
  ex_series (fun n ⇒ Rabs (a n × r^n)).

Lemma CV_disk_le (a : nat → R) (r1 r2 : R) :
  Rabs r1 ≤ Rabs r2 → CV_disk a r2 → CV_disk a r1.
Lemma CV_disk_correct (a : nat → R) (x : R) :
  CV_disk a x → ex_pseries a x.

Lemma CV_disk_0 (a : nat → R) :
  CV_disk a 0.

Definition CV_radius (a : nat → R) : Rbar :=
  Lub_Rbar (CV_disk a).

Lemma CV_radius_ge_0 (a : nat → R) :
  Rbar_le (Finite 0) (CV_radius a).

Lemma CV_radius_bounded (a : nat → R) :
  is_lub_Rbar (fun r ⇒ ∃ M, ∀ n, Rabs (a n × r ^ n) ≤ M) (CV_radius a).

Convergence theorems

Lemma CV_disk_inside (a : nat → R) (x : R) :
  Rbar_lt (Finite (Rabs x)) (CV_radius a)
    → ex_series (fun n ⇒ Rabs (a n × x ^ n)).
Lemma CV_radius_inside (a : nat → R) (x : R) :
  Rbar_lt (Finite (Rabs x)) (CV_radius a)
    → ex_pseries a x.

Lemma CV_disk_outside (a : nat → R) (x : R) :
  Rbar_lt (CV_radius a) (Finite (Rabs x))
    → ¬ is_lim_seq (fun n ⇒ a n × x ^ n) 0.

Lemma CV_radius_ext (a b : nat → R) :
  (∀ n, a n = b n) → CV_radius a = CV_radius b.

Convergence criteria

D'Alembert criterion for power series

Lemma CV_disk_DAlembert_aux (a : nat → R) (x k : R) :
  x ≠ 0 → (∀ n, a n ≠ 0) →
  (is_lim_seq (fun n ⇒ Rabs (a (S n) / a n)) k
    ↔ is_lim_seq (fun n ⇒ Rabs ((a (S n) × x^(S n)) / (a n × x ^ n))) (Rabs x × k)).

Lemma CV_disk_DAlembert (a : nat → R) (x:R) l :
  (∀ n:nat, a n ≠ 0) →
  is_lim_seq (fun n:nat ⇒ Rabs (a (S n) / a n)) (Finite l) →
  (l = 0 ∨ (l ≠ 0 ∧ Rabs x < / l))
    → CV_disk a x.

Lemma CV_radius_finite_DAlembert (a : nat → R) (l : R) :
  (∀ n:nat, a n ≠ 0) → 0 < l →
  is_lim_seq (fun n:nat ⇒ Rabs (a (S n) / a n)) l →
  CV_radius a = Finite (/l).

Lemma CV_radius_infinite_DAlembert (a : nat → R) :
  (∀ n:nat, a n ≠ 0) →
  is_lim_seq (fun n:nat ⇒ Rabs (a (S n) / a n)) 0 →
  CV_radius a = p_infty.

Equivalence with standard library Reals

Lemma CV_radius_Reals_0 (a : nat → R) (r : posreal) :
  Rbar_lt (Finite r) (CV_radius a) → CVN_r (fun n x ⇒ a n × x ^ n) r.

Lemma CV_radius_Reals_1 (a : nat → R) (r : posreal) :
  CVN_r (fun n x ⇒ a n × x ^ n) r → Rbar_le (Finite r) (CV_radius a).

Lemma CV_radius_Reals_2 (a : nat → R) (x : R) :
  Rbar_lt (Finite (Rabs x)) (CV_radius a)
  → ∃ r : posreal, CVU (fun n x ⇒ sum_f_R0 (fun k ⇒ a k × x ^ k) n) (PSeries a) x r.

Operations

Addition of two power series

Section PS_plus.

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

Definition PS_plus (a b : nat → V) (n : nat) : V := plus (a n) (b n).

Lemma is_pseries_plus (a b : nat → V) (x :K) (la lb : V) :
  is_pseries a x la → is_pseries b x lb
    → is_pseries (PS_plus a b) x (plus la lb).

Lemma ex_pseries_plus (a b : nat → V) (x : K) :
  ex_pseries a x → ex_pseries b x
    → ex_pseries (PS_plus a b) x.

End PS_plus.

Lemma PSeries_plus (a b : nat → R) (x : R) :
  ex_pseries a x → ex_pseries b x
    → PSeries (PS_plus a b) x = PSeries a x + PSeries b x.

Lemma CV_disk_plus (a b : nat → R) (x : R) :
  (CV_disk a x) → (CV_disk b x)
  → (CV_disk (PS_plus a b) x).
Lemma CV_radius_plus (a b : nat → R) :
  Rbar_le (Rbar_min (CV_radius a) (CV_radius b)) (CV_radius (PS_plus a b)).

Scalar multiplication

Section PS_scal.

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

Definition PS_scal (c : K) (a : nat → V) (n : nat) : V := scal c (a n).

Lemma is_pseries_scal (c : K) (a : nat → V) (x : K) (l : V) :
  mult x c = mult c x → is_pseries a x l → is_pseries (PS_scal c a) x (scal c l).

Lemma ex_pseries_scal (c : K) (a : nat → V) (x : K) :
  mult x c = mult c x → ex_pseries a x → ex_pseries (PS_scal c a) x.

End PS_scal.

Lemma PSeries_scal (c : R) (a : nat → R) (x : R) :
  PSeries (PS_scal c a) x = c × PSeries a x.

Lemma CV_disk_scal (c : R) (a : nat → R) (x : R) :
  (CV_disk a x)
  → (CV_disk (PS_scal c a) x).

Lemma CV_radius_scal (c : R) (a : nat → R) : c ≠ 0 →
  (CV_radius (PS_scal c a)) = (CV_radius a).

Definition PS_scal_r (c : R) (a : nat → R) (n : nat) : R :=
  a n × c.
Lemma PSeries_scal_r (c : R) (a : nat → R) (x : R) :
  PSeries (PS_scal_r c a) x = PSeries a x × c.

Lemma CV_disk_scal_r (c : R) (a : nat → R) (x : R) :
  (CV_disk a x)
  → (CV_disk (PS_scal_r c a) x).
Lemma CV_radius_scal_r (c : R) (a : nat → R) : c ≠ 0 →
  (CV_radius (PS_scal_r c a)) = (CV_radius a).

Multiplication and division by a variable

Section PS_incr.

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

Definition PS_incr_1 (a : nat → V) (n : nat) : V :=
  match n with
    | 0 ⇒ zero
    | S n ⇒ a n
  end.

Lemma is_pseries_incr_1 (a : nat → V) (x:K) (l : V) :
  is_pseries a x l → is_pseries (PS_incr_1 a) x (scal x l).

Lemma ex_pseries_incr_1 (a : nat → V) (x : K) :
  ex_pseries a x → ex_pseries (PS_incr_1 a) x.

Fixpoint PS_incr_n (a : nat → V) (n k : nat) : V :=
  match n with
    | O ⇒ a k
    | S n ⇒ PS_incr_1 (PS_incr_n a n) k
  end.

Lemma PS_incr_n_simplify (a : nat → V) (n k : nat) :
  PS_incr_n a n k =
  match (le_lt_dec n k) with
    | left _ ⇒ a (k-n)%nat
    | right _ ⇒ zero
  end.

Lemma is_pseries_incr_n (a : nat → V) (n : nat) (x : K) (l : V) :
  is_pseries a x l → is_pseries (PS_incr_n a n) x (scal (pow_n x n) l).

Lemma ex_pseries_incr_n (a : nat → V) (n : nat) (x : K) :
  ex_pseries a x → ex_pseries (PS_incr_n a n) x.

Definition PS_decr_1 (a : nat → V) (n : nat) : V := a (S n).

Lemma is_pseries_decr_1 (a : nat → V) (x y : K) (l : V) :
  mult y x = one → is_pseries a x l
    → is_pseries (PS_decr_1 a) x (scal y (plus l (opp (a O)))).

Lemma ex_pseries_decr_1 (a : nat → V) (x : K) :
 (x = zero ∨ ∃ y, mult y x = one) →
 ex_pseries a x → ex_pseries (PS_decr_1 a) x.

Definition PS_decr_n (a : nat → V) (n k : nat) : V := a (n + k)%nat.

Lemma is_pseries_decr_n (a : nat → V) (n : nat) (x y:K) (l : V) :
  mult y x = one → (0 < n)%nat → is_pseries a x l
    → is_pseries (PS_decr_n a n) x (scal (pow_n y n) (plus l (opp (sum_n (fun k ⇒ scal (pow_n x k) (a k)) (n-1)%nat)))).

Lemma ex_pseries_decr_n (a : nat → V) (n : nat) (x : K) :
  (x = zero ∨ ∃ y, mult y x = one) → ex_pseries a x → ex_pseries (PS_decr_n a n) x.

End PS_incr.

Lemma PSeries_incr_1 a x :
  PSeries (PS_incr_1 a) x = x × PSeries a x.

Lemma PSeries_incr_n (a : nat → R) (n : nat) (x : R) :
  PSeries (PS_incr_n a n) x = x^n × PSeries a x.

Lemma PSeries_decr_1 (a : nat → R) (x : R) :
  ex_pseries a x → PSeries a x = a O + x × PSeries (PS_decr_1 a) x.

Lemma PSeries_decr_1_aux (a : nat → R) (x : R) :
  a O = 0 → (PSeries a x) = x × PSeries (PS_decr_1 a) x.

Lemma PSeries_decr_n (a : nat → R) (n : nat) (x : R) :
  ex_pseries a x
    → PSeries a x = sum_f_R0 (fun k ⇒ a k × x^k) n + x^(S n) × PSeries (PS_decr_n a (S n)) x.

Lemma PSeries_decr_n_aux (a : nat → R) (n : nat) (x : R) :
  (∀ k : nat, (k < n)%nat → a k = 0)
    → PSeries a x = x^n × PSeries (PS_decr_n a n) x.

Lemma CV_radius_incr_1 (a : nat → R) :
  CV_radius (PS_incr_1 a) = CV_radius a.
Lemma CV_radius_decr_1 (a : nat → R) :
  CV_radius (PS_decr_1 a) = CV_radius a.

Definition PS_mult (a b : nat → R) n :=
  sum_f_R0 (fun k ⇒ a k × b (n - k)%nat) n.

Lemma is_pseries_mult (a b : nat → R) (x la lb : R) :
  is_pseries a x la → is_pseries b x lb
  → Rbar_lt (Rabs x) (CV_radius a) → Rbar_lt (Rabs x) (CV_radius b)
  → is_pseries (PS_mult a b) x (la × lb).
Lemma ex_pseries_mult (a b : nat → R) (x : R) :
  Rbar_lt (Rabs x) (CV_radius a) → Rbar_lt (Rabs x) (CV_radius b)
  → ex_pseries (PS_mult a b) x.
Lemma PSeries_mult (a b : nat → R) (x : R) :
  Rbar_lt (Rabs x) (CV_radius a) → Rbar_lt (Rabs x) (CV_radius b)
  → PSeries (PS_mult a b) x = PSeries a x × PSeries b x.

Sums on even and odd

Lemma is_pseries_odd_even (a : nat → R) (x l1 l2 : R) :
  is_pseries (fun n ⇒ a (2×n)%nat) (x^2) l1 → is_pseries (fun n ⇒ a (2×n+1)%nat) (x^2) l2
    → is_pseries a x (l1 + x × l2).
Lemma ex_pseries_odd_even (a : nat → R) (x : R) :
  ex_pseries (fun n ⇒ a (2×n)%nat) (x^2) → ex_pseries (fun n ⇒ a (2×n+1)%nat) (x^2)
    → ex_pseries a x.
Lemma PSeries_odd_even (a : nat → R) (x : R) :
  ex_pseries (fun n ⇒ a (2×n)%nat) (x^2) → ex_pseries (fun n ⇒ a (2×n+1)%nat) (x^2)
    → PSeries a x = PSeries (fun n ⇒ a (2×n)%nat) (x^2) + x × PSeries (fun n ⇒ a (2×n+1)%nat) (x^2).

Lemma PSeries_const_0 : ∀ x, PSeries (fun _ ⇒ 0) x = 0.

Lemma CV_radius_const_0 : CV_radius (fun _ ⇒ 0) = p_infty.

Section PS_opp.

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

Definition PS_opp (a : nat → V) (n : nat) : V := opp (a n).

Lemma is_pseries_opp (a : nat → V) (x :K) (l : V) :
  is_pseries a x l → is_pseries (PS_opp a) x (opp l).

Lemma ex_pseries_opp (a : nat → V) (x : K) :
  ex_pseries a x → ex_pseries (PS_opp a) x.

End PS_opp.

Lemma PSeries_opp (a : nat → R) (x : R) :
  PSeries (PS_opp a) x = - PSeries a x.

Lemma CV_radius_opp (a : nat → R) :
  (CV_radius (PS_opp a)) = (CV_radius a).

Section PS_minus.

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

Definition PS_minus (a b : nat → V) (n : nat) : V := plus (a n) (opp (b n)).

Lemma is_pseries_minus (a b : nat → V) (x:K) (la lb : V) :
  is_pseries a x la → is_pseries b x lb
  → is_pseries (PS_minus a b) x (plus la (opp lb)).

Lemma ex_pseries_minus (a b : nat → V) (x : K) :
  ex_pseries a x → ex_pseries b x
  → ex_pseries (PS_minus a b) x.

End PS_minus.

Lemma PSeries_minus (a b : nat → R) (x : R) :
  ex_pseries a x → ex_pseries b x
  → PSeries (PS_minus a b) x = PSeries a x - PSeries b x.

Abel's theorem for power series


Lemma Abel (a : nat → R) :
  Rbar_lt 0 (CV_radius a) → Rbar_lt (CV_radius a) p_infty
  → ex_pseries a (CV_radius a)
  → filterlim (PSeries a) (at_left (CV_radius a)) (locally (PSeries a (CV_radius a))).

Analysis

Continuity


Lemma PSeries_continuity (a : nat → R) (x : R) :
  Rbar_lt (Finite (Rabs x)) (CV_radius a)
    → continuity_pt (PSeries a) x.

Differentiability


Definition PS_derive (a : nat → R) (n : nat) :=
  INR (S n) × a (S n).
Lemma CV_radius_derive (a : nat → R) :
  CV_radius (PS_derive a) = CV_radius a.

Lemma is_derive_PSeries (a : nat → R) (x : R) :
  Rbar_lt (Finite (Rabs x)) (CV_radius a)
    → is_derive (PSeries a) x (PSeries (PS_derive a) x).
Lemma ex_derive_PSeries (a : nat → R) (x : R) :
  Rbar_lt (Finite (Rabs x)) (CV_radius a)
    → ex_derive (PSeries a) x.
Lemma Derive_PSeries (a : nat → R) (x : R) :
  Rbar_lt (Finite (Rabs x)) (CV_radius a)
    → Derive (PSeries a) x = PSeries (PS_derive a) x.

Lemma is_pseries_derive (a : nat → R) x :
  Rbar_lt (Rabs x) (CV_radius a)
    → is_pseries (PS_derive a) x (Derive (PSeries a) x).
Lemma ex_pseries_derive (a : nat → R) (x : R) :
  Rbar_lt (Finite (Rabs x)) (CV_radius a)
    → ex_pseries (PS_derive a) x.

Definition PS_derive_n (n : nat) (a : nat → R) :=
  (fun k ⇒ (INR (fact (k + n)%nat) / INR (fact k)) × a (k + n)%nat).

Lemma is_derive_n_PSeries (n : nat) (a : nat → R) :
  ∀ x, Rbar_lt (Rabs x) (CV_radius a)
    → is_derive_n (PSeries a) n x (PSeries (PS_derive_n n a) x).
Lemma ex_derive_n_PSeries (n : nat) (a : nat → R) (x : R) :
  Rbar_lt (Finite (Rabs x)) (CV_radius a)
    → ex_derive_n (PSeries a) n x.

Lemma Derive_n_PSeries (n : nat) (a : nat → R) (x : R) :
  Rbar_lt (Finite (Rabs x)) (CV_radius a)
    → Derive_n (PSeries a) n x = PSeries (PS_derive_n n a) x.

Lemma CV_radius_derive_n (n : nat) (a : nat → R) :
  CV_radius (PS_derive_n n a) = CV_radius a.

Coefficients

Lemma Derive_n_coef (a : nat → R) (n : nat) :
  Rbar_lt (Finite 0) (CV_radius a)
    → Derive_n (PSeries a) n 0 = a n × (INR (fact n)).

Lemma PSeries_ext_recip (a b : nat → R) (n : nat) :
  Rbar_lt (Finite 0) (CV_radius a) → Rbar_lt (Finite 0) (CV_radius b)
  → locally 0 (fun x ⇒ PSeries a x = PSeries b x)
    → a n = b n.

Lemma mk_pseries (f : R → R) (M : R) (r : Rbar) :
  (∀ n x, Rbar_lt (Finite (Rabs x)) r
    → (ex_derive_n f n x) ∧ Rabs (Derive_n f n x) ≤ M)
  → ∀ x, Rbar_lt (Finite (Rabs x)) r
    → is_pseries (fun n ⇒ Derive_n f n 0 / INR (fact n)) x (f x).