# Theory PartialSummation

Up to index of Isabelle/HOL/HOL-Complex/NumberTheory

theory PartialSummation = Series + FiniteLib + RealLib:

```(*  Title:      PartialSummation.thy
Author:     Kevin Donnelly and Jeremy Avigad
*)

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)))```

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```