# Theory FPS_Convergence

theory FPS_Convergence
imports Generalised_Binomial_Theorem Formal_Power_Series
```(*
Title:    HOL/Analysis/FPS_Convergence.thy
Author:   Manuel Eberl, TU München

Connection of formal power series and actual convergent power series on Banach spaces
(most notably the complex numbers).
*)
section ‹Convergence of Formal Power Series›

theory FPS_Convergence
imports
Generalised_Binomial_Theorem
"HOL-Computational_Algebra.Formal_Power_Series"
begin

text ‹
In this theory, we will connect formal power series (which are algebraic objects) with analytic
functions. This will become more important in complex analysis, and indeed some of the less
trivial results will only be proven there.
›

subsection✐‹tag unimportant› ‹Balls with extended real radius›

(* TODO: This should probably go somewhere else *)

text ‹
The following is a variant of \<^const>‹ball› that also allows an infinite radius.
›
definition eball :: "'a :: metric_space ⇒ ereal ⇒ 'a set" where
"eball z r = {z'. ereal (dist z z') < r}"

lemma in_eball_iff [simp]: "z ∈ eball z0 r ⟷ ereal (dist z0 z) < r"

lemma eball_ereal [simp]: "eball z (ereal r) = ball z r"
by auto

lemma eball_inf [simp]: "eball z ∞ = UNIV"
by auto

lemma eball_empty [simp]: "r ≤ 0 ⟹ eball z r = {}"
proof safe
fix x assume "r ≤ 0" "x ∈ eball z r"
hence "dist z x < r" by simp
also have "… ≤ ereal 0" using ‹r ≤ 0› by (simp add: zero_ereal_def)
finally show "x ∈ {}" by simp
qed

lemma eball_conv_UNION_balls:
"eball z r = (⋃r'∈{r'. ereal r' < r}. ball z r')"
by (cases r) (use dense gt_ex in force)+

lemma eball_mono: "r ≤ r' ⟹ eball z r ≤ eball z r'"
by auto

lemma ball_eball_mono: "ereal r ≤ r' ⟹ ball z r ≤ eball z r'"
using eball_mono[of "ereal r" r'] by simp

lemma open_eball [simp, intro]: "open (eball z r)"
by (cases r) auto

subsection ‹Basic properties of convergent power series›

definition✐‹tag important› fps_conv_radius :: "'a :: {banach, real_normed_div_algebra} fps ⇒ ereal" where

definition✐‹tag important› eval_fps :: "'a :: {banach, real_normed_div_algebra} fps ⇒ 'a ⇒ 'a" where
"eval_fps f z = (∑n. fps_nth f n * z ^ n)"

lemma norm_summable_fps:
fixes f :: "'a :: {banach, real_normed_div_algebra} fps"
shows "norm z < fps_conv_radius f ⟹ summable (λn. norm (fps_nth f n * z ^ n))"

lemma summable_fps:
fixes f :: "'a :: {banach, real_normed_div_algebra} fps"
shows "norm z < fps_conv_radius f ⟹ summable (λn. fps_nth f n * z ^ n)"

theorem sums_eval_fps:
fixes f :: "'a :: {banach, real_normed_div_algebra} fps"
assumes "norm z < fps_conv_radius f"
shows   "(λn. fps_nth f n * z ^ n) sums eval_fps f z"

lemma continuous_on_eval_fps:
fixes f :: "'a :: {banach, real_normed_div_algebra} fps"
shows "continuous_on (eball 0 (fps_conv_radius f)) (eval_fps f)"
proof (subst continuous_on_eq_continuous_at [OF open_eball], safe)
fix x :: 'a assume x: "x ∈ eball 0 (fps_conv_radius f)"
define r where "r = (if fps_conv_radius f = ∞ then norm x + 1 else
(norm x + real_of_ereal (fps_conv_radius f)) / 2)"
have r: "norm x < r ∧ ereal r < fps_conv_radius f"
using x by (cases "fps_conv_radius f")
(auto simp: r_def eball_def split: if_splits)

have "continuous_on (cball 0 r) (λx. ∑i. fps_nth f i * (x - 0) ^ i)"
by (rule powser_continuous_suminf) (insert r, auto simp: fps_conv_radius_def)
hence "continuous_on (cball 0 r) (eval_fps f)"
thus "isCont (eval_fps f) x"
by (rule continuous_on_interior) (use r in auto)
qed

lemma continuous_on_eval_fps' [continuous_intros]:
assumes "continuous_on A g"
assumes "g ` A ⊆ eball 0 (fps_conv_radius f)"
shows   "continuous_on A (λx. eval_fps f (g x))"
using continuous_on_compose2[OF continuous_on_eval_fps assms] .

lemma has_field_derivative_powser:
fixes z :: "'a :: {banach, real_normed_field}"
assumes "ereal (norm z) < conv_radius f"
shows   "((λz. ∑n. f n * z ^ n) has_field_derivative (∑n. diffs f n * z ^ n)) (at z within A)"
proof -
define K where "K = (if conv_radius f = ∞ then norm z + 1
else (norm z + real_of_ereal (conv_radius f)) / 2)"
have K: "norm z < K ∧ ereal K < conv_radius f"
using assms by (cases "conv_radius f") (auto simp: K_def)
have "0 ≤ norm z" by simp
also from K have "… < K" by simp
finally have K_pos: "K > 0" by simp

have "summable (λn. f n * of_real K ^ n)"
using K and K_pos by (intro summable_in_conv_radius) auto
moreover from K and K_pos have "norm z < norm (of_real K :: 'a)" by auto
ultimately show ?thesis
by (rule has_field_derivative_at_within [OF termdiffs_strong])
qed

lemma has_field_derivative_eval_fps:
fixes z :: "'a :: {banach, real_normed_field}"
assumes "norm z < fps_conv_radius f"
shows   "(eval_fps f has_field_derivative eval_fps (fps_deriv f) z) (at z within A)"
proof -
have "(eval_fps f has_field_derivative eval_fps (Abs_fps (diffs (fps_nth f))) z) (at z within A)"
using assms unfolding eval_fps_def fps_nth_Abs_fps fps_conv_radius_def
by (intro has_field_derivative_powser) auto
also have "Abs_fps (diffs (fps_nth f)) = fps_deriv f"
finally show ?thesis .
qed

lemma holomorphic_on_eval_fps [holomorphic_intros]:
fixes z :: "'a :: {banach, real_normed_field}"
assumes "A ⊆ eball 0 (fps_conv_radius f)"
shows   "eval_fps f holomorphic_on A"
proof (rule holomorphic_on_subset [OF _ assms])
show "eval_fps f holomorphic_on eball 0 (fps_conv_radius f)"
proof (subst holomorphic_on_open [OF open_eball], safe, goal_cases)
case (1 x)
thus ?case
by (intro exI[of _ "eval_fps (fps_deriv f) x"]) (auto intro: has_field_derivative_eval_fps)
qed
qed

lemma analytic_on_eval_fps:
fixes z :: "'a :: {banach, real_normed_field}"
assumes "A ⊆ eball 0 (fps_conv_radius f)"
shows   "eval_fps f analytic_on A"
proof (rule analytic_on_subset [OF _ assms])
show "eval_fps f analytic_on eball 0 (fps_conv_radius f)"
using holomorphic_on_eval_fps[of "eball 0 (fps_conv_radius f)"]
by (subst analytic_on_open) auto
qed

lemma continuous_eval_fps [continuous_intros]:
fixes z :: "'a::{real_normed_field,banach}"
assumes "norm z < fps_conv_radius F"
shows   "continuous (at z within A) (eval_fps F)"
proof -
from ereal_dense2[OF assms] obtain K :: real where K: "norm z < K" "K < fps_conv_radius F"
by auto
have "0 ≤ norm z" by simp
also have "norm z < K" by fact
finally have "K > 0" .
from K and ‹K > 0› have "summable (λn. fps_nth F n * of_real K ^ n)"
by (intro summable_fps) auto
from this have "isCont (eval_fps F) z" unfolding eval_fps_def
by (rule isCont_powser) (use K in auto)
thus "continuous (at z within A)  (eval_fps F)"
qed

subsection✐‹tag unimportant› ‹Lower bounds on radius of convergence›

fixes f :: "'a :: {banach, real_normed_field} fps"
fix r :: real assume r: "r > 0" "ereal r < conv_radius (fps_nth f)"
define K where "K = (if conv_radius (fps_nth f) = ∞ then r + 1
else (real_of_ereal (conv_radius (fps_nth f)) + r) / 2)"
have K: "r < K ∧ ereal K < conv_radius (fps_nth f)"
using r by (cases "conv_radius (fps_nth f)") (auto simp: K_def)
have "summable (λn. diffs (fps_nth f) n * of_real r ^ n)"
proof (rule termdiff_converges)
fix x :: 'a assume "norm x < K"
hence "ereal (norm x) < ereal K" by simp
also have "… < conv_radius (fps_nth f)" using K by simp
finally show "summable (λn. fps_nth f n * x ^ n)"
qed (insert K r, auto)
also have "… = (λn. fps_nth (fps_deriv f) n * of_real r ^ n)"
finally show "∃z::'a. norm z = r ∧ summable (λn. fps_nth (fps_deriv f) n * z ^ n)"
using r by (intro exI[of _ "of_real r"]) auto
qed

lemma eval_fps_at_0: "eval_fps f 0 = fps_nth f 0"

proof -
by (intro conv_radius_cong eventually_mono[OF eventually_gt_at_top[of 0]]) auto
thus ?thesis by simp
qed

by (simp only: fps_const_0_eq_0 [symmetric] fps_conv_radius_const)

by (simp only: fps_const_1_eq_1 [symmetric] fps_conv_radius_const)

proof -
have "fps_conv_radius (fps_X ^ n :: 'a fps) = conv_radius (λ_. 0 :: 'a)"
by (intro conv_radius_cong eventually_mono[OF eventually_gt_at_top[of n]])
(auto simp: fps_X_power_iff)
thus ?thesis by simp
qed

using fps_conv_radius_fps_X_power[of 1] by (simp only: power_one_right)

"c ≠ 0 ⟹ fps_conv_radius (fps_const c * f) = fps_conv_radius f"

"c ≠ 0 ⟹ fps_conv_radius (f * fps_const c) = fps_conv_radius f"

by (simp flip: fps_const_neg)

by simp

using conv_radius_mult_ge[of "fps_nth f" "fps_nth g"]

proof (induction n)
case (Suc n)
by simp
also have "… ≤ fps_conv_radius (f * f ^ n)"
finally show ?case by simp
qed simp_all

context
begin

lemma natfun_inverse_bound:
fixes f :: "'a :: {real_normed_field} fps"
assumes "fps_nth f 0 = 1" and "δ > 0"
and summable: "summable (λn. norm (fps_nth f (Suc n)) * δ ^ Suc n)"
and le: "(∑n. norm (fps_nth f (Suc n)) * δ ^ Suc n) ≤ 1"
shows   "norm (natfun_inverse f n) ≤ inverse (δ ^ n)"
proof (induction n rule: less_induct)
case (less m)
show ?case
proof (cases m)
case 0
thus ?thesis using assms by (simp add: field_split_simps norm_inverse norm_divide)
next
case [simp]: (Suc n)
have "norm (natfun_inverse f (Suc n)) =
norm (∑i = Suc 0..Suc n. fps_nth f i * natfun_inverse f (Suc n - i))"
(is "_ = norm ?S") using assms
by (simp add: field_simps norm_mult norm_divide del: sum.cl_ivl_Suc)
also have "norm ?S ≤ (∑i = Suc 0..Suc n. norm (fps_nth f i * natfun_inverse f (Suc n - i)))"
by (rule norm_sum)
also have "… ≤ (∑i = Suc 0..Suc n. norm (fps_nth f i) / δ ^ (Suc n - i))"
proof (intro sum_mono, goal_cases)
case (1 i)
have "norm (fps_nth f i * natfun_inverse f (Suc n - i)) =
norm (fps_nth f i) * norm (natfun_inverse f (Suc n - i))"
also have "… ≤ norm (fps_nth f i) * inverse (δ ^ (Suc n - i))"
using 1 by (intro mult_left_mono less.IH) auto
also have "… = norm (fps_nth f i) / δ ^ (Suc n - i)"
finally show ?case .
qed
also have "… = (∑i = Suc 0..Suc n. norm (fps_nth f i) * δ ^ i) / δ ^ Suc n"
by (subst sum_divide_distrib, rule sum.cong)
(insert ‹δ > 0›, auto simp: field_simps power_diff)
also have "(∑i = Suc 0..Suc n. norm (fps_nth f i) * δ ^ i) =
(∑i=0..n. norm (fps_nth f (Suc i)) * δ ^ (Suc i))"
by (subst sum.atLeast_Suc_atMost_Suc_shift) simp_all
also have "{0..n} = {..<Suc n}" by auto
also have "(∑i< Suc n. norm (fps_nth f (Suc i)) * δ ^ (Suc i)) ≤
(∑n. norm (fps_nth f (Suc n)) * δ ^ (Suc n))"
using ‹δ > 0› by (intro sum_le_suminf ballI mult_nonneg_nonneg zero_le_power summable) auto
also have "… ≤ 1" by fact
finally show ?thesis using ‹δ > 0›
qed
qed

fixes f :: "'a :: {banach, real_normed_field} fps"
assumes "fps_nth f 0 = 1" "fps_conv_radius f > 0"
shows   "fps_conv_radius (inverse f) > 0"
proof -
define h where "h = Abs_fps (λn. norm (fps_nth f n))"
have "continuous_on (eball 0 (fps_conv_radius h)) (eval_fps h)"
by (intro continuous_on_eval_fps)
hence *: "open (eval_fps h -` A ∩ eball 0 ?R)" if "open A" for A
using that by (subst (asm) continuous_on_open_vimage) auto
have "open (eval_fps h -` {..<2} ∩ eball 0 ?R)"
by (rule *) auto
moreover have "0 ∈ eval_fps h -` {..<2} ∩ eball 0 ?R"
using assms by (auto simp: eball_def zero_ereal_def eval_fps_at_0 h_def)
ultimately obtain ε where ε: "ε > 0" "ball 0 ε ⊆ eval_fps h -` {..<2} ∩ eball 0 ?R"
by (subst (asm) open_contains_ball_eq) blast+

define δ where "δ = real_of_ereal (min (ereal ε / 2) (?R / 2))"
have δ: "0 < δ ∧ δ < ε ∧ ereal δ < ?R"
using ‹ε > 0› and assms by (cases ?R) (auto simp: δ_def min_def)

have summable: "summable (λn. norm (fps_nth f n) * δ ^ n)"
hence "(λn. norm (fps_nth f n) * δ ^ n) sums eval_fps h δ"
by (simp add: eval_fps_def summable_sums h_def)
hence "(λn. norm (fps_nth f (Suc n)) * δ ^ Suc n) sums (eval_fps h δ - 1)"
by (subst sums_Suc_iff) (auto simp: assms)
moreover {
from δ have "δ ∈ ball 0 ε" by auto
also have "… ⊆ eval_fps h -` {..<2} ∩ eball 0 ?R" by fact
finally have "eval_fps h δ < 2" by simp
}
ultimately have le: "(∑n. norm (fps_nth f (Suc n)) * δ ^ Suc n) ≤ 1"
from summable have summable: "summable (λn. norm (fps_nth f (Suc n)) * δ ^ Suc n)"
by (subst summable_Suc_iff)

have "0 < δ" using δ by blast
also have "δ = inverse (limsup (λn. ereal (inverse δ)))"
using δ by (subst Limsup_const) auto
also have "… ≤ conv_radius (natfun_inverse f)"
proof (intro ereal_inverse_antimono Limsup_mono
eventually_mono[OF eventually_gt_at_top[of 0]])
fix n :: nat assume n: "n > 0"
have "root n (norm (natfun_inverse f n)) ≤ root n (inverse (δ ^ n))"
using n assms δ le summable
by (intro real_root_le_mono natfun_inverse_bound) auto
also have "… = inverse δ"
using n δ by (simp add: power_inverse [symmetric] real_root_pos2)
finally show "ereal (inverse δ) ≥ ereal (root n (norm (natfun_inverse f n)))"
by (subst ereal_less_eq)
next
have "0 = limsup (λn. 0::ereal)"
by (rule Limsup_const [symmetric]) auto
also have "… ≤ limsup (λn. ereal (root n (norm (natfun_inverse f n))))"
by (intro Limsup_mono) (auto simp: real_root_ge_zero)
finally show "0 ≤ …" by simp
qed
also have "… = fps_conv_radius (inverse f)"
finally show ?thesis by (simp add: zero_ereal_def)
qed

fixes f :: "'a :: {banach, real_normed_field} fps"
assumes "fps_nth f 0 ≠ 0" and "fps_conv_radius f > 0"
shows   "fps_conv_radius (inverse f) > 0"
proof -
let ?c = "fps_nth f 0"
using assms by (subst fps_conv_radius_cmult_left) auto
also have "fps_const ?c * inverse f = inverse (fps_const (inverse ?c) * f)"
using assms by (simp add: fps_inverse_mult fps_const_inverse)
also have "fps_conv_radius … > 0" using assms
finally show ?thesis .
qed

end

fixes c :: "'a :: {banach, real_normed_field}"
shows "fps_conv_radius (fps_exp c) = ∞"
fix z :: 'a
have "(λn. norm (c * z) ^ n /⇩R fact n) sums exp (norm (c * z))"
by (rule exp_converges)
also have "(λn. norm (c * z) ^ n /⇩R fact n) = (λn. norm (fps_nth (fps_exp c) n * z ^ n))"
by (rule ext) (simp add: norm_divide norm_mult norm_power field_split_simps)
finally have "summable …" by (simp add: sums_iff)
thus "summable (λn. fps_nth (fps_exp c) n * z ^ n)"
by (rule summable_norm_cancel)
qed

subsection ‹Evaluating power series›

theorem eval_fps_deriv:
assumes "norm z < fps_conv_radius f"
shows   "eval_fps (fps_deriv f) z = deriv (eval_fps f) z"
by (intro DERIV_imp_deriv [symmetric] has_field_derivative_eval_fps assms)

theorem fps_nth_conv_deriv:
fixes f :: "complex fps"
shows   "fps_nth f n = (deriv ^^ n) (eval_fps f) 0 / fact n"
using assms
proof (induction n arbitrary: f)
case 0
thus ?case by (simp add: eval_fps_def)
next
case (Suc n f)
have "(deriv ^^ Suc n) (eval_fps f) 0 = (deriv ^^ n) (deriv (eval_fps f)) 0"
unfolding funpow_Suc_right o_def ..
also have "eventually (λz::complex. z ∈ eball 0 (fps_conv_radius f)) (nhds 0)"
using Suc.prems by (intro eventually_nhds_in_open) (auto simp: zero_ereal_def)
hence "eventually (λz. deriv (eval_fps f) z = eval_fps (fps_deriv f) z) (nhds 0)"
hence "(deriv ^^ n) (deriv (eval_fps f)) 0 = (deriv ^^ n) (eval_fps (fps_deriv f)) 0"
by (intro higher_deriv_cong_ev refl)
also have "… / fact n = fps_nth (fps_deriv f) n"
by (intro Suc.IH [symmetric]) auto
also have "… / of_nat (Suc n) = fps_nth f (Suc n)"
by (simp add: fps_deriv_def del: of_nat_Suc)
finally show ?case by (simp add: field_split_simps)
qed

theorem eval_fps_eqD:
fixes f g :: "complex fps"
assumes "eventually (λz. eval_fps f z = eval_fps g z) (nhds 0)"
shows   "f = g"
proof (rule fps_ext)
fix n :: nat
have "fps_nth f n = (deriv ^^ n) (eval_fps f) 0 / fact n"
using assms by (intro fps_nth_conv_deriv)
also have "(deriv ^^ n) (eval_fps f) 0 = (deriv ^^ n) (eval_fps g) 0"
by (intro higher_deriv_cong_ev refl assms)
also have "… / fact n = fps_nth g n"
using assms by (intro fps_nth_conv_deriv [symmetric])
finally show "fps_nth f n = fps_nth g n" .
qed

lemma eval_fps_const [simp]:
fixes c :: "'a :: {banach, real_normed_div_algebra}"
shows "eval_fps (fps_const c) z = c"
proof -
have "(λn::nat. if n ∈ {0} then c else 0) sums (∑n∈{0::nat}. c)"
by (rule sums_If_finite_set) auto
also have "?this ⟷ (λn::nat. fps_nth (fps_const c) n * z ^ n) sums (∑n∈{0::nat}. c)"
by (intro sums_cong) auto
also have "(∑n∈{0::nat}. c) = c"
by simp
finally show ?thesis
qed

lemma eval_fps_0 [simp]:
"eval_fps (0 :: 'a :: {banach, real_normed_div_algebra} fps) z = 0"
by (simp only: fps_const_0_eq_0 [symmetric] eval_fps_const)

lemma eval_fps_1 [simp]:
"eval_fps (1 :: 'a :: {banach, real_normed_div_algebra} fps) z = 1"
by (simp only: fps_const_1_eq_1 [symmetric] eval_fps_const)

lemma eval_fps_numeral [simp]:
"eval_fps (numeral n :: 'a :: {banach, real_normed_div_algebra} fps) z = numeral n"
by (simp only: numeral_fps_const eval_fps_const)

lemma eval_fps_X_power [simp]:
"eval_fps (fps_X ^ m :: 'a :: {banach, real_normed_div_algebra} fps) z = z ^ m"
proof -
have "(λn::nat. if n ∈ {m} then z ^ n else 0 :: 'a) sums (∑n∈{m::nat}. z ^ n)"
by (rule sums_If_finite_set) auto
also have "?this ⟷ (λn::nat. fps_nth (fps_X ^ m) n * z ^ n) sums (∑n∈{m::nat}. z ^ n)"
by (intro sums_cong) (auto simp: fps_X_power_iff)
also have "(∑n∈{m::nat}. z ^ n) = z ^ m"
by simp
finally show ?thesis
qed

lemma eval_fps_X [simp]:
"eval_fps (fps_X :: 'a :: {banach, real_normed_div_algebra} fps) z = z"
using eval_fps_X_power[of 1 z] by (simp only: power_one_right)

lemma eval_fps_minus:
fixes f :: "'a :: {banach, real_normed_div_algebra} fps"
assumes "norm z < fps_conv_radius f"
shows   "eval_fps (-f) z = -eval_fps f z"
using assms unfolding eval_fps_def
by (subst suminf_minus [symmetric]) (auto intro!: summable_fps)

fixes f g :: "'a :: {banach, real_normed_div_algebra} fps"
shows   "eval_fps (f + g) z = eval_fps f z + eval_fps g z"
using assms unfolding eval_fps_def
by (subst suminf_add) (auto simp: ring_distribs intro!: summable_fps)

lemma eval_fps_diff:
fixes f g :: "'a :: {banach, real_normed_div_algebra} fps"
shows   "eval_fps (f - g) z = eval_fps f z - eval_fps g z"
using assms unfolding eval_fps_def
by (subst suminf_diff) (auto simp: ring_distribs intro!: summable_fps)

lemma eval_fps_mult:
fixes f g :: "'a :: {banach, real_normed_div_algebra, comm_ring_1} fps"
shows   "eval_fps (f * g) z = eval_fps f z * eval_fps g z"
proof -
have "eval_fps f z * eval_fps g z =
(∑k. ∑i≤k. fps_nth f i * fps_nth g (k - i) * (z ^ i * z ^ (k - i)))"
unfolding eval_fps_def
proof (subst Cauchy_product)
show "summable (λk. norm (fps_nth f k * z ^ k))" "summable (λk. norm (fps_nth g k * z ^ k))"
by (rule norm_summable_fps assms)+
also have "(λk. ∑i≤k. fps_nth f i * fps_nth g (k - i) * (z ^ i * z ^ (k - i))) =
(λk. ∑i≤k. fps_nth f i * fps_nth g (k - i) * z ^ k)"
also have "suminf … = eval_fps (f * g) z"
by (simp add: eval_fps_def fps_mult_nth atLeast0AtMost sum_distrib_right)
finally show ?thesis ..
qed

lemma eval_fps_shift:
fixes f :: "'a :: {banach, real_normed_div_algebra, comm_ring_1} fps"
assumes "n ≤ subdegree f" "norm z < fps_conv_radius f"
shows   "eval_fps (fps_shift n f) z = (if z = 0 then fps_nth f n else eval_fps f z / z ^ n)"
proof (cases "z = 0")
case False
have "eval_fps (fps_shift n f * fps_X ^ n) z = eval_fps (fps_shift n f) z * z ^ n"
using assms by (subst eval_fps_mult) simp_all
also from assms have "fps_shift n f * fps_X ^ n = f"
finally show ?thesis using False by (simp add: field_simps)

lemma eval_fps_exp [simp]:
fixes c :: "'a :: {banach, real_normed_field}"
shows "eval_fps (fps_exp c) z = exp (c * z)" unfolding eval_fps_def exp_def
by (simp add: eval_fps_def exp_def scaleR_conv_of_real field_split_simps)

text ‹
The case of division is more complicated and will therefore not be handled here.
Handling division becomes much more easy using complex analysis, and we will do so once
that is available.
›

subsection ‹Power series expansions of analytic functions›

text ‹
This predicate contains the notion that the given formal power series converges
in some disc of positive radius around the origin and is equal to the given complex
function there.

This relationship is unique in the sense that no complex function can have more than
one formal power series to which it expands, and if two holomorphic functions that are
holomorphic on a connected open set around the origin and have the same power series
expansion, they must be equal on that set.

many purposes, the statment that the series converges to the function in some neighbourhood
of the origin is enough, and that can be shown almost fully automatically in most cases,
as there are straightforward introduction rules to show this.

In particular, when one wants to relate the coefficients of the power series to the
values of the derivatives of the function at the origin, or if one wants to approximate
the coefficients of the series with the singularities of the function, this predicate
is enough.
›
definition✐‹tag important›
has_fps_expansion :: "('a :: {banach,real_normed_div_algebra} ⇒ 'a) ⇒ 'a fps ⇒ bool"
(infixl "has'_fps'_expansion" 60)
where "(f has_fps_expansion F) ⟷
fps_conv_radius F > 0 ∧ eventually (λz. eval_fps F z = f z) (nhds 0)"

named_theorems fps_expansion_intros

lemma fps_nth_fps_expansion:
fixes f :: "complex ⇒ complex"
assumes "f has_fps_expansion F"
shows   "fps_nth F n = (deriv ^^ n) f 0 / fact n"
proof -
have "fps_nth F n = (deriv ^^ n) (eval_fps F) 0 / fact n"
using assms by (intro fps_nth_conv_deriv) (auto simp: has_fps_expansion_def)
also have "(deriv ^^ n) (eval_fps F) 0 = (deriv ^^ n) f 0"
using assms by (intro higher_deriv_cong_ev) (auto simp: has_fps_expansion_def)
finally show ?thesis .
qed

lemma has_fps_expansion_imp_continuous:
fixes F :: "'a::{real_normed_field,banach} fps"
assumes "f has_fps_expansion F"
shows   "continuous (at 0 within A) f"
proof -
from assms have "isCont (eval_fps F) 0"
by (intro continuous_eval_fps) (auto simp: has_fps_expansion_def zero_ereal_def)
also have "?this ⟷ isCont f 0" using assms
by (intro isCont_cong) (auto simp: has_fps_expansion_def)
finally have "isCont f 0" .
thus "continuous (at 0 within A) f"
qed

lemma has_fps_expansion_const [simp, intro, fps_expansion_intros]:
"(λ_. c) has_fps_expansion fps_const c"
by (auto simp: has_fps_expansion_def)

lemma has_fps_expansion_0 [simp, intro, fps_expansion_intros]:
"(λ_. 0) has_fps_expansion 0"
by (auto simp: has_fps_expansion_def)

lemma has_fps_expansion_1 [simp, intro, fps_expansion_intros]:
"(λ_. 1) has_fps_expansion 1"
by (auto simp: has_fps_expansion_def)

lemma has_fps_expansion_numeral [simp, intro, fps_expansion_intros]:
"(λ_. numeral n) has_fps_expansion numeral n"
by (auto simp: has_fps_expansion_def)

lemma has_fps_expansion_fps_X_power [fps_expansion_intros]:
"(λx. x ^ n) has_fps_expansion (fps_X ^ n)"
by (auto simp: has_fps_expansion_def)

lemma has_fps_expansion_fps_X [fps_expansion_intros]:
"(λx. x) has_fps_expansion fps_X"
by (auto simp: has_fps_expansion_def)

lemma has_fps_expansion_cmult_left [fps_expansion_intros]:
fixes c :: "'a :: {banach, real_normed_div_algebra, comm_ring_1}"
assumes "f has_fps_expansion F"
shows   "(λx. c * f x) has_fps_expansion fps_const c * F"
proof (cases "c = 0")
case False
from assms have "eventually (λz. z ∈ eball 0 (fps_conv_radius F)) (nhds 0)"
by (intro eventually_nhds_in_open) (auto simp: has_fps_expansion_def zero_ereal_def)
moreover from assms have "eventually (λz. eval_fps F z = f z) (nhds 0)"
by (auto simp: has_fps_expansion_def)
ultimately have "eventually (λz. eval_fps (fps_const c * F) z = c * f z) (nhds 0)"
with assms and False show ?thesis
qed auto

lemma has_fps_expansion_cmult_right [fps_expansion_intros]:
fixes c :: "'a :: {banach, real_normed_div_algebra, comm_ring_1}"
assumes "f has_fps_expansion F"
shows   "(λx. f x * c) has_fps_expansion F * fps_const c"
proof -
have "F * fps_const c = fps_const c * F"
by (intro fps_ext) (auto simp: mult.commute)
with has_fps_expansion_cmult_left [OF assms] show ?thesis
qed

lemma has_fps_expansion_minus [fps_expansion_intros]:
assumes "f has_fps_expansion F"
shows   "(λx. - f x) has_fps_expansion -F"
proof -
from assms have "eventually (λx. x ∈ eball 0 (fps_conv_radius F)) (nhds 0)"
by (intro eventually_nhds_in_open) (auto simp: has_fps_expansion_def zero_ereal_def)
moreover from assms have "eventually (λx. eval_fps F x = f x) (nhds 0)"
by (auto simp: has_fps_expansion_def)
ultimately have "eventually (λx. eval_fps (-F) x = -f x) (nhds 0)"
by eventually_elim (auto simp: eval_fps_minus)
thus ?thesis using assms by (auto simp: has_fps_expansion_def)
qed

assumes "f has_fps_expansion F" "g has_fps_expansion G"
shows   "(λx. f x + g x) has_fps_expansion F + G"
proof -
by (auto simp: has_fps_expansion_def)
also have "… ≤ fps_conv_radius (F + G)"
finally have radius: "… > 0" .

from assms have "eventually (λx. x ∈ eball 0 (fps_conv_radius F)) (nhds 0)"
"eventually (λx. x ∈ eball 0 (fps_conv_radius G)) (nhds 0)"
by (intro eventually_nhds_in_open; force simp: has_fps_expansion_def zero_ereal_def)+
moreover have "eventually (λx. eval_fps F x = f x) (nhds 0)"
and "eventually (λx. eval_fps G x = g x) (nhds 0)"
using assms by (auto simp: has_fps_expansion_def)
ultimately have "eventually (λx. eval_fps (F + G) x = f x + g x) (nhds 0)"
with radius show ?thesis by (auto simp: has_fps_expansion_def)
qed

lemma has_fps_expansion_diff [fps_expansion_intros]:
assumes "f has_fps_expansion F" "g has_fps_expansion G"
shows   "(λx. f x - g x) has_fps_expansion F - G"
using has_fps_expansion_add[of f F "λx. - g x" "-G"] assms

lemma has_fps_expansion_mult [fps_expansion_intros]:
fixes F G :: "'a :: {banach, real_normed_div_algebra, comm_ring_1} fps"
assumes "f has_fps_expansion F" "g has_fps_expansion G"
shows   "(λx. f x * g x) has_fps_expansion F * G"
proof -
by (auto simp: has_fps_expansion_def)
also have "… ≤ fps_conv_radius (F * G)"
finally have radius: "… > 0" .

from assms have "eventually (λx. x ∈ eball 0 (fps_conv_radius F)) (nhds 0)"
"eventually (λx. x ∈ eball 0 (fps_conv_radius G)) (nhds 0)"
by (intro eventually_nhds_in_open; force simp: has_fps_expansion_def zero_ereal_def)+
moreover have "eventually (λx. eval_fps F x = f x) (nhds 0)"
and "eventually (λx. eval_fps G x = g x) (nhds 0)"
using assms by (auto simp: has_fps_expansion_def)
ultimately have "eventually (λx. eval_fps (F * G) x = f x * g x) (nhds 0)"
by eventually_elim (auto simp: eval_fps_mult)
with radius show ?thesis by (auto simp: has_fps_expansion_def)
qed

lemma has_fps_expansion_inverse [fps_expansion_intros]:
fixes F :: "'a :: {banach, real_normed_field} fps"
assumes "f has_fps_expansion F"
assumes "fps_nth F 0 ≠ 0"
shows   "(λx. inverse (f x)) has_fps_expansion inverse F"
proof -
using assms unfolding has_fps_expansion_def
have "eventually (λx. x ∈ eball 0 (fps_conv_radius F)) (nhds 0)"
"eventually (λx. x ∈ eball 0 (fps_conv_radius (inverse F))) (nhds 0)"
by (intro eventually_nhds_in_open; force simp: has_fps_expansion_def zero_ereal_def)+
moreover have "eventually (λz. eval_fps F z = f z) (nhds 0)"
using assms by (auto simp: has_fps_expansion_def)
ultimately have "eventually (λz. eval_fps (inverse F) z = inverse (f z)) (nhds 0)"
proof eventually_elim
case (elim z)
hence "eval_fps (inverse F * F) z = eval_fps (inverse F) z * f z"
by (subst eval_fps_mult) auto
also have "eval_fps (inverse F * F) z = 1"
using assms by (simp add: inverse_mult_eq_1)
finally show ?case by (auto simp: field_split_simps)
qed
with radius show ?thesis by (auto simp: has_fps_expansion_def)
qed

lemma has_fps_expansion_exp [fps_expansion_intros]:
fixes c :: "'a :: {banach, real_normed_field}"
shows "(λx. exp (c * x)) has_fps_expansion fps_exp c"
by (auto simp: has_fps_expansion_def)

lemma has_fps_expansion_exp1 [fps_expansion_intros]:
"(λx::'a :: {banach, real_normed_field}. exp x) has_fps_expansion fps_exp 1"
using has_fps_expansion_exp[of 1] by simp

lemma has_fps_expansion_exp_neg1 [fps_expansion_intros]:
"(λx::'a :: {banach, real_normed_field}. exp (-x)) has_fps_expansion fps_exp (-1)"
using has_fps_expansion_exp[of "-1"] by simp

lemma has_fps_expansion_deriv [fps_expansion_intros]:
assumes "f has_fps_expansion F"
shows   "deriv f has_fps_expansion fps_deriv F"
proof -
have "eventually (λz. z ∈ eball 0 (fps_conv_radius F)) (nhds 0)"
using assms by (intro eventually_nhds_in_open)
(auto simp: has_fps_expansion_def zero_ereal_def)
moreover from assms have "eventually (λz. eval_fps F z = f z) (nhds 0)"
by (auto simp: has_fps_expansion_def)
then obtain s where "open s" "0 ∈ s" and s: "⋀w. w ∈ s ⟹ eval_fps F w = f w"
by (auto simp: eventually_nhds)
hence "eventually (λw. w ∈ s) (nhds 0)"
by (intro eventually_nhds_in_open) auto
ultimately have "eventually (λz. eval_fps (fps_deriv F) z = deriv f z) (nhds 0)"
proof eventually_elim
case (elim z)
hence "eval_fps (fps_deriv F) z = deriv (eval_fps F) z"
also have "eventually (λw. w ∈ s) (nhds z)"
using elim and ‹open s› by (intro eventually_nhds_in_open) auto
hence "eventually (λw. eval_fps F w = f w) (nhds z)"
hence "deriv (eval_fps F) z = deriv f z"
by (intro deriv_cong_ev refl)
finally show ?case .
qed
with assms and fps_conv_radius_deriv[of F] show ?thesis
by (auto simp: has_fps_expansion_def)
qed

fixes c :: "'a :: {real_normed_field,banach}"
shows "fps_conv_radius (fps_binomial c) = (if c ∈ ℕ then ∞ else 1)"

fixes c :: "'a :: {banach, real_normed_field, field_char_0}"
shows "fps_conv_radius (fps_ln c) = (if c = 0 then ∞ else 1)"
proof (cases "c = 0")
case False
have "conv_radius (λn. 1 / of_nat n :: 'a) = 1"
show "(λn. norm (1 / of_nat n :: 'a) / norm (1 / of_nat (Suc n) :: 'a)) ⇢ 1"
using LIMSEQ_Suc_n_over_n by (simp add: norm_divide del: of_nat_Suc)
qed auto
also have "conv_radius (λn. 1 / of_nat n :: 'a) =
conv_radius (λn. if n = 0 then 0 else (- 1) ^ (n - 1) / of_nat n :: 'a)"
by (intro conv_radius_cong eventually_mono[OF eventually_gt_at_top[of 0]])
finally show ?thesis using False unfolding fps_ln_def
qed (auto simp: fps_ln_def)

assumes "c ≠ (0 :: 'a :: {banach,real_normed_field,field_char_0})"
shows   "fps_conv_radius (fps_ln c) = 1"

fixes c :: "'a :: {banach, real_normed_field, field_char_0}"
shows "fps_conv_radius (fps_sin c) = ∞"
proof (cases "c = 0")
case False
have "∞ = conv_radius (λn. of_real (sin_coeff n) :: 'a)"
proof (rule sym, rule conv_radius_inftyI'', rule summable_norm_cancel, goal_cases)
case (1 z)
show ?case using summable_norm_sin[of z] by (simp add: norm_mult)
qed
also have "… / norm c = conv_radius (λn. c ^ n * of_real (sin_coeff n) :: 'a)"
using False by (subst conv_radius_mult_power) auto
finally show ?thesis by simp
qed simp_all

fixes c :: "'a :: {banach, real_normed_field, field_char_0}"
shows "fps_conv_radius (fps_cos c) = ∞"
proof (cases "c = 0")
case False
have "∞ = conv_radius (λn. of_real (cos_coeff n) :: 'a)"
proof (rule sym, rule conv_radius_inftyI'', rule summable_norm_cancel, goal_cases)
case (1 z)
show ?case using summable_norm_cos[of z] by (simp add: norm_mult)
qed
also have "… / norm c = conv_radius (λn. c ^ n * of_real (cos_coeff n) :: 'a)"
using False by (subst conv_radius_mult_power) auto
finally show ?thesis by simp
qed simp_all

lemma eval_fps_sin [simp]:
fixes z :: "'a :: {banach, real_normed_field, field_char_0}"
shows "eval_fps (fps_sin c) z = sin (c * z)"
proof -
have "(λn. sin_coeff n *⇩R (c * z) ^ n) sums sin (c * z)" by (rule sin_converges)
also have "(λn. sin_coeff n *⇩R (c * z) ^ n) = (λn. fps_nth (fps_sin c) n * z ^ n)"
by (rule ext) (auto simp: sin_coeff_def fps_sin_def power_mult_distrib scaleR_conv_of_real)
finally show ?thesis by (simp add: sums_iff eval_fps_def)
qed

lemma eval_fps_cos [simp]:
fixes z :: "'a :: {banach, real_normed_field, field_char_0}"
shows "eval_fps (fps_cos c) z = cos (c * z)"
proof -
have "(λn. cos_coeff n *⇩R (c * z) ^ n) sums cos (c * z)" by (rule cos_converges)
also have "(λn. cos_coeff n *⇩R (c * z) ^ n) = (λn. fps_nth (fps_cos c) n * z ^ n)"
by (rule ext) (auto simp: cos_coeff_def fps_cos_def power_mult_distrib scaleR_conv_of_real)
finally show ?thesis by (simp add: sums_iff eval_fps_def)
qed

lemma cos_eq_zero_imp_norm_ge:
assumes "cos (z :: complex) = 0"
shows   "norm z ≥ pi / 2"
proof -
from assms obtain n where "z = complex_of_real ((of_int n + 1 / 2) * pi)"
by (auto simp: cos_eq_0 algebra_simps)
also have "norm … = ¦real_of_int n + 1 / 2¦ * pi"
by (subst norm_of_real) (simp_all add: abs_mult)
also have "real_of_int n + 1 / 2 = of_int (2 * n + 1) / 2" by simp
also have "¦…¦ = of_int ¦2 * n + 1¦ / 2" by (subst abs_divide) simp_all
also have "… * pi = of_int ¦2 * n + 1¦ * (pi / 2)" by simp
also have "… ≥ of_int 1 * (pi / 2)"
by (intro mult_right_mono, subst of_int_le_iff) (auto simp: abs_if)
finally show ?thesis by simp
qed

lemma eval_fps_binomial:
fixes c :: complex
assumes "norm z < 1"
shows   "eval_fps (fps_binomial c) z = (1 + z) powr c"
using gen_binomial_complex[OF assms] by (simp add: sums_iff eval_fps_def)

lemma has_fps_expansion_binomial_complex [fps_expansion_intros]:
fixes c :: complex
shows "(λx. (1 + x) powr c) has_fps_expansion fps_binomial c"
proof -
have *: "eventually (λz::complex. z ∈ eball 0 1) (nhds 0)"
by (intro eventually_nhds_in_open) auto
thus ?thesis
by (auto simp: has_fps_expansion_def eval_fps_binomial fps_conv_radius_binomial
intro!: eventually_mono [OF *])
qed

lemma has_fps_expansion_sin [fps_expansion_intros]:
fixes c :: "'a :: {banach, real_normed_field, field_char_0}"
shows "(λx. sin (c * x)) has_fps_expansion fps_sin c"
by (auto simp: has_fps_expansion_def)

lemma has_fps_expansion_sin' [fps_expansion_intros]:
"(λx::'a :: {banach, real_normed_field}. sin x) has_fps_expansion fps_sin 1"
using has_fps_expansion_sin[of 1] by simp

lemma has_fps_expansion_cos [fps_expansion_intros]:
fixes c :: "'a :: {banach, real_normed_field, field_char_0}"
shows "(λx. cos (c * x)) has_fps_expansion fps_cos c"
by (auto simp: has_fps_expansion_def)

lemma has_fps_expansion_cos' [fps_expansion_intros]:
"(λx::'a :: {banach, real_normed_field}. cos x) has_fps_expansion fps_cos 1"
using has_fps_expansion_cos[of 1] by simp

lemma has_fps_expansion_shift [fps_expansion_intros]:
fixes F :: "'a :: {banach, real_normed_field} fps"
assumes "f has_fps_expansion F" and "n ≤ subdegree F"
assumes "c = fps_nth F n"
shows   "(λx. if x = 0 then c else f x / x ^ n) has_fps_expansion (fps_shift n F)"
proof -
have "eventually (λx. x ∈ eball 0 (fps_conv_radius F)) (nhds 0)"
using assms by (intro eventually_nhds_in_open) (auto simp: has_fps_expansion_def zero_ereal_def)
moreover have "eventually (λx. eval_fps F x = f x) (nhds 0)"
using assms by (auto simp: has_fps_expansion_def)
ultimately have "eventually (λx. eval_fps (fps_shift n F) x =
(if x = 0 then c else f x / x ^ n)) (nhds 0)"
by eventually_elim (auto simp: eval_fps_shift assms)
with assms show ?thesis by (auto simp: has_fps_expansion_def)
qed

lemma has_fps_expansion_divide [fps_expansion_intros]:
fixes F G :: "'a :: {banach, real_normed_field} fps"
assumes "f has_fps_expansion F" and "g has_fps_expansion G" and
"subdegree G ≤ subdegree F" "G ≠ 0"
"c = fps_nth F (subdegree G) / fps_nth G (subdegree G)"
shows   "(λx. if x = 0 then c else f x / g x) has_fps_expansion (F / G)"
proof -
define n where "n = subdegree G"
define F' and G' where "F' = fps_shift n F" and "G' = fps_shift n G"
have "F = F' * fps_X ^ n" "G = G' * fps_X ^ n" unfolding F'_def G'_def n_def
by (rule fps_shift_times_fps_X_power [symmetric] le_refl | fact)+
moreover from assms have "fps_nth G' 0 ≠ 0"
ultimately have FG: "F / G = F' * inverse G'"

have "(λx. (if x = 0 then fps_nth F n else f x / x ^ n) *
inverse (if x = 0 then fps_nth G n else g x / x ^ n)) has_fps_expansion F / G"
(is "?h has_fps_expansion _") unfolding FG F'_def G'_def n_def using ‹G ≠ 0›
by (intro has_fps_expansion_mult has_fps_expansion_inverse
has_fps_expansion_shift assms) auto
also have "?h = (λx. if x = 0 then c else f x / g x)"
using assms(5) unfolding n_def
by (intro ext) (auto split: if_splits simp: field_simps)
finally show ?thesis .
qed

lemma has_fps_expansion_divide' [fps_expansion_intros]:
fixes F G :: "'a :: {banach, real_normed_field} fps"
assumes "f has_fps_expansion F" and "g has_fps_expansion G" and "fps_nth G 0 ≠ 0"
shows   "(λx. f x / g x) has_fps_expansion (F / G)"
proof -
have "(λx. if x = 0 then fps_nth F 0 / fps_nth G 0 else f x / g x) has_fps_expansion (F / G)"
(is "?h has_fps_expansion _") using assms(3) by (intro has_fps_expansion_divide assms) auto
also from assms have "fps_nth F 0 = f 0" "fps_nth G 0 = g 0"
by (auto simp: has_fps_expansion_def eval_fps_at_0 dest: eventually_nhds_x_imp_x)
hence "?h = (λx. f x / g x)" by auto
finally show ?thesis .
qed

lemma has_fps_expansion_tan [fps_expansion_intros]:
fixes c :: "'a :: {banach, real_normed_field, field_char_0}"
shows "(λx. tan (c * x)) has_fps_expansion fps_tan c"
proof -
have "(λx. sin (c * x) / cos (c * x)) has_fps_expansion fps_sin c / fps_cos c"
by (intro fps_expansion_intros) auto
thus ?thesis by (simp add: tan_def fps_tan_def)
qed

lemma has_fps_expansion_tan' [fps_expansion_intros]:
"tan has_fps_expansion fps_tan (1 :: 'a :: {banach, real_normed_field, field_char_0})"
using has_fps_expansion_tan[of 1] by simp

lemma has_fps_expansion_imp_holomorphic:
assumes "f has_fps_expansion F"
obtains s where "open s" "0 ∈ s" "f holomorphic_on s" "⋀z. z ∈ s ⟹ f z = eval_fps F z"
proof -
from assms obtain s where s: "open s" "0 ∈ s" "⋀z. z ∈ s ⟹ eval_fps F z = f z"
unfolding has_fps_expansion_def eventually_nhds by blast
let ?s' = "eball 0 (fps_conv_radius F) ∩ s"
have "eval_fps F holomorphic_on ?s'"
by (intro holomorphic_intros) auto
also have "?this ⟷ f holomorphic_on ?s'"
using s by (intro holomorphic_cong) auto
finally show ?thesis using s assms
by (intro that[of ?s']) (auto simp: has_fps_expansion_def zero_ereal_def)
qed

end```