Sums of Functions
In this file we define sums are defined of arbitrary families of partial functions.
Given a countable family of functions, their sum is defined on the intersection of all the domains. As is the case for groups, we will define three different kinds of sums.
We will first consider the case of a family {fi} of functions; we can both define the sum of the first n functions ( ∑0) or the sum of fm through fn ( ∑).
Definition ∑0 (n : N) (f : N -> PartIR) : PartIR.
Defined.
Definition ∑ (m n : N) (f : N -> PartIR) : PartIR.
Defined.
Although ∑ is here defined directly, it has the same relationship
to the ∑0 operator as ∑ has to ∑0. Also, all the results
for ∑ and ∑0 hold when these operators are replaced by their
functional equivalents. This is an immediate consequence of the fact
that the partial functions form a group; however, as we already
mentioned, their forming too big a type makes it impossible to use
those results.
Lemma FSum_FSum0 : forall m n (f : N -> PartIR) x Hx Hx' Hx'',
∑ m n f x Hx [=] ∑0 (S n) f x Hx'[-]∑0 m f x Hx''.
Lemma FSum0_wd : forall m (f g : N -> PartIR),
(forall x HxF HxG i, f i x (HxF i) [=] g i x (HxG i)) ->
forall x HxF HxG, ∑0 m f x HxF [=] ∑0 m g x HxG.
Lemma FSum_one : forall n (f : N -> PartIR) x Hx Hx',
∑ n n f x Hx' [=] f n x Hx.
Lemma FSum_FSum : forall l m n (f : N -> PartIR) x Hx Hx' Hx'',
∑ l m f x Hx[+]∑ (S m) n f x Hx' [=] ∑ l n f x Hx''.
Lemma FSum_first : forall m n (f : N -> PartIR) x Hx Hx' Hx'',
∑ m n f x Hx [=] f m x Hx'[+]∑ (S m) n f x Hx''.
Lemma FSum_last : forall m n (f : N -> PartIR) x Hx Hx' Hx'',
∑ m (S n) f x Hx [=] ∑ m n f x Hx'[+]f (S n) x Hx''.
Lemma FSum_last' : forall m n (f : N -> PartIR) x Hx Hx' Hx'',
0 < n -> ∑ m n f x Hx [=] ∑ m (pred n) f x Hx'[+]f n x Hx''.
Lemma FSum_wd : forall m n (f g : N -> PartIR),
(forall x HxF HxG i, f i x (HxF i) [=] g i x (HxG i)) ->
forall x HxF HxG, ∑ m n f x HxF [=] ∑ m n g x HxG.
Lemma FSum_plus_FSum : forall (f g : N -> PartIR) m n x Hx HxF HxG,
∑ m n (fun i => f i{+}g i) x Hx [=] ∑ m n f x HxF[+]∑ m n g x HxG.
Lemma inv_FSum : forall (f : N -> PartIR) m n x Hx Hx',
∑ m n (fun i => {--} (f i)) x Hx [=] [--] (∑ m n f x Hx').
Lemma FSum_minus_FSum : forall (f g : N -> PartIR) m n x Hx HxF HxG,
∑ m n (fun i => f i{-}g i) x Hx [=] ∑ m n f x HxF[-]∑ m n g x HxG.
Lemma FSum_wd' : forall m n, m <= S n -> forall f g : N -> PartIR,
(forall x HxF HxG i, m <= i -> i <= n -> f i x (HxF i) [=] g i x (HxG i)) ->
forall x HxF HxG, ∑ m n f x HxF [=] ∑ m n g x HxG.
Lemma FSum_resp_less : forall (f g : N -> PartIR) m n, m <= n ->
(forall x HxF HxG i, m <= i -> i <= n -> f i x (HxF i) [<] g i x (HxG i)) ->
forall x HxF HxG, ∑ m n f x HxF [<] ∑ m n g x HxG.
Lemma FSum_resp_leEq : forall (f g : N -> PartIR) m n, m <= S n ->
(forall x HxF HxG i, m <= i -> i <= n -> f i x (HxF i) [<=] g i x (HxG i)) ->
forall x HxF HxG, ∑ m n f x HxF [<=] ∑ m n g x HxG.
Lemma FSum_comm_scal : forall (f : N -> PartIR) c m n x Hx Hx',
∑ m n (fun i => f i{*} [-C-]c) x Hx [=] (∑ m n f{*} [-C-]c) x Hx'.
Lemma FSum_comm_scal' : forall (f : N -> PartIR) c m n x Hx Hx',
∑ m n (fun i => [-C-]c{*}f i) x Hx [=] ( [-C-]c{*}FSum m n f) x Hx'.
Also important is the case when we have a finite family
of exactly n functions; in this case we need
to use the FSumx operator.
Fixpoint FSumx (n : N) : (forall i, i < n -> PartIR) -> PartIR :=
match n return ((forall i, i < n -> PartIR) -> PartIR) with
| O => fun _ => [-C-]0
| S p => fun f => FSumx p (fun i l => f i (lt_S i p l)) {+} f p (lt_n_Sn p)
end.
This operator is well defined, as expected.
Lemma FSumx_wd : forall n (f g : forall i, i < n -> PartIR),
(forall i Hi x HxF HxG, f i Hi x HxF [=] g i Hi x HxG) ->
forall x HxF HxG, FSumx n f x HxF [=] FSumx n g x HxG.
Lemma FSumx_wd' : forall (P : IR -> CProp) n (f g : forall i, i < n -> PartIR),
(forall i H H', ≈ P (f i H) (g i H')) -> ≈ P (FSumx n f) (FSumx n g).
As was already the case for Sumx, in many cases we will need to
explicitly assume that f1 is independent of the proof that
i < n. This holds both for the value and the domain of the partial
function fi.
Definition ext_fun_seq n (f : forall i, i < n -> PartIR) := forall i j, i = j ->
forall Hi Hj x y, x [=] y -> forall Hx Hy, f i Hi x Hx [=] f j Hj y Hy.
Definition ext_fun_seq' n (f : forall i, i < n -> PartIR) := forall i j, i = j ->
forall Hi Hj x y, x [=] y -> Dom (f i Hi) x -> Dom (f j Hj) y.
Under these assumptions, we can characterize the domain and the value of the sum function from the domains and values of the summands:
Lemma FSumx_pred : forall n (f : forall i, i < n -> PartIR),
ext_fun_seq' f -> forall x, Dom (FSumx n f) x -> forall i Hi, Dom (f i Hi) x.
Lemma FSumx_pred' : forall n (f : forall i, i < n -> PartIR),
ext_fun_seq' f -> forall x, (forall i Hi, Dom (f i Hi) x) -> Dom (FSumx n f) x.
Lemma FSumx_char : forall n f x Hx Hf,
FSumx n f x Hx [=] Sumx (fun i Hi => f i Hi x (FSumx_pred n f Hf x Hx i Hi)).
As we did for arbitrary groups, it is often useful to rewrite this sums as ordinary sums.
Definition FSumx_to_FSum n : (forall i, i < n -> PartIR) -> N -> PartIR.
Defined.
Lemma FSumx_lt : forall n (f : forall i, i < n -> PartIR), ext_fun_seq f ->
forall i Hi x Hx Hx', FSumx_to_FSum n f i x Hx [=] f i Hi x Hx'.
Lemma FSumx_le : forall n (f : forall i, i < n -> PartIR), ext_fun_seq f ->
forall i x Hx, n <= i -> FSumx_to_FSum n f i x Hx [=] 0.
Lemma FSum_FSumx_to_FSum : forall n (f : forall i, i < S n -> PartIR),
ext_fun_seq f -> ext_fun_seq' f ->
forall x Hx Hx', ∑ 0 n (FSumx_to_FSum _ f) x Hx [=] FSumx _ f x Hx'.
Some useful lemmas follow.
Lemma FSum0_0 : forall P f, (forall n, ⊆ P (Dom (f n))) -> ≈ P [-C-]0 (∑0 0 f).
Lemma FSum0_S : forall P f n, (forall m, ⊆ P (Dom (f m))) ->
≈ P (∑0 n f{+}f n) (∑0 (S n) f).
Lemma FSum_0 : forall P f n, (forall i, ⊆ P (Dom (f i))) -> ≈ P (f n) (∑ n n f).
Lemma FSum_S : forall P f m n, (forall i, ⊆ P (Dom (f i))) ->
≈ P (∑ m n f{+}f (S n)) (∑ m (S n) f).
Lemma FSum_FSum0' : forall P f m n, (forall i, ⊆ P (Dom (f i))) ->
≈ P (∑ m n f) (∑0 (S n) f{-}FSum0 m f).