# HG changeset patch
# User wenzelm
# Date 1451428804 -3600
# Node ID 720fa884656e7d67e4372f3f8c94b2d35c210602
# Parent  6226261144d7eadaae53c0bc1b03d4830a138669
more symbols;

diff -r 6226261144d7 -r 720fa884656e NEWS
--- a/NEWS	Tue Dec 29 23:20:11 2015 +0100
+++ b/NEWS	Tue Dec 29 23:40:04 2015 +0100
@@ -505,6 +505,7 @@
   notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60)
 
   notation NSLIMSEQ ("((_)/ ----NS> (_))" [60, 60] 60)
+  notation NSLIM ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
 
 * The alternative notation "\<Colon>" for type and sort constraints has been
 removed: in LaTeX document output it looks the same as "::".
diff -r 6226261144d7 -r 720fa884656e etc/abbrevs
--- a/etc/abbrevs	Tue Dec 29 23:20:11 2015 +0100
+++ b/etc/abbrevs	Tue Dec 29 23:40:04 2015 +0100
@@ -8,3 +8,4 @@
 
 (*HOL-NSA*)
 "---->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
+"---->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S"
diff -r 6226261144d7 -r 720fa884656e src/HOL/NSA/CLim.thy
--- a/src/HOL/NSA/CLim.thy	Tue Dec 29 23:20:11 2015 +0100
+++ b/src/HOL/NSA/CLim.thy	Tue Dec 29 23:40:04 2015 +0100
@@ -36,11 +36,11 @@
 
 subsection{*Limit of Complex to Complex Function*}
 
-lemma NSLIM_Re: "f -- a --NS> L ==> (%x. Re(f x)) -- a --NS> Re(L)"
+lemma NSLIM_Re: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L ==> (%x. Re(f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Re(L)"
 by (simp add: NSLIM_def starfunC_approx_Re_Im_iff 
               hRe_hcomplex_of_complex)
 
-lemma NSLIM_Im: "f -- a --NS> L ==> (%x. Im(f x)) -- a --NS> Im(L)"
+lemma NSLIM_Im: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L ==> (%x. Im(f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Im(L)"
 by (simp add: NSLIM_def starfunC_approx_Re_Im_iff 
               hIm_hcomplex_of_complex)
 
@@ -77,7 +77,7 @@
 text""
 (** another equivalence result **)
 lemma NSCLIM_NSCRLIM_iff:
-   "(f -- x --NS> L) = ((%y. cmod(f y - L)) -- x --NS> 0)"
+   "(f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S L) = ((%y. cmod(f y - L)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0)"
 by (simp add: NSLIM_def starfun_norm
     approx_approx_zero_iff [symmetric] approx_minus_iff [symmetric])
 
@@ -89,12 +89,12 @@
 
 (* so this is nicer nonstandard proof *)
 lemma NSCLIM_NSCRLIM_iff2:
-     "(f -- x --NS> L) = ((%y. cmod(f y - L)) -- x --NS> 0)"
+     "(f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S L) = ((%y. cmod(f y - L)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0)"
 by (simp add: LIM_NSLIM_iff [symmetric] CLIM_CRLIM_iff)
 
 lemma NSLIM_NSCRLIM_Re_Im_iff:
-     "(f -- a --NS> L) = ((%x. Re(f x)) -- a --NS> Re(L) &
-                            (%x. Im(f x)) -- a --NS> Im(L))"
+     "(f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L) = ((%x. Re(f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Re(L) &
+                            (%x. Im(f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Im(L))"
 apply (auto intro: NSLIM_Re NSLIM_Im)
 apply (auto simp add: NSLIM_def starfun_Re starfun_Im)
 apply (auto dest!: spec)
@@ -111,7 +111,7 @@
 subsection{*Continuity*}
 
 lemma NSLIM_isContc_iff:
-     "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
+     "(f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S f a) = ((%h. f(a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S f a)"
 by (rule NSLIM_h_iff)
 
 subsection{*Functions from Complex to Reals*}
diff -r 6226261144d7 -r 720fa884656e src/HOL/NSA/HDeriv.thy
--- a/src/HOL/NSA/HDeriv.thy	Tue Dec 29 23:20:11 2015 +0100
+++ b/src/HOL/NSA/HDeriv.thy	Tue Dec 29 23:40:04 2015 +0100
@@ -33,10 +33,10 @@
 subsection {* Derivatives *}
 
 lemma DERIV_NS_iff:
-      "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NS> D)"
+      "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D)"
 by (simp add: DERIV_def LIM_NSLIM_iff)
 
-lemma NS_DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --NS> D"
+lemma NS_DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D"
 by (simp add: DERIV_def LIM_NSLIM_iff)
 
 lemma hnorm_of_hypreal:
@@ -70,7 +70,7 @@
 
 text{*first equivalence *}
 lemma NSDERIV_NSLIM_iff:
-      "(NSDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NS> D)"
+      "(NSDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D)"
 apply (simp add: nsderiv_def NSLIM_def, auto)
 apply (drule_tac x = xa in bspec)
 apply (rule_tac [3] ccontr)
@@ -80,7 +80,7 @@
 
 text{*second equivalence *}
 lemma NSDERIV_NSLIM_iff2:
-     "(NSDERIV f x :> D) = ((%z. (f(z) - f(x)) / (z-x)) -- x --NS> D)"
+     "(NSDERIV f x :> D) = ((%z. (f(z) - f(x)) / (z-x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S D)"
   by (simp add: NSDERIV_NSLIM_iff DERIV_LIM_iff LIM_NSLIM_iff [symmetric])
 
 (* while we're at it! *)
@@ -227,15 +227,15 @@
 text{*Negation of function*}
 lemma NSDERIV_minus: "NSDERIV f x :> D ==> NSDERIV (%x. -(f x)) x :> -D"
 proof (simp add: NSDERIV_NSLIM_iff)
-  assume "(\<lambda>h. (f (x + h) - f x) / h) -- 0 --NS> D"
-  hence deriv: "(\<lambda>h. - ((f(x+h) - f x) / h)) -- 0 --NS> - D"
+  assume "(\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D"
+  hence deriv: "(\<lambda>h. - ((f(x+h) - f x) / h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S - D"
     by (rule NSLIM_minus)
   have "\<forall>h. - ((f (x + h) - f x) / h) = (- f (x + h) + f x) / h"
     by (simp add: minus_divide_left)
   with deriv
-  have "(\<lambda>h. (- f (x + h) + f x) / h) -- 0 --NS> - D" by simp
-  then show "(\<lambda>h. (f (x + h) - f x) / h) -- 0 --NS> D \<Longrightarrow>
-    (\<lambda>h. (f x - f (x + h)) / h) -- 0 --NS> - D" by simp
+  have "(\<lambda>h. (- f (x + h) + f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S - D" by simp
+  then show "(\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D \<Longrightarrow>
+    (\<lambda>h. (f x - f (x + h)) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S - D" by simp
 qed
 
 text{*Subtraction*}
diff -r 6226261144d7 -r 720fa884656e src/HOL/NSA/HLim.thy
--- a/src/HOL/NSA/HLim.thy	Tue Dec 29 23:20:11 2015 +0100
+++ b/src/HOL/NSA/HLim.thy	Tue Dec 29 23:40:04 2015 +0100
@@ -13,8 +13,8 @@
 
 definition
   NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
-            ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) where
-  "f -- a --NS> L =
+            ("((_)/ \<midarrow>(_)/\<rightarrow>\<^sub>N\<^sub>S (_))" [60, 0, 60] 60) where
+  "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L =
     (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
 
 definition
@@ -32,11 +32,11 @@
 
 lemma NSLIM_I:
   "(\<And>x. \<lbrakk>x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> \<Longrightarrow> starfun f x \<approx> star_of L)
-   \<Longrightarrow> f -- a --NS> L"
+   \<Longrightarrow> f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
 by (simp add: NSLIM_def)
 
 lemma NSLIM_D:
-  "\<lbrakk>f -- a --NS> L; x \<noteq> star_of a; x \<approx> star_of a\<rbrakk>
+  "\<lbrakk>f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L; x \<noteq> star_of a; x \<approx> star_of a\<rbrakk>
    \<Longrightarrow> starfun f x \<approx> star_of L"
 by (simp add: NSLIM_def)
 
@@ -45,8 +45,8 @@
 
 lemma NSLIM_mult:
   fixes l m :: "'a::real_normed_algebra"
-  shows "[| f -- x --NS> l; g -- x --NS> m |]
-      ==> (%x. f(x) * g(x)) -- x --NS> (l * m)"
+  shows "[| f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m |]
+      ==> (%x. f(x) * g(x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l * m)"
 by (auto simp add: NSLIM_def intro!: approx_mult_HFinite)
 
 lemma starfun_scaleR [simp]:
@@ -54,53 +54,53 @@
 by transfer (rule refl)
 
 lemma NSLIM_scaleR:
-  "[| f -- x --NS> l; g -- x --NS> m |]
-      ==> (%x. f(x) *\<^sub>R g(x)) -- x --NS> (l *\<^sub>R m)"
+  "[| f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m |]
+      ==> (%x. f(x) *\<^sub>R g(x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l *\<^sub>R m)"
 by (auto simp add: NSLIM_def intro!: approx_scaleR_HFinite)
 
 lemma NSLIM_add:
-     "[| f -- x --NS> l; g -- x --NS> m |]
-      ==> (%x. f(x) + g(x)) -- x --NS> (l + m)"
+     "[| f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m |]
+      ==> (%x. f(x) + g(x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l + m)"
 by (auto simp add: NSLIM_def intro!: approx_add)
 
-lemma NSLIM_const [simp]: "(%x. k) -- x --NS> k"
+lemma NSLIM_const [simp]: "(%x. k) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S k"
 by (simp add: NSLIM_def)
 
-lemma NSLIM_minus: "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L"
+lemma NSLIM_minus: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L ==> (%x. -f(x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S -L"
 by (simp add: NSLIM_def)
 
 lemma NSLIM_diff:
-  "\<lbrakk>f -- x --NS> l; g -- x --NS> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --NS> (l - m)"
+  "\<lbrakk>f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l - m)"
   by (simp only: NSLIM_add NSLIM_minus diff_conv_add_uminus)
 
-lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)"
+lemma NSLIM_add_minus: "[| f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m |] ==> (%x. f(x) + -g(x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l + -m)"
 by (simp only: NSLIM_add NSLIM_minus)
 
 lemma NSLIM_inverse:
   fixes L :: "'a::real_normed_div_algebra"
-  shows "[| f -- a --NS> L;  L \<noteq> 0 |]
-      ==> (%x. inverse(f(x))) -- a --NS> (inverse L)"
+  shows "[| f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L;  L \<noteq> 0 |]
+      ==> (%x. inverse(f(x))) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (inverse L)"
 apply (simp add: NSLIM_def, clarify)
 apply (drule spec)
 apply (auto simp add: star_of_approx_inverse)
 done
 
 lemma NSLIM_zero:
-  assumes f: "f -- a --NS> l" shows "(%x. f(x) - l) -- a --NS> 0"
+  assumes f: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S l" shows "(%x. f(x) - l) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S 0"
 proof -
-  have "(\<lambda>x. f x - l) -- a --NS> l - l"
+  have "(\<lambda>x. f x - l) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S l - l"
     by (rule NSLIM_diff [OF f NSLIM_const])
   thus ?thesis by simp
 qed
 
-lemma NSLIM_zero_cancel: "(%x. f(x) - l) -- x --NS> 0 ==> f -- x --NS> l"
+lemma NSLIM_zero_cancel: "(%x. f(x) - l) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0 ==> f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l"
 apply (drule_tac g = "%x. l" and m = l in NSLIM_add)
 apply (auto simp add: add.assoc)
 done
 
 lemma NSLIM_const_not_eq:
   fixes a :: "'a::real_normed_algebra_1"
-  shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --NS> L"
+  shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
 apply (simp add: NSLIM_def)
 apply (rule_tac x="star_of a + of_hypreal epsilon" in exI)
 apply (simp add: hypreal_epsilon_not_zero approx_def)
@@ -108,35 +108,35 @@
 
 lemma NSLIM_not_zero:
   fixes a :: "'a::real_normed_algebra_1"
-  shows "k \<noteq> 0 \<Longrightarrow> \<not> (\<lambda>x. k) -- a --NS> 0"
+  shows "k \<noteq> 0 \<Longrightarrow> \<not> (\<lambda>x. k) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S 0"
 by (rule NSLIM_const_not_eq)
 
 lemma NSLIM_const_eq:
   fixes a :: "'a::real_normed_algebra_1"
-  shows "(\<lambda>x. k) -- a --NS> L \<Longrightarrow> k = L"
+  shows "(\<lambda>x. k) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> k = L"
 apply (rule ccontr)
 apply (blast dest: NSLIM_const_not_eq)
 done
 
 lemma NSLIM_unique:
   fixes a :: "'a::real_normed_algebra_1"
-  shows "\<lbrakk>f -- a --NS> L; f -- a --NS> M\<rbrakk> \<Longrightarrow> L = M"
+  shows "\<lbrakk>f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L; f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S M\<rbrakk> \<Longrightarrow> L = M"
 apply (drule (1) NSLIM_diff)
 apply (auto dest!: NSLIM_const_eq)
 done
 
 lemma NSLIM_mult_zero:
   fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
-  shows "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0"
+  shows "[| f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0 |] ==> (%x. f(x)*g(x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0"
 by (drule NSLIM_mult, auto)
 
-lemma NSLIM_self: "(%x. x) -- a --NS> a"
+lemma NSLIM_self: "(%x. x) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S a"
 by (simp add: NSLIM_def)
 
 subsubsection {* Equivalence of @{term filterlim} and @{term NSLIM} *}
 
 lemma LIM_NSLIM:
-  assumes f: "f -- a --> L" shows "f -- a --NS> L"
+  assumes f: "f -- a --> L" shows "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
 proof (rule NSLIM_I)
   fix x
   assume neq: "x \<noteq> star_of a"
@@ -164,7 +164,7 @@
 qed
 
 lemma NSLIM_LIM:
-  assumes f: "f -- a --NS> L" shows "f -- a --> L"
+  assumes f: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L" shows "f -- a --> L"
 proof (rule LIM_I)
   fix r::real assume r: "0 < r"
   have "\<exists>s>0. \<forall>x. x \<noteq> star_of a \<and> hnorm (x - star_of a) < s
@@ -190,7 +190,7 @@
     by transfer
 qed
 
-theorem LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)"
+theorem LIM_NSLIM_iff: "(f -- x --> L) = (f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S L)"
 by (blast intro: LIM_NSLIM NSLIM_LIM)
 
 
@@ -200,17 +200,17 @@
   "\<lbrakk>isNSCont f a; y \<approx> star_of a\<rbrakk> \<Longrightarrow> ( *f* f) y \<approx> star_of (f a)"
 by (simp add: isNSCont_def)
 
-lemma isNSCont_NSLIM: "isNSCont f a ==> f -- a --NS> (f a) "
+lemma isNSCont_NSLIM: "isNSCont f a ==> f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (f a) "
 by (simp add: isNSCont_def NSLIM_def)
 
-lemma NSLIM_isNSCont: "f -- a --NS> (f a) ==> isNSCont f a"
+lemma NSLIM_isNSCont: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (f a) ==> isNSCont f a"
 apply (simp add: isNSCont_def NSLIM_def, auto)
 apply (case_tac "y = star_of a", auto)
 done
 
 text{*NS continuity can be defined using NS Limit in
     similar fashion to standard def of continuity*}
-lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f -- a --NS> (f a))"
+lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (f a))"
 by (blast intro: isNSCont_NSLIM NSLIM_isNSCont)
 
 text{*Hence, NS continuity can be given
@@ -237,7 +237,7 @@
 
 (* Prove equivalence between NS limits - *)
 (* seems easier than using standard def  *)
-lemma NSLIM_h_iff: "(f -- a --NS> L) = ((%h. f(a + h)) -- 0 --NS> L)"
+lemma NSLIM_h_iff: "(f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L) = ((%h. f(a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S L)"
 apply (simp add: NSLIM_def, auto)
 apply (drule_tac x = "star_of a + x" in spec)
 apply (drule_tac [2] x = "- star_of a + x" in spec, safe, simp)
@@ -249,7 +249,7 @@
 apply (auto simp add: starfun star_of_def star_n_minus star_n_add add.assoc star_n_zero_num)
 done
 
-lemma NSLIM_isCont_iff: "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
+lemma NSLIM_isCont_iff: "(f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S f a) = ((%h. f(a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S f a)"
   by (fact NSLIM_h_iff)
 
 lemma isNSCont_minus: "isNSCont f a ==> isNSCont (%x. - f x) a"
diff -r 6226261144d7 -r 720fa884656e src/HOL/NSA/HTranscendental.thy
--- a/src/HOL/NSA/HTranscendental.thy	Tue Dec 29 23:20:11 2015 +0100
+++ b/src/HOL/NSA/HTranscendental.thy	Tue Dec 29 23:40:04 2015 +0100
@@ -406,7 +406,7 @@
 
 
 (*
-Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) -- 0 --NS> ln x"
+Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S ln x"
 *)
 
 lemma HFinite_sin [simp]: "sumhr (0, whn, %n. sin_coeff n * x ^ n) \<in> HFinite"