# Theory Summation

theory Summation
imports Main
`(* Author: Florian Haftmann, TU Muenchen *)header {* Some basic facts about discrete summation *}theory Summationimports Mainbegintext {* 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 ..qedtext {* 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 simpqedtext {* 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)qedlemma Σ_Δ:  "Σ (Δ 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 simpqedend`