Sums



Let G be an abelian group.

Section Sums.

Variable G : CAbGroup.

Fixpoint Sumlist (l : list G) : G :=
  match l with
  | nil => 0:G
  | cons x k => x[+]Sumlist k
  end.

Fixpoint Sumx n : (forall i : N, i < n -> G) -> G :=
  match n return ((forall i : N, i < n -> G) -> G) with
  | O => fun _ => 0:G
  | S m => fun f => Sumx m (fun i l => f i (lt_S _ _ l)) [+]f m (lt_n_Sn m)
  end.

It is sometimes useful to view a function defined on {0, ... i-1} as a function on the natural numbers which evaluates to 0 when the input is greater than or equal to i.

Definition part_tot_nat_fun n (f : forall i, i < n -> G) : N -> G.
Defined.

Lemma part_tot_nat_fun_ch1 : forall n (f : forall i, i < n -> G),
 nat_less_n_fun f -> forall i Hi, part_tot_nat_fun n f i [=] f i Hi.

Lemma part_tot_nat_fun_ch2 : forall n (f : forall i, i < n -> G) i,
 n <= i -> part_tot_nat_fun n f i [=] 0.

∑0 defines the sum for i=0..(n-1)

Fixpoint ∑0 (n:nat) (f : N -> G) {struct n} : G :=
  match n with
  | O => 0:G
  | S m => ∑0 m f[+]f m
  end.

∑1 defines the sum for i=m..(n-1)

Definition ∑1 m n f := ∑0 n f[-]∑0 m f.

Definition ∑ m n : (N -> G) -> G := ∑1 m (S n).

∑2 is similar to ∑1, but does not require the summand to be defined outside where it is being added.

Definition ∑2 m n (h : forall i : N, m <= i -> i <= n -> G) : G.
Defined.

Lemma Sum_one : forall n f, ∑ n n f [=] f n.


Lemma Sum_empty : forall n f, 0 < n -> ∑ n (pred n) f [=] 0.


Lemma Sum_Sum : forall l m n f, ∑ l m f[+]∑ (S m) n f [=] ∑ l n f.


Lemma Sum_first : forall m n f, ∑ m n f [=] f m[+]∑ (S m) n f.

Lemma Sum_last : forall m n f, ∑ m (S n) f [=] ∑ m n f[+]f (S n).


Lemma Sum_last' : forall m n f, 0 < n -> ∑ m n f [=] ∑ m (pred n) f[+]f n.


We add some extensionality results which will be quite useful when working with integration.

Lemma Sum0_strext : forall f g n, ∑0 n f [#] ∑0 n g -> {i:nat | i < n | f i [#] g i}.

Lemma Sum_strext : forall f g m n, m <= S n ->
 ∑ m n f [#] ∑ m n g -> {i : N | m <= i /\ i <= n | f i [#] g i}.

Lemma Sumx_strext : forall n f g, nat_less_n_fun f -> nat_less_n_fun g ->
 Sumx _ f [#] Sumx _ g -> {N : N | {HN : N < n | f N HN [#] g N HN}}.



Lemma Sum0_strext' : forall f g n, ∑0 n f [#] ∑0 n g -> {i : N | f i [#] g i}.

Lemma Sum_strext' : forall f g m n, ∑ m n f [#] ∑ m n g -> {i : N | f i [#] g i}.

Lemma Sum0_wd : forall m f f', (forall i, f i [=] f' i) -> ∑0 m f [=] ∑0 m f'.

Lemma Sum_wd : forall m n f f', (forall i, f i [=] f' i) -> ∑ m n f [=] ∑ m n f'.

Lemma Sumx_wd : forall n f g, (forall i H, f i H [=] g i H) -> Sumx n f [=] Sumx n g.

Lemma Sum_wd' : forall m n, m <= S n -> forall f f',
 (forall i, m <= i -> i <= n -> f i [=] f' i) -> ∑ m n f [=] ∑ m n f'.





Lemma Sum2_wd : forall m n, m <= S n -> forall f g,
 (forall i Hm Hn, f i Hm Hn [=] g i Hm Hn) -> ∑2 m n f [=] ∑2 m n g.

Lemma Sum0_plus_Sum0 : forall f g m, ∑0 m (fun i => f i[+]g i) [=] ∑0 m f[+]∑0 m g.

Lemma Sum_plus_Sum : forall f g m n, ∑ m n (fun i => f i[+]g i) [=] ∑ m n f[+]∑ m n g.

Lemma Sumx_plus_Sumx : forall n f g, Sumx n f[+]Sumx n g [=] Sumx n (fun i Hi => f i Hi[+]g i Hi).

Lemma Sum2_plus_Sum2 : forall m n, m <= S n -> forall f g,
 ∑2 m n f[+]∑2 m n g [=] ∑2 _ _ (fun i Hm Hn => f i Hm Hn[+]g i Hm Hn).

Lemma inv_Sum0 : forall f n, ∑0 n (fun i => [--] (f i)) [=] [--] (∑0 n f).


Lemma inv_Sum : forall f m n, ∑ m n (fun i => [--] (f i)) [=] [--] (∑ m n f).


Lemma inv_Sumx : forall n f, [--] (Sumx n f) [=] Sumx _ (fun i Hi => [--] (f i Hi)).

Lemma inv_Sum2 : forall m n : N, m <= S n -> forall f,
 [--] (∑2 m n f) [=] ∑2 _ _ (fun i Hm Hn => [--] (f i Hm Hn)).

Lemma Sum_minus_Sum : forall f g m n, ∑ m n (fun i => f i[-]g i) [=] ∑ m n f[-]∑ m n g.


Lemma Sumx_minus_Sumx : forall n f g,
 Sumx n f[-]Sumx n g [=] Sumx _ (fun i Hi => f i Hi[-]g i Hi).

Lemma Sum2_minus_Sum2 : forall m n, m <= S n -> forall f g,
 ∑2 m n f[-]∑2 m n g [=] ∑2 _ _ (fun i Hm Hn => f i Hm Hn[-]g i Hm Hn).

Lemma Sum_apzero : forall f m n,
 m <= n -> ∑ m n f [#] 0 -> {i : N | m <= i /\ i <= n | f i [#] 0}.










Lemma Sum_zero : forall f m n, m <= S n ->
 (forall i, m <= i -> i <= n -> f i [=] 0) -> ∑ m n f [=] 0.






Lemma Sum_term : forall f m i n, m <= i -> i <= n ->
 (forall j, m <= j -> j <> i -> j <= n -> f j [=] 0) -> ∑ m n f [=] f i.







Lemma Sum0_shift : forall f g n, (forall i, f i [=] g (S i)) -> g 0[+]∑0 n f [=] ∑0 (S n) g.



Lemma Sum_shift : forall f g m n,
 (forall i, f i [=] g (S i)) -> ∑ m n f [=] ∑ (S m) (S n) g.


Lemma Sum_big_shift : forall f g k m n, (forall j, m <= j -> f j [=] g (j + k)) ->
 m <= S n -> ∑ m n f [=] ∑ (m + k) (n + k) g.

Lemma Sumx_Sum0 : forall n f g,
 (forall i Hi, f i Hi [=] g i) -> Sumx n f [=] ∑0 n g.

End Sums.


The next results are useful for calculating some special sums, often referred to as ``Mengolli Sums''. Let G be an abelian group.

Section More_Sums.

Variable G : CAbGroup.

Lemma Mengolli_Sum : forall n (f : forall i, i <= n -> G) (g : forall i, i < n -> G),
 nat_less_n_fun' f -> (forall i H, g i H [=] f (S i) H[-]f i (lt_le_weak _ _ H)) ->
 Sumx g [=] f n (le_n n) [-]f 0 (le_O_n n).

Lemma Mengolli_Sum_gen : forall f g : N -> G, (forall n, g n [=] f (S n) [-]f n) ->
 forall m n, m <= S n -> ∑ m n g [=] f (S n) [-]f m.

Lemma str_Mengolli_Sum_gen : forall (f g : N -> G) m n, m <= S n ->
 (forall i, m <= i -> i <= n -> g i [=] f (S i) [-]f i) -> ∑ m n g [=] f (S n) [-]f m.

Lemma Sumx_to_Sum : forall n, 0 < n -> forall f, nat_less_n_fun f ->
 Sumx f [=] ∑ 0 (pred n) (part_tot_nat_fun G n f).

End More_Sums.