Theory Summation

theory Summation
imports Main
(* Author: Florian Haftmann, TU Muenchen *)

header {* Some basic facts about discrete summation *}

theory Summation
imports Main
begin

text {* Auxiliary. *}

lemma add_setsum_orient:
"setsum f {k..<j} + setsum f {l..<k} = setsum f {l..<k} + setsum f {k..<j}"
by (fact add.commute)

lemma add_setsum_int:
fixes j k l :: int
shows "j < k ==> k < l ==> setsum f {j..<k} + setsum f {k..<l} = setsum f {j..<l}"
by (simp_all add: setsum_Un_Int [symmetric] ivl_disj_un)

text {* The shift operator. *}

definition Δ :: "(int => 'a::ab_group_add) => int => 'a" where
"Δ f k = f (k + 1) - f k"

lemma Δ_shift:
"Δ (λk. l + f k) = Δ f"
by (simp add: Δ_def fun_eq_iff)

lemma Δ_same_shift:
assumes "Δ f = Δ g"
shows "∃l. plus l o f = g"
proof -
fix k
from assms have "!!k. Δ f k = Δ g k" by simp
then have k_incr: "!!k. f (k + 1) - g (k + 1) = f k - g k"
by (simp add: Δ_def algebra_simps)
then have "!!k. f ((k - 1) + 1) - g ((k - 1) + 1) = f (k - 1) - g (k - 1)"
by blast
then have k_decr: "!!k. f (k - 1) - g (k - 1) = f k - g k"
by simp
have "!!k. f k - g k = f 0 - g 0"
proof -
fix k
show "f k - g k = f 0 - g 0"
by (induct k rule: int_induct) (simp_all add: k_incr k_decr)
qed
then have "!!k. (plus (g 0 - f 0) o f) k = g k"
by (simp add: algebra_simps)
then have "plus (g 0 - f 0) o f = g" ..
then show ?thesis ..
qed

text {* The formal sum operator. *}

definition Σ :: "(int => 'a::ab_group_add) => int => int => 'a" where
"Σ f j l = (if j < l then setsum f {j..<l}
else if j > l then - setsum f {l..<j}
else 0)"


lemma Σ_same [simp]:
"Σ f j j = 0"
by (simp add: Σ_def)

lemma Σ_positive:
"j < l ==> Σ f j l = setsum f {j..<l}"
by (simp add: Σ_def)

lemma Σ_negative:
"j > l ==> Σ f j l = - Σ f l j"
by (simp add: Σ_def)

lemma add_Σ:
"Σ f j k + Σ f k l = Σ f j l"
by (simp add: Σ_def algebra_simps add_setsum_int)
(simp_all add: add_setsum_orient [of f k j l]
add_setsum_orient [of f j l k]
add_setsum_orient [of f j k l] add_setsum_int)

lemma Σ_incr_upper:
"Σ f j (l + 1) = Σ f j l + f l"
proof -
have "{l..<l+1} = {l}" by auto
then have "Σ f l (l + 1) = f l" by (simp add: Σ_def)
moreover have "Σ f j (l + 1) = Σ f j l + Σ f l (l + 1)" by (simp add: add_Σ)
ultimately show ?thesis by simp
qed

text {* Fundamental lemmas: The relation between @{term Δ} and @{term Σ}. *}

lemma Δ_Σ:
"Δ (Σ f j) = f"
proof
fix k
show "Δ (Σ f j) k = f k"
by (simp add: Δ_def Σ_incr_upper)
qed

lemma Σ_Δ:
"Σ (Δ f) j l = f l - f j"
proof -
from Δ_Σ have "Δ (Σ (Δ f) j) = Δ f" .
then obtain k where "plus k o Σ (Δ f) j = f" by (blast dest: Δ_same_shift)
then have "!!q. f q = k + Σ (Δ f) j q" by (simp add: fun_eq_iff)
then show ?thesis by simp
qed

end