summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | Manuel Eberl <eberlm@in.tum.de> |

Mon, 21 Aug 2017 20:49:15 +0200 | |

changeset 66480 | 4b8d1df8933b |

parent 66479 | 5c0a3f63057d |

child 66481 | d35f7a9f92e2 |

HOL-Analysis: Convergent FPS and infinite sums

--- a/CONTRIBUTORS Mon Aug 21 19:20:02 2017 +0200 +++ b/CONTRIBUTORS Mon Aug 21 20:49:15 2017 +0200 @@ -14,6 +14,11 @@ Prover IDE improvements. Support for SQL databases in Isabelle/Scala: SQLite and PostgreSQL. +* August 2017: Manuel Eberl, TUM + HOL-Analysis: infinite products over natural numbers, + infinite sums over arbitrary sets, connection between formal + power series and analytic complex functions + * March 2017: Alasdair Armstrong, University of Sheffield and Simon Foster, University of York Fixed-point theory and Galois Connections in HOL-Algebra.

--- a/NEWS Mon Aug 21 19:20:02 2017 +0200 +++ b/NEWS Mon Aug 21 20:49:15 2017 +0200 @@ -215,8 +215,8 @@ * Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has been renamed to bij_swap_compose_bij. INCOMPATIBILITY. -* Theory "HOL-Library.Formal_Power_Series": constants E/L/F have been -renamed to fps_exp/fps_ln/fps_hypergeo to avoid polluting the name +* Theory "HOL-Library.Formal_Power_Series": constants X/E/L/F have been +renamed to fps_X/fps_exp/fps_ln/fps_hypergeo to avoid polluting the name space. INCOMPATIBILITY. * Theory "HOL-Library.FinFun" has been moved to AFP (again).

--- a/src/HOL/Analysis/Analysis.thy Mon Aug 21 19:20:02 2017 +0200 +++ b/src/HOL/Analysis/Analysis.thy Mon Aug 21 20:49:15 2017 +0200 @@ -11,6 +11,7 @@ Bounded_Continuous_Function Function_Topology Infinite_Products + Infinite_Set_Sum Weierstrass_Theorems Polytope Jordan_Curve @@ -18,6 +19,7 @@ Great_Picard Poly_Roots Conformal_Mappings + FPS_Convergence Generalised_Binomial_Theorem Gamma_Function begin

--- a/src/HOL/Analysis/Complex_Transcendental.thy Mon Aug 21 19:20:02 2017 +0200 +++ b/src/HOL/Analysis/Complex_Transcendental.thy Mon Aug 21 20:49:15 2017 +0200 @@ -73,6 +73,10 @@ lemma holomorphic_on_exp [holomorphic_intros]: "exp holomorphic_on s" by (simp add: field_differentiable_within_exp holomorphic_on_def) +lemma holomorphic_on_exp' [holomorphic_intros]: + "f holomorphic_on s \<Longrightarrow> (\<lambda>x. exp (f x)) holomorphic_on s" + using holomorphic_on_compose[OF _ holomorphic_on_exp] by (simp add: o_def) + subsection\<open>Euler and de Moivre formulas.\<close> text\<open>The sine series times @{term i}\<close>

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Analysis/FPS_Convergence.thy Mon Aug 21 20:49:15 2017 +0200 @@ -0,0 +1,1277 @@ +(* + 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 \<open>Convergence of formal power series\<close> +theory FPS_Convergence +imports + Conformal_Mappings + Generalised_Binomial_Theorem + "HOL-Computational_Algebra.Formal_Power_Series" +begin + +subsection \<open>Balls with extended real radius\<close> + +text \<open> + The following is a variant of @{const ball} that also allows an infinite radius. +\<close> +definition eball :: "'a :: metric_space \<Rightarrow> ereal \<Rightarrow> 'a set" where + "eball z r = {z'. ereal (dist z z') < r}" + +lemma in_eball_iff [simp]: "z \<in> eball z0 r \<longleftrightarrow> ereal (dist z0 z) < r" + by (simp add: eball_def) + +lemma eball_ereal [simp]: "eball z (ereal r) = ball z r" + by auto + +lemma eball_inf [simp]: "eball z \<infinity> = UNIV" + by auto + +lemma eball_empty [simp]: "r \<le> 0 \<Longrightarrow> eball z r = {}" +proof safe + fix x assume "r \<le> 0" "x \<in> eball z r" + hence "dist z x < r" by simp + also have "\<dots> \<le> ereal 0" using \<open>r \<le> 0\<close> by (simp add: zero_ereal_def) + finally show "x \<in> {}" by simp +qed + +lemma eball_conv_UNION_balls: + "eball z r = (\<Union>r'\<in>{r'. ereal r' < r}. ball z r')" + by (cases r) (use dense gt_ex in force)+ + +lemma eball_mono: "r \<le> r' \<Longrightarrow> eball z r \<le> eball z r'" + by auto + +lemma ball_eball_mono: "ereal r \<le> r' \<Longrightarrow> ball z r \<le> 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 \<open>Basic properties of convergent power series\<close> + +definition fps_conv_radius :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> ereal" where + "fps_conv_radius f = conv_radius (fps_nth f)" + +definition eval_fps :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> 'a \<Rightarrow> 'a" where + "eval_fps f z = (\<Sum>n. fps_nth f n * z ^ n)" + +definition fps_expansion :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex fps" where + "fps_expansion f z0 = Abs_fps (\<lambda>n. (deriv ^^ n) f z0 / fact n)" + +lemma norm_summable_fps: + fixes f :: "'a :: {banach, real_normed_div_algebra} fps" + shows "norm z < fps_conv_radius f \<Longrightarrow> summable (\<lambda>n. norm (fps_nth f n * z ^ n))" + by (rule abs_summable_in_conv_radius) (simp_all add: fps_conv_radius_def) + +lemma summable_fps: + fixes f :: "'a :: {banach, real_normed_div_algebra} fps" + shows "norm z < fps_conv_radius f \<Longrightarrow> summable (\<lambda>n. fps_nth f n * z ^ n)" + by (rule summable_in_conv_radius) (simp_all add: fps_conv_radius_def) + +lemma sums_eval_fps: + fixes f :: "'a :: {banach, real_normed_div_algebra} fps" + assumes "norm z < fps_conv_radius f" + shows "(\<lambda>n. fps_nth f n * z ^ n) sums eval_fps f z" + using assms unfolding eval_fps_def fps_conv_radius_def + by (intro summable_sums summable_in_conv_radius) simp_all + +lemma + fixes r :: ereal + assumes "f holomorphic_on eball z0 r" + shows conv_radius_fps_expansion: "fps_conv_radius (fps_expansion f z0) \<ge> r" + and eval_fps_expansion: "\<And>z. z \<in> eball z0 r \<Longrightarrow> eval_fps (fps_expansion f z0) (z - z0) = f z" + and eval_fps_expansion': "\<And>z. norm z < r \<Longrightarrow> eval_fps (fps_expansion f z0) z = f (z0 + z)" +proof - + have "(\<lambda>n. fps_nth (fps_expansion f z0) n * (z - z0) ^ n) sums f z" + if "z \<in> ball z0 r'" "ereal r' < r" for z r' + proof - + from that(2) have "ereal r' \<le> r" by simp + from assms(1) and this have "f holomorphic_on ball z0 r'" + by (rule holomorphic_on_subset[OF _ ball_eball_mono]) + from holomorphic_power_series [OF this that(1)] + show ?thesis by (simp add: fps_expansion_def) + qed + hence *: "(\<lambda>n. fps_nth (fps_expansion f z0) n * (z - z0) ^ n) sums f z" + if "z \<in> eball z0 r" for z + using that by (subst (asm) eball_conv_UNION_balls) blast + show "fps_conv_radius (fps_expansion f z0) \<ge> r" unfolding fps_conv_radius_def + proof (rule conv_radius_geI_ex) + fix r' :: real assume r': "r' > 0" "ereal r' < r" + thus "\<exists>z. norm z = r' \<and> summable (\<lambda>n. fps_nth (fps_expansion f z0) n * z ^ n)" + using *[of "z0 + of_real r'"] + by (intro exI[of _ "of_real r'"]) (auto simp: summable_def dist_norm) + qed + show "eval_fps (fps_expansion f z0) (z - z0) = f z" if "z \<in> eball z0 r" for z + using *[OF that] by (simp add: eval_fps_def sums_iff) + show "eval_fps (fps_expansion f z0) z = f (z0 + z)" if "ereal (norm z) < r" for z + using *[of "z0 + z"] and that by (simp add: eval_fps_def sums_iff dist_norm) +qed + +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 \<in> eball 0 (fps_conv_radius f)" + define r where "r = (if fps_conv_radius f = \<infinity> then norm x + 1 else + (norm x + real_of_ereal (fps_conv_radius f)) / 2)" + have r: "norm x < r \<and> 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) (\<lambda>x. \<Sum>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)" + by (simp add: eval_fps_def) + 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 \<subseteq> eball 0 (fps_conv_radius f)" + shows "continuous_on A (\<lambda>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 "((\<lambda>z. \<Sum>n. f n * z ^ n) has_field_derivative (\<Sum>n. diffs f n * z ^ n)) (at z within A)" +proof - + define K where "K = (if conv_radius f = \<infinity> then norm z + 1 + else (norm z + real_of_ereal (conv_radius f)) / 2)" + have K: "norm z < K \<and> ereal K < conv_radius f" + using assms by (cases "conv_radius f") (auto simp: K_def) + have "0 \<le> norm z" by simp + also from K have "\<dots> < K" by simp + finally have K_pos: "K > 0" by simp + + have "summable (\<lambda>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" + by (simp add: fps_eq_iff diffs_def) + finally show ?thesis . +qed + +lemma holomorphic_on_eval_fps [holomorphic_intros]: + fixes z :: "'a :: {banach, real_normed_field}" + assumes "A \<subseteq> 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 \<subseteq> 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 + + +subsection \<open>Lower bounds on radius of convergence\<close> + +lemma fps_conv_radius_deriv: + fixes f :: "'a :: {banach, real_normed_field} fps" + shows "fps_conv_radius (fps_deriv f) \<ge> fps_conv_radius f" + unfolding fps_conv_radius_def +proof (rule conv_radius_geI_ex) + fix r :: real assume r: "r > 0" "ereal r < conv_radius (fps_nth f)" + define K where "K = (if conv_radius (fps_nth f) = \<infinity> then r + 1 + else (real_of_ereal (conv_radius (fps_nth f)) + r) / 2)" + have K: "r < K \<and> ereal K < conv_radius (fps_nth f)" + using r by (cases "conv_radius (fps_nth f)") (auto simp: K_def) + have "summable (\<lambda>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 "\<dots> < conv_radius (fps_nth f)" using K by simp + finally show "summable (\<lambda>n. fps_nth f n * x ^ n)" + by (intro summable_in_conv_radius) auto + qed (insert K r, auto) + also have "\<dots> = (\<lambda>n. fps_nth (fps_deriv f) n * of_real r ^ n)" + by (simp add: fps_deriv_def diffs_def) + finally show "\<exists>z::'a. norm z = r \<and> summable (\<lambda>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" + by (simp add: eval_fps_def) + +lemma fps_conv_radius_norm [simp]: + "fps_conv_radius (Abs_fps (\<lambda>n. norm (fps_nth f n))) = fps_conv_radius f" + by (simp add: fps_conv_radius_def) + +lemma fps_conv_radius_const [simp]: "fps_conv_radius (fps_const c) = \<infinity>" +proof - + have "fps_conv_radius (fps_const c) = conv_radius (\<lambda>_. 0 :: 'a)" + unfolding fps_conv_radius_def + by (intro conv_radius_cong eventually_mono[OF eventually_gt_at_top[of 0]]) auto + thus ?thesis by simp +qed + +lemma fps_conv_radius_0 [simp]: "fps_conv_radius 0 = \<infinity>" + by (simp only: fps_const_0_eq_0 [symmetric] fps_conv_radius_const) + +lemma fps_conv_radius_1 [simp]: "fps_conv_radius 1 = \<infinity>" + by (simp only: fps_const_1_eq_1 [symmetric] fps_conv_radius_const) + +lemma fps_conv_radius_numeral [simp]: "fps_conv_radius (numeral n) = \<infinity>" + by (simp add: numeral_fps_const) + +lemma fps_conv_radius_fps_X_power [simp]: "fps_conv_radius (fps_X ^ n) = \<infinity>" +proof - + have "fps_conv_radius (fps_X ^ n :: 'a fps) = conv_radius (\<lambda>_. 0 :: 'a)" + unfolding fps_conv_radius_def + 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 + +lemma fps_conv_radius_fps_X [simp]: "fps_conv_radius fps_X = \<infinity>" + using fps_conv_radius_fps_X_power[of 1] by (simp only: power_one_right) + +lemma fps_conv_radius_shift [simp]: + "fps_conv_radius (fps_shift n f) = fps_conv_radius f" + by (simp add: fps_conv_radius_def fps_shift_def conv_radius_shift) + +lemma fps_conv_radius_cmult_left: + "c \<noteq> 0 \<Longrightarrow> fps_conv_radius (fps_const c * f) = fps_conv_radius f" + unfolding fps_conv_radius_def by (simp add: conv_radius_cmult_left) + +lemma fps_conv_radius_cmult_right: + "c \<noteq> 0 \<Longrightarrow> fps_conv_radius (f * fps_const c) = fps_conv_radius f" + unfolding fps_conv_radius_def by (simp add: conv_radius_cmult_right) + +lemma fps_conv_radius_uminus [simp]: + "fps_conv_radius (-f) = fps_conv_radius f" + using fps_conv_radius_cmult_left[of "-1" f] + by (simp add: fps_const_neg [symmetric] del: fps_const_neg) + +lemma fps_conv_radius_add: "fps_conv_radius (f + g) \<ge> min (fps_conv_radius f) (fps_conv_radius g)" + unfolding fps_conv_radius_def using conv_radius_add_ge[of "fps_nth f" "fps_nth g"] + by simp + +lemma fps_conv_radius_diff: "fps_conv_radius (f - g) \<ge> min (fps_conv_radius f) (fps_conv_radius g)" + using fps_conv_radius_add[of f "-g"] by simp + +lemma fps_conv_radius_mult: "fps_conv_radius (f * g) \<ge> min (fps_conv_radius f) (fps_conv_radius g)" + using conv_radius_mult_ge[of "fps_nth f" "fps_nth g"] + by (simp add: fps_mult_nth fps_conv_radius_def atLeast0AtMost) + +lemma fps_conv_radius_power: "fps_conv_radius (f ^ n) \<ge> fps_conv_radius f" +proof (induction n) + case (Suc n) + hence "fps_conv_radius f \<le> min (fps_conv_radius f) (fps_conv_radius (f ^ n))" + by simp + also have "\<dots> \<le> fps_conv_radius (f * f ^ n)" + by (rule fps_conv_radius_mult) + 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 "\<delta> > 0" + and summable: "summable (\<lambda>n. norm (fps_nth f (Suc n)) * \<delta> ^ Suc n)" + and le: "(\<Sum>n. norm (fps_nth f (Suc n)) * \<delta> ^ Suc n) \<le> 1" + shows "norm (natfun_inverse f n) \<le> inverse (\<delta> ^ n)" +proof (induction n rule: less_induct) + case (less m) + show ?case + proof (cases m) + case 0 + thus ?thesis using assms by (simp add: divide_simps norm_inverse norm_divide) + next + case [simp]: (Suc n) + have "norm (natfun_inverse f (Suc n)) = + norm (\<Sum>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 \<le> (\<Sum>i = Suc 0..Suc n. norm (fps_nth f i * natfun_inverse f (Suc n - i)))" + by (rule norm_sum) + also have "\<dots> \<le> (\<Sum>i = Suc 0..Suc n. norm (fps_nth f i) / \<delta> ^ (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))" + by (simp add: norm_mult) + also have "\<dots> \<le> norm (fps_nth f i) * inverse (\<delta> ^ (Suc n - i))" + using 1 by (intro mult_left_mono less.IH) auto + also have "\<dots> = norm (fps_nth f i) / \<delta> ^ (Suc n - i)" + by (simp add: divide_simps) + finally show ?case . + qed + also have "\<dots> = (\<Sum>i = Suc 0..Suc n. norm (fps_nth f i) * \<delta> ^ i) / \<delta> ^ Suc n" + by (subst sum_divide_distrib, rule sum.cong) + (insert \<open>\<delta> > 0\<close>, auto simp: field_simps power_diff) + also have "(\<Sum>i = Suc 0..Suc n. norm (fps_nth f i) * \<delta> ^ i) = + (\<Sum>i=0..n. norm (fps_nth f (Suc i)) * \<delta> ^ (Suc i))" + by (subst sum.atLeast_Suc_atMost_Suc_shift) simp_all + also have "{0..n} = {..<Suc n}" by auto + also have "(\<Sum>i< Suc n. norm (fps_nth f (Suc i)) * \<delta> ^ (Suc i)) \<le> + (\<Sum>n. norm (fps_nth f (Suc n)) * \<delta> ^ (Suc n))" + using \<open>\<delta> > 0\<close> by (intro sum_le_suminf ballI mult_nonneg_nonneg zero_le_power summable) auto + also have "\<dots> \<le> 1" by fact + finally show ?thesis using \<open>\<delta> > 0\<close> + by (simp add: divide_right_mono divide_simps) + qed +qed + +private lemma fps_conv_radius_inverse_pos_aux: + 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 - + let ?R = "fps_conv_radius f" + define h where "h = Abs_fps (\<lambda>n. norm (fps_nth f n))" + have [simp]: "fps_conv_radius h = ?R" by (simp add: h_def) + have "continuous_on (eball 0 (fps_conv_radius h)) (eval_fps h)" + by (intro continuous_on_eval_fps) + hence *: "open (eval_fps h -` A \<inter> eball 0 ?R)" if "open A" for A + using that by (subst (asm) continuous_on_open_vimage) auto + have "open (eval_fps h -` {..<2} \<inter> eball 0 ?R)" + by (rule *) auto + moreover have "0 \<in> eval_fps h -` {..<2} \<inter> eball 0 ?R" + using assms by (auto simp: eball_def zero_ereal_def eval_fps_at_0 h_def) + ultimately obtain \<epsilon> where \<epsilon>: "\<epsilon> > 0" "ball 0 \<epsilon> \<subseteq> eval_fps h -` {..<2} \<inter> eball 0 ?R" + by (subst (asm) open_contains_ball_eq) blast+ + + define \<delta> where "\<delta> = real_of_ereal (min (ereal \<epsilon> / 2) (?R / 2))" + have \<delta>: "0 < \<delta> \<and> \<delta> < \<epsilon> \<and> ereal \<delta> < ?R" + using \<open>\<epsilon> > 0\<close> and assms by (cases ?R) (auto simp: \<delta>_def min_def) + + have summable: "summable (\<lambda>n. norm (fps_nth f n) * \<delta> ^ n)" + using \<delta> by (intro summable_in_conv_radius) (simp_all add: fps_conv_radius_def) + hence "(\<lambda>n. norm (fps_nth f n) * \<delta> ^ n) sums eval_fps h \<delta>" + by (simp add: eval_fps_def summable_sums h_def) + hence "(\<lambda>n. norm (fps_nth f (Suc n)) * \<delta> ^ Suc n) sums (eval_fps h \<delta> - 1)" + by (subst sums_Suc_iff) (auto simp: assms) + moreover { + from \<delta> have "\<delta> \<in> ball 0 \<epsilon>" by auto + also have "\<dots> \<subseteq> eval_fps h -` {..<2} \<inter> eball 0 ?R" by fact + finally have "eval_fps h \<delta> < 2" by simp + } + ultimately have le: "(\<Sum>n. norm (fps_nth f (Suc n)) * \<delta> ^ Suc n) \<le> 1" + by (simp add: sums_iff) + from summable have summable: "summable (\<lambda>n. norm (fps_nth f (Suc n)) * \<delta> ^ Suc n)" + by (subst summable_Suc_iff) + + have "0 < \<delta>" using \<delta> by blast + also have "\<delta> = inverse (limsup (\<lambda>n. ereal (inverse \<delta>)))" + using \<delta> by (subst Limsup_const) auto + also have "\<dots> \<le> conv_radius (natfun_inverse f)" + unfolding conv_radius_def + 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)) \<le> root n (inverse (\<delta> ^ n))" + using n assms \<delta> le summable + by (intro real_root_le_mono natfun_inverse_bound) auto + also have "\<dots> = inverse \<delta>" + using n \<delta> by (simp add: power_inverse [symmetric] real_root_pos2) + finally show "ereal (inverse \<delta>) \<ge> ereal (root n (norm (natfun_inverse f n)))" + by (subst ereal_less_eq) + next + have "0 = limsup (\<lambda>n. 0::ereal)" + by (rule Limsup_const [symmetric]) auto + also have "\<dots> \<le> limsup (\<lambda>n. ereal (root n (norm (natfun_inverse f n))))" + by (intro Limsup_mono) (auto simp: real_root_ge_zero) + finally show "0 \<le> \<dots>" by simp + qed + also have "\<dots> = fps_conv_radius (inverse f)" + using assms by (simp add: fps_conv_radius_def fps_inverse_def) + finally show ?thesis by (simp add: zero_ereal_def) +qed + +lemma fps_conv_radius_inverse_pos: + fixes f :: "'a :: {banach, real_normed_field} fps" + assumes "fps_nth f 0 \<noteq> 0" and "fps_conv_radius f > 0" + shows "fps_conv_radius (inverse f) > 0" +proof - + let ?c = "fps_nth f 0" + have "fps_conv_radius (inverse f) = fps_conv_radius (fps_const ?c * inverse f)" + 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 \<dots> > 0" using assms + by (intro fps_conv_radius_inverse_pos_aux) + (auto simp: fps_conv_radius_cmult_left) + finally show ?thesis . +qed + +end + +lemma fps_conv_radius_exp [simp]: + fixes c :: "'a :: {banach, real_normed_field}" + shows "fps_conv_radius (fps_exp c) = \<infinity>" + unfolding fps_conv_radius_def +proof (rule conv_radius_inftyI'') + fix z :: 'a + have "(\<lambda>n. norm (c * z) ^ n /\<^sub>R fact n) sums exp (norm (c * z))" + by (rule exp_converges) + also have "(\<lambda>n. norm (c * z) ^ n /\<^sub>R fact n) = (\<lambda>n. norm (fps_nth (fps_exp c) n * z ^ n))" + by (rule ext) (simp add: norm_divide norm_mult norm_power divide_simps power_mult_distrib) + finally have "summable \<dots>" by (simp add: sums_iff) + thus "summable (\<lambda>n. fps_nth (fps_exp c) n * z ^ n)" + by (rule summable_norm_cancel) +qed + + +subsection \<open>Evaluating power series\<close> + +lemma 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) + +lemma fps_nth_conv_deriv: + fixes f :: "complex fps" + assumes "fps_conv_radius f > 0" + 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 (\<lambda>z::complex. z \<in> eball 0 (fps_conv_radius f)) (nhds 0)" + using Suc.prems by (intro eventually_nhds_in_open) (auto simp: zero_ereal_def) + hence "eventually (\<lambda>z. deriv (eval_fps f) z = eval_fps (fps_deriv f) z) (nhds 0)" + by eventually_elim (simp add: eval_fps_deriv) + 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 "\<dots> / fact n = fps_nth (fps_deriv f) n" + using Suc.prems fps_conv_radius_deriv[of f] + by (intro Suc.IH [symmetric]) auto + also have "\<dots> / 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: divide_simps) +qed + +lemma eval_fps_eqD: + fixes f g :: "complex fps" + assumes "fps_conv_radius f > 0" "fps_conv_radius g > 0" + assumes "eventually (\<lambda>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 "\<dots> / 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 "(\<lambda>n::nat. if n \<in> {0} then c else 0) sums (\<Sum>n\<in>{0::nat}. c)" + by (rule sums_If_finite_set) auto + also have "?this \<longleftrightarrow> (\<lambda>n::nat. fps_nth (fps_const c) n * z ^ n) sums (\<Sum>n\<in>{0::nat}. c)" + by (intro sums_cong) auto + also have "(\<Sum>n\<in>{0::nat}. c) = c" + by simp + finally show ?thesis + by (simp add: eval_fps_def sums_iff) +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 "(\<lambda>n::nat. if n \<in> {m} then z ^ n else 0 :: 'a) sums (\<Sum>n\<in>{m::nat}. z ^ n)" + by (rule sums_If_finite_set) auto + also have "?this \<longleftrightarrow> (\<lambda>n::nat. fps_nth (fps_X ^ m) n * z ^ n) sums (\<Sum>n\<in>{m::nat}. z ^ n)" + by (intro sums_cong) (auto simp: fps_X_power_iff) + also have "(\<Sum>n\<in>{m::nat}. z ^ n) = z ^ m" + by simp + finally show ?thesis + by (simp add: eval_fps_def sums_iff) +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) + +lemma eval_fps_add: + fixes f g :: "'a :: {banach, real_normed_div_algebra} fps" + assumes "norm z < fps_conv_radius f" "norm z < fps_conv_radius g" + 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" + assumes "norm z < fps_conv_radius f" "norm z < fps_conv_radius g" + 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" + assumes "norm z < fps_conv_radius f" "norm z < fps_conv_radius g" + shows "eval_fps (f * g) z = eval_fps f z * eval_fps g z" +proof - + have "eval_fps f z * eval_fps g z = + (\<Sum>k. \<Sum>i\<le>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 (\<lambda>k. norm (fps_nth f k * z ^ k))" "summable (\<lambda>k. norm (fps_nth g k * z ^ k))" + by (rule norm_summable_fps assms)+ + qed (simp_all add: algebra_simps) + also have "(\<lambda>k. \<Sum>i\<le>k. fps_nth f i * fps_nth g (k - i) * (z ^ i * z ^ (k - i))) = + (\<lambda>k. \<Sum>i\<le>k. fps_nth f i * fps_nth g (k - i) * z ^ k)" + by (intro ext sum.cong refl) (simp add: power_add [symmetric]) + also have "suminf \<dots> = 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 \<le> 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" + by (simp add: fps_shift_times_fps_X_power) + finally show ?thesis using False by (simp add: field_simps) +qed (simp_all add: eval_fps_at_0) + +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 divide_simps power_mult_distrib) + +lemma + fixes f :: "complex fps" and r :: ereal + assumes "\<And>z. ereal (norm z) < r \<Longrightarrow> eval_fps f z \<noteq> 0" + shows fps_conv_radius_inverse: "fps_conv_radius (inverse f) \<ge> min r (fps_conv_radius f)" + and eval_fps_inverse: "\<And>z. ereal (norm z) < fps_conv_radius f \<Longrightarrow> ereal (norm z) < r \<Longrightarrow> + eval_fps (inverse f) z = inverse (eval_fps f z)" +proof - + define R where "R = min (fps_conv_radius f) r" + have *: "fps_conv_radius (inverse f) \<ge> min r (fps_conv_radius f) \<and> + (\<forall>z\<in>eball 0 (min (fps_conv_radius f) r). eval_fps (inverse f) z = inverse (eval_fps f z))" + proof (cases "min r (fps_conv_radius f) > 0") + case True + define f' where "f' = fps_expansion (\<lambda>z. inverse (eval_fps f z)) 0" + have holo: "(\<lambda>z. inverse (eval_fps f z)) holomorphic_on eball 0 (min r (fps_conv_radius f))" + using assms by (intro holomorphic_intros) auto + from holo have radius: "fps_conv_radius f' \<ge> min r (fps_conv_radius f)" + unfolding f'_def by (rule conv_radius_fps_expansion) + have eval_f': "eval_fps f' z = inverse (eval_fps f z)" + if "norm z < fps_conv_radius f" "norm z < r" for z + using that unfolding f'_def by (subst eval_fps_expansion'[OF holo]) auto + + have "f * f' = 1" + proof (rule eval_fps_eqD) + from radius and True have "0 < min (fps_conv_radius f) (fps_conv_radius f')" + by (auto simp: min_def split: if_splits) + also have "\<dots> \<le> fps_conv_radius (f * f')" by (rule fps_conv_radius_mult) + finally show "\<dots> > 0" . + next + from True have "R > 0" by (auto simp: R_def) + hence "eventually (\<lambda>z. z \<in> eball 0 R) (nhds 0)" + by (intro eventually_nhds_in_open) (auto simp: zero_ereal_def) + thus "eventually (\<lambda>z. eval_fps (f * f') z = eval_fps 1 z) (nhds 0)" + proof eventually_elim + case (elim z) + hence "eval_fps (f * f') z = eval_fps f z * eval_fps f' z" + using radius by (intro eval_fps_mult) + (auto simp: R_def min_def split: if_splits intro: less_trans) + also have "eval_fps f' z = inverse (eval_fps f z)" + using elim by (intro eval_f') (auto simp: R_def) + also from elim have "eval_fps f z \<noteq> 0" + by (intro assms) (auto simp: R_def) + hence "eval_fps f z * inverse (eval_fps f z) = eval_fps 1 z" + by simp + finally show "eval_fps (f * f') z = eval_fps 1 z" . + qed + qed simp_all + hence "f' = inverse f" + by (intro fps_inverse_unique [symmetric]) (simp_all add: mult_ac) + with eval_f' and radius show ?thesis by simp + next + case False + hence *: "eball 0 R = {}" + by (intro eball_empty) (auto simp: R_def min_def split: if_splits) + show ?thesis + proof safe + from False have "min r (fps_conv_radius f) \<le> 0" + by (simp add: min_def) + also have "0 \<le> fps_conv_radius (inverse f)" + by (simp add: fps_conv_radius_def conv_radius_nonneg) + finally show "min r (fps_conv_radius f) \<le> \<dots>" . + qed (unfold * [unfolded R_def], auto) + qed + + from * show "fps_conv_radius (inverse f) \<ge> min r (fps_conv_radius f)" by blast + from * show "eval_fps (inverse f) z = inverse (eval_fps f z)" + if "ereal (norm z) < fps_conv_radius f" "ereal (norm z) < r" for z + using that by auto +qed + +lemma + fixes f g :: "complex fps" and r :: ereal + defines "R \<equiv> Min {r, fps_conv_radius f, fps_conv_radius g}" + assumes "fps_conv_radius f > 0" "fps_conv_radius g > 0" "r > 0" + assumes nz: "\<And>z. z \<in> eball 0 r \<Longrightarrow> eval_fps g z \<noteq> 0" + shows fps_conv_radius_divide': "fps_conv_radius (f / g) \<ge> R" + and eval_fps_divide': + "ereal (norm z) < R \<Longrightarrow> eval_fps (f / g) z = eval_fps f z / eval_fps g z" +proof - + from nz[of 0] and \<open>r > 0\<close> have nz': "fps_nth g 0 \<noteq> 0" + by (auto simp: eval_fps_at_0 zero_ereal_def) + have "R \<le> min r (fps_conv_radius g)" + by (auto simp: R_def intro: min.coboundedI2) + also have "min r (fps_conv_radius g) \<le> fps_conv_radius (inverse g)" + by (intro fps_conv_radius_inverse assms) (auto simp: zero_ereal_def) + finally have radius: "fps_conv_radius (inverse g) \<ge> R" . + have "R \<le> min (fps_conv_radius f) (fps_conv_radius (inverse g))" + by (intro radius min.boundedI) (auto simp: R_def intro: min.coboundedI1 min.coboundedI2) + also have "\<dots> \<le> fps_conv_radius (f * inverse g)" + by (rule fps_conv_radius_mult) + also have "f * inverse g = f / g" + by (intro fps_divide_unit [symmetric] nz') + finally show "fps_conv_radius (f / g) \<ge> R" . + + assume z: "ereal (norm z) < R" + have "eval_fps (f * inverse g) z = eval_fps f z * eval_fps (inverse g) z" + using radius by (intro eval_fps_mult less_le_trans[OF z]) + (auto simp: R_def intro: min.coboundedI1 min.coboundedI2) + also have "eval_fps (inverse g) z = inverse (eval_fps g z)" using \<open>r > 0\<close> + by (intro eval_fps_inverse[where r = r] less_le_trans[OF z] nz) + (auto simp: R_def intro: min.coboundedI1 min.coboundedI2) + also have "f * inverse g = f / g" by fact + finally show "eval_fps (f / g) z = eval_fps f z / eval_fps g z" by (simp add: divide_simps) +qed + +lemma + fixes f g :: "complex fps" and r :: ereal + defines "R \<equiv> Min {r, fps_conv_radius f, fps_conv_radius g}" + assumes "subdegree g \<le> subdegree f" + assumes "fps_conv_radius f > 0" "fps_conv_radius g > 0" "r > 0" + assumes "\<And>z. z \<in> eball 0 r \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> eval_fps g z \<noteq> 0" + shows fps_conv_radius_divide: "fps_conv_radius (f / g) \<ge> R" + and eval_fps_divide: + "ereal (norm z) < R \<Longrightarrow> c = fps_nth f (subdegree g) / fps_nth g (subdegree g) \<Longrightarrow> + eval_fps (f / g) z = (if z = 0 then c else eval_fps f z / eval_fps g z)" +proof - + define f' g' where "f' = fps_shift (subdegree g) f" and "g' = fps_shift (subdegree g) g" + have f_eq: "f = f' * fps_X ^ subdegree g" and g_eq: "g = g' * fps_X ^ subdegree g" + unfolding f'_def g'_def by (rule subdegree_decompose' le_refl | fact)+ + have subdegree: "subdegree f' = subdegree f - subdegree g" "subdegree g' = 0" + using assms(2) by (simp_all add: f'_def g'_def) + have [simp]: "fps_conv_radius f' = fps_conv_radius f" "fps_conv_radius g' = fps_conv_radius g" + by (simp_all add: f'_def g'_def) + have [simp]: "fps_nth f' 0 = fps_nth f (subdegree g)" + "fps_nth g' 0 = fps_nth g (subdegree g)" by (simp_all add: f'_def g'_def) + have g_nz: "g \<noteq> 0" + proof - + define z :: complex where "z = (if r = \<infinity> then 1 else of_real (real_of_ereal r / 2))" + from \<open>r > 0\<close> have "z \<in> eball 0 r" + by (cases r) (auto simp: z_def eball_def) + moreover have "z \<noteq> 0" using \<open>r > 0\<close> + by (cases r) (auto simp: z_def) + ultimately have "eval_fps g z \<noteq> 0" by (rule assms(6)) + thus "g \<noteq> 0" by auto + qed + have fg: "f / g = f' * inverse g'" + by (subst f_eq, subst (2) g_eq) (insert g_nz, simp add: fps_divide_unit) + + have g'_nz: "eval_fps g' z \<noteq> 0" if z: "norm z < min r (fps_conv_radius g)" for z + proof (cases "z = 0") + case False + with assms and z have "eval_fps g z \<noteq> 0" by auto + also from z have "eval_fps g z = eval_fps g' z * z ^ subdegree g" + by (subst g_eq) (auto simp: eval_fps_mult) + finally show ?thesis by auto + qed (insert \<open>g \<noteq> 0\<close>, auto simp: g'_def eval_fps_at_0) + + have "R \<le> min (min r (fps_conv_radius g)) (fps_conv_radius g')" + by (auto simp: R_def min.coboundedI1 min.coboundedI2) + also have "\<dots> \<le> fps_conv_radius (inverse g')" + using g'_nz by (rule fps_conv_radius_inverse) + finally have conv_radius_inv: "R \<le> fps_conv_radius (inverse g')" . + hence "R \<le> fps_conv_radius (f' * inverse g')" + by (intro order.trans[OF _ fps_conv_radius_mult]) + (auto simp: R_def intro: min.coboundedI1 min.coboundedI2) + thus "fps_conv_radius (f / g) \<ge> R" by (simp add: fg) + + fix z c :: complex assume z: "ereal (norm z) < R" + assume c: "c = fps_nth f (subdegree g) / fps_nth g (subdegree g)" + show "eval_fps (f / g) z = (if z = 0 then c else eval_fps f z / eval_fps g z)" + proof (cases "z = 0") + case False + from z and conv_radius_inv have "ereal (norm z) < fps_conv_radius (inverse g')" + by simp + with z have "eval_fps (f / g) z = eval_fps f' z * eval_fps (inverse g') z" + unfolding fg by (subst eval_fps_mult) (auto simp: R_def) + also have "eval_fps (inverse g') z = inverse (eval_fps g' z)" + using z by (intro eval_fps_inverse[of "min r (fps_conv_radius g')"] g'_nz) (auto simp: R_def) + also have "eval_fps f' z * \<dots> = eval_fps f z / eval_fps g z" + using z False assms(2) by (simp add: f'_def g'_def eval_fps_shift R_def) + finally show ?thesis using False by simp + qed (simp_all add: eval_fps_at_0 fg field_simps c) +qed + + +subsection \<open>Power series expansion of complex functions\<close> + +text \<open> + 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. + + More concrete statements about the radius of convergence can usually be made, but for + 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. +\<close> +definition has_fps_expansion :: "('a :: {banach,real_normed_div_algebra} \<Rightarrow> 'a) \<Rightarrow> 'a fps \<Rightarrow> bool" + (infixl "has'_fps'_expansion" 60) + where "(f has_fps_expansion F) \<longleftrightarrow> + fps_conv_radius F > 0 \<and> eventually (\<lambda>z. eval_fps F z = f z) (nhds 0)" + +named_theorems fps_expansion_intros + +lemma fps_nth_fps_expansion: + fixes f :: "complex \<Rightarrow> 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_fps_expansion [intro]: + assumes "open A" "0 \<in> A" "f holomorphic_on A" + shows "f has_fps_expansion fps_expansion f 0" +proof - + from assms(1,2) obtain r where r: "r > 0 " "ball 0 r \<subseteq> A" + by (auto simp: open_contains_ball) + have holo: "f holomorphic_on eball 0 (ereal r)" + using r(2) and assms(3) by auto + from r(1) have "0 < ereal r" by simp + also have "r \<le> fps_conv_radius (fps_expansion f 0)" + using holo by (intro conv_radius_fps_expansion) auto + finally have "\<dots> > 0" . + moreover have "eventually (\<lambda>z. z \<in> ball 0 r) (nhds 0)" + using r(1) by (intro eventually_nhds_in_open) auto + hence "eventually (\<lambda>z. eval_fps (fps_expansion f 0) z = f z) (nhds 0)" + by eventually_elim (subst eval_fps_expansion'[OF holo], auto) + ultimately show ?thesis using r(1) by (auto simp: has_fps_expansion_def) +qed + +lemma has_fps_expansion_const [simp, intro, fps_expansion_intros]: + "(\<lambda>_. c) has_fps_expansion fps_const c" + by (auto simp: has_fps_expansion_def) + +lemma has_fps_expansion_0 [simp, intro, fps_expansion_intros]: + "(\<lambda>_. 0) has_fps_expansion 0" + by (auto simp: has_fps_expansion_def) + +lemma has_fps_expansion_1 [simp, intro, fps_expansion_intros]: + "(\<lambda>_. 1) has_fps_expansion 1" + by (auto simp: has_fps_expansion_def) + +lemma has_fps_expansion_numeral [simp, intro, fps_expansion_intros]: + "(\<lambda>_. numeral n) has_fps_expansion numeral n" + by (auto simp: has_fps_expansion_def) + +lemma has_fps_expansion_fps_X_power [fps_expansion_intros]: + "(\<lambda>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]: + "(\<lambda>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 "(\<lambda>x. c * f x) has_fps_expansion fps_const c * F" +proof (cases "c = 0") + case False + from assms have "eventually (\<lambda>z. z \<in> 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 (\<lambda>z. eval_fps F z = f z) (nhds 0)" + by (auto simp: has_fps_expansion_def) + ultimately have "eventually (\<lambda>z. eval_fps (fps_const c * F) z = c * f z) (nhds 0)" + by eventually_elim (simp_all add: eval_fps_mult) + with assms and False show ?thesis + by (auto simp: has_fps_expansion_def fps_conv_radius_cmult_left) +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 "(\<lambda>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 + by (simp add: mult.commute) +qed + +lemma has_fps_expansion_minus [fps_expansion_intros]: + assumes "f has_fps_expansion F" + shows "(\<lambda>x. - f x) has_fps_expansion -F" +proof - + from assms have "eventually (\<lambda>x. x \<in> 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 (\<lambda>x. eval_fps F x = f x) (nhds 0)" + by (auto simp: has_fps_expansion_def) + ultimately have "eventually (\<lambda>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 + +lemma has_fps_expansion_add [fps_expansion_intros]: + assumes "f has_fps_expansion F" "g has_fps_expansion G" + shows "(\<lambda>x. f x + g x) has_fps_expansion F + G" +proof - + from assms have "0 < min (fps_conv_radius F) (fps_conv_radius G)" + by (auto simp: has_fps_expansion_def) + also have "\<dots> \<le> fps_conv_radius (F + G)" + by (rule fps_conv_radius_add) + finally have radius: "\<dots> > 0" . + + from assms have "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius F)) (nhds 0)" + "eventually (\<lambda>x. x \<in> 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 (\<lambda>x. eval_fps F x = f x) (nhds 0)" + and "eventually (\<lambda>x. eval_fps G x = g x) (nhds 0)" + using assms by (auto simp: has_fps_expansion_def) + ultimately have "eventually (\<lambda>x. eval_fps (F + G) x = f x + g x) (nhds 0)" + by eventually_elim (auto simp: eval_fps_add) + 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 "(\<lambda>x. f x - g x) has_fps_expansion F - G" + using has_fps_expansion_add[of f F "\<lambda>x. - g x" "-G"] assms + by (simp add: has_fps_expansion_minus) + +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 "(\<lambda>x. f x * g x) has_fps_expansion F * G" +proof - + from assms have "0 < min (fps_conv_radius F) (fps_conv_radius G)" + by (auto simp: has_fps_expansion_def) + also have "\<dots> \<le> fps_conv_radius (F * G)" + by (rule fps_conv_radius_mult) + finally have radius: "\<dots> > 0" . + + from assms have "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius F)) (nhds 0)" + "eventually (\<lambda>x. x \<in> 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 (\<lambda>x. eval_fps F x = f x) (nhds 0)" + and "eventually (\<lambda>x. eval_fps G x = g x) (nhds 0)" + using assms by (auto simp: has_fps_expansion_def) + ultimately have "eventually (\<lambda>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 \<noteq> 0" + shows "(\<lambda>x. inverse (f x)) has_fps_expansion inverse F" +proof - + have radius: "fps_conv_radius (inverse F) > 0" + using assms unfolding has_fps_expansion_def + by (intro fps_conv_radius_inverse_pos) auto + let ?R = "min (fps_conv_radius F) (fps_conv_radius (inverse F))" + from assms radius + have "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius F)) (nhds 0)" + "eventually (\<lambda>x. x \<in> 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 (\<lambda>z. eval_fps F z = f z) (nhds 0)" + using assms by (auto simp: has_fps_expansion_def) + ultimately have "eventually (\<lambda>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: divide_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 "(\<lambda>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]: + "(\<lambda>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]: + "(\<lambda>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 (\<lambda>z. z \<in> 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 (\<lambda>z. eval_fps F z = f z) (nhds 0)" + by (auto simp: has_fps_expansion_def) + then obtain s where "open s" "0 \<in> s" and s: "\<And>w. w \<in> s \<Longrightarrow> eval_fps F w = f w" + by (auto simp: eventually_nhds) + hence "eventually (\<lambda>w. w \<in> s) (nhds 0)" + by (intro eventually_nhds_in_open) auto + ultimately have "eventually (\<lambda>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" + by (simp add: eval_fps_deriv) + also have "eventually (\<lambda>w. w \<in> s) (nhds z)" + using elim and \<open>open s\<close> by (intro eventually_nhds_in_open) auto + hence "eventually (\<lambda>w. eval_fps F w = f w) (nhds z)" + by eventually_elim (simp add: s) + 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 + +lemma fps_conv_radius_binomial: + fixes c :: "'a :: {real_normed_field,banach}" + shows "fps_conv_radius (fps_binomial c) = (if c \<in> \<nat> then \<infinity> else 1)" + unfolding fps_conv_radius_def by (simp add: conv_radius_gchoose) + +lemma fps_conv_radius_ln: + fixes c :: "'a :: {banach, real_normed_field, field_char_0}" + shows "fps_conv_radius (fps_ln c) = (if c = 0 then \<infinity> else 1)" +proof (cases "c = 0") + case False + have "conv_radius (\<lambda>n. 1 / of_nat n :: 'a) = 1" + proof (rule conv_radius_ratio_limit_nonzero) + show "(\<lambda>n. norm (1 / of_nat n :: 'a) / norm (1 / of_nat (Suc n) :: 'a)) \<longlonglongrightarrow> 1" + using LIMSEQ_Suc_n_over_n by (simp add: norm_divide del: of_nat_Suc) + qed auto + also have "conv_radius (\<lambda>n. 1 / of_nat n :: 'a) = + conv_radius (\<lambda>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]]) + (simp add: norm_mult norm_divide norm_power) + finally show ?thesis using False unfolding fps_ln_def + by (subst fps_conv_radius_cmult_left) (simp_all add: fps_conv_radius_def) +qed (auto simp: fps_ln_def) + +lemma fps_conv_radius_ln_nonzero [simp]: + assumes "c \<noteq> (0 :: 'a :: {banach,real_normed_field,field_char_0})" + shows "fps_conv_radius (fps_ln c) = 1" + using assms by (simp add: fps_conv_radius_ln) + +lemma fps_conv_radius_sin [simp]: + fixes c :: "'a :: {banach, real_normed_field, field_char_0}" + shows "fps_conv_radius (fps_sin c) = \<infinity>" +proof (cases "c = 0") + case False + have "\<infinity> = conv_radius (\<lambda>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 "\<dots> / norm c = conv_radius (\<lambda>n. c ^ n * of_real (sin_coeff n) :: 'a)" + using False by (subst conv_radius_mult_power) auto + also have "\<dots> = fps_conv_radius (fps_sin c)" unfolding fps_conv_radius_def + by (rule conv_radius_cong_weak) (auto simp add: fps_sin_def sin_coeff_def) + finally show ?thesis by simp +qed simp_all + +lemma fps_conv_radius_cos [simp]: + fixes c :: "'a :: {banach, real_normed_field, field_char_0}" + shows "fps_conv_radius (fps_cos c) = \<infinity>" +proof (cases "c = 0") + case False + have "\<infinity> = conv_radius (\<lambda>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 "\<dots> / norm c = conv_radius (\<lambda>n. c ^ n * of_real (cos_coeff n) :: 'a)" + using False by (subst conv_radius_mult_power) auto + also have "\<dots> = fps_conv_radius (fps_cos c)" unfolding fps_conv_radius_def + by (rule conv_radius_cong_weak) (auto simp add: fps_cos_def cos_coeff_def) + 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 "(\<lambda>n. sin_coeff n *\<^sub>R (c * z) ^ n) sums sin (c * z)" by (rule sin_converges) + also have "(\<lambda>n. sin_coeff n *\<^sub>R (c * z) ^ n) = (\<lambda>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 "(\<lambda>n. cos_coeff n *\<^sub>R (c * z) ^ n) sums cos (c * z)" by (rule cos_converges) + also have "(\<lambda>n. cos_coeff n *\<^sub>R (c * z) ^ n) = (\<lambda>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 \<ge> 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 \<dots> = \<bar>real_of_int n + 1 / 2\<bar> * 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 "\<bar>\<dots>\<bar> = of_int \<bar>2 * n + 1\<bar> / 2" by (subst abs_divide) simp_all + also have "\<dots> * pi = of_int \<bar>2 * n + 1\<bar> * (pi / 2)" by simp + also have "\<dots> \<ge> 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 fps_conv_radius_tan: + fixes c :: complex + assumes "c \<noteq> 0" + shows "fps_conv_radius (fps_tan c) \<ge> pi / (2 * norm c)" +proof - + have "fps_conv_radius (fps_tan c) \<ge> + Min {pi / (2 * norm c), fps_conv_radius (fps_sin c), fps_conv_radius (fps_cos c)}" + unfolding fps_tan_def + proof (rule fps_conv_radius_divide) + fix z :: complex assume "z \<in> eball 0 (pi / (2 * norm c))" + with cos_eq_zero_imp_norm_ge[of "c*z"] assms + show "eval_fps (fps_cos c) z \<noteq> 0" by (auto simp: norm_mult field_simps) + qed (insert assms, auto) + thus ?thesis by (simp add: min_def) +qed + +lemma eval_fps_tan: + fixes c :: complex + assumes "norm z < pi / (2 * norm c)" + shows "eval_fps (fps_tan c) z = tan (c * z)" +proof (cases "c = 0") + case False + show ?thesis unfolding fps_tan_def + proof (subst eval_fps_divide'[where r = "pi / (2 * norm c)"]) + fix z :: complex assume "z \<in> eball 0 (pi / (2 * norm c))" + with cos_eq_zero_imp_norm_ge[of "c*z"] assms + show "eval_fps (fps_cos c) z \<noteq> 0" using False by (auto simp: norm_mult field_simps) + qed (insert False assms, auto simp: field_simps tan_def) +qed simp_all + +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 "(\<lambda>x. (1 + x) powr c) has_fps_expansion fps_binomial c" +proof - + have *: "eventually (\<lambda>z::complex. z \<in> 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 "(\<lambda>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]: + "(\<lambda>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 "(\<lambda>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]: + "(\<lambda>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 \<le> subdegree F" + assumes "c = fps_nth F n" + shows "(\<lambda>x. if x = 0 then c else f x / x ^ n) has_fps_expansion (fps_shift n F)" +proof - + have "eventually (\<lambda>x. x \<in> 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 (\<lambda>x. eval_fps F x = f x) (nhds 0)" + using assms by (auto simp: has_fps_expansion_def) + ultimately have "eventually (\<lambda>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 \<le> subdegree F" "G \<noteq> 0" + "c = fps_nth F (subdegree G) / fps_nth G (subdegree G)" + shows "(\<lambda>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 \<noteq> 0" + by (simp add: G'_def n_def) + ultimately have FG: "F / G = F' * inverse G'" + by (simp add: fps_divide_unit) + + have "(\<lambda>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 \<open>G \<noteq> 0\<close> + by (intro has_fps_expansion_mult has_fps_expansion_inverse + has_fps_expansion_shift assms) auto + also have "?h = (\<lambda>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 \<noteq> 0" + shows "(\<lambda>x. f x / g x) has_fps_expansion (F / G)" +proof - + have "(\<lambda>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 = (\<lambda>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 "(\<lambda>x. tan (c * x)) has_fps_expansion fps_tan c" +proof - + have "(\<lambda>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 \<in> s" "f holomorphic_on s" "\<And>z. z \<in> s \<Longrightarrow> f z = eval_fps F z" +proof - + from assms obtain s where s: "open s" "0 \<in> s" "\<And>z. z \<in> s \<Longrightarrow> eval_fps F z = f z" + unfolding has_fps_expansion_def eventually_nhds by blast + let ?s' = "eball 0 (fps_conv_radius F) \<inter> s" + have "eval_fps F holomorphic_on ?s'" + by (intro holomorphic_intros) auto + also have "?this \<longleftrightarrow> 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 + +lemma residue_fps_expansion_over_power_at_0: + assumes "f has_fps_expansion F" + shows "residue (\<lambda>z. f z / z ^ Suc n) 0 = fps_nth F n" +proof - + from has_fps_expansion_imp_holomorphic[OF assms] guess s . note s = this + have "residue (\<lambda>z. f z / (z - 0) ^ Suc n) 0 = (deriv ^^ n) f 0 / fact n" + using assms s unfolding has_fps_expansion_def + by (intro residue_holomorphic_over_power[of s]) (auto simp: zero_ereal_def) + also from assms have "\<dots> = fps_nth F n" + by (subst fps_nth_fps_expansion) auto + finally show ?thesis by simp +qed + +end

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Analysis/Infinite_Set_Sum.thy Mon Aug 21 20:49:15 2017 +0200 @@ -0,0 +1,570 @@ +(* + Title: HOL/Analysis/Infinite_Set_Sum.thy + Author: Manuel Eberl, TU München + + A theory of sums over possible infinite sets. (Only works for absolute summability) +*) +section \<open>Sums over infinite sets\<close> +theory Infinite_Set_Sum + imports Set_Integral +begin + +(* TODO Move *) +lemma sets_eq_countable: + assumes "countable A" "space M = A" "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets M" + shows "sets M = Pow A" +proof (intro equalityI subsetI) + fix X assume "X \<in> Pow A" + hence "(\<Union>x\<in>X. {x}) \<in> sets M" + by (intro sets.countable_UN' countable_subset[OF _ assms(1)]) (auto intro!: assms(3)) + also have "(\<Union>x\<in>X. {x}) = X" by auto + finally show "X \<in> sets M" . +next + fix X assume "X \<in> sets M" + from sets.sets_into_space[OF this] and assms + show "X \<in> Pow A" by simp +qed + +lemma measure_eqI_countable': + assumes spaces: "space M = A" "space N = A" + assumes sets: "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets M" "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets N" + assumes A: "countable A" + assumes eq: "\<And>a. a \<in> A \<Longrightarrow> emeasure M {a} = emeasure N {a}" + shows "M = N" +proof (rule measure_eqI_countable) + show "sets M = Pow A" + by (intro sets_eq_countable assms) + show "sets N = Pow A" + by (intro sets_eq_countable assms) +qed fact+ + +lemma PiE_singleton: + assumes "f \<in> extensional A" + shows "PiE A (\<lambda>x. {f x}) = {f}" +proof - + { + fix g assume "g \<in> PiE A (\<lambda>x. {f x})" + hence "g x = f x" for x + using assms by (cases "x \<in> A") (auto simp: extensional_def) + hence "g = f" by (simp add: fun_eq_iff) + } + thus ?thesis using assms by (auto simp: extensional_def) +qed + +lemma count_space_PiM_finite: + fixes B :: "'a \<Rightarrow> 'b set" + assumes "finite A" "\<And>i. countable (B i)" + shows "PiM A (\<lambda>i. count_space (B i)) = count_space (PiE A B)" +proof (rule measure_eqI_countable') + show "space (PiM A (\<lambda>i. count_space (B i))) = PiE A B" + by (simp add: space_PiM) + show "space (count_space (PiE A B)) = PiE A B" by simp +next + fix f assume f: "f \<in> PiE A B" + hence "PiE A (\<lambda>x. {f x}) \<in> sets (Pi\<^sub>M A (\<lambda>i. count_space (B i)))" + by (intro sets_PiM_I_finite assms) auto + also from f have "PiE A (\<lambda>x. {f x}) = {f}" + by (intro PiE_singleton) (auto simp: PiE_def) + finally show "{f} \<in> sets (Pi\<^sub>M A (\<lambda>i. count_space (B i)))" . +next + interpret product_sigma_finite "(\<lambda>i. count_space (B i))" + by (intro product_sigma_finite.intro sigma_finite_measure_count_space_countable assms) + thm sigma_finite_measure_count_space + fix f assume f: "f \<in> PiE A B" + hence "{f} = PiE A (\<lambda>x. {f x})" + by (intro PiE_singleton [symmetric]) (auto simp: PiE_def) + also have "emeasure (Pi\<^sub>M A (\<lambda>i. count_space (B i))) \<dots> = + (\<Prod>i\<in>A. emeasure (count_space (B i)) {f i})" + using f assms by (subst emeasure_PiM) auto + also have "\<dots> = (\<Prod>i\<in>A. 1)" + by (intro prod.cong refl, subst emeasure_count_space_finite) (use f in auto) + also have "\<dots> = emeasure (count_space (PiE A B)) {f}" + using f by (subst emeasure_count_space_finite) auto + finally show "emeasure (Pi\<^sub>M A (\<lambda>i. count_space (B i))) {f} = + emeasure (count_space (Pi\<^sub>E A B)) {f}" . +qed (simp_all add: countable_PiE assms) + + + +definition abs_summable_on :: + "('a \<Rightarrow> 'b :: {banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> bool" + (infix "abs'_summable'_on" 50) + where + "f abs_summable_on A \<longleftrightarrow> integrable (count_space A) f" + + +definition infsetsum :: + "('a \<Rightarrow> 'b :: {banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> 'b" + where + "infsetsum f A = lebesgue_integral (count_space A) f" + +syntax (ASCII) + "_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" + ("(3INFSETSUM _:_./ _)" [0, 51, 10] 10) +syntax + "_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" + ("(2\<Sum>\<^sub>a_\<in>_./ _)" [0, 51, 10] 10) +translations \<comment> \<open>Beware of argument permutation!\<close> + "\<Sum>\<^sub>ai\<in>A. b" \<rightleftharpoons> "CONST infsetsum (\<lambda>i. b) A" + +syntax (ASCII) + "_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}" + ("(3INFSETSUM _ |/ _./ _)" [0, 0, 10] 10) +syntax + "_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}" + ("(2\<Sum>\<^sub>a_ | (_)./ _)" [0, 0, 10] 10) +translations + "\<Sum>\<^sub>ax|P. t" => "CONST infsetsum (\<lambda>x. t) {x. P}" + +print_translation \<open> +let + fun sum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] = + if x <> y then raise Match + else + let + val x' = Syntax_Trans.mark_bound_body (x, Tx); + val t' = subst_bound (x', t); + val P' = subst_bound (x', P); + in + Syntax.const @{syntax_const "_qinfsetsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t' + end + | sum_tr' _ = raise Match; +in [(@{const_syntax infsetsum}, K sum_tr')] end +\<close> + + + + +lemma restrict_count_space_subset: + "A \<subseteq> B \<Longrightarrow> restrict_space (count_space B) A = count_space A" + by (subst restrict_count_space) (simp_all add: Int_absorb2) + +lemma abs_summable_on_restrict: + fixes f :: "'a \<Rightarrow> 'b :: {banach, second_countable_topology}" + assumes "A \<subseteq> B" + shows "f abs_summable_on A \<longleftrightarrow> (\<lambda>x. indicator A x *\<^sub>R f x) abs_summable_on B" +proof - + have "count_space A = restrict_space (count_space B) A" + by (rule restrict_count_space_subset [symmetric]) fact+ + also have "integrable \<dots> f \<longleftrightarrow> set_integrable (count_space B) A f" + by (subst integrable_restrict_space) auto + finally show ?thesis + unfolding abs_summable_on_def . +qed + +lemma abs_summable_on_altdef: "f abs_summable_on A \<longleftrightarrow> set_integrable (count_space UNIV) A f" + by (subst abs_summable_on_restrict[of _ UNIV]) (auto simp: abs_summable_on_def) + +lemma abs_summable_on_altdef': + "A \<subseteq> B \<Longrightarrow> f abs_summable_on A \<longleftrightarrow> set_integrable (count_space B) A f" + by (subst abs_summable_on_restrict[of _ B]) (auto simp: abs_summable_on_def) + +lemma abs_summable_on_cong [cong]: + "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> A = B \<Longrightarrow> (f abs_summable_on A) \<longleftrightarrow> (g abs_summable_on B)" + unfolding abs_summable_on_def by (intro integrable_cong) auto + +lemma abs_summable_on_cong_neutral: + assumes "\<And>x. x \<in> A - B \<Longrightarrow> f x = 0" + assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x = 0" + assumes "\<And>x. x \<in> A \<inter> B \<Longrightarrow> f x = g x" + shows "f abs_summable_on A \<longleftrightarrow> g abs_summable_on B" + unfolding abs_summable_on_altdef using assms + by (intro Bochner_Integration.integrable_cong refl) + (auto simp: indicator_def split: if_splits) + +lemma abs_summable_on_restrict': + fixes f :: "'a \<Rightarrow> 'b :: {banach, second_countable_topology}" + assumes "A \<subseteq> B" + shows "f abs_summable_on A \<longleftrightarrow> (\<lambda>x. if x \<in> A then f x else 0) abs_summable_on B" + by (subst abs_summable_on_restrict[OF assms]) (intro abs_summable_on_cong, auto) + +lemma abs_summable_on_nat_iff: + "f abs_summable_on (A :: nat set) \<longleftrightarrow> summable (\<lambda>n. if n \<in> A then norm (f n) else 0)" +proof - + have "f abs_summable_on A \<longleftrightarrow> summable (\<lambda>x. norm (if x \<in> A then f x else 0))" + by (subst abs_summable_on_restrict'[of _ UNIV]) + (simp_all add: abs_summable_on_def integrable_count_space_nat_iff) + also have "(\<lambda>x. norm (if x \<in> A then f x else 0)) = (\<lambda>x. if x \<in> A then norm (f x) else 0)" + by auto + finally show ?thesis . +qed + +lemma abs_summable_on_nat_iff': + "f abs_summable_on (UNIV :: nat set) \<longleftrightarrow> summable (\<lambda>n. norm (f n))" + by (subst abs_summable_on_nat_iff) auto + +lemma abs_summable_on_finite [simp]: "finite A \<Longrightarrow> f abs_summable_on A" + unfolding abs_summable_on_def by (rule integrable_count_space) + +lemma abs_summable_on_empty [simp, intro]: "f abs_summable_on {}" + by simp + +lemma abs_summable_on_subset: + assumes "f abs_summable_on B" and "A \<subseteq> B" + shows "f abs_summable_on A" + unfolding abs_summable_on_altdef + by (rule set_integrable_subset) (insert assms, auto simp: abs_summable_on_altdef) + +lemma abs_summable_on_union [intro]: + assumes "f abs_summable_on A" and "f abs_summable_on B" + shows "f abs_summable_on (A \<union> B)" + using assms unfolding abs_summable_on_altdef by (intro set_integrable_Un) auto + +lemma abs_summable_on_reindex_bij_betw: + assumes "bij_betw g A B" + shows "(\<lambda>x. f (g x)) abs_summable_on A \<longleftrightarrow> f abs_summable_on B" +proof - + have *: "count_space B = distr (count_space A) (count_space B) g" + by (rule distr_bij_count_space [symmetric]) fact + show ?thesis unfolding abs_summable_on_def + by (subst *, subst integrable_distr_eq[of _ _ "count_space B"]) + (insert assms, auto simp: bij_betw_def) +qed + +lemma abs_summable_on_reindex: + assumes "(\<lambda>x. f (g x)) abs_summable_on A" + shows "f abs_summable_on (g ` A)" +proof - + define g' where "g' = inv_into A g" + from assms have "(\<lambda>x. f (g x)) abs_summable_on (g' ` g ` A)" + by (rule abs_summable_on_subset) (auto simp: g'_def inv_into_into) + also have "?this \<longleftrightarrow> (\<lambda>x. f (g (g' x))) abs_summable_on (g ` A)" unfolding g'_def + by (intro abs_summable_on_reindex_bij_betw [symmetric] inj_on_imp_bij_betw inj_on_inv_into) auto + also have "\<dots> \<longleftrightarrow> f abs_summable_on (g ` A)" + by (intro abs_summable_on_cong refl) (auto simp: g'_def f_inv_into_f) + finally show ?thesis . +qed + +lemma abs_summable_reindex_iff: + "inj_on g A \<Longrightarrow> (\<lambda>x. f (g x)) abs_summable_on A \<longleftrightarrow> f abs_summable_on (g ` A)" + by (intro abs_summable_on_reindex_bij_betw inj_on_imp_bij_betw) + +lemma abs_summable_on_Sigma_project: + fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set" + assumes "f abs_summable_on (Sigma A B)" "x \<in> A" + shows "(\<lambda>y. f (x, y)) abs_summable_on (B x)" +proof - + from assms(2) have "f abs_summable_on (Sigma {x} B)" + by (intro abs_summable_on_subset [OF assms(1)]) auto + also have "?this \<longleftrightarrow> (\<lambda>z. f (x, snd z)) abs_summable_on (Sigma {x} B)" + by (rule abs_summable_on_cong) auto + finally have "(\<lambda>y. f (x, y)) abs_summable_on (snd ` Sigma {x} B)" + by (rule abs_summable_on_reindex) + also have "snd ` Sigma {x} B = B x" + using assms by (auto simp: image_iff) + finally show ?thesis . +qed + +lemma abs_summable_on_Times_swap: + "f abs_summable_on A \<times> B \<longleftrightarrow> (\<lambda>(x,y). f (y,x)) abs_summable_on B \<times> A" +proof - + have bij: "bij_betw (\<lambda>(x,y). (y,x)) (B \<times> A) (A \<times> B)" + by (auto simp: bij_betw_def inj_on_def) + show ?thesis + by (subst abs_summable_on_reindex_bij_betw[OF bij, of f, symmetric]) + (simp_all add: case_prod_unfold) +qed + +lemma abs_summable_on_0 [simp, intro]: "(\<lambda>_. 0) abs_summable_on A" + by (simp add: abs_summable_on_def) + +lemma abs_summable_on_uminus [intro]: + "f abs_summable_on A \<Longrightarrow> (\<lambda>x. -f x) abs_summable_on A" + unfolding abs_summable_on_def by (rule Bochner_Integration.integrable_minus) + +lemma abs_summable_on_add [intro]: + assumes "f abs_summable_on A" and "g abs_summable_on A" + shows "(\<lambda>x. f x + g x) abs_summable_on A" + using assms unfolding abs_summable_on_def by (rule Bochner_Integration.integrable_add) + +lemma abs_summable_on_diff [intro]: + assumes "f abs_summable_on A" and "g abs_summable_on A" + shows "(\<lambda>x. f x - g x) abs_summable_on A" + using assms unfolding abs_summable_on_def by (rule Bochner_Integration.integrable_diff) + +lemma abs_summable_on_scaleR_left [intro]: + assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A" + shows "(\<lambda>x. f x *\<^sub>R c) abs_summable_on A" + using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_scaleR_left) + +lemma abs_summable_on_scaleR_right [intro]: + assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A" + shows "(\<lambda>x. c *\<^sub>R f x) abs_summable_on A" + using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_scaleR_right) + +lemma abs_summable_on_cmult_right [intro]: + fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}" + assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A" + shows "(\<lambda>x. c * f x) abs_summable_on A" + using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_mult_right) + +lemma abs_summable_on_cmult_left [intro]: + fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}" + assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A" + shows "(\<lambda>x. f x * c) abs_summable_on A" + using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_mult_left) + + + +lemma not_summable_infsetsum_eq: + "\<not>f abs_summable_on A \<Longrightarrow> infsetsum f A = 0" + by (simp add: abs_summable_on_def infsetsum_def not_integrable_integral_eq) + +lemma infsetsum_altdef: + "infsetsum f A = set_lebesgue_integral (count_space UNIV) A f" + by (subst integral_restrict_space [symmetric]) + (auto simp: restrict_count_space_subset infsetsum_def) + +lemma infsetsum_altdef': + "A \<subseteq> B \<Longrightarrow> infsetsum f A = set_lebesgue_integral (count_space B) A f" + by (subst integral_restrict_space [symmetric]) + (auto simp: restrict_count_space_subset infsetsum_def) + +lemma infsetsum_cong [cong]: + "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> A = B \<Longrightarrow> infsetsum f A = infsetsum g B" + unfolding infsetsum_def by (intro Bochner_Integration.integral_cong) auto + +lemma infsetsum_0 [simp]: "infsetsum (\<lambda>_. 0) A = 0" + by (simp add: infsetsum_def) + +lemma infsetsum_all_0: "(\<And>x. x \<in> A \<Longrightarrow> f x = 0) \<Longrightarrow> infsetsum f A = 0" + by simp + +lemma infsetsum_finite [simp]: "finite A \<Longrightarrow> infsetsum f A = (\<Sum>x\<in>A. f x)" + by (simp add: infsetsum_def lebesgue_integral_count_space_finite) + +lemma infsetsum_nat: + assumes "f abs_summable_on A" + shows "infsetsum f A = (\<Sum>n. if n \<in> A then f n else 0)" +proof - + from assms have "infsetsum f A = (\<Sum>n. indicator A n *\<^sub>R f n)" + unfolding infsetsum_altdef abs_summable_on_altdef by (subst integral_count_space_nat) auto + also have "(\<lambda>n. indicator A n *\<^sub>R f n) = (\<lambda>n. if n \<in> A then f n else 0)" + by auto + finally show ?thesis . +qed + +lemma infsetsum_nat': + assumes "f abs_summable_on UNIV" + shows "infsetsum f UNIV = (\<Sum>n. f n)" + using assms by (subst infsetsum_nat) auto + +lemma sums_infsetsum_nat: + assumes "f abs_summable_on A" + shows "(\<lambda>n. if n \<in> A then f n else 0) sums infsetsum f A" +proof - + from assms have "summable (\<lambda>n. if n \<in> A then norm (f n) else 0)" + by (simp add: abs_summable_on_nat_iff) + also have "(\<lambda>n. if n \<in> A then norm (f n) else 0) = (\<lambda>n. norm (if n \<in> A then f n else 0))" + by auto + finally have "summable (\<lambda>n. if n \<in> A then f n else 0)" + by (rule summable_norm_cancel) + with assms show ?thesis + by (auto simp: sums_iff infsetsum_nat) +qed + +lemma sums_infsetsum_nat': + assumes "f abs_summable_on UNIV" + shows "f sums infsetsum f UNIV" + using sums_infsetsum_nat [OF assms] by simp + +lemma infsetsum_Un_disjoint: + assumes "f abs_summable_on A" "f abs_summable_on B" "A \<inter> B = {}" + shows "infsetsum f (A \<union> B) = infsetsum f A + infsetsum f B" + using assms unfolding infsetsum_altdef abs_summable_on_altdef + by (subst set_integral_Un) auto + +lemma infsetsum_Diff: + assumes "f abs_summable_on B" "A \<subseteq> B" + shows "infsetsum f (B - A) = infsetsum f B - infsetsum f A" +proof - + have "infsetsum f ((B - A) \<union> A) = infsetsum f (B - A) + infsetsum f A" + using assms(2) by (intro infsetsum_Un_disjoint abs_summable_on_subset[OF assms(1)]) auto + also from assms(2) have "(B - A) \<union> A = B" + by auto + ultimately show ?thesis + by (simp add: algebra_simps) +qed + +lemma infsetsum_Un_Int: + assumes "f abs_summable_on (A \<union> B)" + shows "infsetsum f (A \<union> B) = infsetsum f A + infsetsum f B - infsetsum f (A \<inter> B)" +proof - + have "A \<union> B = A \<union> (B - A \<inter> B)" + by auto + also have "infsetsum f \<dots> = infsetsum f A + infsetsum f (B - A \<inter> B)" + by (intro infsetsum_Un_disjoint abs_summable_on_subset[OF assms]) auto + also have "infsetsum f (B - A \<inter> B) = infsetsum f B - infsetsum f (A \<inter> B)" + by (intro infsetsum_Diff abs_summable_on_subset[OF assms]) auto + finally show ?thesis + by (simp add: algebra_simps) +qed + +lemma infsetsum_reindex_bij_betw: + assumes "bij_betw g A B" + shows "infsetsum (\<lambda>x. f (g x)) A = infsetsum f B" +proof - + have *: "count_space B = distr (count_space A) (count_space B) g" + by (rule distr_bij_count_space [symmetric]) fact + show ?thesis unfolding infsetsum_def + by (subst *, subst integral_distr[of _ _ "count_space B"]) + (insert assms, auto simp: bij_betw_def) +qed + +lemma infsetsum_reindex: + assumes "inj_on g A" + shows "infsetsum f (g ` A) = infsetsum (\<lambda>x. f (g x)) A" + by (intro infsetsum_reindex_bij_betw [symmetric] inj_on_imp_bij_betw assms) + +lemma infsetsum_cong_neutral: + assumes "\<And>x. x \<in> A - B \<Longrightarrow> f x = 0" + assumes "\<And>x. x \<in> B - A \<Longrightarrow> g x = 0" + assumes "\<And>x. x \<in> A \<inter> B \<Longrightarrow> f x = g x" + shows "infsetsum f A = infsetsum g B" + unfolding infsetsum_altdef using assms + by (intro Bochner_Integration.integral_cong refl) + (auto simp: indicator_def split: if_splits) + +lemma infsetsum_Sigma: + fixes A :: "'a set" and B :: "'a \<Rightarrow> 'b set" + assumes [simp]: "countable A" and "\<And>i. countable (B i)" + assumes summable: "f abs_summable_on (Sigma A B)" + shows "infsetsum f (Sigma A B) = infsetsum (\<lambda>x. infsetsum (\<lambda>y. f (x, y)) (B x)) A" +proof - + define B' where "B' = (\<Union>i\<in>A. B i)" + have [simp]: "countable B'" + unfolding B'_def by (intro countable_UN assms) + interpret pair_sigma_finite "count_space A" "count_space B'" + by (intro pair_sigma_finite.intro sigma_finite_measure_count_space_countable) fact+ + + have "integrable (count_space (A \<times> B')) (\<lambda>z. indicator (Sigma A B) z *\<^sub>R f z)" + using summable by (subst abs_summable_on_altdef' [symmetric]) (auto simp: B'_def) + also have "?this \<longleftrightarrow> integrable (count_space A \<Otimes>\<^sub>M count_space B') (\<lambda>(x, y). indicator (B x) y *\<^sub>R f (x, y))" + by (intro Bochner_Integration.integrable_cong) + (auto simp: pair_measure_countable indicator_def split: if_splits) + finally have integrable: \<dots> . + + have "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f (x, y)) (B x)) A = + (\<integral>x. infsetsum (\<lambda>y. f (x, y)) (B x) \<partial>count_space A)" + unfolding infsetsum_def by simp + also have "\<dots> = (\<integral>x. \<integral>y. indicator (B x) y *\<^sub>R f (x, y) \<partial>count_space B' \<partial>count_space A)" + by (intro Bochner_Integration.integral_cong infsetsum_altdef'[of _ B'] refl) + (auto simp: B'_def) + also have "\<dots> = (\<integral>(x,y). indicator (B x) y *\<^sub>R f (x, y) \<partial>(count_space A \<Otimes>\<^sub>M count_space B'))" + by (subst integral_fst [OF integrable]) auto + also have "\<dots> = (\<integral>z. indicator (Sigma A B) z *\<^sub>R f z \<partial>count_space (A \<times> B'))" + by (intro Bochner_Integration.integral_cong) + (auto simp: pair_measure_countable indicator_def split: if_splits) + also have "\<dots> = infsetsum f (Sigma A B)" + by (rule infsetsum_altdef' [symmetric]) (auto simp: B'_def) + finally show ?thesis .. +qed + +lemma infsetsum_Times: + fixes A :: "'a set" and B :: "'b set" + assumes [simp]: "countable A" and "countable B" + assumes summable: "f abs_summable_on (A \<times> B)" + shows "infsetsum f (A \<times> B) = infsetsum (\<lambda>x. infsetsum (\<lambda>y. f (x, y)) B) A" + using assms by (subst infsetsum_Sigma) auto + +lemma infsetsum_Times': + fixes A :: "'a set" and B :: "'b set" + fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {banach, second_countable_topology}" + assumes [simp]: "countable A" and [simp]: "countable B" + assumes summable: "(\<lambda>(x,y). f x y) abs_summable_on (A \<times> B)" + shows "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f x y) B) A = infsetsum (\<lambda>(x,y). f x y) (A \<times> B)" + using assms by (subst infsetsum_Times) auto + +lemma infsetsum_swap: + fixes A :: "'a set" and B :: "'b set" + fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {banach, second_countable_topology}" + assumes [simp]: "countable A" and [simp]: "countable B" + assumes summable: "(\<lambda>(x,y). f x y) abs_summable_on A \<times> B" + shows "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f x y) B) A = infsetsum (\<lambda>y. infsetsum (\<lambda>x. f x y) A) B" +proof - + from summable have summable': "(\<lambda>(x,y). f y x) abs_summable_on B \<times> A" + by (subst abs_summable_on_Times_swap) auto + have bij: "bij_betw (\<lambda>(x, y). (y, x)) (B \<times> A) (A \<times> B)" + by (auto simp: bij_betw_def inj_on_def) + have "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f x y) B) A = infsetsum (\<lambda>(x,y). f x y) (A \<times> B)" + using summable by (subst infsetsum_Times) auto + also have "\<dots> = infsetsum (\<lambda>(x,y). f y x) (B \<times> A)" + by (subst infsetsum_reindex_bij_betw[OF bij, of "\<lambda>(x,y). f x y", symmetric]) + (simp_all add: case_prod_unfold) + also have "\<dots> = infsetsum (\<lambda>y. infsetsum (\<lambda>x. f x y) A) B" + using summable' by (subst infsetsum_Times) auto + finally show ?thesis . +qed + +lemma infsetsum_prod_PiE: + fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: {real_normed_field,banach,second_countable_topology}" + assumes finite: "finite A" and countable: "\<And>x. x \<in> A \<Longrightarrow> countable (B x)" + assumes summable: "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B x" + shows "infsetsum (\<lambda>g. \<Prod>x\<in>A. f x (g x)) (PiE A B) = (\<Prod>x\<in>A. infsetsum (f x) (B x))" +proof - + define B' where "B' = (\<lambda>x. if x \<in> A then B x else {})" + from assms have [simp]: "countable (B' x)" for x + by (auto simp: B'_def) + then interpret product_sigma_finite "count_space \<circ> B'" + unfolding o_def by (intro product_sigma_finite.intro sigma_finite_measure_count_space_countable) + have "infsetsum (\<lambda>g. \<Prod>x\<in>A. f x (g x)) (PiE A B) = + (\<integral>g. (\<Prod>x\<in>A. f x (g x)) \<partial>count_space (PiE A B))" + by (simp add: infsetsum_def) + also have "PiE A B = PiE A B'" + by (intro PiE_cong) (simp_all add: B'_def) + hence "count_space (PiE A B) = count_space (PiE A B')" + by simp + also have "\<dots> = PiM A (count_space \<circ> B')" + unfolding o_def using finite by (intro count_space_PiM_finite [symmetric]) simp_all + also have "(\<integral>g. (\<Prod>x\<in>A. f x (g x)) \<partial>\<dots>) = (\<Prod>x\<in>A. infsetsum (f x) (B' x))" + by (subst product_integral_prod) + (insert summable finite, simp_all add: infsetsum_def B'_def abs_summable_on_def) + also have "\<dots> = (\<Prod>x\<in>A. infsetsum (f x) (B x))" + by (intro prod.cong refl) (simp_all add: B'_def) + finally show ?thesis . +qed + +lemma infsetsum_uminus: "infsetsum (\<lambda>x. -f x) A = -infsetsum f A" + unfolding infsetsum_def abs_summable_on_def + by (rule Bochner_Integration.integral_minus) + +lemma infsetsum_add: + assumes "f abs_summable_on A" and "g abs_summable_on A" + shows "infsetsum (\<lambda>x. f x + g x) A = infsetsum f A + infsetsum g A" + using assms unfolding infsetsum_def abs_summable_on_def + by (rule Bochner_Integration.integral_add) + +lemma infsetsum_diff: + assumes "f abs_summable_on A" and "g abs_summable_on A" + shows "infsetsum (\<lambda>x. f x - g x) A = infsetsum f A - infsetsum g A" + using assms unfolding infsetsum_def abs_summable_on_def + by (rule Bochner_Integration.integral_diff) + +lemma infsetsum_scaleR_left: + assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A" + shows "infsetsum (\<lambda>x. f x *\<^sub>R c) A = infsetsum f A *\<^sub>R c" + using assms unfolding infsetsum_def abs_summable_on_def + by (rule Bochner_Integration.integral_scaleR_left) + +lemma infsetsum_scaleR_right: + "infsetsum (\<lambda>x. c *\<^sub>R f x) A = c *\<^sub>R infsetsum f A" + unfolding infsetsum_def abs_summable_on_def + by (subst Bochner_Integration.integral_scaleR_right) auto + +lemma infsetsum_cmult_left: + fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}" + assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A" + shows "infsetsum (\<lambda>x. f x * c) A = infsetsum f A * c" + using assms unfolding infsetsum_def abs_summable_on_def + by (rule Bochner_Integration.integral_mult_left) + +lemma infsetsum_cmult_right: + fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}" + assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A" + shows "infsetsum (\<lambda>x. c * f x) A = c * infsetsum f A" + using assms unfolding infsetsum_def abs_summable_on_def + by (rule Bochner_Integration.integral_mult_right) + +(* TODO Generalise with bounded_linear *) + +end

--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Mon Aug 21 19:20:02 2017 +0200 +++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Mon Aug 21 20:49:15 2017 +0200 @@ -402,53 +402,53 @@ qed -subsection \<open>The eXtractor series X\<close> +subsection \<open>The efps_Xtractor series fps_X\<close> lemma minus_one_power_iff: "(- (1::'a::comm_ring_1)) ^ n = (if even n then 1 else - 1)" by (induct n) auto -definition "X = Abs_fps (\<lambda>n. if n = 1 then 1 else 0)" - -lemma X_mult_nth [simp]: - "(X * (f :: 'a::semiring_1 fps)) $n = (if n = 0 then 0 else f $ (n - 1))" +definition "fps_X = Abs_fps (\<lambda>n. if n = 1 then 1 else 0)" + +lemma fps_X_mult_nth [simp]: + "(fps_X * (f :: 'a::semiring_1 fps)) $n = (if n = 0 then 0 else f $ (n - 1))" proof (cases "n = 0") case False - have "(X * f) $n = (\<Sum>i = 0..n. X $ i * f $ (n - i))" + have "(fps_X * f) $n = (\<Sum>i = 0..n. fps_X $ i * f $ (n - i))" by (simp add: fps_mult_nth) also have "\<dots> = f $ (n - 1)" - using False by (simp add: X_def mult_delta_left sum.delta) + using False by (simp add: fps_X_def mult_delta_left sum.delta) finally show ?thesis using False by simp next case True then show ?thesis - by (simp add: fps_mult_nth X_def) + by (simp add: fps_mult_nth fps_X_def) qed -lemma X_mult_right_nth[simp]: - "((a::'a::semiring_1 fps) * X) $ n = (if n = 0 then 0 else a $ (n - 1))" +lemma fps_X_mult_right_nth[simp]: + "((a::'a::semiring_1 fps) * fps_X) $ n = (if n = 0 then 0 else a $ (n - 1))" proof - - have "(a * X) $ n = (\<Sum>i = 0..n. a $ i * (if n - i = Suc 0 then 1 else 0))" - by (simp add: fps_times_def X_def) + have "(a * fps_X) $ n = (\<Sum>i = 0..n. a $ i * (if n - i = Suc 0 then 1 else 0))" + by (simp add: fps_times_def fps_X_def) also have "\<dots> = (\<Sum>i = 0..n. if i = n - 1 then if n = 0 then 0 else a $ i else 0)" by (intro sum.cong) auto also have "\<dots> = (if n = 0 then 0 else a $ (n - 1))" by (simp add: sum.delta) finally show ?thesis . qed -lemma fps_mult_X_commute: "X * (a :: 'a :: semiring_1 fps) = a * X" +lemma fps_mult_fps_X_commute: "fps_X * (a :: 'a :: semiring_1 fps) = a * fps_X" by (simp add: fps_eq_iff) -lemma X_power_iff: "X ^ n = Abs_fps (\<lambda>m. if m = n then 1 else 0)" +lemma fps_X_power_iff: "fps_X ^ n = Abs_fps (\<lambda>m. if m = n then 1 else 0)" by (induction n) (auto simp: fps_eq_iff) -lemma X_nth[simp]: "X$n = (if n = 1 then 1 else 0)" - by (simp add: X_def) - -lemma X_power_nth[simp]: "(X^k) $n = (if n = k then 1 else 0::'a::comm_ring_1)" - by (simp add: X_power_iff) - -lemma X_power_mult_nth: "(X^k * (f :: 'a::comm_ring_1 fps)) $n = (if n < k then 0 else f $ (n - k))" +lemma fps_X_nth[simp]: "fps_X$n = (if n = 1 then 1 else 0)" + by (simp add: fps_X_def) + +lemma fps_X_power_nth[simp]: "(fps_X^k) $n = (if n = k then 1 else 0::'a::comm_ring_1)" + by (simp add: fps_X_power_iff) + +lemma fps_X_power_mult_nth: "(fps_X^k * (f :: 'a::comm_ring_1 fps)) $n = (if n < k then 0 else f $ (n - k))" apply (induct k arbitrary: n) apply simp unfolding power_Suc mult.assoc @@ -456,32 +456,32 @@ apply auto done -lemma X_power_mult_right_nth: - "((f :: 'a::comm_ring_1 fps) * X^k) $n = (if n < k then 0 else f $ (n - k))" - by (metis X_power_mult_nth mult.commute) - - -lemma X_neq_fps_const [simp]: "(X :: 'a :: zero_neq_one fps) \<noteq> fps_const c" +lemma fps_X_power_mult_right_nth: + "((f :: 'a::comm_ring_1 fps) * fps_X^k) $n = (if n < k then 0 else f $ (n - k))" + by (metis fps_X_power_mult_nth mult.commute) + + +lemma fps_X_neq_fps_const [simp]: "(fps_X :: 'a :: zero_neq_one fps) \<noteq> fps_const c" proof - assume "(X::'a fps) = fps_const (c::'a)" - hence "X$1 = (fps_const (c::'a))$1" by (simp only:) + assume "(fps_X::'a fps) = fps_const (c::'a)" + hence "fps_X$1 = (fps_const (c::'a))$1" by (simp only:) thus False by auto qed -lemma X_neq_zero [simp]: "(X :: 'a :: zero_neq_one fps) \<noteq> 0" - by (simp only: fps_const_0_eq_0[symmetric] X_neq_fps_const) simp - -lemma X_neq_one [simp]: "(X :: 'a :: zero_neq_one fps) \<noteq> 1" - by (simp only: fps_const_1_eq_1[symmetric] X_neq_fps_const) simp - -lemma X_neq_numeral [simp]: "(X :: 'a :: {semiring_1,zero_neq_one} fps) \<noteq> numeral c" - by (simp only: numeral_fps_const X_neq_fps_const) simp - -lemma X_pow_eq_X_pow_iff [simp]: - "(X :: ('a :: {comm_ring_1}) fps) ^ m = X ^ n \<longleftrightarrow> m = n" +lemma fps_X_neq_zero [simp]: "(fps_X :: 'a :: zero_neq_one fps) \<noteq> 0" + by (simp only: fps_const_0_eq_0[symmetric] fps_X_neq_fps_const) simp + +lemma fps_X_neq_one [simp]: "(fps_X :: 'a :: zero_neq_one fps) \<noteq> 1" + by (simp only: fps_const_1_eq_1[symmetric] fps_X_neq_fps_const) simp + +lemma fps_X_neq_numeral [simp]: "(fps_X :: 'a :: {semiring_1,zero_neq_one} fps) \<noteq> numeral c" + by (simp only: numeral_fps_const fps_X_neq_fps_const) simp + +lemma fps_X_pow_eq_fps_X_pow_iff [simp]: + "(fps_X :: ('a :: {comm_ring_1}) fps) ^ m = fps_X ^ n \<longleftrightarrow> m = n" proof - assume "(X :: 'a fps) ^ m = X ^ n" - hence "(X :: 'a fps) ^ m $ m = X ^ n $ m" by (simp only:) + assume "(fps_X :: 'a fps) ^ m = fps_X ^ n" + hence "(fps_X :: 'a fps) ^ m $ m = fps_X ^ n $ m" by (simp only:) thus "m = n" by (simp split: if_split_asm) qed simp_all @@ -553,8 +553,8 @@ lemma subdegree_1 [simp]: "subdegree (1 :: ('a :: zero_neq_one) fps) = 0" by (auto intro!: subdegreeI) -lemma subdegree_X [simp]: "subdegree (X :: ('a :: zero_neq_one) fps) = 1" - by (auto intro!: subdegreeI simp: X_def) +lemma subdegree_fps_X [simp]: "subdegree (fps_X :: ('a :: zero_neq_one) fps) = 1" + by (auto intro!: subdegreeI simp: fps_X_def) lemma subdegree_fps_const [simp]: "subdegree (fps_const c) = 0" by (cases "c = 0") (auto intro!: subdegreeI) @@ -705,33 +705,33 @@ lemma fps_shift_numeral: "fps_shift n (numeral c) = (if n = 0 then numeral c else 0)" by (simp add: numeral_fps_const fps_shift_fps_const) -lemma fps_shift_X_power [simp]: - "n \<le> m \<Longrightarrow> fps_shift n (X ^ m) = (X ^ (m - n) ::'a::comm_ring_1 fps)" +lemma fps_shift_fps_X_power [simp]: + "n \<le> m \<Longrightarrow> fps_shift n (fps_X ^ m) = (fps_X ^ (m - n) ::'a::comm_ring_1 fps)" by (intro fps_ext) (auto simp: fps_shift_def ) -lemma fps_shift_times_X_power: - "n \<le> subdegree f \<Longrightarrow> fps_shift n f * X ^ n = (f :: 'a :: comm_ring_1 fps)" - by (intro fps_ext) (auto simp: X_power_mult_right_nth nth_less_subdegree_zero) - -lemma fps_shift_times_X_power' [simp]: - "fps_shift n (f * X^n) = (f :: 'a :: comm_ring_1 fps)" - by (intro fps_ext) (auto simp: X_power_mult_right_nth nth_less_subdegree_zero) - -lemma fps_shift_times_X_power'': - "m \<le> n \<Longrightarrow> fps_shift n (f * X^m) = fps_shift (n - m) (f :: 'a :: comm_ring_1 fps)" - by (intro fps_ext) (auto simp: X_power_mult_right_nth nth_less_subdegree_zero) +lemma fps_shift_times_fps_X_power: + "n \<le> subdegree f \<Longrightarrow> fps_shift n f * fps_X ^ n = (f :: 'a :: comm_ring_1 fps)" + by (intro fps_ext) (auto simp: fps_X_power_mult_right_nth nth_less_subdegree_zero) + +lemma fps_shift_times_fps_X_power' [simp]: + "fps_shift n (f * fps_X^n) = (f :: 'a :: comm_ring_1 fps)" + by (intro fps_ext) (auto simp: fps_X_power_mult_right_nth nth_less_subdegree_zero) + +lemma fps_shift_times_fps_X_power'': + "m \<le> n \<Longrightarrow> fps_shift n (f * fps_X^m) = fps_shift (n - m) (f :: 'a :: comm_ring_1 fps)" + by (intro fps_ext) (auto simp: fps_X_power_mult_right_nth nth_less_subdegree_zero) lemma fps_shift_subdegree [simp]: "n \<le> subdegree f \<Longrightarrow> subdegree (fps_shift n f) = subdegree (f :: 'a :: comm_ring_1 fps) - n" by (cases "f = 0") (force intro: nth_less_subdegree_zero subdegreeI)+ lemma subdegree_decompose: - "f = fps_shift (subdegree f) f * X ^ subdegree (f :: ('a :: comm_ring_1) fps)" - by (rule fps_ext) (auto simp: X_power_mult_right_nth) + "f = fps_shift (subdegree f) f * fps_X ^ subdegree (f :: ('a :: comm_ring_1) fps)" + by (rule fps_ext) (auto simp: fps_X_power_mult_right_nth) lemma subdegree_decompose': - "n \<le> subdegree (f :: ('a :: comm_ring_1) fps) \<Longrightarrow> f = fps_shift n f * X^n" - by (rule fps_ext) (auto simp: X_power_mult_right_nth intro!: nth_less_subdegree_zero) + "n \<le> subdegree (f :: ('a :: comm_ring_1) fps) \<Longrightarrow> f = fps_shift n f * fps_X^n" + by (rule fps_ext) (auto simp: fps_X_power_mult_right_nth intro!: nth_less_subdegree_zero) lemma fps_shift_fps_shift: "fps_shift (m + n) f = fps_shift m (fps_shift n f)" @@ -745,8 +745,8 @@ assumes "n \<le> subdegree (g :: 'b :: {comm_ring_1} fps)" shows "fps_shift n (h*g) = h * fps_shift n g" proof - - from assms have "g = fps_shift n g * X^n" by (rule subdegree_decompose') - also have "h * ... = (h * fps_shift n g) * X^n" by simp + from assms have "g = fps_shift n g * fps_X^n" by (rule subdegree_decompose') + also have "h * ... = (h * fps_shift n g) * fps_X^n" by simp also have "fps_shift n ... = h * fps_shift n g" by simp finally show ?thesis . qed @@ -798,8 +798,8 @@ by (simp add: numeral_fps_const fps_cutoff_fps_const) lemma fps_shift_cutoff: - "fps_shift n (f :: ('a :: comm_ring_1) fps) * X^n + fps_cutoff n f = f" - by (simp add: fps_eq_iff X_power_mult_right_nth) + "fps_shift n (f :: ('a :: comm_ring_1) fps) * fps_X^n + fps_cutoff n f = f" + by (simp add: fps_eq_iff fps_X_power_mult_right_nth) subsection \<open>Formal Power series form a metric space\<close> @@ -905,11 +905,11 @@ using kp by blast qed -lemma fps_sum_rep_nth: "(sum (\<lambda>i. fps_const(a$i)*X^i) {0..m})$n = +lemma fps_sum_rep_nth: "(sum (\<lambda>i. fps_const(a$i)*fps_X^i) {0..m})$n = (if n \<le> m then a$n else 0::'a::comm_ring_1)" by (auto simp add: fps_sum_nth cond_value_iff cong del: if_weak_cong) -lemma fps_notation: "(\<lambda>n. sum (\<lambda>i. fps_const(a$i) * X^i) {0..n}) \<longlonglongrightarrow> a" +lemma fps_notation: "(\<lambda>n. sum (\<lambda>i. fps_const(a$i) * fps_X^i) {0..n}) \<longlonglongrightarrow> a" (is "?s \<longlonglongrightarrow> a") proof - have "\<exists>n0. \<forall>n \<ge> n0. dist (?s n) a < r" if "r > 0" for r @@ -1153,12 +1153,12 @@ "unit_factor f = fps_shift (subdegree f) f" definition fps_normalize_def [simp]: - "normalize f = (if f = 0 then 0 else X ^ subdegree f)" + "normalize f = (if f = 0 then 0 else fps_X ^ subdegree f)" instance proof fix f :: "'a fps" show "unit_factor f * normalize f = f" - by (simp add: fps_shift_times_X_power) + by (simp add: fps_shift_times_fps_X_power) next fix f g :: "'a fps" show "unit_factor (f * g) = unit_factor f * unit_factor g" @@ -1205,10 +1205,10 @@ from assms nz have "f div g * g = fps_shift n (f * inverse h) * g" by (simp add: fps_divide_def Let_def h_def n_def) - also have "... = fps_shift n (f * inverse h) * X^n * h" unfolding h_def n_def + also have "... = fps_shift n (f * inverse h) * fps_X^n * h" unfolding h_def n_def by (subst subdegree_decompose[of g]) simp - also have "fps_shift n (f * inverse h) * X^n = f * inverse h" - by (rule fps_shift_times_X_power) (simp_all add: nz assms n_def) + also have "fps_shift n (f * inverse h) * fps_X^n = f * inverse h" + by (rule fps_shift_times_fps_X_power) (simp_all add: nz assms n_def) also have "... * h = f * (inverse h * h)" by simp also have "inverse h * h = 1" by (rule inverse_mult_eq_1) simp finally show ?thesis by simp @@ -1246,14 +1246,14 @@ qed (simp_all add: fps_divide_def) private lemma fps_divide_cancel_aux2: - "(f * X^m) div (g * X^m) = f div (g :: 'a :: field fps)" + "(f * fps_X^m) div (g * fps_X^m) = f div (g :: 'a :: field fps)" proof (cases "g = 0") assume [simp]: "g \<noteq> 0" - have "(f * X^m) div (g * X^m) = - fps_shift (subdegree g + m) (f*inverse (fps_shift (subdegree g + m) (g*X^m))*X^m)" + have "(f * fps_X^m) div (g * fps_X^m) = + fps_shift (subdegree g + m) (f*inverse (fps_shift (subdegree g + m) (g*fps_X^m))*fps_X^m)" by (simp add: fps_divide_def Let_def algebra_simps) also have "... = f div g" - by (simp add: fps_shift_times_X_power'' fps_divide_def Let_def) + by (simp add: fps_shift_times_fps_X_power'' fps_divide_def Let_def) finally show ?thesis . qed (simp_all add: fps_divide_def) @@ -1272,11 +1272,11 @@ with nz show ?thesis by (simp add: fps_mod_eq_zero fps_times_divide_eq) next assume "subdegree f < subdegree g" - have g_decomp: "g = h * X^n" unfolding h_def n_def by (rule subdegree_decompose) + have g_decomp: "g = h * fps_X^n" unfolding h_def n_def by (rule subdegree_decompose) have "f div g * g + f mod g = fps_shift n (f * inverse h) * g + fps_cutoff n (f * inverse h) * h" by (simp add: fps_mod_def fps_divide_def Let_def n_def h_def) - also have "... = h * (fps_shift n (f * inverse h) * X^n + fps_cutoff n (f * inverse h))" + also have "... = h * (fps_shift n (f * inverse h) * fps_X^n + fps_cutoff n (f * inverse h))" by (subst g_decomp) (simp add: algebra_simps) also have "... = f * (inverse h * h)" by (subst fps_shift_cutoff) simp @@ -1292,9 +1292,9 @@ proof - define m where "m = subdegree h" define h' where "h' = fps_shift m h" - have h_decomp: "h = h' * X ^ m" unfolding h'_def m_def by (rule subdegree_decompose) + have h_decomp: "h = h' * fps_X ^ m" unfolding h'_def m_def by (rule subdegree_decompose) from \<open>h \<noteq> 0\<close> have [simp]: "h'$0 \<noteq> 0" by (simp add: h'_def m_def) - have "(h * f) div (h * g) = (h' * f * X^m) div (h' * g * X^m)" + have "(h * f) div (h * g) = (h' * f * fps_X^m) div (h' * g * fps_X^m)" by (simp add: h_decomp algebra_simps) also have "... = f div g" by (simp add: fps_divide_cancel_aux1 fps_divide_cancel_aux2) finally show ?thesis . @@ -1306,10 +1306,10 @@ define n h' where dfs: "n = subdegree h" "h' = fps_shift n h" have "(f + g * h) div h = fps_shift n (f * inverse h') + fps_shift n (g * (h * inverse h'))" by (simp add: fps_divide_def Let_def dfs[symmetric] algebra_simps fps_shift_add) - also have "h * inverse h' = (inverse h' * h') * X^n" + also have "h * inverse h' = (inverse h' * h') * fps_X^n" by (subst subdegree_decompose) (simp_all add: dfs) - also have "... = X^n" by (subst inverse_mult_eq_1) (simp_all add: dfs) - also have "fps_shift n (g * X^n) = g" by simp + also have "... = fps_X^n" by (subst inverse_mult_eq_1) (simp_all add: dfs) + also have "fps_shift n (g * fps_X^n) = g" by simp also have "fps_shift n (f * inverse h') = f div h" by (simp add: fps_divide_def Let_def dfs) finally show "(f + g * h) div h = g + f div h" by simp @@ -1354,14 +1354,14 @@ qed (simp add: assms dvd_imp_subdegree_le) lemma fps_shift_altdef: - "fps_shift n f = (f :: 'a :: field fps) div X^n" + "fps_shift n f = (f :: 'a :: field fps) div fps_X^n" by (simp add: fps_divide_def) -lemma fps_div_X_power_nth: "((f :: 'a :: field fps) div X^n) $ k = f $ (k + n)" +lemma fps_div_fps_X_power_nth: "((f :: 'a :: field fps) div fps_X^n) $ k = f $ (k + n)" by (simp add: fps_shift_altdef [symmetric]) -lemma fps_div_X_nth: "((f :: 'a :: field fps) div X) $ k = f $ Suc k" - using fps_div_X_power_nth[of f 1] by simp +lemma fps_div_fps_X_nth: "((f :: 'a :: field fps) div fps_X) $ k = f $ Suc k" + using fps_div_fps_X_power_nth[of f 1] by simp lemma fps_const_inverse: "inverse (fps_const (a::'a::field)) = fps_const (inverse a)" by (cases "a \<noteq> 0", rule fps_inverse_unique) (auto simp: fps_eq_iff) @@ -1419,45 +1419,45 @@ lemma fps_gcd: assumes [simp]: "f \<noteq> 0" "g \<noteq> 0" - shows "gcd f g = X ^ min (subdegree f) (subdegree g)" + shows "gcd f g = fps_X ^ min (subdegree f) (subdegree g)" proof - let ?m = "min (subdegree f) (subdegree g)" - show "gcd f g = X ^ ?m" + show "gcd f g = fps_X ^ ?m" proof (rule sym, rule gcdI) fix d assume "d dvd f" "d dvd g" - thus "d dvd X ^ ?m" by (cases "d = 0") (auto simp: fps_dvd_iff) + thus "d dvd fps_X ^ ?m" by (cases "d = 0") (auto simp: fps_dvd_iff) qed (simp_all add: fps_dvd_iff) qed lemma fps_gcd_altdef: "gcd (f :: 'a :: field fps) g = (if f = 0 \<and> g = 0 then 0 else - if f = 0 then X ^ subdegree g else - if g = 0 then X ^ subdegree f else - X ^ min (subdegree f) (subdegree g))" + if f = 0 then fps_X ^ subdegree g else + if g = 0 then fps_X ^ subdegree f else + fps_X ^ min (subdegree f) (subdegree g))" by (simp add: fps_gcd) lemma fps_lcm: assumes [simp]: "f \<noteq> 0" "g \<noteq> 0" - shows "lcm f g = X ^ max (subdegree f) (subdegree g)" + shows "lcm f g = fps_X ^ max (subdegree f) (subdegree g)" proof - let ?m = "max (subdegree f) (subdegree g)" - show "lcm f g = X ^ ?m" + show "lcm f g = fps_X ^ ?m" proof (rule sym, rule lcmI) fix d assume "f dvd d" "g dvd d" - thus "X ^ ?m dvd d" by (cases "d = 0") (auto simp: fps_dvd_iff) + thus "fps_X ^ ?m dvd d" by (cases "d = 0") (auto simp: fps_dvd_iff) qed (simp_all add: fps_dvd_iff) qed lemma fps_lcm_altdef: "lcm (f :: 'a :: field fps) g = - (if f = 0 \<or> g = 0 then 0 else X ^ max (subdegree f) (subdegree g))" + (if f = 0 \<or> g = 0 then 0 else fps_X ^ max (subdegree f) (subdegree g))" by (simp add: fps_lcm) lemma fps_Gcd: assumes "A - {0} \<noteq> {}" - shows "Gcd A = X ^ (INF f:A-{0}. subdegree f)" + shows "Gcd A = fps_X ^ (INF f:A-{0}. subdegree f)" proof (rule sym, rule GcdI) fix f assume "f \<in> A" - thus "X ^ (INF f:A - {0}. subdegree f) dvd f" + thus "fps_X ^ (INF f:A - {0}. subdegree f) dvd f" by (cases "f = 0") (auto simp: fps_dvd_iff intro!: cINF_lower) next fix d assume d: "\<And>f. f \<in> A \<Longrightarrow> d dvd f" @@ -1465,25 +1465,25 @@ with d[of f] have [simp]: "d \<noteq> 0" by auto from d assms have "subdegree d \<le> (INF f:A-{0}. subdegree f)" by (intro cINF_greatest) (auto simp: fps_dvd_iff[symmetric]) - with d assms show "d dvd X ^ (INF f:A-{0}. subdegree f)" by (simp add: fps_dvd_iff) + with d assms show "d dvd fps_X ^ (INF f:A-{0}. subdegree f)" by (simp add: fps_dvd_iff) qed simp_all lemma fps_Gcd_altdef: "Gcd (A :: 'a :: field fps set) = - (if A \<subseteq> {0} then 0 else X ^ (INF f:A-{0}. subdegree f))" + (if A \<subseteq> {0} then 0 else fps_X ^ (INF f:A-{0}. subdegree f))" using fps_Gcd by auto lemma fps_Lcm: assumes "A \<noteq> {}" "0 \<notin> A" "bdd_above (subdegree`A)" - shows "Lcm A = X ^ (SUP f:A. subdegree f)" + shows "Lcm A = fps_X ^ (SUP f:A. subdegree f)" proof (rule sym, rule LcmI) fix f assume "f \<in> A" moreover from assms(3) have "bdd_above (subdegree ` A)" by auto - ultimately show "f dvd X ^ (SUP f:A. subdegree f)" using assms(2) + ultimately show "f dvd fps_X ^ (SUP f:A. subdegree f)" using assms(2) by (cases "f = 0") (auto simp: fps_dvd_iff intro!: cSUP_upper) next fix d assume d: "\<And>f. f \<in> A \<Longrightarrow> f dvd d" from assms obtain f where f: "f \<in> A" "f \<noteq> 0" by auto - show "X ^ (SUP f:A. subdegree f) dvd d" + show "fps_X ^ (SUP f:A. subdegree f) dvd d" proof (cases "d = 0") assume "d \<noteq> 0" moreover from d have "\<And>f. f \<in> A \<Longrightarrow> f \<noteq> 0 \<Longrightarrow> f dvd d" by blast @@ -1496,7 +1496,7 @@ lemma fps_Lcm_altdef: "Lcm (A :: 'a :: field fps set) = (if 0 \<in> A \<or> \<not>bdd_above (subdegree`A) then 0 else - if A = {} then 1 else X ^ (SUP f:A. subdegree f))" + if A = {} then 1 else fps_X ^ (SUP f:A. subdegree f))" proof (cases "bdd_above (subdegree`A)") assume unbounded: "\<not>bdd_above (subdegree`A)" have "Lcm A = 0" @@ -1568,8 +1568,8 @@ unfolding fps_eq_iff by auto qed -lemma fps_deriv_X[simp]: "fps_deriv X = 1" - by (simp add: fps_deriv_def X_def fps_eq_iff) +lemma fps_deriv_fps_X[simp]: "fps_deriv fps_X = 1" + by (simp add: fps_deriv_def fps_X_def fps_eq_iff) lemma fps_deriv_neg[simp]: "fps_deriv (- (f:: 'a::comm_ring_1 fps)) = - (fps_deriv f)" @@ -1878,7 +1878,7 @@ lemma divide_fps_const [simp]: "f / fps_const (c :: 'a :: field) = fps_const (inverse c) * f" by (cases "c = 0") (simp_all add: fps_divide_unit fps_const_inverse) -(* FIXME: The last part of this proof should go through by simp once we have a proper +(* FIfps_XME: The last part of this proof should go through by simp once we have a proper theorem collection for simplifying division on rings *) lemma fps_divide_deriv: assumes "b dvd (a :: 'a :: field fps)" @@ -1893,28 +1893,28 @@ thus ?thesis by (cases "b = 0") (auto simp: eq_divide_imp) qed -lemma fps_inverse_gp': "inverse (Abs_fps (\<lambda>n. 1::'a::field)) = 1 - X" - by (simp add: fps_inverse_gp fps_eq_iff X_def) - -lemma fps_one_over_one_minus_X_squared: - "inverse ((1 - X)^2 :: 'a :: field fps) = Abs_fps (\<lambda>n. of_nat (n+1))" +lemma fps_inverse_gp': "inverse (Abs_fps (\<lambda>n. 1::'a::field)) = 1 - fps_X" + by (simp add: fps_inverse_gp fps_eq_iff fps_X_def) + +lemma fps_one_over_one_minus_fps_X_squared: + "inverse ((1 - fps_X)^2 :: 'a :: field fps) = Abs_fps (\<lambda>n. of_nat (n+1))" proof - - have "inverse ((1 - X)^2 :: 'a fps) = fps_deriv (inverse (1 - X))" + have "inverse ((1 - fps_X)^2 :: 'a fps) = fps_deriv (inverse (1 - fps_X))" by (subst fps_inverse_deriv) (simp_all add: fps_inverse_power) - also have "inverse (1 - X :: 'a fps) = Abs_fps (\<lambda>_. 1)" + also have "inverse (1 - fps_X :: 'a fps) = Abs_fps (\<lambda>_. 1)" by (subst fps_inverse_gp' [symmetric]) simp also have "fps_deriv \<dots> = Abs_fps (\<lambda>n. of_nat (n + 1))" by (simp add: fps_deriv_def) finally show ?thesis . qed -lemma fps_nth_deriv_X[simp]: "fps_nth_deriv n X = (if n = 0 then X else if n=1 then 1 else 0)" +lemma fps_nth_deriv_fps_X[simp]: "fps_nth_deriv n fps_X = (if n = 0 then fps_X else if n=1 then 1 else 0)" by (cases n) simp_all -lemma fps_inverse_X_plus1: "inverse (1 + X) = Abs_fps (\<lambda>n. (- (1::'a::field)) ^ n)" +lemma fps_inverse_fps_X_plus1: "inverse (1 + fps_X) = Abs_fps (\<lambda>n. (- (1::'a::field)) ^ n)" (is "_ = ?r") proof - - have eq: "(1 + X) * ?r = 1" + have eq: "(1 + fps_X) * ?r = 1" unfolding minus_one_power_iff by (auto simp add: field_simps fps_eq_iff) show ?thesis @@ -1956,7 +1956,7 @@ lemma fps_compose_nth_0 [simp]: "(f oo g) $ 0 = f $ 0" by (simp add: fps_compose_nth) -lemma fps_compose_X[simp]: "a oo X = (a :: 'a::comm_ring_1 fps)" +lemma fps_compose_fps_X[simp]: "a oo fps_X = (a :: 'a::comm_ring_1 fps)" by (simp add: fps_ext fps_compose_def mult_delta_right sum.delta') lemma fps_const_compose[simp]: "fps_const (a::'a::comm_ring_1) oo b = fps_const a" @@ -1968,7 +1968,7 @@ lemma neg_numeral_compose[simp]: "(- numeral k :: 'a::comm_ring_1 fps) oo b = - numeral k" unfolding neg_numeral_fps_const by simp -lemma X_fps_compose_startby0[simp]: "a$0 = 0 \<Longrightarrow> X oo a = (a :: 'a::comm_ring_1 fps)" +lemma fps_X_fps_compose_startby0[simp]: "a$0 = 0 \<Longrightarrow> fps_X oo a = (a :: 'a::comm_ring_1 fps)" by (simp add: fps_eq_iff fps_compose_def mult_delta_left sum.delta not_le) @@ -1978,14 +1978,14 @@ (* {a_{n+k}}_0^infty Corresponds to (f - sum (\<lambda>i. a_i * x^i))/x^h, for h>0*) lemma fps_power_mult_eq_shift: - "X^Suc k * Abs_fps (\<lambda>n. a (n + Suc k)) = - Abs_fps a - sum (\<lambda>i. fps_const (a i :: 'a::comm_ring_1) * X^i) {0 .. k}" + "fps_X^Suc k * Abs_fps (\<lambda>n. a (n + Suc k)) = + Abs_fps a - sum (\<lambda>i. fps_const (a i :: 'a::comm_ring_1) * fps_X^i) {0 .. k}" (is "?lhs = ?rhs") proof - have "?lhs $ n = ?rhs $ n" for n :: nat proof - have "?lhs $ n = (if n < Suc k then 0 else a n)" - unfolding X_power_mult_nth by auto + unfolding fps_X_power_mult_nth by auto also have "\<dots> = ?rhs $ n" proof (induct k) case 0 @@ -1993,14 +1993,14 @@ by (simp add: fps_sum_nth) next case (Suc k) - have "(Abs_fps a - sum (\<lambda>i. fps_const (a i :: 'a) * X^i) {0 .. Suc k})$n = - (Abs_fps a - sum (\<lambda>i. fps_const (a i :: 'a) * X^i) {0 .. k} - - fps_const (a (Suc k)) * X^ Suc k) $ n" + have "(Abs_fps a - sum (\<lambda>i. fps_const (a i :: 'a) * fps_X^i) {0 .. Suc k})$n = + (Abs_fps a - sum (\<lambda>i. fps_const (a i :: 'a) * fps_X^i) {0 .. k} - + fps_const (a (Suc k)) * fps_X^ Suc k) $ n" by (simp add: field_simps) - also have "\<dots> = (if n < Suc k then 0 else a n) - (fps_const (a (Suc k)) * X^ Suc k)$n" + also have "\<dots> = (if n < Suc k then 0 else a n) - (fps_const (a (Suc k)) * fps_X^ Suc k)$n" using Suc.hyps[symmetric] unfolding fps_sub_nth by simp also have "\<dots> = (if n < Suc (Suc k) then 0 else a n)" - unfolding X_power_mult_right_nth + unfolding fps_X_power_mult_right_nth apply (auto simp add: not_less fps_const_def) apply (rule cong[of a a, OF refl]) apply arith @@ -2021,29 +2021,29 @@ (* If f reprents {a_n} and P is a polynomial, then P(xD) f represents {P(n) a_n}*) -definition "XD = op * X \<circ> fps_deriv" - -lemma XD_add[simp]:"XD (a + b) = XD a + XD (b :: 'a::comm_ring_1 fps)" - by (simp add: XD_def field_simps) - -lemma XD_mult_const[simp]:"XD (fps_const (c::'a::comm_ring_1) * a) = fps_const c * XD a" - by (simp add: XD_def field_simps) - -lemma XD_linear[simp]: "XD (fps_const c * a + fps_const d * b) = - fps_const c * XD a + fps_const d * XD (b :: 'a::comm_ring_1 fps)" +definition "fps_XD = op * fps_X \<circ> fps_deriv" + +lemma fps_XD_add[simp]:"fps_XD (a + b) = fps_XD a + fps_XD (b :: 'a::comm_ring_1 fps)" + by (simp add: fps_XD_def field_simps) + +lemma fps_XD_mult_const[simp]:"fps_XD (fps_const (c::'a::comm_ring_1) * a) = fps_const c * fps_XD a" + by (simp add: fps_XD_def field_simps) + +lemma fps_XD_linear[simp]: "fps_XD (fps_const c * a + fps_const d * b) = + fps_const c * fps_XD a + fps_const d * fps_XD (b :: 'a::comm_ring_1 fps)" by simp -lemma XDN_linear: - "(XD ^^ n) (fps_const c * a + fps_const d * b) = - fps_const c * (XD ^^ n) a + fps_const d * (XD ^^ n) (b :: 'a::comm_ring_1 fps)" +lemma fps_XDN_linear: + "(fps_XD ^^ n) (fps_const c * a + fps_const d * b) = + fps_const c * (fps_XD ^^ n) a + fps_const d * (fps_XD ^^ n) (b :: 'a::comm_ring_1 fps)" by (induct n) simp_all -lemma fps_mult_X_deriv_shift: "X* fps_deriv a = Abs_fps (\<lambda>n. of_nat n* a$n)" +lemma fps_mult_fps_X_deriv_shift: "fps_X* fps_deriv a = Abs_fps (\<lambda>n. of_nat n* a$n)" by (simp add: fps_eq_iff) -lemma fps_mult_XD_shift: - "(XD ^^ k) (a :: 'a::comm_ring_1 fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)" - by (induct k arbitrary: a) (simp_all add: XD_def fps_eq_iff field_simps del: One_nat_def) +lemma fps_mult_fps_XD_shift: + "(fps_XD ^^ k) (a :: 'a::comm_ring_1 fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)" + by (induct k arbitrary: a) (simp_all add: fps_XD_def fps_eq_iff field_simps del: One_nat_def) subsubsection \<open>Rule 3\<close> @@ -2051,15 +2051,15 @@ text \<open>Rule 3 is trivial and is given by \<open>fps_times_def\<close>.\<close> -subsubsection \<open>Rule 5 --- summation and "division" by (1 - X)\<close> - -lemma fps_divide_X_minus1_sum_lemma: - "a = ((1::'a::comm_ring_1 fps) - X) * Abs_fps (\<lambda>n. sum (\<lambda>i. a $ i) {0..n})" +subsubsection \<open>Rule 5 --- summation and "division" by (1 - fps_X)\<close> + +lemma fps_divide_fps_X_minus1_sum_lemma: + "a = ((1::'a::comm_ring_1 fps) - fps_X) * Abs_fps (\<lambda>n. sum (\<lambda>i. a $ i) {0..n})" proof - let ?sa = "Abs_fps (\<lambda>n. sum (\<lambda>i. a $ i) {0..n})" - have th0: "\<And>i. (1 - (X::'a fps)) $ i = (if i = 0 then 1 else if i = 1 then - 1 else 0)" + have th0: "\<And>i. (1 - (fps_X::'a fps)) $ i = (if i = 0 then 1 else if i = 1 then - 1 else 0)" by simp - have "a$n = ((1 - X) * ?sa) $ n" for n + have "a$n = ((1 - fps_X) * ?sa) $ n" for n proof (cases "n = 0") case True then show ?thesis @@ -2073,7 +2073,7 @@ using False by simp_all have f: "finite {0}" "finite {1}" "finite {2 .. n}" "finite {0 .. n - 1}" "finite {n}" by simp_all - have "((1 - X) * ?sa) $ n = sum (\<lambda>i. (1 - X)$ i * ?sa $ (n - i)) {0 .. n}" + have "((1 - fps_X) * ?sa) $ n = sum (\<lambda>i. (1 - fps_X)$ i * ?sa $ (n - i)) {0 .. n}" by (simp add: fps_mult_nth) also have "\<dots> = a$n" unfolding th0 @@ -2090,16 +2090,16 @@ unfolding fps_eq_iff by blast qed -lemma fps_divide_X_minus1_sum: - "a /((1::'a::field fps) - X) = Abs_fps (\<lambda>n. sum (\<lambda>i. a $ i) {0..n})" +lemma fps_divide_fps_X_minus1_sum: + "a /((1::'a::field fps) - fps_X) = Abs_fps (\<lambda>n. sum (\<lambda>i. a $ i) {0..n})" proof - - let ?X = "1 - (X::'a fps)" - have th0: "?X $ 0 \<noteq> 0" + let ?fps_X = "1 - (fps_X::'a fps)" + have th0: "?fps_X $ 0 \<noteq> 0" by simp - have "a /?X = ?X * Abs_fps (\<lambda>n::nat. sum (op $ a) {0..n}) * inverse ?X" - using fps_divide_X_minus1_sum_lemma[of a, symmetric] th0 + have "a /?fps_X = ?fps_X * Abs_fps (\<lambda>n::nat. sum (op $ a) {0..n}) * inverse ?fps_X" + using fps_divide_fps_X_minus1_sum_lemma[of a, symmetric] th0 by (simp add: fps_divide_def mult.assoc) - also have "\<dots> = (inverse ?X * ?X) * Abs_fps (\<lambda>n::nat. sum (op $ a) {0..n}) " + also have "\<dots> = (inverse ?fps_X * ?fps_X) * Abs_fps (\<lambda>n::nat. sum (op $ a) {0..n}) " by (simp add: ac_simps) finally show ?thesis by (simp add: inverse_mult_eq_1[OF th0]) @@ -2495,10 +2495,10 @@ also have "subdegree \<dots> = Suc m * subdegree g" by (rule subdegree_power) finally have [simp]: "subdegree f = subdegree g" by (subst (asm) Suc_mult_cancel1) - have "fps_shift (subdegree f) f * X ^ subdegree f = f" + have "fps_shift (subdegree f) f * fps_X ^ subdegree f = f" by (rule subdegree_decompose [symmetric]) also have "\<dots> ^ Suc m = g ^ Suc m" by fact - also have "g = fps_shift (subdegree g) g * X ^ subdegree g" + also have "g = fps_shift (subdegree g) g * fps_X ^ subdegree g" by (rule subdegree_decompose) also have "subdegree f = subdegree g" by fact finally have "fps_shift (subdegree g) f ^ Suc m = fps_shift (subdegree g) g ^ Suc m" @@ -3127,17 +3127,17 @@ then show ?thesis by (simp add: fps_eq_iff) qed -lemma fps_mult_X_plus_1_nth: - "((1+X)*a) $n = (if n = 0 then (a$n :: 'a::comm_ring_1) else a$n + a$(n - 1))" +lemma fps_mult_fps_X_plus_1_nth: + "((1+fps_X)*a) $n = (if n = 0 then (a$n :: 'a::comm_ring_1) else a$n + a$(n - 1))" proof (cases n) case 0 then show ?thesis by (simp add: fps_mult_nth) next case (Suc m) - have "((1 + X)*a) $ n = sum (\<lambda>i. (1 + X) $ i * a $ (n - i)) {0..n}" + have "((1 + fps_X)*a) $ n = sum (\<lambda>i. (1 + fps_X) $ i * a $ (n - i)) {0..n}" by (simp add: fps_mult_nth) - also have "\<dots> = sum (\<lambda>i. (1+X)$i * a$(n-i)) {0.. 1}" + also have "\<dots> = sum (\<lambda>i. (1+fps_X)$i * a$(n-i)) {0.. 1}" unfolding Suc by (rule sum.mono_neutral_right) auto also have "\<dots> = (if n = 0 then (a$n :: 'a::comm_ring_1) else a$n + a$(n - 1))" by (simp add: Suc) @@ -3145,14 +3145,14 @@ qed -subsection \<open>Finite FPS (i.e. polynomials) and X\<close> - -lemma fps_poly_sum_X: +subsection \<open>Finite FPS (i.e. polynomials) and fps_X\<close> + +lemma fps_poly_sum_fps_X: assumes "\<forall>i > n. a$i = (0::'a::comm_ring_1)" - shows "a = sum (\<lambda>i. fps_const (a$i) * X^i) {0..n}" (is "a = ?r") + shows "a = sum (\<lambda>i. fps_const (a$i) * fps_X^i) {0..n}" (is "a = ?r") proof - have "a$i = ?r$i" for i - unfolding fps_sum_nth fps_mult_left_const_nth X_power_nth + unfolding fps_sum_nth fps_mult_left_const_nth fps_X_power_nth by (simp add: mult_delta_right sum.delta' assms) then show ?thesis unfolding fps_eq_iff by blast @@ -3163,23 +3163,23 @@ fun compinv :: "'a fps \<Rightarrow> nat \<Rightarrow> 'a::field" where - "compinv a 0 = X$0" + "compinv a 0 = fps_X$0" | "compinv a (Suc n) = - (X$ Suc n - sum (\<lambda>i. (compinv a i) * (a^i)$Suc n) {0 .. n}) / (a$1) ^ Suc n" + (fps_X$ Suc n - sum (\<lambda>i. (compinv a i) * (a^i)$Suc n) {0 .. n}) / (a$1) ^ Suc n" definition "fps_inv a = Abs_fps (compinv a)" lemma fps_inv: assumes a0: "a$0 = 0" and a1: "a$1 \<noteq> 0" - shows "fps_inv a oo a = X" + shows "fps_inv a oo a = fps_X" proof - let ?i = "fps_inv a oo a" - have "?i $n = X$n" for n + have "?i $n = fps_X$n" for n proof (induct n rule: nat_less_induct) fix n - assume h: "\<forall>m<n. ?i$m = X$m" - show "?i $ n = X$n" + assume h: "\<forall>m<n. ?i$m = fps_X$m" + show "?i $ n = fps_X$n" proof (cases n) case 0 then show ?thesis using a0 @@ -3189,9 +3189,9 @@ have "?i $ n = sum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1} + fps_inv a $ Suc n1 * (a $ 1)^ Suc n1" by (simp only: fps_compose_nth) (simp add: Suc startsby_zero_power_nth_same [OF a0] del: power_Suc) also have "\<dots> = sum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1} + - (X$ Suc n1 - sum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1})" + (fps_X$ Suc n1 - sum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1})" using a0 a1 Suc by (simp add: fps_inv_def) - also have "\<dots> = X$n" using Suc by simp + also have "\<dots> = fps_X$n" using Suc by simp finally show ?thesis . qed qed @@ -3238,7 +3238,7 @@ by (simp add: fps_eq_iff) qed -lemma fps_inv_ginv: "fps_inv = fps_ginv X" +lemma fps_inv_ginv: "fps_inv = fps_ginv fps_X" apply (auto simp add: fun_eq_iff fps_eq_iff fps_inv_def fps_ginv_def) apply (induct_tac n rule: nat_less_induct) apply auto @@ -3427,7 +3427,7 @@ lemma fps_compose_sub_distrib: "(a - b) oo (c::'a::ring_1 fps) = (a oo c) - (b oo c)" using fps_compose_add_distrib [of a "- b" c] by (simp add: fps_compose_uminus) -lemma X_fps_compose: "X oo a = Abs_fps (\<lambda>n. if n = 0 then (0::'a::comm_ring_1) else a$n)" +lemma fps_X_fps_compose: "fps_X oo a = Abs_fps (\<lambda>n. if n = 0 then (0::'a::comm_ring_1) else a$n)" by (simp add: fps_eq_iff fps_compose_nth mult_delta_left sum.delta) lemma fps_inverse_compose: @@ -3463,16 +3463,16 @@ (is "?one oo a = _") proof - have o0: "?one $ 0 \<noteq> 0" by simp - have th0: "(1 - X) $ 0 \<noteq> (0::'a)" by simp + have th0: "(1 - fps_X) $ 0 \<noteq> (0::'a)" by simp from fps_inverse_gp[where ?'a = 'a] - have "inverse ?one = 1 - X" by (simp add: fps_eq_iff) - then have "inverse (inverse ?one) = inverse (1 - X)" by simp - then have th: "?one = 1/(1 - X)" unfolding fps_inverse_idempotent[OF o0] + have "inverse ?one = 1 - fps_X" by (simp add: fps_eq_iff) + then have "inverse (inverse ?one) = inverse (1 - fps_X)" by simp + then have th: "?one = 1/(1 - fps_X)" unfolding fps_inverse_idempotent[OF o0] by (simp add: fps_divide_def) show ?thesis unfolding th unfolding fps_divide_compose[OF a0 th0] - fps_compose_1 fps_compose_sub_distrib X_fps_compose_startby0[OF a0] .. + fps_compose_1 fps_compose_sub_distrib fps_X_fps_compose_startby0[OF a0] .. qed lemma fps_const_power [simp]: "fps_const (c::'a::ring_1) ^ n = fps_const (c^n)" @@ -3535,7 +3535,7 @@ lemma fps_X_power_compose: assumes a0: "a$0=0" - shows "X^k oo a = (a::'a::idom fps)^k" + shows "fps_X^k oo a = (a::'a::idom fps)^k" (is "?l = ?r") proof (cases k) case 0 @@ -3564,7 +3564,7 @@ lemma fps_inv_right: assumes a0: "a$0 = 0" and a1: "a$1 \<noteq> 0" - shows "a oo fps_inv a = X" + shows "a oo fps_inv a = fps_X" proof - let ?ia = "fps_inv a" let ?iaa = "a oo fps_inv a" @@ -3572,12 +3572,12 @@ by (simp add: fps_inv_def) have th1: "?iaa $ 0 = 0" using a0 a1 by (simp add: fps_inv_def fps_compose_nth) - have th2: "X$0 = 0" + have th2: "fps_X$0 = 0" by simp - from fps_inv[OF a0 a1] have "a oo (fps_inv a oo a) = a oo X" + from fps_inv[OF a0 a1] have "a oo (fps_inv a oo a) = a oo fps_X" by simp - then have "(a oo fps_inv a) oo a = X oo a" - by (simp add: fps_compose_assoc[OF a0 th0] X_fps_compose_startby0[OF a0]) + then have "(a oo fps_inv a) oo a = fps_X oo a" + by (simp add: fps_compose_assoc[OF a0 th0] fps_X_fps_compose_startby0[OF a0]) with fps_compose_inj_right[OF a0 a1] show ?thesis by simp qed @@ -3612,13 +3612,13 @@ by (simp add: fps_inv_def) from a1 have ra1: "?r a $ 1 \<noteq> 0" by (simp add: fps_inv_def field_simps) - have X0: "X$0 = 0" + have fps_X0: "fps_X$0 = 0" by simp - from fps_inv[OF ra0 ra1] have "?r (?r a) oo ?r a = X" . - then have "?r (?r a) oo ?r a oo a = X oo a" + from fps_inv[OF ra0 ra1] have "?r (?r a) oo ?r a = fps_X" . + then have "?r (?r a) oo ?r a oo a = fps_X oo a" by simp then have "?r (?r a) oo (?r a oo a) = a" - unfolding X_fps_compose_startby0[OF a0] + unfolding fps_X_fps_compose_startby0[OF a0] unfolding fps_compose_assoc[OF a0 ra0, symmetric] . then show ?thesis unfolding fps_inv[OF a0 a1] by simp @@ -3661,13 +3661,13 @@ lemma fps_ginv_deriv: assumes a0:"a$0 = (0::'a::field)" and a1: "a$1 \<noteq> 0" - shows "fps_deriv (fps_ginv b a) = (fps_deriv b / fps_deriv a) oo fps_ginv X a" + shows "fps_deriv (fps_ginv b a) = (fps_deriv b / fps_deriv a) oo fps_ginv fps_X a" proof - let ?ia = "fps_ginv b a" - let ?iXa = "fps_ginv X a" + let ?ifps_Xa = "fps_ginv fps_X a" let ?d = "fps_deriv" let ?dia = "?d ?ia" - have iXa0: "?iXa $ 0 = 0" + have ifps_Xa0: "?ifps_Xa $ 0 = 0" by (simp add: fps_ginv_def) have da0: "?d a $ 0 \<noteq> 0" using a1 by simp @@ -3679,21 +3679,21 @@ by simp with a1 have "(?d ?ia oo a) * (inverse (?d a) * ?d a) = ?d b / ?d a" by (simp add: fps_divide_unit) - then have "(?d ?ia oo a) oo ?iXa = (?d b / ?d a) oo ?iXa" + then have "(?d ?ia oo a) oo ?ifps_Xa = (?d b / ?d a) oo ?ifps_Xa" unfolding inverse_mult_eq_1[OF da0] by simp - then have "?d ?ia oo (a oo ?iXa) = (?d b / ?d a) oo ?iXa" - unfolding fps_compose_assoc[OF iXa0 a0] . + then have "?d ?ia oo (a oo ?ifps_Xa) = (?d b / ?d a) oo ?ifps_Xa" + unfolding fps_compose_assoc[OF ifps_Xa0 a0] . then show ?thesis unfolding fps_inv_ginv[symmetric] unfolding fps_inv_right[OF a0 a1] by simp qed lemma fps_compose_linear: - "fps_compose (f :: 'a :: comm_ring_1 fps) (fps_const c * X) = Abs_fps (\<lambda>n. c^n * f $ n)" + "fps_compose (f :: 'a :: comm_ring_1 fps) (fps_const c * fps_X) = Abs_fps (\<lambda>n. c^n * f $ n)" by (simp add: fps_eq_iff fps_compose_def power_mult_distrib if_distrib sum.delta' cong: if_cong) lemma fps_compose_uminus': - "fps_compose f (-X :: 'a :: comm_ring_1 fps) = Abs_fps (\<lambda>n. (-1)^n * f $ n)" + "fps_compose f (-fps_X :: 'a :: comm_ring_1 fps) = Abs_fps (\<lambda>n. (-1)^n * f $ n)" using fps_compose_linear[of f "-1"] by (simp only: fps_const_neg [symmetric] fps_const_1_eq_1) simp @@ -3768,21 +3768,21 @@ "fps_nth_deriv n (fps_exp (a::'a::field_char_0)) = (fps_const a)^n * (fps_exp a)" by (induct n) auto -lemma X_compose_fps_exp[simp]: "X oo fps_exp (a::'a::field) = fps_exp a - 1" - by (simp add: fps_eq_iff X_fps_compose) +lemma fps_X_compose_fps_exp[simp]: "fps_X oo fps_exp (a::'a::field) = fps_exp a - 1" + by (simp add: fps_eq_iff fps_X_fps_compose) lemma fps_inv_fps_exp_compose: assumes a: "a \<noteq> 0" - shows "fps_inv (fps_exp a - 1) oo (fps_exp a - 1) = X" - and "(fps_exp a - 1) oo fps_inv (fps_exp a - 1) = X" + shows "fps_inv (fps_exp a - 1) oo (fps_exp a - 1) = fps_X" + and "(fps_exp a - 1) oo fps_inv (fps_exp a - 1) = fps_X" proof - let ?b = "fps_exp a - 1" have b0: "?b $ 0 = 0" by simp have b1: "?b $ 1 \<noteq> 0" by (simp add: a) - from fps_inv[OF b0 b1] show "fps_inv (fps_exp a - 1) oo (fps_exp a - 1) = X" . - from fps_inv_right[OF b0 b1] show "(fps_exp a - 1) oo fps_inv (fps_exp a - 1) = X" . + from fps_inv[OF b0 b1] show "fps_inv (fps_exp a - 1) oo (fps_exp a - 1) = fps_X" . + from fps_inv_right[OF b0 b1] show "(fps_exp a - 1) oo fps_inv (fps_exp a - 1) = fps_X" . qed lemma fps_exp_power_mult: "(fps_exp (c::'a::field_char_0))^n = fps_exp (of_nat n * c)" @@ -3804,11 +3804,11 @@ qed lemma fps_exp_compose_linear [simp]: - "fps_exp (d::'a::field_char_0) oo (fps_const c * X) = fps_exp (c * d)" + "fps_exp (d::'a::field_char_0) oo (fps_const c * fps_X) = fps_exp (c * d)" by (simp add: fps_compose_linear fps_exp_def fps_eq_iff power_mult_distrib) lemma fps_fps_exp_compose_minus [simp]: - "fps_compose (fps_exp c) (-X) = fps_exp (-c :: 'a :: field_char_0)" + "fps_compose (fps_exp c) (-fps_X) = fps_exp (-c :: 'a :: field_char_0)" using fps_exp_compose_linear[of c "-1 :: 'a"] unfolding fps_const_neg [symmetric] fps_const_1_eq_1 by simp @@ -3844,14 +3844,14 @@ lemma Abs_fps_if_0: "Abs_fps (\<lambda>n. if n = 0 then (v::'a::ring_1) else f n) = - fps_const v + X * Abs_fps (\<lambda>n. f (Suc n))" + fps_const v + fps_X * Abs_fps (\<lambda>n. f (Suc n))" by (auto simp add: fps_eq_iff) definition fps_ln :: "'a::field_char_0 \<Rightarrow> 'a fps" where "fps_ln c = fps_const (1/c) * Abs_fps (\<lambda>n. if n = 0 then 0 else (- 1) ^ (n - 1) / of_nat n)" -lemma fps_ln_deriv: "fps_deriv (fps_ln c) = fps_const (1/c) * inverse (1 + X)" - unfolding fps_inverse_X_plus1 +lemma fps_ln_deriv: "fps_deriv (fps_ln c) = fps_const (1/c) * inverse (1 + fps_X)" + unfolding fps_inverse_fps_X_plus1 by (simp add: fps_ln_def fps_eq_iff del: of_nat_Suc) lemma fps_ln_nth: "fps_ln c $ n = (if n = 0 then 0 else 1/c * ((- 1) ^ (n - 1) / of_nat n))" @@ -3870,13 +3870,13 @@ have "fps_deriv (fps_exp a - 1) oo fps_inv (fps_exp a - 1) = (fps_const a * (fps_exp a - 1) + fps_const a) oo fps_inv (fps_exp a - 1)" by (simp add: field_simps) - also have "\<dots> = fps_const a * (X + 1)" + also have "\<dots> = fps_const a * (fps_X + 1)" apply (simp add: fps_compose_add_distrib fps_const_mult_apply_left[symmetric] fps_inv_right[OF b0 b1]) apply (simp add: field_simps) done - finally have eq: "fps_deriv (fps_exp a - 1) oo fps_inv (fps_exp a - 1) = fps_const a * (X + 1)" . + finally have eq: "fps_deriv (fps_exp a - 1) oo fps_inv (fps_exp a - 1) = fps_const a * (fps_X + 1)" . from fps_inv_deriv[OF b0 b1, unfolded eq] - have "fps_deriv (fps_inv ?b) = fps_const (inverse a) / (X + 1)" + have "fps_deriv (fps_inv ?b) = fps_const (inverse a) / (fps_X + 1)" using a by (simp add: fps_const_inverse eq fps_divide_def fps_inverse_mult) then have "fps_deriv ?l = fps_deriv ?r" by (simp add: fps_ln_deriv add.commute fps_divide_def divide_inverse) @@ -3891,7 +3891,7 @@ (is "?r = ?l") proof- from c0 d0 have eq: "1/c + 1/d = (c+d)/(c*d)" by (simp add: field_simps) - have "fps_deriv ?r = fps_const (1/c + 1/d) * inverse (1 + X)" + have "fps_deriv ?r = fps_const (1/c + 1/d) * inverse (1 + fps_X)" by (simp add: fps_ln_deriv fps_const_add[symmetric] algebra_simps del: fps_const_add) also have "\<dots> = fps_deriv ?l" apply (simp add: fps_ln_deriv) @@ -3901,9 +3901,9 @@ unfolding fps_deriv_eq_iff by simp qed -lemma X_dvd_fps_ln [simp]: "X dvd fps_ln c" +lemma fps_X_dvd_fps_ln [simp]: "fps_X dvd fps_ln c" proof - - have "fps_ln c = X * Abs_fps (\<lambda>n. (-1) ^ n / (of_nat (Suc n) * c))" + have "fps_ln c = fps_X * Abs_fps (\<lambda>n. (-1) ^ n / (of_nat (Suc n) * c))" by (intro fps_ext) (auto simp: fps_ln_def of_nat_diff) thus ?thesis by simp qed @@ -3918,11 +3918,11 @@ lemma fps_binomial_ODE_unique: fixes c :: "'a::field_char_0" - shows "fps_deriv a = (fps_const c * a) / (1 + X) \<longleftrightarrow> a = fps_const (a$0) * fps_binomial c" + shows "fps_deriv a = (fps_const c * a) / (1 + fps_X) \<longleftrightarrow> a = fps_const (a$0) * fps_binomial c" (is "?lhs \<longleftrightarrow> ?rhs") proof let ?da = "fps_deriv a" - let ?x1 = "(1 + X):: 'a fps" + let ?x1 = "(1 + fps_X):: 'a fps" let ?l = "?x1 * ?da" let ?r = "fps_const c * a" @@ -3985,10 +3985,10 @@ qed lemma fps_binomial_ODE_unique': - "(fps_deriv a = fps_const c * a / (1 + X) \<and> a $ 0 = 1) \<longleftrightarrow> (a = fps_binomial c)" + "(fps_deriv a = fps_const c * a / (1 + fps_X) \<and> a $ 0 = 1) \<longleftrightarrow> (a = fps_binomial c)" by (subst fps_binomial_ODE_unique) auto -lemma fps_binomial_deriv: "fps_deriv (fps_binomial c) = fps_const c * fps_binomial c / (1 + X)" +lemma fps_binomial_deriv: "fps_deriv (fps_binomial c) = fps_const c * fps_binomial c / (1 + fps_X)" proof - let ?a = "fps_binomial c" have th0: "?a = fps_const (?a$0) * ?a" by (simp) @@ -4001,13 +4001,13 @@ let ?b = "fps_binomial" let ?db = "\<lambda>x. fps_deriv (?b x)" have "fps_deriv ?P = ?db c * ?b d + ?b c * ?db d - ?db (c + d)" by simp - also have "\<dots> = inverse (1 + X) * + also have "\<dots> = inverse (1 + fps_X) * (fps_const c * ?b c * ?b d + fps_const d * ?b c * ?b d - fps_const (c+d) * ?b (c + d))" unfolding fps_binomial_deriv by (simp add: fps_divide_def field_simps) - also have "\<dots> = (fps_const (c + d)/ (1 + X)) * ?P" + also have "\<dots> = (fps_const (c + d)/ (1 + fps_X)) * ?P" by (simp add: field_simps fps_divide_unit fps_const_add[symmetric] del: fps_const_add) - finally have th0: "fps_deriv ?P = fps_const (c+d) * ?P / (1 + X)" + finally have th0: "fps_deriv ?P = fps_const (c+d) * ?P / (1 + fps_X)" by (simp add: fps_divide_def) have "?P = fps_const (?P$0) * ?b (c + d)" unfolding fps_binomial_ODE_unique[symmetric] @@ -4016,35 +4016,35 @@ then show ?thesis by simp qed -lemma fps_binomial_minus_one: "fps_binomial (- 1) = inverse (1 + X)" +lemma fps_binomial_minus_one: "fps_binomial (- 1) = inverse (1 + fps_X)" (is "?l = inverse ?r") proof- have th: "?r$0 \<noteq> 0" by simp - have th': "fps_deriv (inverse ?r) = fps_const (- 1) * inverse ?r / (1 + X)" + have th': "fps_deriv (inverse ?r) = fps_const (- 1) * inverse ?r / (1 + fps_X)" by (simp add: fps_inverse_deriv[OF th] fps_divide_def power2_eq_square mult.commute fps_const_neg[symmetric] del: fps_const_neg) have eq: "inverse ?r $ 0 = 1" by (simp add: fps_inverse_def) - from iffD1[OF fps_binomial_ODE_unique[of "inverse (1 + X)" "- 1"] th'] eq + from iffD1[OF fps_binomial_ODE_unique[of "inverse (1 + fps_X)" "- 1"] th'] eq show ?thesis by (simp add: fps_inverse_def) qed -lemma fps_binomial_of_nat: "fps_binomial (of_nat n) = (1 + X :: 'a :: field_char_0 fps) ^ n" +lemma fps_binomial_of_nat: "fps_binomial (of_nat n) = (1 + fps_X :: 'a :: field_char_0 fps) ^ n" proof (cases "n = 0") case [simp]: True - have "fps_deriv ((1 + X) ^ n :: 'a fps) = 0" by simp - also have "\<dots> = fps_const (of_nat n) * (1 + X) ^ n / (1 + X)" by (simp add: fps_binomial_def) + have "fps_deriv ((1 + fps_X) ^ n :: 'a fps) = 0" by simp + also have "\<dots> = fps_const (of_nat n) * (1 + fps_X) ^ n / (1 + fps_X)" by (simp add: fps_binomial_def) finally show ?thesis by (subst sym, subst fps_binomial_ODE_unique' [symmetric]) simp_all next case False - have "fps_deriv ((1 + X) ^ n :: 'a fps) = fps_const (of_nat n) * (1 + X) ^ (n - 1)" + have "fps_deriv ((1 + fps_X) ^ n :: 'a fps) = fps_const (of_nat n) * (1 + fps_X) ^ (n - 1)" by (simp add: fps_deriv_power) - also have "(1 + X :: 'a fps) $ 0 \<noteq> 0" by simp - hence "(1 + X :: 'a fps) \<noteq> 0" by (intro notI) (simp only: , simp) - with False have "(1 + X :: 'a fps) ^ (n - 1) = (1 + X) ^ n / (1 + X)" + also have "(1 + fps_X :: 'a fps) $ 0 \<noteq> 0" by simp + hence "(1 + fps_X :: 'a fps) \<noteq> 0" by (intro notI) (simp only: , simp) + with False have "(1 + fps_X :: 'a fps) ^ (n - 1) = (1 + fps_X) ^ n / (1 + fps_X)" by (cases n) (simp_all ) - also have "fps_const (of_nat n :: 'a) * ((1 + X) ^ n / (1 + X)) = - fps_const (of_nat n) * (1 + X) ^ n / (1 + X)" + also have "fps_const (of_nat n :: 'a) * ((1 + fps_X) ^ n / (1 + fps_X)) = + fps_const (of_nat n) * (1 + fps_X) ^ n / (1 + fps_X)" by (simp add: unit_div_mult_swap) finally show ?thesis by (subst sym, subst fps_binomial_ODE_unique' [symmetric]) (simp_all add: fps_power_nth) @@ -4056,24 +4056,24 @@ lemma fps_binomial_power: "fps_binomial a ^ n = fps_binomial (of_nat n * a)" by (induction n) (simp_all add: fps_binomial_add_mult ring_distribs) -lemma fps_binomial_1: "fps_binomial 1 = 1 + X" +lemma fps_binomial_1: "fps_binomial 1 = 1 + fps_X" using fps_binomial_of_nat[of 1] by simp lemma fps_binomial_minus_of_nat: - "fps_binomial (- of_nat n) = inverse ((1 + X :: 'a :: field_char_0 fps) ^ n)" + "fps_binomial (- of_nat n) = inverse ((1 + fps_X :: 'a :: field_char_0 fps) ^ n)" by (rule sym, rule fps_inverse_unique) (simp add: fps_binomial_of_nat [symmetric] fps_binomial_add_mult [symmetric]) -lemma one_minus_const_X_power: - "c \<noteq> 0 \<Longrightarrow> (1 - fps_const c * X) ^ n = - fps_compose (fps_binomial (of_nat n)) (-fps_const c * X)" +lemma one_minus_const_fps_X_power: + "c \<noteq> 0 \<Longrightarrow> (1 - fps_const c * fps_X) ^ n = + fps_compose (fps_binomial (of_nat n)) (-fps_const c * fps_X)" by (subst fps_binomial_of_nat) (simp add: fps_compose_power [symmetric] fps_compose_add_distrib fps_const_neg [symmetric] del: fps_const_neg) -lemma one_minus_X_const_neg_power: - "inverse ((1 - fps_const c * X) ^ n) = - fps_compose (fps_binomial (-of_nat n)) (-fps_const c * X)" +lemma one_minus_fps_X_const_neg_power: + "inverse ((1 - fps_const c * fps_X) ^ n) = + fps_compose (fps_binomial (-of_nat n)) (-fps_const c * fps_X)" proof (cases "c = 0") case False thus ?thesis @@ -4082,17 +4082,17 @@ fps_const_neg [symmetric] del: fps_const_neg) qed simp -lemma X_plus_const_power: - "c \<noteq> 0 \<Longrightarrow> (X + fps_const c) ^ n = - fps_const (c^n) * fps_compose (fps_binomial (of_nat n)) (fps_const (inverse c) * X)" +lemma fps_X_plus_const_power: + "c \<noteq> 0 \<Longrightarrow> (fps_X + fps_const c) ^ n = + fps_const (c^n) * fps_compose (fps_binomial (of_nat n)) (fps_const (inverse c) * fps_X)" by (subst fps_binomial_of_nat) (simp add: fps_compose_power [symmetric] fps_binomial_of_nat fps_compose_add_distrib fps_const_power [symmetric] power_mult_distrib [symmetric] algebra_simps inverse_mult_eq_1' del: fps_const_power) -lemma X_plus_const_neg_power: - "c \<noteq> 0 \<Longrightarrow> inverse ((X + fps_const c) ^ n) = - fps_const (inverse c^n) * fps_compose (fps_binomial (-of_nat n)) (fps_const (inverse c) * X)" +lemma fps_X_plus_const_neg_power: + "c \<noteq> 0 \<Longrightarrow> inverse ((fps_X + fps_const c) ^ n) = + fps_const (inverse c^n) * fps_compose (fps_binomial (-of_nat n)) (fps_const (inverse c) * fps_X)" by (subst fps_binomial_minus_of_nat) (simp add: fps_compose_power [symmetric] fps_binomial_of_nat fps_compose_add_distrib fps_const_power [symmetric] power_mult_distrib [symmetric] fps_inverse_compose @@ -4101,11 +4101,11 @@ del: fps_const_power) -lemma one_minus_const_X_neg_power': - "n > 0 \<Longrightarrow> inverse ((1 - fps_const (c :: 'a :: field_char_0) * X) ^ n) = +lemma one_minus_const_fps_X_neg_power': + "n > 0 \<Longrightarrow> inverse ((1 - fps_const (c :: 'a :: field_char_0) * fps_X) ^ n) = Abs_fps (\<lambda>k. of_nat ((n + k - 1) choose k) * c^k)" apply (rule fps_ext) - apply (subst one_minus_X_const_neg_power, subst fps_const_neg, subst fps_compose_linear) + apply (subst one_minus_fps_X_const_neg_power, subst fps_const_neg, subst fps_compose_linear) apply (simp add: power_mult_distrib [symmetric] mult.assoc [symmetric] gbinomial_minus binomial_gbinomial of_nat_diff) done @@ -4546,7 +4546,7 @@ by (simp add: fps_of_int [symmetric]) lemma fps_numeral_fps_const: "numeral i = fps_const (numeral i :: 'a::comm_ring_1)" - by (fact numeral_fps_const) (* FIXME: duplicate *) + by (fact numeral_fps_const) (* FIfps_XME: duplicate *) lemma fps_cos_fps_exp_ii: "fps_cos c = (fps_exp (\<i> * c) + fps_exp (- \<i> * c)) / fps_const 2" proof - @@ -4610,10 +4610,10 @@ lemma fps_hypergeo_fps_exp[simp]: "fps_hypergeo [] [] c = fps_exp c" by (simp add: fps_eq_iff) -lemma fps_hypergeo_1_0[simp]: "fps_hypergeo [1] [] c = 1/(1 - fps_const c * X)" +lemma fps_hypergeo_1_0[simp]: "fps_hypergeo [1] [] c = 1/(1 - fps_const c * fps_X)" proof - - let ?a = "(Abs_fps (\<lambda>n. 1)) oo (fps_const c * X)" - have th0: "(fps_const c * X) $ 0 = 0" by simp + let ?a = "(Abs_fps (\<lambda>n. 1)) oo (fps_const c * fps_X)" + have th0: "(fps_const c * fps_X) $ 0 = 0" by simp show ?thesis unfolding gp[OF th0, symmetric] by (auto simp add: fps_eq_iff pochhammer_fact[symmetric] fps_compose_nth power_mult_distrib cond_value_iff sum.delta' cong del: if_weak_cong) @@ -4645,26 +4645,26 @@ apply (simp add: algebra_simps) done -lemma XD_nth[simp]: "XD a $ n = (if n = 0 then 0 else of_nat n * a$n)" - by (simp add: XD_def) - -lemma XD_0th[simp]: "XD a $ 0 = 0" +lemma fps_XD_nth[simp]: "fps_XD a $ n = (if n = 0 then 0 else of_nat n * a$n)" + by (simp add: fps_XD_def) + +lemma fps_XD_0th[simp]: "fps_XD a $ 0 = 0" by simp -lemma XD_Suc[simp]:" XD a $ Suc n = of_nat (Suc n) * a $ Suc n" +lemma fps_XD_Suc[simp]:" fps_XD a $ Suc n = of_nat (Suc n) * a $ Suc n" by simp -definition "XDp c a = XD a + fps_const c * a" - -lemma XDp_nth[simp]: "XDp c a $ n = (c + of_nat n) * a$n" - by (simp add: XDp_def algebra_simps) - -lemma XDp_commute: "XDp b \<circ> XDp (c::'a::comm_ring_1) = XDp c \<circ> XDp b" - by (auto simp add: XDp_def fun_eq_iff fps_eq_iff algebra_simps) - -lemma XDp0 [simp]: "XDp 0 = XD" +definition "fps_XDp c a = fps_XD a + fps_const c * a" + +lemma fps_XDp_nth[simp]: "fps_XDp c a $ n = (c + of_nat n) * a$n" + by (simp add: fps_XDp_def algebra_simps) + +lemma fps_XDp_commute: "fps_XDp b \<circ> fps_XDp (c::'a::comm_ring_1) = fps_XDp c \<circ> fps_XDp b" + by (auto simp add: fps_XDp_def fun_eq_iff fps_eq_iff algebra_simps) + +lemma fps_XDp0 [simp]: "fps_XDp 0 = fps_XD" by (simp add: fun_eq_iff fps_eq_iff) -lemma XDp_fps_integral [simp]: "XDp 0 (fps_integral a c) = X * a" +lemma fps_XDp_fps_integral [simp]: "fps_XDp 0 (fps_integral a c) = fps_X * a" by (simp add: fps_eq_iff fps_integral_def) lemma fps_hypergeo_minus_nat: @@ -4687,11 +4687,11 @@ lemma pochhammer_rec_if: "pochhammer a n = (if n = 0 then 1 else a * pochhammer (a + 1) (n - 1))" by (cases n) (simp_all add: pochhammer_rec) -lemma XDp_foldr_nth [simp]: "foldr (\<lambda>c r. XDp c \<circ> r) cs (\<lambda>c. XDp c a) c0 $ n = +lemma fps_XDp_foldr_nth [simp]: "foldr (\<lambda>c r. fps_XDp c \<circ> r) cs (\<lambda>c. fps_XDp c a) c0 $ n = foldr (\<lambda>c r. (c + of_nat n) * r) cs (c0 + of_nat n) * a$n" by (induct cs arbitrary: c0) (auto simp add: algebra_simps) -lemma genric_XDp_foldr_nth: +lemma genric_fps_XDp_foldr_nth: assumes f: "\<forall>n c a. f c a $ n = (of_nat n + k c) * a$n" shows "foldr (\<lambda>c r. f c \<circ> r) cs (\<lambda>c. g c a) c0 $ n = foldr (\<lambda>c r. (k c + of_nat n) * r) cs (g c0 a $ n)" @@ -4732,22 +4732,22 @@ instance fps :: (comm_ring_1) complete_space proof - fix X :: "nat \<Rightarrow> 'a fps" - assume "Cauchy X" - obtain M where M: "\<forall>i. \<forall>m \<ge> M i. \<forall>j \<le> i. X (M i) $ j = X m $ j" + fix fps_X :: "nat \<Rightarrow> 'a fps" + assume "Cauchy fps_X" + obtain M where M: "\<forall>i. \<forall>m \<ge> M i. \<forall>j \<le> i. fps_X (M i) $ j = fps_X m $ j" proof - - have "\<exists>M. \<forall>m \<ge> M. \<forall>j\<le>i. X M $ j = X m $ j" for i + have "\<exists>M. \<forall>m \<ge> M. \<forall>j\<le>i. fps_X M $ j = fps_X m $ j" for i proof - have "0 < inverse ((2::real)^i)" by simp - from metric_CauchyD[OF \<open>Cauchy X\<close> this] dist_less_imp_nth_equal + from metric_CauchyD[OF \<open>Cauchy fps_X\<close> this] dist_less_imp_nth_equal show ?thesis by blast qed then show ?thesis using that by metis qed - show "convergent X" + show "convergent fps_X" proof (rule convergentI) - show "X \<longlonglongrightarrow> Abs_fps (\<lambda>i. X (M i) $ i)" + show "fps_X \<longlonglongrightarrow> Abs_fps (\<lambda>i. fps_X (M i) $ i)" unfolding tendsto_iff proof safe fix e::real assume e: "0 < e" @@ -4758,19 +4758,27 @@ by (auto simp: eventually_sequentially) have "eventually (\<lambda>x. M i \<le> x) sequentially" by (auto simp: eventually_sequentially) - then show "eventually (\<lambda>x. dist (X x) (Abs_fps (\<lambda>i. X (M i) $ i)) < e) sequentially" + then show "eventually (\<lambda>x. dist (fps_X x) (Abs_fps (\<lambda>i. fps_X (M i) $ i)) < e) sequentially" proof eventually_elim fix x assume x: "M i \<le> x" - have "X (M i) $ j = X (M j) $ j" if "j \<le> i" for j + have "fps_X (M i) $ j = fps_X (M j) $ j" if "j \<le> i" for j using M that by (metis nat_le_linear) - with x have "dist (X x) (Abs_fps (\<lambda>j. X (M j) $ j)) < inverse (2 ^ i)" + with x have "dist (fps_X x) (Abs_fps (\<lambda>j. fps_X (M j) $ j)) < inverse (2 ^ i)" using M by (force simp: dist_less_eq_nth_equal) also note \<open>inverse (2 ^ i) < e\<close> - finally show "dist (X x) (Abs_fps (\<lambda>j. X (M j) $ j)) < e" . + finally show "dist (fps_X x) (Abs_fps (\<lambda>j. fps_X (M j) $ j)) < e" . qed qed qed qed +(* TODO: Figure out better notation for this thing *) +no_notation fps_nth (infixl "$" 75) + +bundle fps_notation +begin +notation fps_nth (infixl "$" 75) end + +end

--- a/src/HOL/Computational_Algebra/Polynomial_FPS.thy Mon Aug 21 19:20:02 2017 +0200 +++ b/src/HOL/Computational_Algebra/Polynomial_FPS.thy Mon Aug 21 20:49:15 2017 +0200 @@ -8,6 +8,10 @@ imports Polynomial Formal_Power_Series begin +context + includes fps_notation +begin + definition fps_of_poly where "fps_of_poly p = Abs_fps (coeff p)" @@ -39,7 +43,7 @@ lemma fps_of_poly_numeral' [simp]: "fps_of_poly [:numeral n:] = numeral n" by (simp add: numeral_fps_const fps_of_poly_const [symmetric] numeral_poly) -lemma fps_of_poly_X [simp]: "fps_of_poly [:0, 1:] = X" +lemma fps_of_poly_fps_X [simp]: "fps_of_poly [:0, 1:] = fps_X" by (auto simp add: fps_of_poly_def fps_eq_iff coeff_pCons split: nat.split) lemma fps_of_poly_add: "fps_of_poly (p + q) = fps_of_poly p + fps_of_poly q" @@ -71,8 +75,8 @@ by (induction xs) (simp_all add: fps_of_poly_mult) lemma fps_of_poly_pCons: - "fps_of_poly (pCons (c :: 'a :: semiring_1) p) = fps_const c + fps_of_poly p * X" - by (subst fps_mult_X_commute [symmetric], intro fps_ext) + "fps_of_poly (pCons (c :: 'a :: semiring_1) p) = fps_const c + fps_of_poly p * fps_X" + by (subst fps_mult_fps_X_commute [symmetric], intro fps_ext) (auto simp: fps_of_poly_def coeff_pCons split: nat.split) lemma fps_of_poly_pderiv: "fps_of_poly (pderiv p) = fps_deriv (fps_of_poly p)" @@ -81,10 +85,10 @@ lemma fps_of_poly_power: "fps_of_poly (p ^ n) = fps_of_poly p ^ n" by (induction n) (simp_all add: fps_of_poly_mult) -lemma fps_of_poly_monom: "fps_of_poly (monom (c :: 'a :: comm_ring_1) n) = fps_const c * X ^ n" +lemma fps_of_poly_monom: "fps_of_poly (monom (c :: 'a :: comm_ring_1) n) = fps_const c * fps_X ^ n" by (intro fps_ext) simp_all -lemma fps_of_poly_monom': "fps_of_poly (monom (1 :: 'a :: comm_ring_1) n) = X ^ n" +lemma fps_of_poly_monom': "fps_of_poly (monom (1 :: 'a :: comm_ring_1) n) = fps_X ^ n" by (simp add: fps_of_poly_monom) lemma fps_of_poly_div: @@ -139,7 +143,7 @@ lemmas fps_of_poly_simps = - fps_of_poly_0 fps_of_poly_1 fps_of_poly_numeral fps_of_poly_const fps_of_poly_X + fps_of_poly_0 fps_of_poly_1 fps_of_poly_numeral fps_of_poly_const fps_of_poly_fps_X fps_of_poly_add fps_of_poly_diff fps_of_poly_uminus fps_of_poly_mult fps_of_poly_smult fps_of_poly_sum fps_of_poly_sum_list fps_of_poly_prod fps_of_poly_prod_list fps_of_poly_pCons fps_of_poly_pderiv fps_of_poly_power fps_of_poly_monom @@ -153,7 +157,7 @@ fps_compose_add_distrib fps_compose_mult_distrib) lemmas reify_fps_atom = - fps_of_poly_0 fps_of_poly_1' fps_of_poly_numeral' fps_of_poly_const fps_of_poly_X + fps_of_poly_0 fps_of_poly_1' fps_of_poly_numeral' fps_of_poly_const fps_of_poly_fps_X text \<open> @@ -163,7 +167,7 @@ polynomial \<open>p\<close>. This may sound trivial, but it covers a number of annoying side conditions like - @{term "1 + X \<noteq> 0"} that would otherwise not be solved automatically. + @{term "1 + fps_X \<noteq> 0"} that would otherwise not be solved automatically. \<close> ML \<open> @@ -208,7 +212,7 @@ | (Const (@{const_name "Rings.divide"}, _) $ _ $ (Const (@{const_name "Num.numeral"}, _) $ _)) => ct |> (Conv.fun_conv (Conv.arg_conv reify_conv) then_conv rewr @{thms fps_of_poly_divide_numeral [symmetric]}) - | (Const (@{const_name "Power.power"}, _) $ Const (@{const_name "X"},_) $ _) => ct |> ( + | (Const (@{const_name "Power.power"}, _) $ Const (@{const_name "fps_X"},_) $ _) => ct |> ( rewr @{thms fps_of_poly_monom' [symmetric]}) | (Const (@{const_name "Power.power"}, _) $ _ $ _) => ct |> ( Conv.fun_conv (Conv.arg_conv reify_conv) @@ -232,10 +236,10 @@ simproc_setup poly_fps_eq ("(f :: 'a fps) = g") = \<open>K (K Poly_Fps.eq_simproc)\<close> -lemma fps_of_poly_linear: "fps_of_poly [:a,1 :: 'a :: field:] = X + fps_const a" +lemma fps_of_poly_linear: "fps_of_poly [:a,1 :: 'a :: field:] = fps_X + fps_const a" by simp -lemma fps_of_poly_linear': "fps_of_poly [:1,a :: 'a :: field:] = 1 + fps_const a * X" +lemma fps_of_poly_linear': "fps_of_poly [:1,a :: 'a :: field:] = 1 + fps_const a * fps_X" by simp lemma fps_of_poly_cutoff [simp]: @@ -308,3 +312,5 @@ qed (simp_all add: poly_subdegree_def prefix_length_def) end + +end