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.
Copyright (C) 2011-2015 Catherine Lelay
Copyright (C) 2011-2015 Guillaume Melquiond
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.
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
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.
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).
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.
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.
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.
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))).
Lemma PSeries_continuity (a : nat → R) (x : R) :
Rbar_lt (Finite (Rabs x)) (CV_radius a)
→ continuity_pt (PSeries a) x.
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).