--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Thu Aug 22 12:28:41 2002 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Thu Aug 22 20:49:43 2002 +0200
@@ -11,7 +11,7 @@
text {*
A linear form @{text f} on a normed vector space @{text "(V, \<parallel>\<cdot>\<parallel>)"}
- is \emph{continuous}, iff it is bounded, i.~e.
+ is \emph{continuous}, iff it is bounded, i.e.
\begin{center}
@{text "\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
\end{center}
@@ -20,28 +20,21 @@
linear forms:
*}
-constdefs
- is_continuous ::
- "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
- "is_continuous V norm f \<equiv>
- is_linearform V f \<and> (\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x)"
+locale continuous = var V + norm_syntax + linearform +
+ assumes bounded: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
lemma continuousI [intro]:
- "is_linearform V f \<Longrightarrow> (\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * norm x)
- \<Longrightarrow> is_continuous V norm f"
- by (unfold is_continuous_def) blast
-
-lemma continuous_linearform [intro?]:
- "is_continuous V norm f \<Longrightarrow> is_linearform V f"
- by (unfold is_continuous_def) blast
-
-lemma continuous_bounded [intro?]:
- "is_continuous V norm f
- \<Longrightarrow> \<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
- by (unfold is_continuous_def) blast
+ includes norm_syntax + linearform
+ assumes r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>"
+ shows "continuous V norm f"
+proof
+ show "linearform V f" .
+ from r have "\<exists>c. \<forall>x\<in>V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by blast
+ then show "continuous_axioms V norm f" ..
+qed
-subsection{* The norm of a linear form *}
+subsection {* The norm of a linear form *}
text {*
The least real number @{text c} for which holds
@@ -62,174 +55,133 @@
element in this set. This element must be @{text "{} \<ge> 0"} so that
@{text function_norm} has the norm properties. Furthermore
it does not have to change the norm in all other cases, so it must
- be @{text 0}, as all other elements of are @{text "{} \<ge> 0"}.
+ be @{text 0}, as all other elements are @{text "{} \<ge> 0"}.
- Thus we define the set @{text B} the supremum is taken from as
+ Thus we define the set @{text B} where the supremum is taken from as
+ follows:
\begin{center}
@{text "{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}"}
\end{center}
-*}
-constdefs
- B :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a::{plus, minus, zero} \<Rightarrow> real) \<Rightarrow> real set"
- "B V norm f \<equiv>
- {0} \<union> {\<bar>f x\<bar> * inverse (norm x) | x. x \<noteq> 0 \<and> x \<in> V}"
-
-text {*
- @{text n} is the function norm of @{text f}, iff @{text n} is the
- supremum of @{text B}.
+ @{text function_norm} is equal to the supremum of @{text B}, if the
+ supremum exists (otherwise it is undefined).
*}
-constdefs
- is_function_norm ::
- "('a::{minus,plus,zero} \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> bool"
- "is_function_norm f V norm fn \<equiv> is_Sup UNIV (B V norm f) fn"
-
-text {*
- @{text function_norm} is equal to the supremum of @{text B}, if the
- supremum exists. Otherwise it is undefined.
-*}
+locale function_norm = norm_syntax +
+ fixes B
+ defines "B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}"
+ fixes function_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
+ defines "\<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
-constdefs
- function_norm :: "('a::{minus,plus,zero} \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> real"
- "function_norm f V norm \<equiv> Sup UNIV (B V norm f)"
+lemma (in function_norm) B_not_empty [intro]: "0 \<in> B V f"
+ by (unfold B_def) simp
-syntax
- function_norm :: "('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> real" ("\<parallel>_\<parallel>_,_")
-
-lemma B_not_empty: "0 \<in> B V norm f"
- by (unfold B_def) blast
+locale (open) functional_vectorspace =
+ normed_vectorspace + function_norm +
+ fixes cont
+ defines "cont f \<equiv> continuous V norm f"
text {*
The following lemma states that every continuous linear form on a
normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.
*}
-lemma ex_fnorm [intro?]:
- "is_normed_vectorspace V norm \<Longrightarrow> is_continuous V norm f
- \<Longrightarrow> is_function_norm f V norm \<parallel>f\<parallel>V,norm"
-proof (unfold function_norm_def is_function_norm_def
- is_continuous_def Sup_def, elim conjE, rule someI2_ex)
- assume "is_normed_vectorspace V norm"
- assume "is_linearform V f"
- and e: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
-
+lemma (in functional_vectorspace) function_norm_works:
+ includes continuous
+ shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
+proof -
txt {* The existence of the supremum is shown using the
- completeness of the reals. Completeness means, that
- every non-empty bounded set of reals has a
- supremum. *}
- show "\<exists>a. is_Sup UNIV (B V norm f) a"
- proof (unfold is_Sup_def, rule reals_complete)
-
+ completeness of the reals. Completeness means, that every
+ non-empty bounded set of reals has a supremum. *}
+ have "\<exists>a. lub (B V f) a"
+ proof (rule real_complete)
txt {* First we have to show that @{text B} is non-empty: *}
-
- show "\<exists>X. X \<in> B V norm f"
- proof
- show "0 \<in> (B V norm f)" by (unfold B_def) blast
- qed
+ have "0 \<in> B V f" ..
+ thus "\<exists>x. x \<in> B V f" ..
txt {* Then we have to show that @{text B} is bounded: *}
-
- from e show "\<exists>Y. isUb UNIV (B V norm f) Y"
- proof
-
+ show "\<exists>c. \<forall>y \<in> B V f. y \<le> c"
+ proof -
txt {* We know that @{text f} is bounded by some value @{text c}. *}
-
- fix c assume a: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
- def b \<equiv> "max c 0"
+ from bounded obtain c where c: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
- show "?thesis"
- proof (intro exI isUbI setleI ballI, unfold B_def,
- elim UnE CollectE exE conjE singletonE)
-
- txt {* To proof the thesis, we have to show that there is some
- constant @{text b}, such that @{text "y \<le> b"} for all
- @{text "y \<in> B"}. Due to the definition of @{text B} there are
- two cases for @{text "y \<in> B"}. If @{text "y = 0"} then
- @{text "y \<le> max c 0"}: *}
-
- fix y assume "y = (0::real)"
- show "y \<le> b" by (simp! add: le_maxI2)
-
- txt {* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
- @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *}
+ txt {* To prove the thesis, we have to show that there is some
+ @{text b}, such that @{text "y \<le> b"} for all @{text "y \<in>
+ B"}. Due to the definition of @{text B} there are two cases. *}
- next
- fix x y
- assume "x \<in> V" "x \<noteq> 0"
-
- txt {* The thesis follows by a short calculation using the
- fact that @{text f} is bounded. *}
+ def b \<equiv> "max c 0"
+ have "\<forall>y \<in> B V f. y \<le> b"
+ proof
+ fix y assume y: "y \<in> B V f"
+ show "y \<le> b"
+ proof cases
+ assume "y = 0"
+ thus ?thesis by (unfold b_def) arith
+ next
+ txt {* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
+ @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *}
+ assume "y \<noteq> 0"
+ with y obtain x where y_rep: "y = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
+ and x: "x \<in> V" and neq: "x \<noteq> 0"
+ by (auto simp add: B_def real_divide_def)
+ from x neq have gt: "0 < \<parallel>x\<parallel>" ..
- assume "y = \<bar>f x\<bar> * inverse (norm x)"
- also have "... \<le> c * norm x * inverse (norm x)"
- proof (rule real_mult_le_le_mono2)
- show "0 \<le> inverse (norm x)"
- by (rule order_less_imp_le, rule real_inverse_gt_0,
- rule normed_vs_norm_gt_zero)
- from a show "\<bar>f x\<bar> \<le> c * norm x" ..
+ txt {* The thesis follows by a short calculation using the
+ fact that @{text f} is bounded. *}
+
+ note y_rep
+ also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
+ proof (rule real_mult_le_le_mono2)
+ from c show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
+ from gt have "0 < inverse \<parallel>x\<parallel>" by (rule real_inverse_gt_0)
+ thus "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le)
+ qed
+ also have "\<dots> = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)"
+ by (rule real_mult_assoc)
+ also
+ from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp
+ hence "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by (simp add: real_mult_inv_right1)
+ also have "c * 1 \<le> b" by (simp add: b_def le_maxI1)
+ finally show "y \<le> b" .
qed
- also have "... = c * (norm x * inverse (norm x))"
- by (rule real_mult_assoc)
- also have "(norm x * inverse (norm x)) = (1::real)"
- proof (rule real_mult_inv_right1)
- show nz: "norm x \<noteq> 0"
- by (rule not_sym, rule lt_imp_not_eq,
- rule normed_vs_norm_gt_zero)
- qed
- also have "c * ... \<le> b " by (simp! add: le_maxI1)
- finally show "y \<le> b" .
- qed simp
+ qed
+ thus ?thesis ..
qed
qed
+ then show ?thesis
+ by (unfold function_norm_def) (rule the_lubI_ex)
+qed
+
+lemma (in functional_vectorspace) function_norm_ub [intro?]:
+ includes continuous
+ assumes b: "b \<in> B V f"
+ shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
+proof -
+ have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" by (rule function_norm_works)
+ from this and b show ?thesis ..
+qed
+
+lemma (in functional_vectorspace) function_norm_least [intro?]:
+ includes continuous
+ assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"
+ shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
+proof -
+ have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" by (rule function_norm_works)
+ from this and b show ?thesis ..
qed
text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}
-lemma fnorm_ge_zero [intro?]:
- "is_continuous V norm f \<Longrightarrow> is_normed_vectorspace V norm
- \<Longrightarrow> 0 \<le> \<parallel>f\<parallel>V,norm"
+lemma (in functional_vectorspace) function_norm_ge_zero [iff]:
+ includes continuous
+ shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
proof -
- assume c: "is_continuous V norm f"
- and n: "is_normed_vectorspace V norm"
-
txt {* The function norm is defined as the supremum of @{text B}.
- So it is @{text "\<ge> 0"} if all elements in @{text B} are
- @{text "\<ge> 0"}, provided the supremum exists and @{text B} is not
- empty. *}
-
- show ?thesis
- proof (unfold function_norm_def, rule sup_ub1)
- show "\<forall>x \<in> (B V norm f). 0 \<le> x"
- proof (intro ballI, unfold B_def,
- elim UnE singletonE CollectE exE conjE)
- fix x r
- assume "x \<in> V" "x \<noteq> 0"
- and r: "r = \<bar>f x\<bar> * inverse (norm x)"
-
- have ge: "0 \<le> \<bar>f x\<bar>" by (simp! only: abs_ge_zero)
- have "0 \<le> inverse (norm x)"
- by (rule order_less_imp_le, rule real_inverse_gt_0, rule)(***
- proof (rule order_less_imp_le);
- show "0 < inverse (norm x)";
- proof (rule real_inverse_gt_zero);
- show "0 < norm x"; ..;
- qed;
- qed; ***)
- with ge show "0 \<le> r"
- by (simp only: r, rule real_le_mult_order1a)
- qed (simp!)
-
- txt {* Since @{text f} is continuous the function norm exists: *}
-
- have "is_function_norm f V norm \<parallel>f\<parallel>V,norm" ..
- thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
- by (unfold is_function_norm_def function_norm_def)
-
- txt {* @{text B} is non-empty by construction: *}
-
- show "0 \<in> B V norm f" by (rule B_not_empty)
- qed
+ So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>
+ 0"}, provided the supremum exists and @{text B} is not empty. *}
+ have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" by (rule function_norm_works)
+ moreover have "0 \<in> B V f" ..
+ ultimately show ?thesis ..
qed
text {*
@@ -239,141 +191,79 @@
\end{center}
*}
-lemma norm_fx_le_norm_f_norm_x:
- "is_continuous V norm f \<Longrightarrow> is_normed_vectorspace V norm \<Longrightarrow> x \<in> V
- \<Longrightarrow> \<bar>f x\<bar> \<le> \<parallel>f\<parallel>V,norm * norm x"
-proof -
- assume "is_normed_vectorspace V norm" "x \<in> V"
- and c: "is_continuous V norm f"
- have v: "is_vectorspace V" ..
-
- txt{* The proof is by case analysis on @{text x}. *}
-
- show ?thesis
- proof cases
-
- txt {* For the case @{text "x = 0"} the thesis follows from the
- linearity of @{text f}: for every linear function holds
- @{text "f 0 = 0"}. *}
-
- assume "x = 0"
- have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by (simp!)
- also from v continuous_linearform have "f 0 = 0" ..
- also note abs_zero
- also have "0 \<le> \<parallel>f\<parallel>V,norm * norm x"
- proof (rule real_le_mult_order1a)
- show "0 \<le> \<parallel>f\<parallel>V,norm" ..
- show "0 \<le> norm x" ..
+lemma (in functional_vectorspace) function_norm_le_cong:
+ includes continuous + vectorspace_linearform
+ assumes x: "x \<in> V"
+ shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
+proof cases
+ assume "x = 0"
+ then have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by simp
+ also have "f 0 = 0" ..
+ also have "\<bar>\<dots>\<bar> = 0" by simp
+ also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
+ proof (rule real_le_mult_order1a)
+ show "0 \<le> \<parallel>f\<parallel>\<hyphen>V" ..
+ show "0 \<le> norm x" ..
+ qed
+ finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
+next
+ assume "x \<noteq> 0"
+ with x have neq: "\<parallel>x\<parallel> \<noteq> 0" by simp
+ then have "\<bar>f x\<bar> = (\<bar>f x\<bar> * inverse \<parallel>x\<parallel>) * \<parallel>x\<parallel>" by simp
+ also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
+ proof (rule real_mult_le_le_mono2)
+ from x show "0 \<le> \<parallel>x\<parallel>" ..
+ show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
+ proof
+ from x and neq show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
+ by (auto simp add: B_def real_divide_def)
qed
- finally
- show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>V,norm * norm x" .
-
- next
- assume "x \<noteq> 0"
- have n: "0 < norm x" ..
- hence nz: "norm x \<noteq> 0"
- by (simp only: lt_imp_not_eq)
-
- txt {* For the case @{text "x \<noteq> 0"} we derive the following fact
- from the definition of the function norm:*}
-
- have l: "\<bar>f x\<bar> * inverse (norm x) \<le> \<parallel>f\<parallel>V,norm"
- proof (unfold function_norm_def, rule sup_ub)
- from ex_fnorm [OF _ c]
- show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
- by (simp! add: is_function_norm_def function_norm_def)
- show "\<bar>f x\<bar> * inverse (norm x) \<in> B V norm f"
- by (unfold B_def, intro UnI2 CollectI exI [of _ x]
- conjI, simp)
- qed
-
- txt {* The thesis now follows by a short calculation: *}
-
- have "\<bar>f x\<bar> = \<bar>f x\<bar> * 1" by (simp!)
- also from nz have "1 = inverse (norm x) * norm x"
- by (simp add: real_mult_inv_left1)
- also have "\<bar>f x\<bar> * ... = \<bar>f x\<bar> * inverse (norm x) * norm x"
- by (simp! add: real_mult_assoc)
- also from n l have "... \<le> \<parallel>f\<parallel>V,norm * norm x"
- by (simp add: real_mult_le_le_mono2)
- finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>V,norm * norm x" .
qed
+ finally show ?thesis .
qed
text {*
\medskip The function norm is the least positive real number for
which the following inequation holds:
\begin{center}
- @{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+ @{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
\end{center}
*}
-lemma fnorm_le_ub:
- "is_continuous V norm f \<Longrightarrow> is_normed_vectorspace V norm \<Longrightarrow>
- \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x \<Longrightarrow> 0 \<le> c
- \<Longrightarrow> \<parallel>f\<parallel>V,norm \<le> c"
-proof (unfold function_norm_def)
- assume "is_normed_vectorspace V norm"
- assume c: "is_continuous V norm f"
- assume fb: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
- and "0 \<le> c"
-
- txt {* Suppose the inequation holds for some @{text "c \<ge> 0"}. If
- @{text c} is an upper bound of @{text B}, then @{text c} is greater
- than the function norm since the function norm is the least upper
- bound. *}
-
- show "Sup UNIV (B V norm f) \<le> c"
- proof (rule sup_le_ub)
- from ex_fnorm [OF _ c]
- show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
- by (simp! add: is_function_norm_def function_norm_def)
-
- txt {* @{text c} is an upper bound of @{text B}, i.e. every
- @{text "y \<in> B"} is less than @{text c}. *}
-
- show "isUb UNIV (B V norm f) c"
- proof (intro isUbI setleI ballI)
- fix y assume "y \<in> B V norm f"
- thus le: "y \<le> c"
- proof (unfold B_def, elim UnE CollectE exE conjE singletonE)
-
- txt {* The first case for @{text "y \<in> B"} is @{text "y = 0"}. *}
-
- assume "y = 0"
- show "y \<le> c" by (blast!)
-
- txt{* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
- @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *}
-
- next
- fix x
- assume "x \<in> V" "x \<noteq> 0"
-
- have lz: "0 < norm x"
- by (simp! add: normed_vs_norm_gt_zero)
-
- have nz: "norm x \<noteq> 0"
- proof (rule not_sym)
- from lz show "0 \<noteq> norm x"
- by (simp! add: order_less_imp_not_eq)
- qed
-
- from lz have "0 < inverse (norm x)"
- by (simp! add: real_inverse_gt_0)
- hence inverse_gez: "0 \<le> inverse (norm x)"
- by (rule order_less_imp_le)
-
- assume "y = \<bar>f x\<bar> * inverse (norm x)"
- also from inverse_gez have "... \<le> c * norm x * inverse (norm x)"
- proof (rule real_mult_le_le_mono2)
- show "\<bar>f x\<bar> \<le> c * norm x" by (rule bspec)
- qed
- also have "... \<le> c" by (simp add: nz real_mult_assoc)
- finally show ?thesis .
- qed
- qed blast
+lemma (in functional_vectorspace) function_norm_least [intro?]:
+ includes continuous
+ assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
+ shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"
+proof (rule function_norm_least)
+ fix b assume b: "b \<in> B V f"
+ show "b \<le> c"
+ proof cases
+ assume "b = 0"
+ with ge show ?thesis by simp
+ next
+ assume "b \<noteq> 0"
+ with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
+ and x_neq: "x \<noteq> 0" and x: "x \<in> V"
+ by (auto simp add: B_def real_divide_def)
+ note b_rep
+ also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
+ proof (rule real_mult_le_le_mono2)
+ have "0 < \<parallel>x\<parallel>" ..
+ then show "0 \<le> inverse \<parallel>x\<parallel>" by simp
+ from ineq and x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
+ qed
+ also have "\<dots> = c"
+ proof -
+ from x_neq and x have "\<parallel>x\<parallel> \<noteq> 0" by simp
+ then show ?thesis by simp
+ qed
+ finally show ?thesis .
qed
qed
+lemmas [iff?] =
+ functional_vectorspace.function_norm_ge_zero
+ functional_vectorspace.function_norm_le_cong
+ functional_vectorspace.function_norm_least
+
end