Theory Transcendental
section ‹Power Series, Transcendental Functions etc.›
theory Transcendental
imports Series Deriv NthRoot
begin
text ‹A theorem about the factcorial function on the reals.›
lemma square_fact_le_2_fact: "fact n * fact n ≤ (fact (2 * n) :: real)"
proof (induct n)
case 0
then show ?case by simp
next
case (Suc n)
have "(fact (Suc n)) * (fact (Suc n)) = of_nat (Suc n) * of_nat (Suc n) * (fact n * fact n :: real)"
by (simp add: field_simps)
also have "… ≤ of_nat (Suc n) * of_nat (Suc n) * fact (2 * n)"
by (rule mult_left_mono [OF Suc]) simp
also have "… ≤ of_nat (Suc (Suc (2 * n))) * of_nat (Suc (2 * n)) * fact (2 * n)"
by (rule mult_right_mono)+ (auto simp: field_simps)
also have "… = fact (2 * Suc n)" by (simp add: field_simps)
finally show ?case .
qed
lemma fact_in_Reals: "fact n ∈ ℝ"
by (induction n) auto
lemma of_real_fact [simp]: "of_real (fact n) = fact n"
by (metis of_nat_fact of_real_of_nat_eq)
lemma pochhammer_of_real: "pochhammer (of_real x) n = of_real (pochhammer x n)"
by (simp add: pochhammer_prod)
lemma norm_fact [simp]: "norm (fact n :: 'a::real_normed_algebra_1) = fact n"
proof -
have "(fact n :: 'a) = of_real (fact n)"
by simp
also have "norm … = fact n"
by (subst norm_of_real) simp
finally show ?thesis .
qed
lemma root_test_convergence:
fixes f :: "nat ⇒ 'a::banach"
assumes f: "(λn. root n (norm (f n))) ⇢ x"
and "x < 1"
shows "summable f"
proof -
have "0 ≤ x"
by (rule LIMSEQ_le[OF tendsto_const f]) (auto intro!: exI[of _ 1])
from ‹x < 1› obtain z where z: "x < z" "z < 1"
by (metis dense)
from f ‹x < z› have "eventually (λn. root n (norm (f n)) < z) sequentially"
by (rule order_tendstoD)
then have "eventually (λn. norm (f n) ≤ z^n) sequentially"
using eventually_ge_at_top
proof eventually_elim
fix n
assume less: "root n (norm (f n)) < z" and n: "1 ≤ n"
from power_strict_mono[OF less, of n] n show "norm (f n) ≤ z ^ n"
by simp
qed
then show "summable f"
unfolding eventually_sequentially
using z ‹0 ≤ x› by (auto intro!: summable_comparison_test[OF _ summable_geometric])
qed
subsection ‹More facts about binomial coefficients›
text ‹
These facts could have been proven before, but having real numbers
makes the proofs a lot easier.
›
lemma central_binomial_odd:
"odd n ⟹ n choose (Suc (n div 2)) = n choose (n div 2)"
proof -
assume "odd n"
hence "Suc (n div 2) ≤ n" by presburger
hence "n choose (Suc (n div 2)) = n choose (n - Suc (n div 2))"
by (rule binomial_symmetric)
also from ‹odd n› have "n - Suc (n div 2) = n div 2" by presburger
finally show ?thesis .
qed
lemma binomial_less_binomial_Suc:
assumes k: "k < n div 2"
shows "n choose k < n choose (Suc k)"
proof -
from k have k': "k ≤ n" "Suc k ≤ n" by simp_all
from k' have "real (n choose k) = fact n / (fact k * fact (n - k))"
by (simp add: binomial_fact)
also from k' have "n - k = Suc (n - Suc k)" by simp
also from k' have "fact … = (real n - real k) * fact (n - Suc k)"
by (subst fact_Suc) (simp_all add: of_nat_diff)
also from k have "fact k = fact (Suc k) / (real k + 1)" by (simp add: field_simps)
also have "fact n / (fact (Suc k) / (real k + 1) * ((real n - real k) * fact (n - Suc k))) =
(n choose (Suc k)) * ((real k + 1) / (real n - real k))"
using k by (simp add: field_split_simps binomial_fact)
also from assms have "(real k + 1) / (real n - real k) < 1" by simp
finally show ?thesis using k by (simp add: mult_less_cancel_left)
qed
lemma binomial_strict_mono:
assumes "k < k'" "2*k' ≤ n"
shows "n choose k < n choose k'"
proof -
from assms have "k ≤ k' - 1" by simp
thus ?thesis
proof (induction rule: inc_induct)
case base
with assms binomial_less_binomial_Suc[of "k' - 1" n]
show ?case by simp
next
case (step k)
from step.prems step.hyps assms have "n choose k < n choose (Suc k)"
by (intro binomial_less_binomial_Suc) simp_all
also have "… < n choose k'" by (rule step.IH)
finally show ?case .
qed
qed
lemma binomial_mono:
assumes "k ≤ k'" "2*k' ≤ n"
shows "n choose k ≤ n choose k'"
using assms binomial_strict_mono[of k k' n] by (cases "k = k'") simp_all
lemma binomial_strict_antimono:
assumes "k < k'" "2 * k ≥ n" "k' ≤ n"
shows "n choose k > n choose k'"
proof -
from assms have "n choose (n - k) > n choose (n - k')"
by (intro binomial_strict_mono) (simp_all add: algebra_simps)
with assms show ?thesis by (simp add: binomial_symmetric [symmetric])
qed
lemma binomial_antimono:
assumes "k ≤ k'" "k ≥ n div 2" "k' ≤ n"
shows "n choose k ≥ n choose k'"
proof (cases "k = k'")
case False
note not_eq = False
show ?thesis
proof (cases "k = n div 2 ∧ odd n")
case False
with assms(2) have "2*k ≥ n" by presburger
with not_eq assms binomial_strict_antimono[of k k' n]
show ?thesis by simp
next
case True
have "n choose k' ≤ n choose (Suc (n div 2))"
proof (cases "k' = Suc (n div 2)")
case False
with assms True not_eq have "Suc (n div 2) < k'" by simp
with assms binomial_strict_antimono[of "Suc (n div 2)" k' n] True
show ?thesis by auto
qed simp_all
also from True have "… = n choose k" by (simp add: central_binomial_odd)
finally show ?thesis .
qed
qed simp_all
lemma binomial_maximum: "n choose k ≤ n choose (n div 2)"
proof -
have "k ≤ n div 2 ⟷ 2*k ≤ n" by linarith
consider "2*k ≤ n" | "2*k ≥ n" "k ≤ n" | "k > n" by linarith
thus ?thesis
proof cases
case 1
thus ?thesis by (intro binomial_mono) linarith+
next
case 2
thus ?thesis by (intro binomial_antimono) simp_all
qed (simp_all add: binomial_eq_0)
qed
lemma binomial_maximum': "(2*n) choose k ≤ (2*n) choose n"
using binomial_maximum[of "2*n"] by simp
lemma central_binomial_lower_bound:
assumes "n > 0"
shows "4^n / (2*real n) ≤ real ((2*n) choose n)"
proof -
from binomial[of 1 1 "2*n"]
have "4 ^ n = (∑k≤2*n. (2*n) choose k)"
by (simp add: power_mult power2_eq_square One_nat_def [symmetric] del: One_nat_def)
also have "{..2*n} = {0<..<2*n} ∪ {0,2*n}" by auto
also have "(∑k∈…. (2*n) choose k) =
(∑k∈{0<..<2*n}. (2*n) choose k) + (∑k∈{0,2*n}. (2*n) choose k)"
by (subst sum.union_disjoint) auto
also have "(∑k∈{0,2*n}. (2*n) choose k) ≤ (∑k≤1. (n choose k)⇧2)"
by (cases n) simp_all
also from assms have "… ≤ (∑k≤n. (n choose k)⇧2)"
by (intro sum_mono2) auto
also have "… = (2*n) choose n" by (rule choose_square_sum)
also have "(∑k∈{0<..<2*n}. (2*n) choose k) ≤ (∑k∈{0<..<2*n}. (2*n) choose n)"
by (intro sum_mono binomial_maximum')
also have "… = card {0<..<2*n} * ((2*n) choose n)" by simp
also have "card {0<..<2*n} ≤ 2*n - 1" by (cases n) simp_all
also have "(2 * n - 1) * (2 * n choose n) + (2 * n choose n) = ((2*n) choose n) * (2*n)"
using assms by (simp add: algebra_simps)
finally have "4 ^ n ≤ (2 * n choose n) * (2 * n)" by simp_all
hence "real (4 ^ n) ≤ real ((2 * n choose n) * (2 * n))"
by (subst of_nat_le_iff)
with assms show ?thesis by (simp add: field_simps)
qed
subsection ‹Properties of Power Series›
lemma powser_zero [simp]: "(∑n. f n * 0 ^ n) = f 0"
for f :: "nat ⇒ 'a::real_normed_algebra_1"
proof -
have "(∑n<1. f n * 0 ^ n) = (∑n. f n * 0 ^ n)"
by (subst suminf_finite[where N="{0}"]) (auto simp: power_0_left)
then show ?thesis by simp
qed
lemma powser_sums_zero: "(λn. a n * 0^n) sums a 0"
for a :: "nat ⇒ 'a::real_normed_div_algebra"
using sums_finite [of "{0}" "λn. a n * 0 ^ n"]
by simp
lemma powser_sums_zero_iff [simp]: "(λn. a n * 0^n) sums x ⟷ a 0 = x"
for a :: "nat ⇒ 'a::real_normed_div_algebra"
using powser_sums_zero sums_unique2 by blast
text ‹
Power series has a circle or radius of convergence: if it sums for ‹x›,
then it sums absolutely for ‹z› with \<^term>‹¦z¦ < ¦x¦›.›
lemma powser_insidea:
fixes x z :: "'a::real_normed_div_algebra"
assumes 1: "summable (λn. f n * x^n)"
and 2: "norm z < norm x"
shows "summable (λn. norm (f n * z ^ n))"
proof -
from 2 have x_neq_0: "x ≠ 0" by clarsimp
from 1 have "(λn. f n * x^n) ⇢ 0"
by (rule summable_LIMSEQ_zero)
then have "convergent (λn. f n * x^n)"
by (rule convergentI)
then have "Cauchy (λn. f n * x^n)"
by (rule convergent_Cauchy)
then have "Bseq (λn. f n * x^n)"
by (rule Cauchy_Bseq)
then obtain K where 3: "0 < K" and 4: "∀n. norm (f n * x^n) ≤ K"
by (auto simp: Bseq_def)
have "∃N. ∀n≥N. norm (norm (f n * z ^ n)) ≤ K * norm (z ^ n) * inverse (norm (x^n))"
proof (intro exI allI impI)
fix n :: nat
assume "0 ≤ n"
have "norm (norm (f n * z ^ n)) * norm (x^n) =
norm (f n * x^n) * norm (z ^ n)"
by (simp add: norm_mult abs_mult)
also have "… ≤ K * norm (z ^ n)"
by (simp only: mult_right_mono 4 norm_ge_zero)
also have "… = K * norm (z ^ n) * (inverse (norm (x^n)) * norm (x^n))"
by (simp add: x_neq_0)
also have "… = K * norm (z ^ n) * inverse (norm (x^n)) * norm (x^n)"
by (simp only: mult.assoc)
finally show "norm (norm (f n * z ^ n)) ≤ K * norm (z ^ n) * inverse (norm (x^n))"
by (simp add: mult_le_cancel_right x_neq_0)
qed
moreover have "summable (λn. K * norm (z ^ n) * inverse (norm (x^n)))"
proof -
from 2 have "norm (norm (z * inverse x)) < 1"
using x_neq_0
by (simp add: norm_mult nonzero_norm_inverse divide_inverse [where 'a=real, symmetric])
then have "summable (λn. norm (z * inverse x) ^ n)"
by (rule summable_geometric)
then have "summable (λn. K * norm (z * inverse x) ^ n)"
by (rule summable_mult)
then show "summable (λn. K * norm (z ^ n) * inverse (norm (x^n)))"
using x_neq_0
by (simp add: norm_mult nonzero_norm_inverse power_mult_distrib
power_inverse norm_power mult.assoc)
qed
ultimately show "summable (λn. norm (f n * z ^ n))"
by (rule summable_comparison_test)
qed
lemma powser_inside:
fixes f :: "nat ⇒ 'a::{real_normed_div_algebra,banach}"
shows
"summable (λn. f n * (x^n)) ⟹ norm z < norm x ⟹
summable (λn. f n * (z ^ n))"
by (rule powser_insidea [THEN summable_norm_cancel])
lemma powser_times_n_limit_0:
fixes x :: "'a::{real_normed_div_algebra,banach}"
assumes "norm x < 1"
shows "(λn. of_nat n * x ^ n) ⇢ 0"
proof -
have "norm x / (1 - norm x) ≥ 0"
using assms by (auto simp: field_split_simps)
moreover obtain N where N: "norm x / (1 - norm x) < of_int N"
using ex_le_of_int by (meson ex_less_of_int)
ultimately have N0: "N>0"
by auto
then have *: "real_of_int (N + 1) * norm x / real_of_int N < 1"
using N assms by (auto simp: field_simps)
have **: "real_of_int N * (norm x * (real_of_nat (Suc n) * norm (x ^ n))) ≤
real_of_nat n * (norm x * ((1 + N) * norm (x ^ n)))" if "N ≤ int n" for n :: nat
proof -
from that have "real_of_int N * real_of_nat (Suc n) ≤ real_of_nat n * real_of_int (1 + N)"
by (simp add: algebra_simps)
then have "(real_of_int N * real_of_nat (Suc n)) * (norm x * norm (x ^ n)) ≤
(real_of_nat n * (1 + N)) * (norm x * norm (x ^ n))"
using N0 mult_mono by fastforce
then show ?thesis
by (simp add: algebra_simps)
qed
show ?thesis using *
by (rule summable_LIMSEQ_zero [OF summable_ratio_test, where N1="nat N"])
(simp add: N0 norm_mult field_simps ** del: of_nat_Suc of_int_add)
qed
corollary lim_n_over_pown:
fixes x :: "'a::{real_normed_field,banach}"
shows "1 < norm x ⟹ ((λn. of_nat n / x^n) ⤏ 0) sequentially"
using powser_times_n_limit_0 [of "inverse x"]
by (simp add: norm_divide field_split_simps)
lemma sum_split_even_odd:
fixes f :: "nat ⇒ real"
shows "(∑i<2 * n. if even i then f i else g i) = (∑i<n. f (2 * i)) + (∑i<n. g (2 * i + 1))"
proof (induct n)
case 0
then show ?case by simp
next
case (Suc n)
have "(∑i<2 * Suc n. if even i then f i else g i) =
(∑i<n. f (2 * i)) + (∑i<n. g (2 * i + 1)) + (f (2 * n) + g (2 * n + 1))"
using Suc.hyps unfolding One_nat_def by auto
also have "… = (∑i<Suc n. f (2 * i)) + (∑i<Suc n. g (2 * i + 1))"
by auto
finally show ?case .
qed
lemma sums_if':
fixes g :: "nat ⇒ real"
assumes "g sums x"
shows "(λ n. if even n then 0 else g ((n - 1) div 2)) sums x"
unfolding sums_def
proof (rule LIMSEQ_I)
fix r :: real
assume "0 < r"
from ‹g sums x›[unfolded sums_def, THEN LIMSEQ_D, OF this]
obtain no where no_eq: "⋀n. n ≥ no ⟹ (norm (sum g {..<n} - x) < r)"
by blast
let ?SUM = "λ m. ∑i<m. if even i then 0 else g ((i - 1) div 2)"
have "(norm (?SUM m - x) < r)" if "m ≥ 2 * no" for m
proof -
from that have "m div 2 ≥ no" by auto
have sum_eq: "?SUM (2 * (m div 2)) = sum g {..< m div 2}"
using sum_split_even_odd by auto
then have "(norm (?SUM (2 * (m div 2)) - x) < r)"
using no_eq unfolding sum_eq using ‹m div 2 ≥ no› by auto
moreover
have "?SUM (2 * (m div 2)) = ?SUM m"
proof (cases "even m")
case True
then show ?thesis
by (auto simp: even_two_times_div_two)
next
case False
then have eq: "Suc (2 * (m div 2)) = m" by simp
then have "even (2 * (m div 2))" using ‹odd m› by auto
have "?SUM m = ?SUM (Suc (2 * (m div 2)))" unfolding eq ..
also have "… = ?SUM (2 * (m div 2))" using ‹even (2 * (m div 2))› by auto
finally show ?thesis by auto
qed
ultimately show ?thesis by auto
qed
then show "∃no. ∀ m ≥ no. norm (?SUM m - x) < r"
by blast
qed
lemma sums_if:
fixes g :: "nat ⇒ real"
assumes "g sums x" and "f sums y"
shows "(λ n. if even n then f (n div 2) else g ((n - 1) div 2)) sums (x + y)"
proof -
let ?s = "λ n. if even n then 0 else f ((n - 1) div 2)"
have if_sum: "(if B then (0 :: real) else E) + (if B then T else 0) = (if B then T else E)"
for B T E
by (cases B) auto
have g_sums: "(λ n. if even n then 0 else g ((n - 1) div 2)) sums x"
using sums_if'[OF ‹g sums x›] .
have if_eq: "⋀B T E. (if ¬ B then T else E) = (if B then E else T)"
by auto
have "?s sums y" using sums_if'[OF ‹f sums y›] .
from this[unfolded sums_def, THEN LIMSEQ_Suc]
have "(λn. if even n then f (n div 2) else 0) sums y"
by (simp add: lessThan_Suc_eq_insert_0 sum.atLeast1_atMost_eq image_Suc_lessThan
if_eq sums_def cong del: if_weak_cong)
from sums_add[OF g_sums this] show ?thesis
by (simp only: if_sum)
qed
subsection ‹Alternating series test / Leibniz formula›
lemma sums_alternating_upper_lower:
fixes a :: "nat ⇒ real"
assumes mono: "⋀n. a (Suc n) ≤ a n"
and a_pos: "⋀n. 0 ≤ a n"
and "a ⇢ 0"
shows "∃l. ((∀n. (∑i<2*n. (- 1)^i*a i) ≤ l) ∧ (λ n. ∑i<2*n. (- 1)^i*a i) ⇢ l) ∧
((∀n. l ≤ (∑i<2*n + 1. (- 1)^i*a i)) ∧ (λ n. ∑i<2*n + 1. (- 1)^i*a i) ⇢ l)"
(is "∃l. ((∀n. ?f n ≤ l) ∧ _) ∧ ((∀n. l ≤ ?g n) ∧ _)")
proof (rule nested_sequence_unique)
have fg_diff: "⋀n. ?f n - ?g n = - a (2 * n)" by auto
show "∀n. ?f n ≤ ?f (Suc n)"
proof
show "?f n ≤ ?f (Suc n)" for n
using mono[of "2*n"] by auto
qed
show "∀n. ?g (Suc n) ≤ ?g n"
proof
show "?g (Suc n) ≤ ?g n" for n
using mono[of "Suc (2*n)"] by auto
qed
show "∀n. ?f n ≤ ?g n"
proof
show "?f n ≤ ?g n" for n
using fg_diff a_pos by auto
qed
show "(λn. ?f n - ?g n) ⇢ 0"
unfolding fg_diff
proof (rule LIMSEQ_I)
fix r :: real
assume "0 < r"
with ‹a ⇢ 0›[THEN LIMSEQ_D] obtain N where "⋀ n. n ≥ N ⟹ norm (a n - 0) < r"
by auto
then have "∀n ≥ N. norm (- a (2 * n) - 0) < r"
by auto
then show "∃N. ∀n ≥ N. norm (- a (2 * n) - 0) < r"
by auto
qed
qed
lemma summable_Leibniz':
fixes a :: "nat ⇒ real"
assumes a_zero: "a ⇢ 0"
and a_pos: "⋀n. 0 ≤ a n"
and a_monotone: "⋀n. a (Suc n) ≤ a n"
shows summable: "summable (λ n. (-1)^n * a n)"
and "⋀n. (∑i<2*n. (-1)^i*a i) ≤ (∑i. (-1)^i*a i)"
and "(λn. ∑i<2*n. (-1)^i*a i) ⇢ (∑i. (-1)^i*a i)"
and "⋀n. (∑i. (-1)^i*a i) ≤ (∑i<2*n+1. (-1)^i*a i)"
and "(λn. ∑i<2*n+1. (-1)^i*a i) ⇢ (∑i. (-1)^i*a i)"
proof -
let ?S = "λn. (-1)^n * a n"
let ?P = "λn. ∑i<n. ?S i"
let ?f = "λn. ?P (2 * n)"
let ?g = "λn. ?P (2 * n + 1)"
obtain l :: real
where below_l: "∀ n. ?f n ≤ l"
and "?f ⇢ l"
and above_l: "∀ n. l ≤ ?g n"
and "?g ⇢ l"
using sums_alternating_upper_lower[OF a_monotone a_pos a_zero] by blast
let ?Sa = "λm. ∑n<m. ?S n"
have "?Sa ⇢ l"
proof (rule LIMSEQ_I)
fix r :: real
assume "0 < r"
with ‹?f ⇢ l›[THEN LIMSEQ_D]
obtain f_no where f: "⋀n. n ≥ f_no ⟹ norm (?f n - l) < r"
by auto
from ‹0 < r› ‹?g ⇢ l›[THEN LIMSEQ_D]
obtain g_no where g: "⋀n. n ≥ g_no ⟹ norm (?g n - l) < r"
by auto
have "norm (?Sa n - l) < r" if "n ≥ (max (2 * f_no) (2 * g_no))" for n
proof -
from that have "n ≥ 2 * f_no" and "n ≥ 2 * g_no" by auto
show ?thesis
proof (cases "even n")
case True
then have n_eq: "2 * (n div 2) = n"
by (simp add: even_two_times_div_two)
with ‹n ≥ 2 * f_no› have "n div 2 ≥ f_no"
by auto
from f[OF this] show ?thesis
unfolding n_eq atLeastLessThanSuc_atLeastAtMost .
next
case False
then have "even (n - 1)" by simp
then have n_eq: "2 * ((n - 1) div 2) = n - 1"
by (simp add: even_two_times_div_two)
then have range_eq: "n - 1 + 1 = n"
using odd_pos[OF False] by auto
from n_eq ‹n ≥ 2 * g_no› have "(n - 1) div 2 ≥ g_no"
by auto
from g[OF this] show ?thesis
by (simp only: n_eq range_eq)
qed
qed
then show "∃no. ∀n ≥ no. norm (?Sa n - l) < r" by blast
qed
then have sums_l: "(λi. (-1)^i * a i) sums l"
by (simp only: sums_def)
then show "summable ?S"
by (auto simp: summable_def)
have "l = suminf ?S" by (rule sums_unique[OF sums_l])
fix n
show "suminf ?S ≤ ?g n"
unfolding sums_unique[OF sums_l, symmetric] using above_l by auto
show "?f n ≤ suminf ?S"
unfolding sums_unique[OF sums_l, symmetric] using below_l by auto
show "?g ⇢ suminf ?S"
using ‹?g ⇢ l› ‹l = suminf ?S› by auto
show "?f ⇢ suminf ?S"
using ‹?f ⇢ l› ‹l = suminf ?S› by auto
qed
theorem summable_Leibniz:
fixes a :: "nat ⇒ real"
assumes a_zero: "a ⇢ 0"
and "monoseq a"
shows "summable (λ n. (-1)^n * a n)" (is "?summable")
and "0 < a 0 ⟶
(∀n. (∑i. (- 1)^i*a i) ∈ { ∑i<2*n. (- 1)^i * a i .. ∑i<2*n+1. (- 1)^i * a i})" (is "?pos")
and "a 0 < 0 ⟶
(∀n. (∑i. (- 1)^i*a i) ∈ { ∑i<2*n+1. (- 1)^i * a i .. ∑i<2*n. (- 1)^i * a i})" (is "?neg")
and "(λn. ∑i<2*n. (- 1)^i*a i) ⇢ (∑i. (- 1)^i*a i)" (is "?f")
and "(λn. ∑i<2*n+1. (- 1)^i*a i) ⇢ (∑i. (- 1)^i*a i)" (is "?g")
proof -
have "?summable ∧ ?pos ∧ ?neg ∧ ?f ∧ ?g"
proof (cases "(∀n. 0 ≤ a n) ∧ (∀m. ∀n≥m. a n ≤ a m)")
case True
then have ord: "⋀n m. m ≤ n ⟹ a n ≤ a m"
and ge0: "⋀n. 0 ≤ a n"
by auto
have mono: "a (Suc n) ≤ a n" for n
using ord[where n="Suc n" and m=n] by auto
note leibniz = summable_Leibniz'[OF ‹a ⇢ 0› ge0]
from leibniz[OF mono]
show ?thesis using ‹0 ≤ a 0› by auto
next
let ?a = "λn. - a n"
case False
with monoseq_le[OF ‹monoseq a› ‹a ⇢ 0›]
have "(∀ n. a n ≤ 0) ∧ (∀m. ∀n≥m. a m ≤ a n)" by auto
then have ord: "⋀n m. m ≤ n ⟹ ?a n ≤ ?a m" and ge0: "⋀ n. 0 ≤ ?a n"
by auto
have monotone: "?a (Suc n) ≤ ?a n" for n
using ord[where n="Suc n" and m=n] by auto
note leibniz =
summable_Leibniz'[OF _ ge0, of "λx. x",
OF tendsto_minus[OF ‹a ⇢ 0›, unfolded minus_zero] monotone]
have "summable (λ n. (-1)^n * ?a n)"
using leibniz(1) by auto
then obtain l where "(λ n. (-1)^n * ?a n) sums l"
unfolding summable_def by auto
from this[THEN sums_minus] have "(λ n. (-1)^n * a n) sums -l"
by auto
then have ?summable by (auto simp: summable_def)
moreover
have "¦- a - - b¦ = ¦a - b¦" for a b :: real
unfolding minus_diff_minus by auto
from suminf_minus[OF leibniz(1), unfolded mult_minus_right minus_minus]
have move_minus: "(∑n. - ((- 1) ^ n * a n)) = - (∑n. (- 1) ^ n * a n)"
by auto
have ?pos using ‹0 ≤ ?a 0› by auto
moreover have ?neg
using leibniz(2,4)
unfolding mult_minus_right sum_negf move_minus neg_le_iff_le
by auto
moreover have ?f and ?g
using leibniz(3,5)[unfolded mult_minus_right sum_negf move_minus, THEN tendsto_minus_cancel]
by auto
ultimately show ?thesis by auto
qed
then show ?summable and ?pos and ?neg and ?f and ?g
by safe
qed
subsection ‹Term-by-Term Differentiability of Power Series›
definition diffs :: "(nat ⇒ 'a::ring_1) ⇒ nat ⇒ 'a"
where "diffs c = (λn. of_nat (Suc n) * c (Suc n))"
text ‹Lemma about distributing negation over it.›
lemma diffs_minus: "diffs (λn. - c n) = (λn. - diffs c n)"
by (simp add: diffs_def)
lemma diffs_equiv:
fixes x :: "'a::{real_normed_vector,ring_1}"
shows "summable (λn. diffs c n * x^n) ⟹
(λn. of_nat n * c n * x^(n - Suc 0)) sums (∑n. diffs c n * x^n)"
unfolding diffs_def
by (simp add: summable_sums sums_Suc_imp)
lemma lemma_termdiff1:
fixes z :: "'a :: {monoid_mult,comm_ring}"
shows "(∑p<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =
(∑p<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))"
by (auto simp: algebra_simps power_add [symmetric])
lemma sumr_diff_mult_const2: "sum f {..<n} - of_nat n * r = (∑i<n. f i - r)"
for r :: "'a::ring_1"
by (simp add: sum_subtractf)
lemma lemma_termdiff2:
fixes h :: "'a::field"
assumes h: "h ≠ 0"
shows "((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0) =
h * (∑p< n - Suc 0. ∑q< n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q))"
(is "?lhs = ?rhs")
proof (cases n)
case (Suc m)
have 0: "⋀x k. (∑n<Suc k. h * (z ^ x * (z ^ (k - n) * (h + z) ^ n))) =
(∑j<Suc k. h * ((h + z) ^ j * z ^ (x + k - j)))"
by (auto simp add: power_add [symmetric] mult.commute intro: sum.cong)
have *: "(∑i<m. z ^ i * ((z + h) ^ (m - i) - z ^ (m - i))) =
(∑i<m. ∑j<m - i. h * ((z + h) ^ j * z ^ (m - Suc j)))"
by (force simp add: less_iff_Suc_add sum_distrib_left diff_power_eq_sum ac_simps 0
simp del: sum.lessThan_Suc power_Suc intro: sum.cong)
have "h * ?lhs = (z + h) ^ n - z ^ n - h * of_nat n * z ^ (n - Suc 0)"
by (simp add: right_diff_distrib diff_divide_distrib h mult.assoc [symmetric])
also have "... = h * ((∑p<Suc m. (z + h) ^ p * z ^ (m - p)) - of_nat (Suc m) * z ^ m)"
by (simp add: Suc diff_power_eq_sum h right_diff_distrib [symmetric] mult.assoc
del: power_Suc sum.lessThan_Suc of_nat_Suc)
also have "... = h * ((∑p<Suc m. (z + h) ^ (m - p) * z ^ p) - of_nat (Suc m) * z ^ m)"
by (subst sum.nat_diff_reindex[symmetric]) simp
also have "... = h * (∑i<Suc m. (z + h) ^ (m - i) * z ^ i - z ^ m)"
by (simp add: sum_subtractf)
also have "... = h * ?rhs"
by (simp add: lemma_termdiff1 sum_distrib_left Suc *)
finally have "h * ?lhs = h * ?rhs" .
then show ?thesis
by (simp add: h)
qed auto
lemma real_sum_nat_ivl_bounded2:
fixes K :: "'a::linordered_semidom"
assumes f: "⋀p::nat. p < n ⟹ f p ≤ K" and K: "0 ≤ K"
shows "sum f {..<n-k} ≤ of_nat n * K"
proof -
have "sum f {..<n-k} ≤ (∑i<n - k. K)"
by (rule sum_mono [OF f]) auto
also have "... ≤ of_nat n * K"
by (auto simp: mult_right_mono K)
finally show ?thesis .
qed
lemma lemma_termdiff3:
fixes h z :: "'a::real_normed_field"
assumes 1: "h ≠ 0"
and 2: "norm z ≤ K"
and 3: "norm (z + h) ≤ K"
shows "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0)) ≤
of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h"
proof -
have "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0)) =
norm (∑p<n - Suc 0. ∑q<n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q)) * norm h"
by (metis (lifting, no_types) lemma_termdiff2 [OF 1] mult.commute norm_mult)
also have "… ≤ of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2)) * norm h"
proof (rule mult_right_mono [OF _ norm_ge_zero])
from norm_ge_zero 2 have K: "0 ≤ K"
by (rule order_trans)
have le_Kn: "norm ((z + h) ^ i * z ^ j) ≤ K ^ n" if "i + j = n" for i j n
proof -
have "norm (z + h) ^ i * norm z ^ j ≤ K ^ i * K ^ j"
by (intro mult_mono power_mono 2 3 norm_ge_zero zero_le_power K)
also have "... = K^n"
by (metis power_add that)
finally show ?thesis
by (simp add: norm_mult norm_power)
qed
then have "⋀p q.
⟦p < n; q < n - Suc 0⟧ ⟹ norm ((z + h) ^ q * z ^ (n - 2 - q)) ≤ K ^ (n - 2)"
by (simp del: subst_all)
then
show "norm (∑p<n - Suc 0. ∑q<n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q)) ≤
of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2))"
by (intro order_trans [OF norm_sum]
real_sum_nat_ivl_bounded2 mult_nonneg_nonneg of_nat_0_le_iff zero_le_power K)
qed
also have "… = of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h"
by (simp only: mult.assoc)
finally show ?thesis .
qed
lemma lemma_termdiff4:
fixes f :: "'a::real_normed_vector ⇒ 'b::real_normed_vector"
and k :: real
assumes k: "0 < k"
and le: "⋀h. h ≠ 0 ⟹ norm h < k ⟹ norm (f h) ≤ K * norm h"
shows "f ─0→ 0"
proof (rule tendsto_norm_zero_cancel)
show "(λh. norm (f h)) ─0→ 0"
proof (rule real_tendsto_sandwich)
show "eventually (λh. 0 ≤ norm (f h)) (at 0)"
by simp
show "eventually (λh. norm (f h) ≤ K * norm h) (at 0)"
using k by (auto simp: eventually_at dist_norm le)
show "(λh. 0) ─(0::'a)→ (0::real)"
by (rule tendsto_const)
have "(λh. K * norm h) ─(0::'a)→ K * norm (0::'a)"
by (intro tendsto_intros)
then show "(λh. K * norm h) ─(0::'a)→ 0"
by simp
qed
qed
lemma lemma_termdiff5:
fixes g :: "'a::real_normed_vector ⇒ nat ⇒ 'b::banach"
and k :: real
assumes k: "0 < k"
and f: "summable f"
and le: "⋀h n. h ≠ 0 ⟹ norm h < k ⟹ norm (g h n) ≤ f n * norm h"
shows "(λh. suminf (g h)) ─0→ 0"
proof (rule lemma_termdiff4 [OF k])
fix h :: 'a
assume "h ≠ 0" and "norm h < k"
then have 1: "∀n. norm (g h n) ≤ f n * norm h"
by (simp add: le)
then have "∃N. ∀n≥N. norm (norm (g h n)) ≤ f n * norm h"
by simp
moreover from f have 2: "summable (λn. f n * norm h)"
by (rule summable_mult2)
ultimately have 3: "summable (λn. norm (g h n))"
by (rule summable_comparison_test)
then have "norm (suminf (g h)) ≤ (∑n. norm (g h n))"
by (rule summable_norm)
also from 1 3 2 have "(∑n. norm (g h n)) ≤ (∑n. f n * norm h)"
by (simp add: suminf_le)
also from f have "(∑n. f n * norm h) = suminf f * norm h"
by (rule suminf_mult2 [symmetric])
finally show "norm (suminf (g h)) ≤ suminf f * norm h" .
qed
lemma termdiffs_aux:
fixes x :: "'a::{real_normed_field,banach}"
assumes 1: "summable (λn. diffs (diffs c) n * K ^ n)"
and 2: "norm x < norm K"
shows "(λh. ∑n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) ─0→ 0"
proof -
from dense [OF 2] obtain r where r1: "norm x < r" and r2: "r < norm K"
by fast
from norm_ge_zero r1 have r: "0 < r"
by (rule order_le_less_trans)
then have r_neq_0: "r ≠ 0" by simp
show ?thesis
proof (rule lemma_termdiff5)
show "0 < r - norm x"
using r1 by simp
from r r2 have "norm (of_real r::'a) < norm K"
by simp
with 1 have "summable (λn. norm (diffs (diffs c) n * (of_real r ^ n)))"
by (rule powser_insidea)
then have "summable (λn. diffs (diffs (λn. norm (c n))) n * r ^ n)"
using r by (simp add: diffs_def norm_mult norm_power del: of_nat_Suc)
then have "summable (λn. of_nat n * diffs (λn. norm (c n)) n * r ^ (n - Suc 0))"
by (rule diffs_equiv [THEN sums_summable])
also have "(λn. of_nat n * diffs (λn. norm (c n)) n * r ^ (n - Suc 0)) =
(λn. diffs (λm. of_nat (m - Suc 0) * norm (c m) * inverse r) n * (r ^ n))"
by (simp add: diffs_def r_neq_0 fun_eq_iff split: nat_diff_split)
finally have "summable
(λn. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0))"
by (rule diffs_equiv [THEN sums_summable])
also have
"(λn. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0)) =
(λn. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))"
by (rule ext) (simp add: r_neq_0 split: nat_diff_split)
finally show "summable (λn. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))" .
next
fix h :: 'a and n
assume h: "h ≠ 0"
assume "norm h < r - norm x"
then have "norm x + norm h < r" by simp
with norm_triangle_ineq
have xh: "norm (x + h) < r"
by (rule order_le_less_trans)
have "norm (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0))
≤ real n * (real (n - Suc 0) * (r ^ (n - 2) * norm h))"
by (metis (mono_tags, lifting) h mult.assoc lemma_termdiff3 less_eq_real_def r1 xh)
then show "norm (c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) ≤
norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2) * norm h"
by (simp only: norm_mult mult.assoc mult_left_mono [OF _ norm_ge_zero])
qed
qed
lemma termdiffs:
fixes K x :: "'a::{real_normed_field,banach}"
assumes 1: "summable (λn. c n * K ^ n)"
and 2: "summable (λn. (diffs c) n * K ^ n)"
and 3: "summable (λn. (diffs (diffs c)) n * K ^ n)"
and 4: "norm x < norm K"
shows "DERIV (λx. ∑n. c n * x^n) x :> (∑n. (diffs c) n * x^n)"
unfolding DERIV_def
proof (rule LIM_zero_cancel)
show "(λh. (suminf (λn. c n * (x + h) ^ n) - suminf (λn. c n * x^n)) / h
- suminf (λn. diffs c n * x^n)) ─0→ 0"
proof (rule LIM_equal2)
show "0 < norm K - norm x"
using 4 by (simp add: less_diff_eq)
next
fix h :: 'a
assume "norm (h - 0) < norm K - norm x"
then have "norm x + norm h < norm K" by simp
then have 5: "norm (x + h) < norm K"
by (rule norm_triangle_ineq [THEN order_le_less_trans])
have "summable (λn. c n * x^n)"
and "summable (λn. c n * (x + h) ^ n)"
and "summable (λn. diffs c n * x^n)"
using 1 2 4 5 by (auto elim: powser_inside)
then have "((∑n. c n * (x + h) ^ n) - (∑n. c n * x^n)) / h - (∑n. diffs c n * x^n) =
(∑n. (c n * (x + h) ^ n - c n * x^n) / h - of_nat n * c n * x ^ (n - Suc 0))"
by (intro sums_unique sums_diff sums_divide diffs_equiv summable_sums)
then show "((∑n. c n * (x + h) ^ n) - (∑n. c n * x^n)) / h - (∑n. diffs c n * x^n) =
(∑n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0)))"
by (simp add: algebra_simps)
next
show "(λh. ∑n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) ─0→ 0"
by (rule termdiffs_aux [OF 3 4])
qed
qed
subsection ‹The Derivative of a Power Series Has the Same Radius of Convergence›
lemma termdiff_converges:
fixes x :: "'a::{real_normed_field,banach}"
assumes K: "norm x < K"
and sm: "⋀x. norm x < K ⟹ summable(λn. c n * x ^ n)"
shows "summable (λn. diffs c n * x ^ n)"
proof (cases "x = 0")
case True
then show ?thesis
using powser_sums_zero sums_summable by auto
next
case False
then have "K > 0"
using K less_trans zero_less_norm_iff by blast
then obtain r :: real where r: "norm x < norm r" "norm r < K" "r > 0"
using K False
by (auto simp: field_simps abs_less_iff add_pos_pos intro: that [of "(norm x + K) / 2"])
have to0: "(λn. of_nat n * (x / of_real r) ^ n) ⇢ 0"
using r by (simp add: norm_divide powser_times_n_limit_0 [of "x / of_real r"])
obtain N where N: "⋀n. n≥N ⟹ real_of_nat n * norm x ^ n < r ^ n"
using r LIMSEQ_D [OF to0, of 1]
by (auto simp: norm_divide norm_mult norm_power field_simps)
have "summable (λn. (of_nat n * c n) * x ^ n)"
proof (rule summable_comparison_test')
show "summable (λn. norm (c n * of_real r ^ n))"
apply (rule powser_insidea [OF sm [of "of_real ((r+K)/2)"]])
using N r norm_of_real [of "r + K", where 'a = 'a] by auto
show "⋀n. N ≤ n ⟹ norm (of_nat n * c n * x ^ n) ≤ norm (c n * of_real r ^ n)"
using N r by (fastforce simp add: norm_mult norm_power less_eq_real_def)
qed
then have "summable (λn. (of_nat (Suc n) * c(Suc n)) * x ^ Suc n)"
using summable_iff_shift [of "λn. of_nat n * c n * x ^ n" 1]
by simp
then have "summable (λn. (of_nat (Suc n) * c(Suc n)) * x ^ n)"
using False summable_mult2 [of "λn. (of_nat (Suc n) * c(Suc n) * x ^ n) * x" "inverse x"]
by (simp add: mult.assoc) (auto simp: ac_simps)
then show ?thesis
by (simp add: diffs_def)
qed
lemma termdiff_converges_all:
fixes x :: "'a::{real_normed_field,banach}"
assumes "⋀x. summable (λn. c n * x^n)"
shows "summable (λn. diffs c n * x^n)"
by (rule termdiff_converges [where K = "1 + norm x"]) (use assms in auto)
lemma termdiffs_strong:
fixes K x :: "'a::{real_normed_field,banach}"
assumes sm: "summable (λn. c n * K ^ n)"
and K: "norm x < norm K"
shows "DERIV (λx. ∑n. c n * x^n) x :> (∑n. diffs c n * x^n)"
proof -
have "norm K + norm x < norm K + norm K"
using K by force
then have K2: "norm ((of_real (norm K) + of_real (norm x)) / 2 :: 'a) < norm K"
by (auto simp: norm_triangle_lt norm_divide field_simps)
then have [simp]: "norm ((of_real (norm K) + of_real (norm x)) :: 'a) < norm K * 2"
by simp
have "summable (λn. c n * (of_real (norm x + norm K) / 2) ^ n)"
by (metis K2 summable_norm_cancel [OF powser_insidea [OF sm]] add.commute of_real_add)
moreover have "⋀x. norm x < norm K ⟹ summable (λn. diffs c n * x ^ n)"
by (blast intro: sm termdiff_converges powser_inside)
moreover have "⋀x. norm x < norm K ⟹ summable (λn. diffs(diffs c) n * x ^ n)"
by (blast intro: sm termdiff_converges powser_inside)
ultimately show ?thesis
by (rule termdiffs [where K = "of_real (norm x + norm K) / 2"])
(use K in ‹auto simp: field_simps simp flip: of_real_add›)
qed
lemma termdiffs_strong_converges_everywhere:
fixes K x :: "'a::{real_normed_field,banach}"
assumes "⋀y. summable (λn. c n * y ^ n)"
shows "((λx. ∑n. c n * x^n) has_field_derivative (∑n. diffs c n * x^n)) (at x)"
using termdiffs_strong[OF assms[of "of_real (norm x + 1)"], of x]
by (force simp del: of_real_add)
lemma termdiffs_strong':
fixes z :: "'a :: {real_normed_field,banach}"
assumes "⋀z. norm z < K ⟹ summable (λn. c n * z ^ n)"
assumes "norm z < K"
shows "((λz. ∑n. c n * z^n) has_field_derivative (∑n. diffs c n * z^n)) (at z)"
proof (rule termdiffs_strong)
define L :: real where "L = (norm z + K) / 2"
have "0 ≤ norm z" by simp
also note ‹norm z < K›
finally have K: "K ≥ 0" by simp
from assms K have L: "L ≥ 0" "norm z < L" "L < K" by (simp_all add: L_def)
from L show "norm z < norm (of_real L :: 'a)" by simp
from L show "summable (λn. c n * of_real L ^ n)" by (intro assms(1)) simp_all
qed
lemma termdiffs_sums_strong:
fixes z :: "'a :: {banach,real_normed_field}"
assumes sums: "⋀z. norm z < K ⟹ (λn. c n * z ^ n) sums f z"
assumes deriv: "(f has_field_derivative f') (at z)"
assumes norm: "norm z < K"
shows "(λn. diffs c n * z ^ n) sums f'"
proof -
have summable: "summable (λn. diffs c n * z^n)"
by (intro termdiff_converges[OF norm] sums_summable[OF sums])
from norm have "eventually (λz. z ∈ norm -` {..<K}) (nhds z)"
by (intro eventually_nhds_in_open open_vimage)
(simp_all add: continuous_on_norm)
hence eq: "eventually (λz. (∑n. c n * z^n) = f z) (nhds z)"
by eventually_elim (insert sums, simp add: sums_iff)
have "((λz. ∑n. c n * z^n) has_field_derivative (∑n. diffs c n * z^n)) (at z)"
by (intro termdiffs_strong'[OF _ norm] sums_summable[OF sums])
hence "(f has_field_derivative (∑n. diffs c n * z^n)) (at z)"
by (subst (asm) DERIV_cong_ev[OF refl eq refl])
from this and deriv have "(∑n. diffs c n * z^n) = f'" by (rule DERIV_unique)
with summable show ?thesis by (simp add: sums_iff)
qed
lemma isCont_powser:
fixes K x :: "'a::{real_normed_field,banach}"
assumes "summable (λn. c n * K ^ n)"
assumes "norm x < norm K"
shows "isCont (λx. ∑n. c n * x^n) x"
using termdiffs_strong[OF assms] by (blast intro!: DERIV_isCont)
lemmas isCont_powser' = isCont_o2[OF _ isCont_powser]
lemma isCont_powser_converges_everywhere:
fixes K x :: "'a::{real_normed_field,banach}"
assumes "⋀y. summable (λn. c n * y ^ n)"
shows "isCont (λx. ∑n. c n * x^n) x"
using termdiffs_strong[OF assms[of "of_real (norm x + 1)"], of x]
by (force intro!: DERIV_isCont simp del: of_real_add)
lemma powser_limit_0:
fixes a :: "nat ⇒ 'a::{real_normed_field,banach}"
assumes s: "0 < s"
and sm: "⋀x. norm x < s ⟹ (λn. a n * x ^ n) sums (f x)"
shows "(f ⤏ a 0) (at 0)"
proof -
have "norm (of_real s / 2 :: 'a) < s"
using s by (auto simp: norm_divide)
then have "summable (λn. a n * (of_real s / 2) ^ n)"
by (rule sums_summable [OF sm])
then have "((λx. ∑n. a n * x ^ n) has_field_derivative (∑n. diffs a n * 0 ^ n)) (at 0)"
by (rule termdiffs_strong) (use s in ‹auto simp: norm_divide›)
then have "isCont (λx. ∑n. a n * x ^ n) 0"
by (blast intro: DERIV_continuous)
then have "((λx. ∑n. a n * x ^ n) ⤏ a 0) (at 0)"
by (simp add: continuous_within)
moreover have "(λx. f x - (∑n. a n * x ^ n)) ─0→ 0"
apply (clarsimp simp: LIM_eq)
apply (rule_tac x=s in exI)
using s sm sums_unique by fastforce
ultimately show ?thesis
by (rule Lim_transform)
qed
lemma powser_limit_0_strong:
fixes a :: "nat ⇒ 'a::{real_normed_field,banach}"
assumes s: "0 < s"
and sm: "⋀x. x ≠ 0 ⟹ norm x < s ⟹ (λn. a n * x ^ n) sums (f x)"
shows "(f ⤏ a 0) (at 0)"
proof -
have *: "((λx. if x = 0 then a 0 else f x) ⤏ a 0) (at 0)"
by (rule powser_limit_0 [OF s]) (auto simp: powser_sums_zero sm)
show ?thesis
using "*" by (auto cong: Lim_cong_within)
qed
subsection ‹Derivability of power series›
lemma DERIV_series':
fixes f :: "real ⇒ nat ⇒ real"
assumes DERIV_f: "⋀ n. DERIV (λ x. f x n) x0 :> (f' x0 n)"
and allf_summable: "⋀ x. x ∈ {a <..< b} ⟹ summable (f x)"
and x0_in_I: "x0 ∈ {a <..< b}"
and "summable (f' x0)"
and "summable L"
and L_def: "⋀n x y. x ∈ {a <..< b} ⟹ y ∈ {a <..< b} ⟹ ¦f x n - f y n¦ ≤ L n * ¦x - y¦"
shows "DERIV (λ x. suminf (f x)) x0 :> (suminf (f' x0))"
unfolding DERIV_def
proof (rule LIM_I)
fix r :: real
assume "0 < r" then have "0 < r/3" by auto
obtain N_L where N_L: "⋀ n. N_L ≤ n ⟹ ¦ ∑ i. L (i + n) ¦ < r/3"
using suminf_exist_split[OF ‹0 < r/3› ‹summable L›] by auto
obtain N_f' where N_f': "⋀ n. N_f' ≤ n ⟹ ¦ ∑ i. f' x0 (i + n) ¦ < r/3"
using suminf_exist_split[OF ‹0 < r/3› ‹summable (f' x0)›] by auto
let ?N = "Suc (max N_L N_f')"
have "¦ ∑ i. f' x0 (i + ?N) ¦ < r/3" (is "?f'_part < r/3")
and L_estimate: "¦ ∑ i. L (i + ?N) ¦ < r/3"
using N_L[of "?N"] and N_f' [of "?N"] by auto
let ?diff = "λi x. (f (x0 + x) i - f x0 i) / x"
let ?r = "r / (3 * real ?N)"
from ‹0 < r› have "0 < ?r" by simp
let ?s = "λn. SOME s. 0 < s ∧ (∀ x. x ≠ 0 ∧ ¦ x ¦ < s ⟶ ¦ ?diff n x - f' x0 n ¦ < ?r)"
define S' where "S' = Min (?s ` {..< ?N })"
have "0 < S'"
unfolding S'_def
proof (rule iffD2[OF Min_gr_iff])
show "∀x ∈ (?s ` {..< ?N }). 0 < x"
proof
fix x
assume "x ∈ ?s ` {..<?N}"
then obtain n where "x = ?s n" and "n ∈ {..<?N}"
using image_iff[THEN iffD1] by blast
from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF ‹0 < ?r›, unfolded real_norm_def]
obtain s where s_bound: "0 < s ∧ (∀x. x ≠ 0 ∧ ¦x¦ < s ⟶ ¦?diff n x - f' x0 n¦ < ?r)"
by auto
have "0 < ?s n"
by (rule someI2[where a=s]) (auto simp: s_bound simp del: of_nat_Suc)
then show "0 < x" by (simp only: ‹x = ?s n›)
qed
qed auto
define S where "S = min (min (x0 - a) (b - x0)) S'"
then have "0 < S" and S_a: "S ≤ x0 - a" and S_b: "S ≤ b - x0"
and "S ≤ S'" using x0_in_I and ‹0 < S'›
by auto
have "¦(suminf (f (x0 + x)) - suminf (f x0)) / x - suminf (f' x0)¦ < r"
if "x ≠ 0" and "¦x¦ < S" for x
proof -
from that have x_in_I: "x0 + x ∈ {a <..< b}"
using S_a S_b by auto
note diff_smbl = summable_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]]
note div_smbl = summable_divide[OF diff_smbl]
note all_smbl = summable_diff[OF div_smbl ‹summable (f' x0)›]
note ign = summable_ignore_initial_segment[where k="?N"]
note diff_shft_smbl = summable_diff[OF ign[OF allf_summable[OF x_in_I]] ign[OF allf_summable[OF x0_in_I]]]
note div_shft_smbl = summable_divide[OF diff_shft_smbl]
note all_shft_smbl = summable_diff[OF div_smbl ign[OF ‹summable (f' x0)›]]
have 1: "¦(¦?diff (n + ?N) x¦)¦ ≤ L (n + ?N)" for n
proof -
have "¦?diff (n + ?N) x¦ ≤ L (n + ?N) * ¦(x0 + x) - x0¦ / ¦x¦"
using divide_right_mono[OF L_def[OF x_in_I x0_in_I] abs_ge_zero]
by (simp only: abs_divide)
with ‹x ≠ 0› show ?thesis by auto
qed
note 2 = summable_rabs_comparison_test[OF _ ign[OF ‹summable L›]]
from 1 have "¦ ∑ i. ?diff (i + ?N) x ¦ ≤ (∑ i. L (i + ?N))"
by (metis (lifting) abs_idempotent
order_trans[OF summable_rabs[OF 2] suminf_le[OF _ 2 ign[OF ‹summable L›]]])
then have "¦∑i. ?diff (i + ?N) x¦ ≤ r / 3" (is "?L_part ≤ r/3")
using L_estimate by auto
have "¦∑n<?N. ?diff n x - f' x0 n¦ ≤ (∑n<?N. ¦?diff n x - f' x0 n¦)" ..
also have "… < (∑n<?N. ?r)"
proof (rule sum_strict_mono)
fix n
assume "n ∈ {..< ?N}"
have "¦x¦ < S" using ‹¦x¦ < S› .
also have "S ≤ S'" using ‹S ≤ S'› .
also have "S' ≤ ?s n"
unfolding S'_def
proof (rule Min_le_iff[THEN iffD2])
have "?s n ∈ (?s ` {..<?N}) ∧ ?s n ≤ ?s n"
using ‹n ∈ {..< ?N}› by auto
then show "∃ a ∈ (?s ` {..<?N}). a ≤ ?s n"
by blast
qed auto
finally have "¦x¦ < ?s n" .
from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF ‹0 < ?r›,
unfolded real_norm_def diff_0_right, unfolded some_eq_ex[symmetric], THEN conjunct2]
have "∀x. x ≠ 0 ∧ ¦x¦ < ?s n ⟶ ¦?diff n x - f' x0 n¦ < ?r" .
with ‹x ≠ 0› and ‹¦x¦ < ?s n› show "¦?diff n x - f' x0 n¦ < ?r"
by blast
qed auto
also have "… = of_nat (card {..<?N}) * ?r"
by (rule sum_constant)
also have "… = real ?N * ?r"
by simp
also have "… = r/3"
by (auto simp del: of_nat_Suc)
finally have "¦∑n<?N. ?diff n x - f' x0 n ¦ < r / 3" (is "?diff_part < r / 3") .
from suminf_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]]
have "¦(suminf (f (x0 + x)) - (suminf (f x0))) / x - suminf (f' x0)¦ =
¦∑n. ?diff n x - f' x0 n¦"
unfolding suminf_diff[OF div_smbl ‹summable (f' x0)›, symmetric]
using suminf_divide[OF diff_smbl, symmetric] by auto
also have "… ≤ ?diff_part + ¦(∑n. ?diff (n + ?N) x) - (∑ n. f' x0 (n + ?N))¦"
unfolding suminf_split_initial_segment[OF all_smbl, where k="?N"]
unfolding suminf_diff[OF div_shft_smbl ign[OF ‹summable (f' x0)›]]
apply (simp only: add.commute)
using abs_triangle_ineq by blast
also have "… ≤ ?diff_part + ?L_part + ?f'_part"
using abs_triangle_ineq4 by auto
also have "… < r /3 + r/3 + r/3"
using ‹?diff_part < r/3› ‹?L_part ≤ r/3› and ‹?f'_part < r/3›
by (rule add_strict_mono [OF add_less_le_mono])
finally show ?thesis
by auto
qed
then show "∃s > 0. ∀ x. x ≠ 0 ∧ norm (x - 0) < s ⟶
norm (((∑n. f (x0 + x) n) - (∑n. f x0 n)) / x - (∑n. f' x0 n)) < r"
using ‹0 < S› by auto
qed
lemma DERIV_power_series':
fixes f :: "nat ⇒ real"
assumes converges: "⋀x. x ∈ {-R <..< R} ⟹ summable (λn. f n * real (Suc n) * x^n)"
and x0_in_I: "x0 ∈ {-R <..< R}"
and "0 < R"
shows "DERIV (λx. (∑n. f n * x^(Suc n))) x0 :> (∑n. f n * real (Suc n) * x0^n)"
(is "DERIV (λx. suminf (?f x)) x0 :> suminf (?f' x0)")
proof -
have for_subinterval: "DERIV (λx. suminf (?f x)) x0 :> suminf (?f' x0)"
if "0 < R'" and "R' < R" and "-R' < x0" and "x0 < R'" for R'
proof -
from that have "x0 ∈ {-R' <..< R'}" and "R' ∈ {-R <..< R}" and "x0 ∈ {-R <..< R}"
by auto
show ?thesis
proof (rule DERIV_series')
show "summable (λ n. ¦f n * real (Suc n) * R'^n¦)"
proof -
have "(R' + R) / 2 < R" and "0 < (R' + R) / 2"
using ‹0 < R'› ‹0 < R› ‹R' < R› by (auto simp: field_simps)
then have in_Rball: "(R' + R) / 2 ∈ {-R <..< R}"
using ‹R' < R› by auto
have "norm R' < norm ((R' + R) / 2)"
using ‹0 < R'› ‹0 < R› ‹R' < R› by (auto simp: field_simps)
from powser_insidea[OF converges[OF in_Rball] this] show ?thesis
by auto
qed
next
fix n x y
assume "x ∈ {-R' <..< R'}" and "y ∈ {-R' <..< R'}"
show "¦?f x n - ?f y n¦ ≤ ¦f n * real (Suc n) * R'^n¦ * ¦x-y¦"
proof -
have "¦f n * x ^ (Suc n) - f n * y ^ (Suc n)¦ =
(¦f n¦ * ¦<