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