Series of Real Numbers
In this file we develop a theory of series of real numbers.Definitions
A series is simply a sequence from the natural numbers into the reals. To each such sequence we can assign a sequence of partial sums.
Let x:nat->IR.
For subsequent purposes it will be very useful to be able to write the difference between two arbitrary elements of the sequence of partial sums as a sum of elements of the original sequence.
A series is convergent iff its sequence of partial Sums is a
Cauchy sequence. To each convergent series we can assign a Sum.
Definition convergent := Cauchy_prop ∑n.
Definition ∑0∞ (H : convergent) := Lim (Build_CauchySeq _ _ H).
Divergence can be characterized in a positive way, which will sometimes
be useful. We thus define divergence of sequences and series and prove the
obvious fact that no sequence can be both convergent and divergent, whether
considered either as a sequence or as a series.
Definition divergent_seq (a : N -> IR) := {e : IR | 0 [<] e |
forall k, {m : N | {n : N | k <= m /\ k <= n /\ e [<=] AbsIR (a m[-]a n)}}}.
Definition divergent := divergent_seq ∑n.
Lemma conv_imp_not_div : forall a, Cauchy_prop a -> ~ (divergent_seq a).
Lemma div_imp_not_conv : forall a, divergent_seq a -> ~ (Cauchy_prop a).
Lemma convergent_imp_not_divergent : convergent -> ~ divergent.
Lemma divergent_imp_not_convergent : divergent -> ~ convergent.
Finally we have the well known fact that every convergent series converges
to zero as a sequence.
Lemma series_seq_Lim : convergent -> Cauchy_Lim_prop2 x 0.
Lemma series_seq_Lim' : convergent -> forall H, Lim (Build_CauchySeq _ x H) [=] 0.
End Definitions.
Section More_Definitions.
Variable x : N -> IR.
We also define absolute convergence.
Definition abs_convergent := convergent (fun n => AbsIR (x n)).
End More_Definitions.
Section Power_Series.
Specially important is the case when c is a real number
whose absolute value is less than 1; in this case not only the power series is convergent, but
we can also compute its sum.
Let c be a real number between -1 and 1.
Let c be a real number between -1 and 1.
Variable c : IR.
Hypothesis Hc : AbsIR c [<] 1.
Lemma c_exp_Lim : Cauchy_Lim_prop2 (power_series c) 0.
Lemma power_series_Lim1 : forall H : 1[-]c [#] 0,
Cauchy_Lim_prop2 (∑n (power_series c)) (1[/] _[//]H).
Lemma power_series_conv : convergent (power_series c).
Lemma power_series_sum : forall H Hc,
∑0∞ (power_series c) Hc [=] (1[/] 1[-]c[//]H).
End Power_Series.
Section Operations.
Operations
Some operations with series preserve convergence. We start by defining the series that is zero everywhere.
Lemma conv_zero_series : convergent (fun n => 0).
Lemma series_sum_zero : forall H : convergent (fun n => 0), ∑0∞ _ H [=] 0.
Next we consider extensionality, as well as the sum and difference
of two convergent series.
Let x,y:nat->IR be convergent series.
Let x,y:nat->IR be convergent series.
Variables x y : N -> IR.
Hypothesis convX : convergent x.
Hypothesis convY : convergent y.
Lemma convergent_wd : (forall n, x n [=] y n) -> convergent x -> convergent y.
Lemma series_sum_wd : (forall n, x n [=] y n) -> ∑0∞ _ convX [=] ∑0∞ _ convY.
Lemma conv_series_plus : convergent (fun n => x n[+]y n).
Lemma series_sum_plus : forall H : convergent (fun n => x n[+]y n),
∑0∞ _ H [=] ∑0∞ _ convX[+]∑0∞ _ convY.
Lemma conv_series_minus : convergent (fun n => x n[-]y n).
Lemma series_sum_minus : forall H : convergent (fun n => x n[-]y n),
∑0∞ _ H [=] ∑0∞ _ convX[-]∑0∞ _ convY.
Multiplication by a scalar c is also permitted.
Variable c : IR.
Lemma conv_series_mult_scal : convergent (fun n => c[*]x n).
Lemma series_sum_mult_scal : forall H : convergent (fun n => c[*]x n),
∑0∞ _ H [=] c[*]∑0∞ _ convX.
End Operations.
Section More_Operations.
Variable x : N -> IR.
Hypothesis convX : convergent x.
As a corollary, we get the series of the inverses.
Lemma conv_series_inv : convergent (fun n => [--] (x n)).
Lemma series_sum_inv : forall H : convergent (fun n => [--] (x n)),
∑0∞ _ H [=] [--] (∑0∞ _ convX).
End More_Operations.
Section Almost_Everywhere.
Almost Everywhere
In this section we strengthen some of the convergence results for sequences and derive an important corollary for series.
Let x,y : N->IR be equal after some natural number.
Variables x y : N -> IR.
Definition aew_eq := {n : N | forall k, n <= k -> x k [=] y k}.
Hypothesis aew_equal : aew_eq.
Lemma aew_Cauchy : Cauchy_prop x -> Cauchy_prop y.
Lemma aew_Cauchy2 : forall c, Cauchy_Lim_prop2 x c -> Cauchy_Lim_prop2 y c.
Lemma aew_series_conv : convergent x -> convergent y.
End Almost_Everywhere.
Section Cauchy_Almost_Everywhere.
Suppose furthermore that x,y are Cauchy sequences.
Variables x y : CauchySeq IR.
Hypothesis aew_equal : aew_eq x y.
Lemma aew_Lim : Lim x [=] Lim y.
End Cauchy_Almost_Everywhere.
Section Convergence_Criteria.
We include the comparison test for series, both in a strong and in a less
general (but simpler) form.
Lemma str_comparison : forall y, convergent y ->
{k : N | forall n, k <= n -> AbsIR (x n) [<=] y n} -> convergent x.
Lemma comparison : forall y,
convergent y -> (forall n, AbsIR (x n) [<=] y n) -> convergent x.
As a corollary, we get that every absolutely convergent series converges.
Next we have the ratio test, both as a positive and negative result.
Lemma divergent_crit : {r : IR | 0 [<] r | forall n, {m : N | n <= m | r [<=] AbsIR (x m)}} ->
divergent x.
Lemma tail_series : forall y, convergent y ->
{k : N | {N : N | forall n, N <= n -> x n [=] y (n + k)}} -> convergent x.
Lemma join_series : convergent x -> forall y,
{k : N | {N : N | forall n, N <= n -> x n [=] y (n + k)}} -> convergent y.
End Convergence_Criteria.
Section More_CC.
Variable x : N -> IR.
Lemma ratio_test_conv : {N : N |
{c : IR | c [<] 1 | 0 [<=] c /\ (forall n, N <= n -> AbsIR (x (S n)) [<=] c[*]AbsIR (x n))}} ->
convergent x.
Lemma ratio_test_div : {N : N |
{c : IR | 1 [<=] c | forall n, N <= n -> c[*]AbsIR (x n) [<] AbsIR (x (S n))}} ->
divergent x.
End More_CC.
Section Alternate_Series.
Alternate Series
Alternate series are a special case. Suppose that x is nonnegative and decreasing convergent to 0.
Variable x : N -> IR.
Hypothesis pos_x : forall n : N, 0 [<=] x n.
Hypothesis Lim_x : Cauchy_Lim_prop2 x 0.
Hypothesis mon_x : forall n : N, x (S n) [<=] x n.
Lemma alternate_series_conv : convergent (fun n => [--]1[^]n[*]x n).
End Alternate_Series.
Section Important_Numbers.
Important Numbers
We end this chapter by defining two important numbers in mathematics: pi and e, both as sums of convergent series.
Definition e_series (n : N) := 1[/] _[//]nring_fac_ap_zero IR n.
Lemma e_series_conv : convergent e_series.
Definition E := ∑0∞ _ e_series_conv.
Definition pi_series n :=
[--]1[^]n[*] (1[/] _[//]Greater_imp_ap IR _ _ (pos_nring_S _ (n + n))).
Lemma pi_series_conv : convergent pi_series.
Definition pi := 4[*]∑0∞ _ pi_series_conv.
End Important_Numbers.