Theory Partial_Summation
section ‹Partial summation›
theory Partial_Summation
imports
"HOL-Analysis.Analysis"
Arithmetic_Summatory
begin
lemma finite_vimage_real_of_nat_greaterThanAtMost: "finite (real -` {y<..x})"
proof (rule finite_subset)
show "real -` {y<..x} ⊆ {nat ⌊y⌋..nat ⌈x⌉}"
by (cases "x ≥ 0"; cases "y ≥ 0")
(auto simp: nat_le_iff le_nat_iff le_ceiling_iff floor_le_iff)
qed auto
context
fixes a :: "nat ⇒ 'a :: {banach, real_normed_algebra}"
fixes f f' :: "real ⇒ 'a"
fixes A
fixes X :: "real set"
fixes x y :: real
defines "A ≡ sum_upto a"
assumes fin: "finite X"
assumes xy: "0 ≤ y" "y < x"
assumes deriv: "⋀z. z ∈ {y..x} - X ⟹ (f has_vector_derivative f' z) (at z)"
assumes cont_f: "continuous_on {y..x} f"
begin
lemma partial_summation_strong:
"((λt. A t * f' t) has_integral
(A x * f x - A y * f y - (∑n ∈ real -` {y<..x}. a n * f n))) {y..x}"
proof -
define chi :: "nat ⇒ real ⇒ real" where "chi = (λn t. if n ≤ t then 1 else 0)"
have "((λt. sum_upto (λn. a n * (chi n t *⇩R f' t)) x) has_integral
(sum_upto (λn. a n * (f x - f (max n y))) x)) {y..x}" (is "(_ has_integral ?I) _")
unfolding sum_upto_def
proof (intro has_integral_sum ballI finite_Nats_le_real, goal_cases)
case (1 n)
have "(f' has_integral (f x - f (max n y))) {max n y..x}"
using xy 1
by (intro fundamental_theorem_of_calculus_strong[OF fin])
(auto intro!: continuous_on_subset[OF cont_f] deriv)
also have "?this ⟷ ((λt. (if t ∈ {max n y..x} then 1 else 0) *⇩R f' t)
has_integral (f x - f (max n y))) {max n y..x}"
by (intro has_integral_cong) (simp_all add: chi_def)
finally have "((λt. (if t ∈ {max n y..x} then 1 else 0) *⇩R f' t)
has_integral (f x - f (max n y))) {y..x}"
by (rule has_integral_on_superset) auto
also have "?this ⟷ ((λt. chi n t *⇩R f' t) has_integral (f x - f (max n y))) {y..x}"
by (intro has_integral_cong) (auto simp: chi_def)
finally show ?case by (intro has_integral_mult_right)
qed
also have "?this ⟷ ((λt. A t * f' t) has_integral ?I) {y..x}"
unfolding sum_upto_def A_def chi_def sum_distrib_right using xy
by (intro has_integral_cong sum.mono_neutral_cong_right finite_Nats_le_real) auto
also have "sum_upto (λn. a n * (f x - f (max (real n) y))) x =
A x * f x - (∑n | n > 0 ∧ real n ≤ x. a n * f (max (real n) y))"
by (simp add: sum_upto_def ring_distribs sum_subtractf sum_distrib_right A_def)
also have "{n. n > 0 ∧ real n ≤ x} = {n. n > 0 ∧ real n ≤ y} ∪ real -` {y<..x}"
using xy by auto
also have "sum (λn. a n * f (max (real n) y)) … =
(∑n | 0 < n ∧ real n ≤ y. a n * f (max (real n) y)) +
(∑n ∈ real -` {y<..x}. a n * f (max (real n) y))" (is "_ = ?S1 + ?S2")
by (intro sum.union_disjoint finite_Nats_le_real finite_vimage_real_of_nat_greaterThanAtMost)
auto
also have "?S1 = sum_upto (λn. a n * f y) y" unfolding sum_upto_def
by (intro sum.cong refl) (auto simp: max_def)
also have "… = A y * f y" by (simp add: A_def sum_upto_def sum_distrib_right)
also have "?S2 = (∑n ∈ real -` {y<..x}. a n * f n)"
by (intro sum.cong refl) (auto simp: max_def)
finally show ?thesis by (simp add: algebra_simps)
qed
lemma partial_summation_integrable_strong:
"(λt. A t * f' t) integrable_on {y..x}"
and partial_summation_strong':
"(∑n∈real -` {y<..x}. a n * f n) =
A x * f x - A y * f y - integral {y..x} (λt. A t * f' t)"
using partial_summation_strong by (simp_all add: has_integral_iff algebra_simps)
end
context
fixes a :: "nat ⇒ 'a :: {banach, real_normed_algebra}"
fixes f f' :: "real ⇒ 'a"
fixes A
fixes X :: "real set"
fixes x :: real
defines "A ≡ sum_upto a"
assumes fin: "finite X"
assumes x: "x > 0"
assumes deriv: "⋀z. z ∈ {0..x} - X ⟹ (f has_vector_derivative f' z) (at z)"
assumes cont_f: "continuous_on {0..x} f"
begin
lemma partial_summation_sum_upto_strong:
"((λt. A t * f' t) has_integral (A x * f x - sum_upto (λn. a n * f n) x)) {0..x}"
proof -
have "(∑n∈real -` {0<..x}. a n * f n) = sum_upto (λn. a n * f n) x"
unfolding sum_upto_def by (intro sum.cong refl) auto
thus ?thesis
using partial_summation_strong[OF fin order.refl x deriv cont_f, of a]
by (simp_all add: A_def)
qed
lemma partial_summation_integrable_sum_upto_strong:
"(λt. A t * f' t) integrable_on {0..x}"
and partial_summation_sum_upto_strong':
"sum_upto (λn. a n * f n) x =
A x * f x - integral {0..x} (λt. A t * f' t)"
using partial_summation_sum_upto_strong by (simp_all add: has_integral_iff algebra_simps)
end
end