# HG changeset patch
# User huffman
# Date 1243877802 25200
# Node ID 3d18766ddc4bc69f66da638ba1a96d4ea4a96661
# Parent  2ad53771c30f892bf441c2fbddad0ede35a6afe5
limits of inverse using filters

diff -r 2ad53771c30f -r 3d18766ddc4b src/HOL/Lim.thy
--- a/src/HOL/Lim.thy	Mon Jun 01 08:04:19 2009 -0700
+++ b/src/HOL/Lim.thy	Mon Jun 01 10:36:42 2009 -0700
@@ -413,67 +413,16 @@
 
 subsubsection {* Derived theorems about @{term LIM} *}
 
-lemma LIM_inverse_lemma:
-  fixes x :: "'a::real_normed_div_algebra"
-  assumes r: "0 < r"
-  assumes x: "norm (x - 1) < min (1/2) (r/2)"
-  shows "norm (inverse x - 1) < r"
-proof -
-  from r have r2: "0 < r/2" by simp
-  from x have 0: "x \<noteq> 0" by clarsimp
-  from x have x': "norm (1 - x) < min (1/2) (r/2)"
-    by (simp only: norm_minus_commute)
-  hence less1: "norm (1 - x) < r/2" by simp
-  have "norm (1::'a) - norm x \<le> norm (1 - x)" by (rule norm_triangle_ineq2)
-  also from x' have "norm (1 - x) < 1/2" by simp
-  finally have "1/2 < norm x" by simp
-  hence "inverse (norm x) < inverse (1/2)"
-    by (rule less_imp_inverse_less, simp)
-  hence less2: "norm (inverse x) < 2"
-    by (simp add: nonzero_norm_inverse 0)
-  from less1 less2 r2 norm_ge_zero
-  have "norm (1 - x) * norm (inverse x) < (r/2) * 2"
-    by (rule mult_strict_mono)
-  thus "norm (inverse x - 1) < r"
-    by (simp only: norm_mult [symmetric] left_diff_distrib, simp add: 0)
-qed
+lemma LIM_inverse:
+  fixes L :: "'a::real_normed_div_algebra"
+  shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L"
+unfolding LIM_conv_tendsto
+by (rule tendsto_inverse)
 
 lemma LIM_inverse_fun:
   assumes a: "a \<noteq> (0::'a::real_normed_div_algebra)"
   shows "inverse -- a --> inverse a"
-proof (rule LIM_equal2)
-  from a show "0 < norm a" by simp
-next
-  fix x assume "norm (x - a) < norm a"
-  hence "x \<noteq> 0" by auto
-  with a show "inverse x = inverse (inverse a * x) * inverse a"
-    by (simp add: nonzero_inverse_mult_distrib
-                  nonzero_imp_inverse_nonzero
-                  nonzero_inverse_inverse_eq mult_assoc)
-next
-  have 1: "inverse -- 1 --> inverse (1::'a)"
-    apply (rule LIM_I)
-    apply (rule_tac x="min (1/2) (r/2)" in exI)
-    apply (simp add: LIM_inverse_lemma)
-    done
-  have "(\<lambda>x. inverse a * x) -- a --> inverse a * a"
-    by (intro LIM_mult LIM_ident LIM_const)
-  hence "(\<lambda>x. inverse a * x) -- a --> 1"
-    by (simp add: a)
-  with 1 have "(\<lambda>x. inverse (inverse a * x)) -- a --> inverse 1"
-    by (rule LIM_compose)
-  hence "(\<lambda>x. inverse (inverse a * x)) -- a --> 1"
-    by simp
-  hence "(\<lambda>x. inverse (inverse a * x) * inverse a) -- a --> 1 * inverse a"
-    by (intro LIM_mult LIM_const)
-  thus "(\<lambda>x. inverse (inverse a * x) * inverse a) -- a --> inverse a"
-    by simp
-qed
-
-lemma LIM_inverse:
-  fixes L :: "'a::real_normed_div_algebra"
-  shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L"
-by (rule LIM_inverse_fun [THEN LIM_compose])
+by (rule LIM_inverse [OF LIM_ident a])
 
 lemma LIM_sgn:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
diff -r 2ad53771c30f -r 3d18766ddc4b src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon Jun 01 08:04:19 2009 -0700
+++ b/src/HOL/Limits.thy	Mon Jun 01 10:36:42 2009 -0700
@@ -81,6 +81,27 @@
 using assms by (auto elim!: eventually_rev_mp)
 
 
+subsection {* Boundedness *}
+
+definition
+  Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" where
+  "Bfun S F = (\<exists>K>0. eventually (\<lambda>i. norm (S i) \<le> K) F)"
+
+lemma BfunI: assumes K: "eventually (\<lambda>i. norm (X i) \<le> K) F" shows "Bfun X F"
+unfolding Bfun_def
+proof (intro exI conjI allI)
+  show "0 < max K 1" by simp
+next
+  show "eventually (\<lambda>i. norm (X i) \<le> max K 1) F"
+    using K by (rule eventually_elim1, simp)
+qed
+
+lemma BfunE:
+  assumes "Bfun S F"
+  obtains B where "0 < B" and "eventually (\<lambda>i. norm (S i) \<le> B) F"
+using assms unfolding Bfun_def by fast
+
+
 subsection {* Convergence to Zero *}
 
 definition
@@ -95,6 +116,10 @@
   "\<lbrakk>Zfun S F; 0 < r\<rbrakk> \<Longrightarrow> eventually (\<lambda>i. norm (S i) < r) F"
 unfolding Zfun_def by simp
 
+lemma Zfun_ssubst:
+  "eventually (\<lambda>i. X i = Y i) F \<Longrightarrow> Zfun Y F \<Longrightarrow> Zfun X F"
+unfolding Zfun_def by (auto elim!: eventually_rev_mp)
+
 lemma Zfun_zero: "Zfun (\<lambda>i. 0) F"
 unfolding Zfun_def by simp
 
@@ -103,7 +128,7 @@
 
 lemma Zfun_imp_Zfun:
   assumes X: "Zfun X F"
-  assumes Y: "\<And>n. norm (Y n) \<le> norm (X n) * K"
+  assumes Y: "eventually (\<lambda>i. norm (Y i) \<le> norm (X i) * K) F"
   shows "Zfun (\<lambda>n. Y n) F"
 proof (cases)
   assume K: "0 < K"
@@ -114,26 +139,34 @@
       using K by (rule divide_pos_pos)
     then have "eventually (\<lambda>i. norm (X i) < r / K) F"
       using ZfunD [OF X] by fast
-    then show "eventually (\<lambda>i. norm (Y i) < r) F"
-    proof (rule eventually_elim1)
-      fix i assume "norm (X i) < r / K"
+    with Y show "eventually (\<lambda>i. norm (Y i) < r) F"
+    proof (rule eventually_elim2)
+      fix i
+      assume *: "norm (Y i) \<le> norm (X i) * K"
+      assume "norm (X i) < r / K"
       hence "norm (X i) * K < r"
         by (simp add: pos_less_divide_eq K)
       thus "norm (Y i) < r"
-        by (simp add: order_le_less_trans [OF Y])
+        by (simp add: order_le_less_trans [OF *])
     qed
   qed
 next
   assume "\<not> 0 < K"
   hence K: "K \<le> 0" by (simp only: not_less)
-  {
-    fix i
-    have "norm (Y i) \<le> norm (X i) * K" by (rule Y)
-    also have "\<dots> \<le> norm (X i) * 0"
-      using K norm_ge_zero by (rule mult_left_mono)
-    finally have "norm (Y i) = 0" by simp
-  }
-  thus ?thesis by (simp add: Zfun_zero)
+  show ?thesis
+  proof (rule ZfunI)
+    fix r :: real
+    assume "0 < r"
+    from Y show "eventually (\<lambda>i. norm (Y i) < r) F"
+    proof (rule eventually_elim1)
+      fix i
+      assume "norm (Y i) \<le> norm (X i) * K"
+      also have "\<dots> \<le> norm (X i) * 0"
+        using K norm_ge_zero by (rule mult_left_mono)
+      finally show "norm (Y i) < r"
+        using `0 < r` by simp
+    qed
+  qed
 qed
 
 lemma Zfun_le: "\<lbrakk>Zfun Y F; \<forall>n. norm (X n) \<le> norm (Y n)\<rbrakk> \<Longrightarrow> Zfun X F"
@@ -176,6 +209,8 @@
 proof -
   obtain K where "\<And>x. norm (f x) \<le> norm x * K"
     using bounded by fast
+  then have "eventually (\<lambda>i. norm (f (X i)) \<le> norm (X i) * K) F"
+    by simp
   with X show ?thesis
     by (rule Zfun_imp_Zfun)
 qed
@@ -293,4 +328,135 @@
 by (simp only: tendsto_Zfun_iff prod_diff_prod
                Zfun_add Zfun Zfun_left Zfun_right)
 
+
+subsection {* Continuity of Inverse *}
+
+lemma (in bounded_bilinear) Zfun_prod_Bfun:
+  assumes X: "Zfun X F"
+  assumes Y: "Bfun Y F"
+  shows "Zfun (\<lambda>n. X n ** Y n) F"
+proof -
+  obtain K where K: "0 \<le> K"
+    and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
+    using nonneg_bounded by fast
+  obtain B where B: "0 < B"
+    and norm_Y: "eventually (\<lambda>i. norm (Y i) \<le> B) F"
+    using Y by (rule BfunE)
+  have "eventually (\<lambda>i. norm (X i ** Y i) \<le> norm (X i) * (B * K)) F"
+  using norm_Y proof (rule eventually_elim1)
+    fix i
+    assume *: "norm (Y i) \<le> B"
+    have "norm (X i ** Y i) \<le> norm (X i) * norm (Y i) * K"
+      by (rule norm_le)
+    also have "\<dots> \<le> norm (X i) * B * K"
+      by (intro mult_mono' order_refl norm_Y norm_ge_zero
+                mult_nonneg_nonneg K *)
+    also have "\<dots> = norm (X i) * (B * K)"
+      by (rule mult_assoc)
+    finally show "norm (X i ** Y i) \<le> norm (X i) * (B * K)" .
+  qed
+  with X show ?thesis
+  by (rule Zfun_imp_Zfun)
+qed
+
+lemma (in bounded_bilinear) flip:
+  "bounded_bilinear (\<lambda>x y. y ** x)"
+apply default
+apply (rule add_right)
+apply (rule add_left)
+apply (rule scaleR_right)
+apply (rule scaleR_left)
+apply (subst mult_commute)
+using bounded by fast
+
+lemma (in bounded_bilinear) Bfun_prod_Zfun:
+  assumes X: "Bfun X F"
+  assumes Y: "Zfun Y F"
+  shows "Zfun (\<lambda>n. X n ** Y n) F"
+using flip Y X by (rule bounded_bilinear.Zfun_prod_Bfun)
+
+lemma inverse_diff_inverse:
+  "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
+   \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
+by (simp add: algebra_simps)
+
+lemma Bfun_inverse_lemma:
+  fixes x :: "'a::real_normed_div_algebra"
+  shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r"
+apply (subst nonzero_norm_inverse, clarsimp)
+apply (erule (1) le_imp_inverse_le)
+done
+
+lemma Bfun_inverse:
+  fixes a :: "'a::real_normed_div_algebra"
+  assumes X: "tendsto X a F"
+  assumes a: "a \<noteq> 0"
+  shows "Bfun (\<lambda>n. inverse (X n)) F"
+proof -
+  from a have "0 < norm a" by simp
+  hence "\<exists>r>0. r < norm a" by (rule dense)
+  then obtain r where r1: "0 < r" and r2: "r < norm a" by fast
+  have "eventually (\<lambda>i. dist (X i) a < r) F"
+    using tendstoD [OF X r1] by fast
+  hence "eventually (\<lambda>i. norm (inverse (X i)) \<le> inverse (norm a - r)) F"
+  proof (rule eventually_elim1)
+    fix i
+    assume "dist (X i) a < r"
+    hence 1: "norm (X i - a) < r"
+      by (simp add: dist_norm)
+    hence 2: "X i \<noteq> 0" using r2 by auto
+    hence "norm (inverse (X i)) = inverse (norm (X i))"
+      by (rule nonzero_norm_inverse)
+    also have "\<dots> \<le> inverse (norm a - r)"
+    proof (rule le_imp_inverse_le)
+      show "0 < norm a - r" using r2 by simp
+    next
+      have "norm a - norm (X i) \<le> norm (a - X i)"
+        by (rule norm_triangle_ineq2)
+      also have "\<dots> = norm (X i - a)"
+        by (rule norm_minus_commute)
+      also have "\<dots> < r" using 1 .
+      finally show "norm a - r \<le> norm (X i)" by simp
+    qed
+    finally show "norm (inverse (X i)) \<le> inverse (norm a - r)" .
+  qed
+  thus ?thesis by (rule BfunI)
+qed
+
+lemma tendsto_inverse_lemma:
+  fixes a :: "'a::real_normed_div_algebra"
+  shows "\<lbrakk>tendsto X a F; a \<noteq> 0; eventually (\<lambda>i. X i \<noteq> 0) F\<rbrakk>
+         \<Longrightarrow> tendsto (\<lambda>i. inverse (X i)) (inverse a) F"
+apply (subst tendsto_Zfun_iff)
+apply (rule Zfun_ssubst)
+apply (erule eventually_elim1)
+apply (erule (1) inverse_diff_inverse)
+apply (rule Zfun_minus)
+apply (rule Zfun_mult_left)
+apply (rule mult.Bfun_prod_Zfun)
+apply (erule (1) Bfun_inverse)
+apply (simp add: tendsto_Zfun_iff)
+done
+
+lemma tendsto_inverse:
+  fixes a :: "'a::real_normed_div_algebra"
+  assumes X: "tendsto X a F"
+  assumes a: "a \<noteq> 0"
+  shows "tendsto (\<lambda>i. inverse (X i)) (inverse a) F"
+proof -
+  from a have "0 < norm a" by simp
+  with X have "eventually (\<lambda>i. dist (X i) a < norm a) F"
+    by (rule tendstoD)
+  then have "eventually (\<lambda>i. X i \<noteq> 0) F"
+    unfolding dist_norm by (auto elim!: eventually_elim1)
+  with X a show ?thesis
+    by (rule tendsto_inverse_lemma)
+qed
+
+lemma tendsto_divide:
+  fixes a b :: "'a::real_normed_field"
+  shows "\<lbrakk>tendsto X a F; tendsto Y b F; b \<noteq> 0\<rbrakk>
+    \<Longrightarrow> tendsto (\<lambda>n. X n / Y n) (a / b) F"
+by (simp add: mult.tendsto tendsto_inverse divide_inverse)
+
 end
diff -r 2ad53771c30f -r 3d18766ddc4b src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Mon Jun 01 08:04:19 2009 -0700
+++ b/src/HOL/SEQ.thy	Mon Jun 01 10:36:42 2009 -0700
@@ -132,6 +132,13 @@
 apply (drule_tac x="n - k" in spec, simp)
 done
 
+lemma Bseq_conv_Bfun: "Bseq X \<longleftrightarrow> Bfun X sequentially"
+unfolding Bfun_def eventually_sequentially
+apply (rule iffI)
+apply (simp add: Bseq_def, fast)
+apply (fast intro: BseqI2')
+done
+
 
 subsection {* Sequences That Converge to Zero *}
 
@@ -156,7 +163,8 @@
   assumes X: "Zseq X"
   assumes Y: "\<And>n. norm (Y n) \<le> norm (X n) * K"
   shows "Zseq (\<lambda>n. Y n)"
-using assms unfolding Zseq_conv_Zfun by (rule Zfun_imp_Zfun)
+using X Y Zfun_imp_Zfun [of X sequentially Y K]
+unfolding Zseq_conv_Zfun by simp
 
 lemma Zseq_le: "\<lbrakk>Zseq Y; \<forall>n. norm (X n) \<le> norm (Y n)\<rbrakk> \<Longrightarrow> Zseq X"
 by (erule_tac K="1" in Zseq_imp_Zseq, simp)
@@ -180,54 +188,14 @@
 unfolding Zseq_conv_Zfun by (rule Zfun)
 
 lemma (in bounded_bilinear) Zseq_prod_Bseq:
-  assumes X: "Zseq X"
-  assumes Y: "Bseq Y"
-  shows "Zseq (\<lambda>n. X n ** Y n)"
-proof -
-  obtain K where K: "0 \<le> K"
-    and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
-    using nonneg_bounded by fast
-  obtain B where B: "0 < B"
-    and norm_Y: "\<And>n. norm (Y n) \<le> B"
-    using Y [unfolded Bseq_def] by fast
-  from X show ?thesis
-  proof (rule Zseq_imp_Zseq)
-    fix n::nat
-    have "norm (X n ** Y n) \<le> norm (X n) * norm (Y n) * K"
-      by (rule norm_le)
-    also have "\<dots> \<le> norm (X n) * B * K"
-      by (intro mult_mono' order_refl norm_Y norm_ge_zero
-                mult_nonneg_nonneg K)
-    also have "\<dots> = norm (X n) * (B * K)"
-      by (rule mult_assoc)
-    finally show "norm (X n ** Y n) \<le> norm (X n) * (B * K)" .
-  qed
-qed
+  "Zseq X \<Longrightarrow> Bseq Y \<Longrightarrow> Zseq (\<lambda>n. X n ** Y n)"
+unfolding Zseq_conv_Zfun Bseq_conv_Bfun
+by (rule Zfun_prod_Bfun)
 
 lemma (in bounded_bilinear) Bseq_prod_Zseq:
-  assumes X: "Bseq X"
-  assumes Y: "Zseq Y"
-  shows "Zseq (\<lambda>n. X n ** Y n)"
-proof -
-  obtain K where K: "0 \<le> K"
-    and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
-    using nonneg_bounded by fast
-  obtain B where B: "0 < B"
-    and norm_X: "\<And>n. norm (X n) \<le> B"
-    using X [unfolded Bseq_def] by fast
-  from Y show ?thesis
-  proof (rule Zseq_imp_Zseq)
-    fix n::nat
-    have "norm (X n ** Y n) \<le> norm (X n) * norm (Y n) * K"
-      by (rule norm_le)
-    also have "\<dots> \<le> B * norm (Y n) * K"
-      by (intro mult_mono' order_refl norm_X norm_ge_zero
-                mult_nonneg_nonneg K)
-    also have "\<dots> = norm (Y n) * (B * K)"
-      by (simp only: mult_ac)
-    finally show "norm (X n ** Y n) \<le> norm (Y n) * (B * K)" .
-  qed
-qed
+  "Bseq X \<Longrightarrow> Zseq Y \<Longrightarrow> Zseq (\<lambda>n. X n ** Y n)"
+unfolding Zseq_conv_Zfun Bseq_conv_Bfun
+by (rule Bfun_prod_Zfun)
 
 lemma (in bounded_bilinear) Zseq_left:
   "Zseq X \<Longrightarrow> Zseq (\<lambda>n. X n ** a)"
@@ -363,11 +331,6 @@
   shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
 by (rule mult.LIMSEQ)
 
-lemma inverse_diff_inverse:
-  "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
-   \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
-by (simp add: algebra_simps)
-
 lemma Bseq_inverse_lemma:
   fixes x :: "'a::real_normed_div_algebra"
   shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r"
@@ -377,69 +340,15 @@
 
 lemma Bseq_inverse:
   fixes a :: "'a::real_normed_div_algebra"
-  assumes X: "X ----> a"
-  assumes a: "a \<noteq> 0"
-  shows "Bseq (\<lambda>n. inverse (X n))"
-proof -
-  from a have "0 < norm a" by simp
-  hence "\<exists>r>0. r < norm a" by (rule dense)
-  then obtain r where r1: "0 < r" and r2: "r < norm a" by fast
-  obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> norm (X n - a) < r"
-    using LIMSEQ_D [OF X r1] by fast
-  show ?thesis
-  proof (rule BseqI2' [rule_format])
-    fix n assume n: "N \<le> n"
-    hence 1: "norm (X n - a) < r" by (rule N)
-    hence 2: "X n \<noteq> 0" using r2 by auto
-    hence "norm (inverse (X n)) = inverse (norm (X n))"
-      by (rule nonzero_norm_inverse)
-    also have "\<dots> \<le> inverse (norm a - r)"
-    proof (rule le_imp_inverse_le)
-      show "0 < norm a - r" using r2 by simp
-    next
-      have "norm a - norm (X n) \<le> norm (a - X n)"
-        by (rule norm_triangle_ineq2)
-      also have "\<dots> = norm (X n - a)"
-        by (rule norm_minus_commute)
-      also have "\<dots> < r" using 1 .
-      finally show "norm a - r \<le> norm (X n)" by simp
-    qed
-    finally show "norm (inverse (X n)) \<le> inverse (norm a - r)" .
-  qed
-qed
-
-lemma LIMSEQ_inverse_lemma:
-  fixes a :: "'a::real_normed_div_algebra"
-  shows "\<lbrakk>X ----> a; a \<noteq> 0; \<forall>n. X n \<noteq> 0\<rbrakk>
-         \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> inverse a"
-apply (subst LIMSEQ_Zseq_iff)
-apply (simp add: inverse_diff_inverse nonzero_imp_inverse_nonzero)
-apply (rule Zseq_minus)
-apply (rule Zseq_mult_left)
-apply (rule mult.Bseq_prod_Zseq)
-apply (erule (1) Bseq_inverse)
-apply (simp add: LIMSEQ_Zseq_iff)
-done
+  shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
+unfolding LIMSEQ_conv_tendsto Bseq_conv_Bfun
+by (rule Bfun_inverse)
 
 lemma LIMSEQ_inverse:
   fixes a :: "'a::real_normed_div_algebra"
-  assumes X: "X ----> a"
-  assumes a: "a \<noteq> 0"
-  shows "(\<lambda>n. inverse (X n)) ----> inverse a"
-proof -
-  from a have "0 < norm a" by simp
-  then obtain k where "\<forall>n\<ge>k. norm (X n - a) < norm a"
-    using LIMSEQ_D [OF X] by fast
-  hence "\<forall>n\<ge>k. X n \<noteq> 0" by auto
-  hence k: "\<forall>n. X (n + k) \<noteq> 0" by simp
-
-  from X have "(\<lambda>n. X (n + k)) ----> a"
-    by (rule LIMSEQ_ignore_initial_segment)
-  hence "(\<lambda>n. inverse (X (n + k))) ----> inverse a"
-    using a k by (rule LIMSEQ_inverse_lemma)
-  thus "(\<lambda>n. inverse (X n)) ----> inverse a"
-    by (rule LIMSEQ_offset)
-qed
+  shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> inverse a"
+unfolding LIMSEQ_conv_tendsto
+by (rule tendsto_inverse)
 
 lemma LIMSEQ_divide:
   fixes a b :: "'a::real_normed_field"