CoRN.ftc.FunctSums

Require Export CSumsReals.
Require Export PartFunEquality.
Set Automatic Introduction.

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 {f_i} of functions; we can both define the sum of the first n functions ( ∑₀) or the sum of f_m through f_n ( ∑).

Definition ∑₀ (n : nat) (f : nat → PartIR) : PartIR.
Proof.
intros.
apply Build_PartFunct with (fun x : IR ⇒ ∀ n : nat, Dom (f n) x)
   (fun (x : IR) (Hx : ∀ n : nat, Dom (f n) x) ⇒ Sum0 n (fun n : nat ⇒ Part (f n) x (Hx n))).
  intros x y H H0 n0.
  apply (dom_wd _ (f n0) x).
   apply H.
  assumption.
intros x y Hx Hy H.
elim (Sum0_strext' _ _ _ _ H); intros i Hi.
apply pfstrx with (f i) (Hx i) (Hy i); assumption.
Defined.

Definition ∑ (m n : nat) (f : nat → PartIR) : PartIR.
Proof.
intros.
apply Build_PartFunct with (fun x : IR ⇒ ∀ n : nat, Dom (f n) x)
   (fun (x : IR) (Hx : ∀ n : nat, Dom (f n) x) ⇒ Sum m n (fun n : nat ⇒ Part (f n) x (Hx n))).
  intros x y H H0 n0.
  apply (dom_wd _ (f n0) x).
   apply H.
  assumption.
intros x y Hx Hy H.
elim (Sum_strext' _ _ _ _ _ H); intros i Hi.
apply pfstrx with (f i) (Hx i) (Hy i); assumption.
Defined.

Although ∑ is here defined directly, it has the same relationship to the ∑₀ operator as Sum has to Sum0. Also, all the results for Sum and Sum0 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 : ∀ m n (f : nat → PartIR) x Hx Hx' Hx'',
∑ m n f x Hx [=] ∑₀ (S n) f x Hx'[-]∑₀ m f x Hx''.
Proof.
intros.
simpl in |- *; unfold Sum, Sum1 in |- *; simpl in |- ×.
apply cg_minus_wd; try apply bin_op_wd_unfolded; try apply Sum0_wd; intros; algebra.
Qed.

Lemma FSum0_wd : ∀ m (f g : nat → PartIR),
(∀ x HxF HxG i, f i x (HxF i) [=] g i x (HxG i)) →
∀ x HxF HxG, ∑₀ m f x HxF [=] ∑₀ m g x HxG.
Proof.
intros.
simpl in |- ×.
apply Sum0_wd.
intros; simpl in |- *; algebra.
Qed.

Lemma FSum_one : ∀ n (f : nat → PartIR) x Hx Hx',
∑ n n f x Hx' [=] f n x Hx.
Proof.
intros.
simpl in |- ×.
eapply eq_transitive_unfolded.
  apply Sum_one.
simpl in |- *; rational.
Qed.

Lemma FSum_FSum : ∀ l m n (f : nat → PartIR) x Hx Hx' Hx'',
∑ l m f x Hx [+]∑ (S m) n f x Hx' [=] ∑ l n f x Hx''.
Proof.
intros.
simpl in |- ×.
eapply eq_transitive_unfolded.
  2: apply Sum_Sum with (l := l) (m := m).
apply bin_op_wd_unfolded; apply Sum_wd; intros; rational.
Qed.

Lemma FSum_first : ∀ m n (f : nat → PartIR) x Hx Hx' Hx'',
∑ m n f x Hx [=] f m x Hx'[+]∑ (S m) n f x Hx''.
Proof.
intros.
simpl in |- ×.
eapply eq_transitive_unfolded.
  apply Sum_first.
apply bin_op_wd_unfolded; try apply Sum_wd; intros; rational.
Qed.

Lemma FSum_last : ∀ m n (f : nat → PartIR) x Hx Hx' Hx'',
∑ m (S n) f x Hx [=] ∑ m n f x Hx'[+]f (S n) x Hx''.
Proof.
intros.
simpl in |- ×.
eapply eq_transitive_unfolded.
  apply Sum_last.
apply bin_op_wd_unfolded; try apply Sum_wd; intros; rational.
Qed.

Lemma FSum_last' : ∀ m n (f : nat → PartIR) x Hx Hx' Hx'',
0 < n → ∑ m n f x Hx [=] ∑ m (pred n) f x Hx'[+]f n x Hx''.
Proof.
intros.
simpl in |- ×.
eapply eq_transitive_unfolded.
  apply Sum_last'.
  assumption.
apply bin_op_wd_unfolded; try apply Sum_wd; intros; rational.
Qed.

Lemma FSum_wd : ∀ m n (f g : nat → PartIR),
(∀ x HxF HxG i, f i x (HxF i) [=] g i x (HxG i)) →
∀ x HxF HxG, ∑ m n f x HxF [=] ∑ m n g x HxG.
Proof.
intros.
simpl in |- ×.
apply Sum_wd.
algebra.
Qed.

Lemma FSum_plus_FSum : ∀ (f g : nat → 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.
Proof.
intros.
simpl in |- ×.
eapply eq_transitive_unfolded.
  2: apply Sum_plus_Sum.
apply Sum_wd; intros; rational.
Qed.

Lemma inv_FSum : ∀ (f : nat → PartIR) m n x Hx Hx',
∑ m n (fun i ⇒ {--} (f i )) x Hx [=] [--] (∑ m n f x Hx').
Proof.
intros.
simpl in |- ×.
eapply eq_transitive_unfolded.
  2: apply inv_Sum.
apply Sum_wd; intros; rational.
Qed.

Lemma FSum_minus_FSum : ∀ (f g : nat → 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.
Proof.
intros.
simpl in |- ×.
eapply eq_transitive_unfolded.
  2: apply Sum_minus_Sum.
apply Sum_wd; intros; rational.
Qed.

Lemma FSum_wd' : ∀ m n, m ≤ S n → ∀ f g : nat → PartIR,
(∀ x HxF HxG i, m ≤ i → i ≤ n → f i x (HxF i) [=] g i x (HxG i)) →
∀ x HxF HxG, ∑ m n f x HxF [=] ∑ m n g x HxG.
Proof.
intros.
simpl in |- ×.
apply Sum_wd'; try assumption.
algebra.
Qed.

Lemma FSum_resp_less : ∀ (f g : nat → PartIR) m n, m ≤ n →
(∀ x HxF HxG i, m ≤ i → i ≤ n → f i x (HxF i) [<] g i x (HxG i)) →
∀ x HxF HxG, ∑ m n f x HxF [<] ∑ m n g x HxG.
Proof.
intros f g m n H H0 x HxF HxG.
simpl in |- ×.
apply Sum_resp_less; try assumption.
intros; apply H0; assumption.
Qed.

Lemma FSum_resp_leEq : ∀ (f g : nat → PartIR) m n, m ≤ S n →
(∀ x HxF HxG i, m ≤ i → i ≤ n → f i x (HxF i) [<=] g i x (HxG i)) →
∀ x HxF HxG, ∑ m n f x HxF [<=] ∑ m n g x HxG.
Proof.
intros f g m n H H0 x HxF HxG.
simpl in |- ×.
apply Sum_resp_leEq; try assumption.
intros; apply H0; assumption.
Qed.

Lemma FSum_comm_scal : ∀ (f : nat → PartIR) c m n x Hx Hx',
∑ m n (fun i ⇒ f i {*} [-C -]c) x Hx [=] (∑ m n f {*} [-C -]c) x Hx'.
Proof.
intros.
simpl in |- ×.
eapply eq_transitive_unfolded.
  2: apply (Sum_comm_scal (fun n : nat ⇒ f n x (ProjIR1 Hx' n)) c m n).
apply Sum_wd; intros; rational.
Qed.

Lemma FSum_comm_scal' : ∀ (f : nat → PartIR) c m n x Hx Hx',
∑ m n (fun i ⇒ [-C -]c {*}f i) x Hx [=] ( [-C -]c {*}∑ m n f) x Hx'.
Proof.
intros.
simpl in |- ×.
eapply eq_transitive_unfolded.
  2: apply (Sum_comm_scal' (fun n : nat ⇒ f n x (ProjIR2 Hx' n)) c m n).
apply Sum_wd; intros; rational.
Qed.

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 : nat) : (∀ i, i < n → PartIR) → PartIR :=
  match n return ((∀ 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 : ∀ n (f g : ∀ i, i < n → PartIR),
(∀ i Hi x HxF HxG, f i Hi x HxF [=] g i Hi x HxG) →
∀ x HxF HxG, FSumx n f x HxF [=] FSumx n g x HxG.
Proof.
intro; case n.
  intros; simpl in |- *; algebra.
clear n.
simple induction n.
  intros; simpl in |- *; algebra.
clear n; intro.
cut {p : nat | S n = p}; [ intro H | ∃ (S n); auto ].
elim H; intros p Hp.
rewrite Hp; intros.
simpl in |- ×.
apply bin_op_wd_unfolded.
  apply H0.
  intros; apply H1.
apply H1.
Qed.

Lemma FSumx_wd' : ∀ (P : IR → CProp) n (f g : ∀ i, i < n → PartIR),
(∀ i H H', Feq P (f i H) (g i H')) → Feq P (FSumx n f) (FSumx n g).
Proof.
intros; induction n as [| n Hrecn].
  simpl in |- *; apply Feq_reflexive; apply included_IR.
simpl in |- *; apply Feq_plus; auto.
Qed.

As was already the case for Sumx, in many cases we will need to explicitly assume that f₁ is independent of the proof that i [<] n. This holds both for the value and the domain of the partial function f_i.

Definition ext_fun_seq n (f : ∀ i, i < n → PartIR) := ∀ i j, i = j →
∀ Hi Hj x y, x [=] y → ∀ Hx Hy, f i Hi x Hx [=] f j Hj y Hy.

Definition ext_fun_seq' n (f : ∀ i, i < n → PartIR) := ∀ i j, i = j →
∀ Hi Hj x y, x [=] y → Dom (f i Hi) x → Dom (f j Hj) y.

Implicit Arguments ext_fun_seq [n].
Implicit Arguments ext_fun_seq' [n].

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 : ∀ n (f : ∀ i, i < n → PartIR),
ext_fun_seq' f → ∀ x, Dom (FSumx n f) x → ∀ i Hi, Dom (f i Hi) x.
Proof.
intros n f H x H0 i Hi; red in H; induction n as [| n Hrecn].
  elimtype False; inversion Hi.
elim (le_lt_eq_dec _ _ Hi); intro.
  cut (i < n); [ intro | auto with arith ].
  set (g := fun i Hi ⇒ f i (lt_S _ _ Hi)) in ×.
  apply H with i (lt_S _ _ H1) x.
    auto.
   algebra.
  change (Dom (g i H1) x) in |- ×.
  apply Hrecn.
   unfold g in |- *; intros.
   apply H with i0 (lt_S i0 n Hi0) x0; auto.
  inversion_clear H0; assumption.
elim H0; intros H1 H2; clear H0 H1.
apply H with n (lt_n_Sn n) x; auto.
  symmetry in |- *; auto.
algebra.
Qed.

Lemma FSumx_pred' : ∀ n (f : ∀ i, i < n → PartIR),
ext_fun_seq' f → ∀ x, (∀ i Hi, Dom (f i Hi) x) → Dom (FSumx n f) x.
Proof.
intros n f H x H0; induction n as [| n Hrecn].
  simpl in |- *; auto.
split.
  apply Hrecn.
   red in |- *; intros.
   red in H.
   exact (H _ _ H1 _ _ _ _ H2 X).
  intros; auto.
apply H0.
Qed.

Lemma FSumx_char : ∀ 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)).
Proof.
intro; induction n as [| n Hrecn].
  algebra.
intros; simpl in |- ×.
apply bin_op_wd_unfolded; algebra.
cut (ext_fun_seq' (fun i Hi ⇒ f i (lt_S i n Hi))).
  intro H.
  eapply eq_transitive_unfolded.
   apply Hrecn with (Hf := H).
  apply Sumx_wd; intros; simpl in |- *; algebra.
intros i j H H0 H' x0 y H1 H2.
apply Hf with i (lt_S i n H0) x0; auto.
Qed.

As we did for arbitrary groups, it is often useful to rewrite this sums as ordinary sums.

Definition FSumx_to_FSum n : (∀ i, i < n → PartIR) → nat → PartIR.
Proof.
intros f i.
elim (le_lt_dec n i); intro.
  apply ( [-C -][0]:PartIR).
apply (f i b).
Defined.

Lemma FSumx_lt : ∀ n (f : ∀ i, i < n → PartIR), ext_fun_seq f →
∀ i Hi x Hx Hx', FSumx_to_FSum n f i x Hx [=] f i Hi x Hx'.
Proof.
do 6 intro.
unfold FSumx_to_FSum in |- ×.
elim (le_lt_dec n i); intro; simpl in |- ×.
  elimtype False; apply (le_not_lt n i); auto.
intros; apply H; auto.
algebra.
Qed.

Lemma FSumx_le : ∀ n (f : ∀ i, i < n → PartIR), ext_fun_seq f →
∀ i x Hx, n ≤ i → FSumx_to_FSum n f i x Hx [=] [0].
Proof.
do 5 intro.
unfold FSumx_to_FSum in |- ×.
elim (le_lt_dec n i); intro; simpl in |- ×.
  intro; algebra.
intros; elimtype False; apply (le_not_lt n i); auto.
Qed.

Lemma FSum_FSumx_to_FSum : ∀ n (f : ∀ i, i < S n → PartIR),
ext_fun_seq f → ext_fun_seq' f →
∀ x Hx Hx', ∑ 0 n (FSumx_to_FSum _ f) x Hx [=] FSumx _ f x Hx'.
Proof.
simple induction n.
  intros; simpl in |- ×.
  eapply eq_transitive_unfolded.
   apply Sum_one.
  simpl in |- ×.
  cut (0 < 1); [ intro | apply lt_n_Sn ].
  astepr (Part (f 0 (lt_n_Sn 0)) x (ProjIR2 Hx')).
  apply FSumx_lt; assumption.
clear n; intros n H f H0 H1 x Hx Hx'.
simpl in |- ×.
eapply eq_transitive_unfolded.
  apply Sum_last.
apply bin_op_wd_unfolded.
  set (g := fun i (l : i < S n) ⇒ f i (lt_S _ _ l)) in ×.
  cut (ext_fun_seq g); intros.
   cut (ext_fun_seq' g).
    intro H3.
    astepr (FSumx n (fun i (l : i < n) ⇒ g i (lt_S _ _ l)) x
      (ProjIR1 (ProjIR1 Hx')) [+]g n (lt_n_Sn n) x (ProjIR2 (ProjIR1 Hx'))).
    cut (Dom (FSumx _ g) x).
     intro H4; cut (∀ m : nat, Dom (FSumx_to_FSum (S n) g m) x).
      intro Hx''.
      simpl in H.
      apply eq_transitive_unfolded with (Sum 0 n (fun m : nat ⇒ FSumx_to_FSum (S n) g m x (Hx'' m))).
       2: apply H with (f := g); try assumption.
      apply Sum_wd'.
       auto with arith.
      intros.
      cut (i < S (S n)); [ intro | auto with arith ].
      apply eq_transitive_unfolded with (f i H7 x (FSumx_pred _ _ H1 x Hx' i H7)).
       apply FSumx_lt; assumption.
      cut (i < S n); [ intro | auto with arith ].
      apply eq_transitive_unfolded with (g i H8 x (FSumx_pred _ _ H3 x H4 i H8)).
       2: apply eq_symmetric_unfolded; apply FSumx_lt; assumption.
      unfold g in |- *; apply H0; auto.
      algebra.
     intro.
     simpl in Hx.
     generalize (Hx m); clear H4 H3 H2 Hx.
     unfold FSumx_to_FSum in |- ×.
     elim (le_lt_dec (S n) m); elim (le_lt_dec (S (S n)) m); do 2 intro; simpl in |- *; intro.
        auto.
       auto.
      unfold g in |- *; apply FSumx_pred with (n := S (S n)); assumption.
     unfold g in |- *; apply FSumx_pred with (n := S (S n)); assumption.
    simpl in Hx'.
    unfold g in |- *; inversion_clear Hx'; intros; assumption.
   unfold g in |- *; red in |- *; intros.
   red in H1; apply H1 with i (lt_S _ _ Hi) x0; auto.
  unfold g in |- *; red in |- *; intros.
  red in H0; apply H0; auto.
apply FSumx_lt; auto.
Qed.

Some useful lemmas follow.

Lemma FSum0_0 : ∀ P f, (∀ n, included P (Dom (f n))) → Feq P [-C -][0] (∑₀ 0 f).
Proof.
intros P f H.
FEQ.
simpl in |- ×.
red in |- *; intros; apply (H n); auto.
Qed.

Lemma FSum0_S : ∀ P f n, (∀ m, included P (Dom (f m))) →
Feq P (∑₀ n f {+}f n) (∑₀ (S n) f).
Proof.
intros P f n H.
FEQ.
   apply included_FPlus; auto.
   simpl in |- *; red in |- *; intros.
   apply (H n0); auto.
  simpl in |- ×.
  red in |- *; intros; apply (H n0); auto.
simpl in |- *; apply bin_op_wd_unfolded; algebra.
apply Sum0_wd; algebra.
Qed.

Lemma FSum_0 : ∀ P f n, (∀ i, included P (Dom (f i))) → Feq P (f n) (∑ n n f).
Proof.
intros P f n H.
FEQ.
  simpl in |- ×.
  red in |- *; intros; apply (H n0); auto.
simpl in |- ×.
apply eq_symmetric_unfolded.
eapply eq_transitive_unfolded.
  apply Sum_one.
algebra.
Qed.

Lemma FSum_S : ∀ P f m n, (∀ i, included P (Dom (f i))) →
Feq P (∑ m n f {+}f (S n)) (∑ m (S n) f).
Proof.
intros P f m n H.
apply eq_imp_Feq.
   apply included_FPlus; auto.
   simpl in |- ×.
   red in |- *; intros; apply (H n0); auto.
  simpl in |- ×.
  red in |- *; intros; apply (H n0); auto.
intros; simpl in |- *; apply eq_symmetric_unfolded.
eapply eq_transitive_unfolded.
  apply Sum_last.
algebra.
Qed.

Lemma FSum_FSum0' : ∀ P f m n, (∀ i, included P (Dom (f i))) →
Feq P (∑ m n f) (∑₀ (S n) f {-}∑₀ m f).
Proof.
intros P f m n H.
apply eq_imp_Feq.
   red in |- *; intros; intro; apply (H n0); auto.
  apply included_FMinus; red in |- *; intros; intro; apply (H n0); auto.
intros.
apply eq_transitive_unfolded with (Part _ _ (ProjIR1 Hx') [-]∑₀ m f _ (ProjIR2 Hx')).
  apply FSum_FSum0.
simpl in |- *; rational.
Qed.