Sequences of Functions
In this file we define some more operators on functions, namely sequences and limits. These concepts are defined only for continuous functions.
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
A sequence of functions is simply an object of type N->PartIR. However, we will be interested mostly in convergent and Cauchy sequences. Several definitions of these concepts will be formalized; they mirror the several different ways in which a Cauchy sequence can be defined. For a discussion on the different notions of convergent see Bishop 1967.
Variables a b : IR.
Hypothesis Hab : a [<=] b.
Variable f : N -> PartIR.
Variable F : PartIR.
Hypothesis contf : forall n : N, Continuous_I Hab (f n).
Hypothesis contF : Continuous_I Hab F.
Definition Cauchy_fun_seq := forall e, 0 [<] e -> {N : N | forall m n, N <= m -> N <= n ->
forall x Hx, AbsIR (f m x (incf m x Hx) [-]f n x (incf n x Hx)) [<=] e}.
Definition conv_fun_seq' := forall e, 0 [<] e -> {N : N | forall n, N <= n ->
forall x Hx, AbsIR (f n x (incf n x Hx) [-]F x (incF x Hx)) [<=] e}.
Definition conv_norm_fun_seq := forall k, {N : N | forall n, N <= n ->
Norm_Funct (Continuous_I_minus _ _ _ _ _ (contf n) contF) [<=] one_div_succ k}.
Definition Cauchy_fun_seq1 := forall k, {N : N | forall m n, N <= m -> N <= n ->
Norm_Funct (Continuous_I_minus _ _ _ _ _ (contf m) (contf n)) [<=] one_div_succ k}.
Definition Cauchy_fun_seq' := forall k, {N : N | forall m n, N <= m -> N <= n ->
forall x Hx, AbsIR (Part _ _ (incf m x Hx) [-]Part _ _ (incf n x Hx)) [<=] one_div_succ k}.
Definition Cauchy_fun_seq2 := forall e, 0 [<] e -> {N : N | forall m, N <= m ->
forall x Hx, AbsIR (Part _ _ (incf m x Hx) [-]Part _ _ (incf N x Hx)) [<=] e}.
These definitions are all shown to be equivalent.
Lemma Cauchy_fun_seq_seq' : Cauchy_fun_seq -> Cauchy_fun_seq'.
Lemma Cauchy_fun_seq'_seq : Cauchy_fun_seq' -> Cauchy_fun_seq.
Lemma conv_Cauchy_fun_seq' : conv_fun_seq' -> Cauchy_fun_seq.
Lemma Cauchy_fun_seq_seq2 : Cauchy_fun_seq -> Cauchy_fun_seq2.
Lemma Cauchy_fun_seq2_seq : Cauchy_fun_seq2 -> Cauchy_fun_seq.
Lemma conv_fun_seq'_norm : conv_fun_seq' -> conv_norm_fun_seq.
Lemma conv_fun_norm_seq : conv_norm_fun_seq -> conv_fun_seq'.
Lemma Cauchy_fun_seq1_seq' : Cauchy_fun_seq1 -> Cauchy_fun_seq'.
Lemma Cauchy_fun_seq'_seq1 : Cauchy_fun_seq' -> Cauchy_fun_seq1.
Lemma Cauchy_fun_seq_seq1 : Cauchy_fun_seq -> Cauchy_fun_seq1.
Lemma Cauchy_fun_seq1_seq : Cauchy_fun_seq1 -> Cauchy_fun_seq.
A Cauchy sequence of functions is pointwise a Cauchy sequence.
Lemma Cauchy_fun_real : Cauchy_fun_seq -> forall x Hx,
Cauchy_prop (fun n => Part _ _ (incf n x Hx)).
End Definitions.
Section More_Definitions.
Variables a b : IR.
Hypothesis Hab : a [<=] b.
Variable f : N -> PartIR.
Hypothesis contf : forall n : N, Continuous_I Hab (f n).
We can also say that f is simply convergent if it converges to some
continuous function. Notice that we do not quantify directly over
partial functions, for reasons which were already explained.
Definition conv_fun_seq := {f' : CSetoid_fun (subset (Compact Hab)) IR |
{contf' : Continuous_I Hab (PartInt f') |
conv_fun_seq' a b Hab f (PartInt f') contf contf'}}.
It is useful to extract the limit as a partial function:
Hypothesis H : Cauchy_fun_seq _ _ _ f contf.
Definition Cauchy_fun_seq_Lim : PartIR.
Defined.
End More_Definitions.
Section Irrelevance_of_Proofs.
Irrelevance of Proofs
This section contains a number of technical results stating mainly that being a Cauchy sequence or converging to some limit is a property of the sequence itself and independent of the proofs we supply of its continuity or the continuity of its limit.
Variables a b : IR.
Hypothesis Hab : a [<=] b.
Variable f : N -> PartIR.
Hypotheses contf contf0 : forall n : N, Continuous_I Hab (f n).
Variable F : PartIR.
Hypotheses contF contF0 : Continuous_I Hab F.
Lemma conv_fun_seq'_wd : conv_fun_seq' _ _ _ _ _ contf contF ->
conv_fun_seq' _ _ _ _ _ contf0 contF0.
Lemma Cauchy_fun_seq'_wd : Cauchy_fun_seq' _ _ _ _ contf ->
Cauchy_fun_seq' _ _ _ _ contf0.
Lemma Cauchy_fun_seq2_wd : Cauchy_fun_seq2 _ _ _ _ contf ->
Cauchy_fun_seq2 _ _ _ _ contf0.
Lemma conv_norm_fun_seq_wd : conv_norm_fun_seq _ _ _ _ _ contf contF ->
conv_norm_fun_seq _ _ _ _ _ contf0 contF0.
Lemma Cauchy_fun_seq1_wd : Cauchy_fun_seq1 _ _ _ _ contf ->
Cauchy_fun_seq1 _ _ _ _ contf0.
End Irrelevance_of_Proofs.
Section More_Proof_Irrelevance.
Lemma conv_fun_seq_wd : forall a b Hab f contf contf0,
conv_fun_seq a b Hab f contf -> conv_fun_seq a b Hab f contf0.
End More_Proof_Irrelevance.
Section More_Properties.
Other Properties
Still more technical details---a convergent sequence converges to its limit; the limit is a continuous function; and convergence is well defined with respect to functional equality in the interval [a,b].
Variables a b : IR.
Hypothesis Hab : a [<=] b.
Variables f g : N -> PartIR.
Hypotheses contf contf0 : forall n, Continuous_I Hab (f n).
Hypotheses contg contg0 : forall n, Continuous_I Hab (g n).
Lemma Cauchy_conv_fun_seq' : forall H contf',
conv_fun_seq' _ _ _ _ (Cauchy_fun_seq_Lim _ _ _ f contf H) contf contf'.
Variables F G : PartIR.
Hypotheses contF contF0 : Continuous_I Hab F.
Hypotheses contG contG0 : Continuous_I Hab G.
Lemma conv_fun_seq'_wdl : (forall n, ≈ I (f n) (g n)) ->
conv_fun_seq' _ _ _ _ _ contf contF -> conv_fun_seq' _ _ _ _ _ contg contF0.
Lemma conv_fun_seq'_wdr : ≈ I F G ->
conv_fun_seq' _ _ _ _ _ contf contF -> conv_fun_seq' _ _ _ _ _ contf0 contG.
Lemma conv_fun_seq'_wdl' : (forall n, ≈ I (f n) (g n)) ->
conv_fun_seq' _ _ _ _ _ contf contF -> conv_fun_seq' _ _ _ _ _ contg contF.
Lemma conv_fun_seq'_wdr' : ≈ I F G ->
conv_fun_seq' _ _ _ _ _ contf contF -> conv_fun_seq' _ _ _ _ _ contf contG.
Lemma Cauchy_fun_seq_wd : (forall n, ≈ I (f n) (g n)) ->
Cauchy_fun_seq _ _ _ _ contf -> Cauchy_fun_seq _ _ _ _ contg.
Lemma Cauchy_cont_Lim : forall H : Cauchy_fun_seq a b Hab f contf,
Continuous_I Hab (Cauchy_fun_seq_Lim _ _ _ _ contf H).
Included.
Qed.
Lemma Cauchy_conv_fun_seq : Cauchy_fun_seq _ _ _ _ contf ->
conv_fun_seq _ _ _ _ contf.
Lemma conv_Cauchy_fun_seq : conv_fun_seq _ _ _ _ contf ->
Cauchy_fun_seq _ _ _ _ contf.
More interesting is the fact that a convergent sequence of functions converges pointwise as a sequence of real numbers.
Lemma fun_conv_imp_seq_conv : conv_fun_seq' _ _ _ _ _ contf contF -> forall x,
Compact Hab x -> forall Hxf HxF, Cauchy_Lim_prop2 (fun n => f n x (Hxf n)) (F x HxF).
And a sequence of real numbers converges iff the corresponding sequence of constant functions converges to the corresponding constant function.
Lemma seq_conv_imp_fun_conv : forall x y, Cauchy_Lim_prop2 x y ->
forall Hf HF, conv_fun_seq' a b Hab (fun n => [-C-] (x n)) [-C-]y Hf HF.
End More_Properties.
Section Algebraic_Properties.
Algebraic Properties
We now study how convergence is affected by algebraic operations, and some algebraic properties of the limit function.
Variables a b : IR.
Hypothesis Hab : a [<=] b.
Variables f g : N -> PartIR.
Hypothesis contf : forall n, Continuous_I Hab (f n).
Hypothesis contg : forall n, Continuous_I Hab (g n).
First, the limit function is unique.
Lemma FLim_unique : forall F G HF HG, conv_fun_seq' a b Hab f F contf HF ->
conv_fun_seq' a b Hab f G contf HG -> ≈ (Compact Hab) F G.
Constant sequences (not sequences of constant functions!) always converge.
Lemma fun_Lim_seq_const : forall H contH contH',
conv_fun_seq' a b Hab (fun n => H) H contH contH'.
Lemma fun_Cauchy_prop_const : forall H (contH:Continuous_I Hab H),
Cauchy_fun_seq a b Hab (fun n => H) (fun n => contH).
We now prove that if two sequences converge than their sum (difference, product) also converge to the sum (difference, product) of their limits.
Variables F G : PartIR.
Hypothesis contF : Continuous_I Hab F.
Hypothesis contG : Continuous_I Hab G.
Hypothesis convF : conv_fun_seq' a b Hab f F contf contF.
Hypothesis convG : conv_fun_seq' a b Hab g G contg contG.
Lemma fun_Lim_seq_plus' : forall H H',
conv_fun_seq' a b Hab (fun n => f n{+}g n) (F{+}G) H H'.
Lemma fun_Lim_seq_minus' : forall H H',
conv_fun_seq' a b Hab (fun n => f n{-}g n) (F{-}G) H H'.
Lemma fun_Lim_seq_mult' : forall H H',
conv_fun_seq' a b Hab (fun n => f n{*}g n) (F{*}G) H H'.
End Algebraic_Properties.
Section More_Algebraic_Properties.
Variables a b : IR.
Hypothesis Hab : a [<=] b.
Variables f g : N -> PartIR.
Hypothesis contf : forall n : N, Continuous_I Hab (f n).
Hypothesis contg : forall n : N, Continuous_I Hab (g n).
The same is true if we don't make the limits explicit.
Lemma fun_Lim_seq_plus : forall H H', conv_fun_seq' a b Hab (fun n => f n{+}g n)
(Cauchy_fun_seq_Lim _ _ _ _ _ Hf{+}Cauchy_fun_seq_Lim _ _ _ _ _ Hg) H H'.
Lemma fun_Cauchy_prop_plus : forall H, Cauchy_fun_seq a b Hab (fun n => f n{+}g n) H.
Lemma fun_Lim_seq_minus : forall H H', conv_fun_seq' a b Hab (fun n => f n{-}g n)
(Cauchy_fun_seq_Lim _ _ _ _ _ Hf{-}Cauchy_fun_seq_Lim _ _ _ _ _ Hg) H H'.
Lemma fun_Cauchy_prop_minus : forall H, Cauchy_fun_seq a b Hab (fun n => f n{-}g n) H.
Lemma fun_Lim_seq_mult : forall H H', conv_fun_seq' a b Hab (fun n => f n{*}g n)
(Cauchy_fun_seq_Lim _ _ _ _ _ Hf{*}Cauchy_fun_seq_Lim _ _ _ _ _ Hg) H H'.
Lemma fun_Cauchy_prop_mult : forall H, Cauchy_fun_seq a b Hab (fun n => f n{*}g n) H.
End More_Algebraic_Properties.
Section Still_More_Algebraic_Properties.
Variables a b : IR.
Hypothesis Hab : a [<=] b.
Variable f : N -> PartIR.
Hypothesis contf : forall n, Continuous_I Hab (f n).
Hypothesis Hf : Cauchy_fun_seq _ _ _ _ contf.
As a corollary, we get the analogous property for the sequence of algebraic inverse functions.
Lemma fun_Lim_seq_inv : forall H H', conv_fun_seq' a b Hab
(fun n => {--} (f n)) {--} (Cauchy_fun_seq_Lim _ _ _ _ _ Hf) H H'.
Included.
Included.
Qed.
Lemma fun_Cauchy_prop_inv : forall H, Cauchy_fun_seq a b Hab (fun n => {--} (f n)) H.
End Still_More_Algebraic_Properties.