Section Definitions.

Series of Functions



We now turn our attention to series of functions. Like it was already the case for sequences, we will mainly rewrite the results we proved for series of real numbers in a different way.

Throughout this section:
  • a and b will be real numbers and the interval [a,b] will be denoted by I;
  • f, g and h will denote sequences of continuous functions;
  • F, G and H will denote continuous functions.




Definitions



As before, we will consider only sequences of continuous functions defined in a compact interval. For this, partial sums are defined and convergence is simply the convergence of the sequence of partial sums.

Variables a b : IR.
Hypothesis Hab : a [<=] b.

Variable f : N -> PartIR.

Definition ∑n (n : N) := ∑0 n f.

Lemma fun_seq_part_sum_cont : (forall n, Continuous_I Hab (f n)) -> forall n,
 Continuous_I Hab (∑n n).

Definition fun_series_convergent := {contf : _ |
  Cauchy_fun_seq _ _ Hab ∑n (fun_seq_part_sum_cont contf)}.

For what comes up next we need to know that the convergence of a series of functions implies pointwise convergence of the corresponding real number series.

Lemma fun_series_conv_imp_conv : fun_series_convergent ->
 forall x, I x -> forall Hx, convergent (fun n => f n x (Hx n)).

We then define the sum of the series as being the pointwise sum of the corresponding series.

Hypothesis H : fun_series_convergent.


Lemma Fun_Series_Sum_strext : forall x y Hx Hy,
 ∑0∞ _ (fun_series_conv_imp_conv H x Hx (fun n => incf n x Hx)) [#]
  ∑0∞ _ (fun_series_conv_imp_conv H y Hy (fun n => incf n y Hy)) -> x [#] y.

Definition ∑0∞ : PartIR.
Defined.

End Definitions.



Section More_Definitions.

Variables a b : IR.
Hypothesis Hab : a [<=] b.

Variable f : N -> PartIR.

A series can also be absolutely convergent.

Definition fun_series_abs_convergent := fun_series_convergent _ _ Hab
 (fun n => FAbs (f n)).

End More_Definitions.

Section Operations.


Variables a b : IR.
Hypothesis Hab : a [<=] b.

Lemma fun_seq_part_sum_n : forall f (H' : forall n, Continuous_I Hab (f n)) m n,
 0 < n -> m <= n -> ≈ I (∑n f n{-}fun_seq_part_sum f m) (∑ m (pred n) f).

Lemma conv_fun_const_series : forall x, convergent x ->
 fun_series_convergent _ _ Hab (fun n => [-C-] (x n)).

Lemma fun_const_series_sum : forall y H
 (H' : fun_series_convergent _ _ Hab (fun n => [-C-] (y n))) x Hx, ∑0∞ H' x Hx [=] ∑0∞ y H.

Lemma conv_zero_fun_series : fun_series_convergent _ _ Hab (fun n => [-C-]0).

Lemma Fun_Series_Sum_zero : forall (H : fun_series_convergent _ _ Hab (fun n => [-C-]0))
 x Hx, ∑0∞ H x Hx [=] 0.

Variables f g : N -> PartIR.

Lemma fun_series_convergent_wd : (forall n, ≈ I (f n) (g n)) ->
 fun_series_convergent _ _ Hab f -> fun_series_convergent _ _ Hab g.


Hypothesis convF : fun_series_convergent _ _ Hab f.
Hypothesis convG : fun_series_convergent _ _ Hab g.

Lemma Fun_Series_Sum_wd' : (forall n, ≈ I (f n) (g n)) -> ≈ I (∑0∞ convF) (∑0∞ convG).
Included.
Included.
Qed.

Lemma conv_fun_series_plus : fun_series_convergent _ _ Hab (fun n => f n{+}g n).
Included.
Qed.

Lemma Fun_Series_Sum_plus : forall H : fun_series_convergent _ _ Hab (fun n => f n{+}g n),
 ≈ I (∑0∞ H) (∑0∞ convF{+}Fun_Series_Sum convG).
Included.
Included.

Qed.

Lemma conv_fun_series_minus : fun_series_convergent _ _ Hab (fun n => f n{-}g n).
Included.
Qed.

Lemma Fun_Series_Sum_min : forall H : fun_series_convergent _ _ Hab (fun n => f n{-}g n),
 ≈ I (∑0∞ H) (∑0∞ convF{-}Fun_Series_Sum convG).
Included.
Included.

Qed.

Let c:IR.

Variable c : IR.
Variable H : PartIR.
Hypothesis contH : Continuous_I Hab H.

Lemma conv_fun_series_scal : fun_series_convergent _ _ Hab (fun n => H{*}f n).

Lemma Fun_Series_Sum_scal : forall H' : fun_series_convergent _ _ Hab (fun n => H{*}f n),
 ≈ I (∑0∞ H') (H{*}Fun_Series_Sum convF).



End Operations.

Section More_Operations.

Variables a b : IR.
Hypothesis Hab : a [<=] b.

Variable f : N -> PartIR.
Hypothesis convF : fun_series_convergent _ _ Hab f.

Lemma conv_fun_series_inv : fun_series_convergent _ _ Hab (fun n => {--} (f n)).


Lemma Fun_Series_Sum_inv : forall H : fun_series_convergent _ _ Hab (fun n => {--} (f n)),
 ≈ I (∑0∞ H) {--} (∑0∞ convF).



End More_Operations.

Section Other_Results.

Variables a b : IR.
Hypothesis Hab : a [<=] b.

Variable f : N -> PartIR.

Hypothesis convF : fun_series_convergent a b Hab f.

The following relate the sum series with the limit of the sequence of partial sums; as a corollary we get the continuity of the sum of the series.

Lemma Fun_Series_Sum_char' : forall contf H,
 ≈ (Compact Hab) (∑0∞ convF) (Cauchy_fun_seq_Lim _ _ Hab (∑n f) contf H).

Lemma fun_series_conv : forall H H',
 conv_fun_seq' a b Hab (∑n f) (∑0∞ convF) H H'.


Lemma Fun_Series_Sum_cont : Continuous_I Hab (∑0∞ convF).


Lemma Fun_Series_Sum_char : ≈ (Compact Hab)
 (Cauchy_fun_seq_Lim _ _ Hab (∑n f) _ (ProjT2 convF)) (∑0∞ convF).

Lemma Fun_Series_Sum_as_Lim : forall Hf H',
 conv_fun_seq' _ _ Hab (∑n f) (∑0∞ convF) Hf H'.

End Other_Results.


Section Convergence_Criteria.

Convergence Criteria



Most of the convergence criteria for series of real numbers carry over to series of real-valued functions, so again we just present them without comments.

Variables a b : IR.
Hypothesis Hab : a [<=] b.

Variable f : N -> PartIR.
Hypothesis contF : forall n : N, Continuous_I Hab (f n).

Lemma fun_str_comparison : forall g, fun_series_convergent _ _ Hab g ->
 {k : N | forall n, k <= n -> forall x, I x -> forall Hx Hx', AbsIR (f n x Hx) [<=] g n x Hx'} ->
 fun_series_convergent _ _ Hab f.









Lemma fun_comparison : forall g, fun_series_convergent _ _ Hab g ->
 (forall n x, I x -> forall Hx Hx', AbsIR (f n x Hx) [<=] g n x Hx') ->
 fun_series_convergent _ _ Hab f.

Lemma abs_imp_conv : fun_series_abs_convergent _ _ Hab f ->
 fun_series_convergent _ _ Hab f.

Lemma fun_ratio_test_conv : {N : N | {c : IR | c [<] 1 | 0 [<=] c /\
 (forall x, I x -> forall n, N <= n -> forall Hx Hx', AbsIR (f (S n) x Hx') [<=] c[*]AbsIR (f n x Hx))}} ->
 fun_series_convergent _ _ Hab f.

End Convergence_Criteria.