Theory PartialSummation (Isabelle2004: April 2004)

(*  Title:      PartialSummation.thy
    Author:     Kevin Donnelly and Jeremy Avigad
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
*)

header "Partial Summation"

theory PartialSummation = Series + FiniteLib + RealLib:;

lemma partial_sum: "!x. F(x) = sumr 0 x (%n. f(n+1)) ==>
  sumr a (a + c + 1) (%n. f(n + 1) * G(n + 1)) = F(a + c + 1) * G(a + c + 1) -
  sumr a (a + c) (%n. F(n+1) * (G(n+2) - G(n+1))) - F(a) * G(a + 1)";
apply(induct_tac c);
apply(auto simp add: ring_eq_simps);
done;

lemma partial_sum0: "!x. F(x) = sumr 0 x (%n. f(n+1)) ==>
  sumr 0 (c + 1) (%n. f(n + 1) * G(n + 1)) = F(c + 1) * G(c + 1) -
  sumr 0 (c) (%n. F(n+1) * (G(n+2) - G(n+1)))";
apply(insert partial_sum[of F f 0]);
by(force);

subsection {* Added later *}

lemma partial_sum_b: "ALL x. (F::nat=>real)(x) = (∑n=1..x. f n) ==> 
    1 <= a ==>
      (∑n=a..a + c. f(n + 1) * G(n + 1)) = F(a + c + 1) * G(a + c + 1) -
      (∑n=a..a + c - 1. F(n+1) * (G(n+2) - G(n+1))) - F(a) * G(a + 1)";
  apply (subst setsum_sumr5)+;
  apply (subst partial_sum);
  apply (rule allI);
  apply (subst setsum_sumr4 [THEN sym]);
  apply (erule spec);
  apply simp;
done;

lemma partial_sum_b0: "ALL x. 1 <= x --> 
    (F::nat=>real)(x) = (∑n=1..x. f n) ==> 
      (∑n=1..x + 1. f n * G n) = F(x + 1) * G(x + 1) -
      (∑n=1..x. F n * (G (n + 1) - G n))";
  apply (subst setsum_sumr4)+;
  apply (subst partial_sum0);
  apply (rule allI);
  apply (subst setsum_sumr4 [THEN sym]);
  apply (subgoal_tac "(if x = 0 then 0 else F x) = ?s");
  apply assumption;
  apply force;
  apply simp;
done;

declare One_nat_def [simp del];

lemma another_partial_sum: 
  "(∑n=1..x+1. (F::nat=>'b::ordered_ring)(n) * (G n - G (n - 1))) = 
     F(x + 1) * G(x + 1) - F 1 * G 0 + 
    (∑n=1..x. G n * (F n - F (n+1)))";
  apply (induct x);
  apply (simp add: ring_eq_simps);
  apply (subst Suc_plus1)+;
  apply (subst setsum_range_plus_one_nat');back;
  apply force;
  apply (erule ssubst);
  apply (simp add: ring_eq_simps compare_rls);
  apply (subst setsum_range_plus_one_nat');
  apply force;
  apply (simp add: ring_eq_simps compare_rls);
done;

lemma another_partial_sum2: "(∑n=1..x. G n * (F n - F (n+1))) = 
  (∑n=1..x+1. (F::nat=>'b::ordered_ring)(n) * (G n - G (n - 1))) - 
     F(x + 1) * G(x + 1) + F 1 * G 0"; 
  apply (subst another_partial_sum);
  apply (simp add: ring_eq_simps);
done;

declare One_nat_def [simp add];

end

lemma partial_sum:

  ∀x. F x = sumr 0 x (%n. f (n + 1))
  ==> sumr a (a + c + 1) (%n. f (n + 1) * G (n + 1)) =
      F (a + c + 1) * G (a + c + 1) -
      sumr a (a + c) (%n. F (n + 1) * (G (n + 2) - G (n + 1))) -
      F a * G (a + 1)

lemma partial_sum0:

  ∀x. F x = sumr 0 x (%n. f (n + 1))
  ==> sumr 0 (c + 1) (%n. f (n + 1) * G (n + 1)) =
      F (c + 1) * G (c + 1) - sumr 0 c (%n. F (n + 1) * (G (n + 2) - G (n + 1)))

Added later

lemma partial_sum_b:

  [| ∀x. F x = setsum f {1..x}; 1 ≤ a |]
  ==> (∑n = a..a + c. f (n + 1) * G (n + 1)) =
      F (a + c + 1) * G (a + c + 1) -
      (∑n = a..a + c - 1. F (n + 1) * (G (n + 2) - G (n + 1))) -
      F a * G (a + 1)

lemma partial_sum_b0:

  ∀x. 1 ≤ x --> F x = setsum f {1..x}
  ==> (∑n = 1..x + 1. f n * G n) =
      F (x + 1) * G (x + 1) - (∑n = 1..x. F n * (G (n + 1) - G n))

lemma another_partial_sum:

  (∑n = 1..x + 1. F n * (G n - G (n - 1))) =
  F (x + 1) * G (x + 1) - F 1 * G 0 + (∑n = 1..x. G n * (F n - F (n + 1)))

lemma another_partial_sum2:

  (∑n = 1..x. G n * (F n - F (n + 1))) =
  (∑n = 1..x + 1. F n * (G n - G (n - 1))) - F (x + 1) * G (x + 1) + F 1 * G 0