Section Maps_into_Compacts.

Section Part_Funct.

Composition

Preservation results for functional composition are treated in this separate file. We start by defining some auxiliary predicates, and then prove the preservation of continuity through composition and the chain rule for differentiation, both for compact and arbitrary intervals.

Throughout this section:

a, b : IR and I will denote [a,b];
c, d : IR and J will denote [c,d];
F, F', G, G' will be partial functions.

Maps into Compacts

Both continuity and differentiability proofs require extra hypothesis on the functions involved---namely, that every compact interval is mapped into another compact interval. We define this concept for partial functions, and prove some trivial results.

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

Variables c d : IR.
Hypothesis Hcd : c [<=] d.

Hypothesis Hf : ⊆ (Compact Hab) (Dom F).

Definition maps_into_compacts := ⊆ (Compact Hcd) (Dom G) and
(forall x Hx, I x -> Compact Hcd (F x Hx)).

Hypothesis maps : maps_into_compacts.

Lemma maps_lemma' : forall x Hx, I x -> Compact Hcd (F x Hx).

Lemma maps_lemma : forall x, I x -> forall Hx, Compact Hcd (F x Hx).

Lemma maps_lemma_inc : ⊆ (Compact Hcd) (Dom G).

End Part_Funct.

End Maps_into_Compacts.

Section Mapping.

As was the case for division of partial functions, this condition completely characterizes the domain of the composite function.

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

Variables c d : IR.
Hypothesis Hcd : c [<=] d.

Hypothesis Hf : ⊆ (Compact Hab) (Dom F).
Hypothesis Hg : ⊆ (Compact Hcd) (Dom G).
Hypothesis maps : maps_into_compacts F G a b Hab c d Hcd.

Lemma included_comp : ⊆ (Compact Hab) (Dom (G[o]F)).

End Mapping.

Section Interval_Continuity.

Continuity

We now prove that the composition of two continuous partial functions is continuous.

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

Variables c d : IR.
Hypothesis Hcd : c [<=] d.

Variables F G : PartIR.

Hypothesis contF : Continuous_I Hab F.
Hypothesis contG : Continuous_I Hcd G.
Hypothesis Hmap : maps_into_compacts F G a b Hab c d Hcd.

Lemma Continuous_I_comp : Continuous_I Hab (G[o]F).

End Interval_Continuity.

Section Derivative.

Derivative

We now work with the derivative relation and prove the chain rule for partial functions.

Variables F F' G G' : PartIR.

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

Variables c d : IR.
Hypothesis Hcd' : c [<] d.

Hypothesis derF : Derivative_I Hab' F F'.
Hypothesis derG : Derivative_I Hcd' G G'.
Hypothesis Hmap : maps_into_compacts F G a b Hab c d Hcd.

Lemma included_comp' : ⊆ (Compact Hab) (Dom (G'[o]F)).

Lemma maps' : maps_into_compacts F G' a b Hab c d Hcd.

Lemma Derivative_I_comp : Derivative_I Hab' (G[o]F) ((G'[o]F) {*}F').

The next lemma will be useful when we move on to differentiability.

Lemma Diffble_I_comp_aux : Diffble_I Hab' (G[o]F).

End Derivative.

Section Differentiability.

Differentiability

Finally, we move on to differentiability.

Variables F G : PartIR.

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

Variables c d : IR.
Hypothesis Hcd' : c [<] d.

Hypothesis diffF : Diffble_I Hab' F.
Hypothesis diffG : Diffble_I Hcd' G.
Hypothesis Hmap : maps_into_compacts F G a b Hab c d Hcd.

Lemma Diffble_I_comp : Diffble_I Hab' (G[o]F).

End Differentiability.

Section Sequences.

**Sequences

Here we show that the limit of sequences of compositions is the composition of the limits.

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

Variables c d : IR.
Hypothesis Hcd : c [<=] d.

Variable f : N -> PartIR.
Variable g : N -> PartIR.
Hypothesis contf : forall n, Continuous_I Hab (f n).
Hypothesis contg : forall n, Continuous_I Hcd (g n).
Hypothesis rangef : forall n, forall (x : IR) (Hx : Dom (f n) x), I x -> Compact Hcd (f n x Hx).

Section ExplicitLimit.

Variables F G : PartIR.

Hypothesis contF : Continuous_I Hab F.
Hypothesis contG : Continuous_I Hcd G.

Hypothesis convF : conv_fun_seq' _ _ Hab f F contf contF.
Hypothesis convG : conv_fun_seq' _ _ Hcd g G contg contG.

Let incF := contin_imp_inc _ _ _ _ contF.
Let incG := contin_imp_inc _ _ _ _ contG.

Hypothesis rangeF : forall (x : IR) (Hx : Dom F x), I x -> Compact Hcd (F x Hx).

Lemma fun_Lim_seq_comp' : forall H H',
conv_fun_seq' a b Hab (fun n => g n[o]f n) (G[o]F) H H'.

End ExplicitLimit.

The same is true if we don't make the limits explicit.

Lemma fun_Lim_seq_comp : forall H H', conv_fun_seq' a b Hab (fun n => g n[o]f n)
(Cauchy_fun_seq_Lim _ _ _ _ _ Hg[o]Cauchy_fun_seq_Lim _ _ _ _ _ Hf) H H'.

End Sequences.

Section Series.

**Series

Here we show that the limit of series of composition by a constant function (on the right) is the composition with the limit.

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

Variables c d : IR.
Hypothesis Hcd : c [<=] d.

Variable g : N -> PartIR.
Variable F : PartIR.
Hypothesis contF : Continuous_I Hab F.

Hypothesis convG : fun_series_convergent _ _ Hcd g.
Hypothesis rangeF : forall (x : IR) (Hx : Dom F x), Compact Hab x -> (Compact Hcd) (F x Hx).

Lemma conv_fun_series_comp : fun_series_convergent _ _ Hab (fun n => g n[o]F).

Lemma Fun_Series_Sum_comp : forall H' : fun_series_convergent _ _ Hab (fun n => g n[o]F),
≈ I (∑₀^∞ H') (∑₀^∞ convG[o]F).

End Series.

Section Generalized_Intervals.

Generalizations

We now generalize this results to arbitrary intervals. We begin by generalizing the notion of mapping compacts into compacts.

We assume I,J to be proper intervals.

Variables I J : interval.
Hypothesis pI : proper I.
Hypothesis pJ : proper J.

Definition maps_compacts_into_weak (F : PartIR) := forall a b Hab, ⊆ (compact a b Hab) I ->
{c : IR | {d : IR | {Hcd : _ | ⊆ (Compact Hcd) J and
(forall x Hx, Compact Hab x -> compact c d Hcd (F x Hx))}}}.

Now everything comes naturally:

Lemma comp_inc_lemma : forall F,
maps_compacts_into_weak F -> forall x Hx, I x -> J (F x Hx).

Variables F F' G G' : PartIR.
Hypothesis Hmap : maps_compacts_into_weak F.

Lemma Continuous_comp : Continuous I F -> Continuous J G -> Continuous I (G[o]F).
Included.
Qed.

Definition maps_compacts_into (F : PartIR) := forall a b Hab, ⊆ (compact a b Hab) I ->
{c : IR | {d : IR | {Hcd : _ | ⊆ (Compact (less_leEq _ _ _ Hcd)) J and
(forall x Hx, Compact Hab x -> compact c d (less_leEq _ _ _ Hcd) (F x Hx))}}}.

Lemma maps_compacts_into_strict_imp_weak : forall F,
maps_compacts_into F -> maps_compacts_into_weak F.

Hypothesis Hmap' : maps_compacts_into F.

Lemma Derivative_comp : Derivative I pI F F' -> Derivative J pJ G G' ->
Derivative I pI (G[o]F) ((G'[o]F) {*}F').
Included.
Included.
Qed.

Variable g : N -> PartIR.

Hypothesis contF : Continuous I F.
Hypothesis convG : fun_series_convergent_IR J g.

Lemma FSeries_Sum_comp_conv : fun_series_convergent_IR I (fun n => g n[o]F).

Lemma FSeries_Sum_comp : forall H' : fun_series_convergent_IR I (fun n => g n[o]F),
≈ I (∑'_∞ H') (∑'_∞ convG[o]F).
Included.
Qed.

Variable f : N -> PartIR.

Hypothesis contf : forall n, Continuous I (f n).
Hypothesis contg : forall n, Continuous J (g n).
Hypothesis contG : Continuous J G.
Hypothesis Hmapf : forall a b Hab, ⊆ (compact a b Hab) I ->
{c : IR | {d : IR | {Hcd : _ | ⊆ (Compact Hcd) J and
(forall n x Hx, Compact Hab x -> compact c d Hcd (f n x Hx))}}}.

Lemma fun_Lim_seq_comp'_IR :
(conv_fun_seq'_IR _ _ _ contf contF) ->
(conv_fun_seq'_IR _ _ _ contg contG) ->
forall H H', conv_fun_seq'_IR I (fun n => g n[o]f n) (G[o]F) H H'.
Included.
Qed.

Hypothesis Hf : Cauchy_fun_seq_IR _ _ contf.
Hypothesis Hg : Cauchy_fun_seq_IR _ _ contg.

Lemma fun_Lim_seq_comp_IR : forall H H', conv_fun_seq'_IR I (fun n => g n[o]f n)
(Cauchy_fun_seq_Lim_IR _ _ _ Hg[o]Cauchy_fun_seq_Lim_IR _ _ _ Hf) H H'.

End Generalized_Intervals.

Section Corollaries.

Finally, some criteria to prove that a function with a specific domain maps compacts into compacts:

Definition positive_fun P F := ⊆ P (Dom F) and
{c : IR | 0 [<] c | forall y, P y -> forall Hy, c [<=] F y Hy}.

Definition negative_fun P F := ⊆ P (Dom F) and
{c : IR | c [<] 0 | forall y, P y -> forall Hy, F y Hy [<=] c}.

Lemma positive_imp_maps_compacts_into : forall (J : interval) F,
positive_fun J F -> Continuous J F -> maps_compacts_into J ((⋅,+∞) 0) F.

Lemma negative_imp_maps_compacts_into : forall (J : interval) F,
negative_fun J F -> Continuous J F -> maps_compacts_into J ((-∞,⋅) 0) F.

Lemma Continuous_imp_maps_compacts_into : forall J F,
Continuous J F -> maps_compacts_into J (-∞,+∞) F.

As a corollary, we get the generalization of differentiability property.

Lemma Diffble_comp : forall I J pI pJ F G, maps_compacts_into I J F ->
Diffble I pI F -> Diffble J pJ G -> Diffble I pI (G[o]F).

End Corollaries.