Sums over Reals



Let c be a real.

Here we prove that sum_(m≤ i ≤ n) c^k = frac (c^(n+1) -c^m) (c-1)

Section Sums_over_Reals.

Variable c : IR.

Lemma Sum0_c_exp : forall H m, ∑0 m (fun i => c[^]i) [=] (c[^]m[-]1[/] c[-]1[//]H).


Lemma Sum_c_exp : forall H m n,
 ∑ m n (fun i => c[^]i) [=] (c[^]S n[-]c[^]m[/] c[-]1[//]H).

The following formulation is often more useful if c < 1.

Lemma Sum_c_exp' : forall H m n,
 ∑ m n (fun i => c[^]i) [=] (c[^]m[-]c[^]S n[/] 1[-]c[//]H).


End Sums_over_Reals.


Lemma diff_is_Sum0 : forall (s : N -> IR) n, s n[-]s 0 [=] ∑0 n (fun i => s (S i) [-]s i).


Lemma diff_is_sum : forall (s : N -> IR) N m,
 N < m -> s m[-]s N [=] ∑ N (pred m) (fun i => s (S i) [-]s i).


Lemma Sum0_pres_less : forall s t : N -> IR, (forall i, s i [<] t i) -> forall n, ∑0 n s [<=] ∑0 n t.

Lemma Sum_pres_less : forall s t : N -> IR,
 (forall i, s i [<] t i) -> forall N m, N <= m -> ∑ N m s [<=] ∑ N m t.

Lemma Sum_pres_leEq : forall s t : N -> IR,
 (forall i, s i [<=] t i) -> forall N m, N <= m -> ∑ N m s [<=] ∑ N m t.

Lemma Sum0_comm_scal : forall (s : N -> IR) a m,
 ∑0 m (fun i => s i[*]a) [=] ∑0 m s [*]a.





Lemma Sum_comm_scal : forall (s : N -> IR) a N m,
 ∑ N m (fun i => s i[*]a) [=] ∑ N m s [*]a.


Lemma Sum0_comm_scal' : forall (s : N -> IR) a m,
 ∑0 m (fun i => a[*]s i) [=] a[*]∑0 m s.

Lemma Sum_comm_scal' : forall (s : N -> IR) a m n,
 ∑ m n (fun i => a[*]s i) [=] a[*]∑ m n s.

Lemma Sumx_comm_scal' : forall n (a : IR) (f : forall i, i < n -> IR),
 Sumx (fun i H => a[*]f i H) [=] a[*]Sumx f.

Lemma Sum2_comm_scal' : forall a m n (f: forall i, m <= i -> i <= n -> IR),
 m <= S n -> ∑2 (fun i Hm Hn => a[*]f i Hm Hn) [=] a[*]∑2 f.