--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Sat Dec 16 21:41:14 2000 +0100
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Sat Dec 16 21:41:51 2000 +0100
@@ -9,377 +9,374 @@
subsection {* Continuous linear forms*}
-text{* A linear form $f$ on a normed vector space $(V, \norm{\cdot})$
-is \emph{continuous}, iff it is bounded, i.~e.
-\[\Ex {c\in R}{\All {x\in V} {|f\ap x| \leq c \cdot \norm x}}\]
-In our application no other functions than linear forms are considered,
-so we can define continuous linear forms as bounded linear forms:
+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.
+ \begin{center}
+ @{text "\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+ \end{center}
+ In our application no other functions than linear forms are
+ considered, so we can define continuous linear forms as bounded
+ linear forms:
*}
constdefs
is_continuous ::
- "['a::{plus, minus, zero} set, 'a => real, 'a => real] => bool"
- "is_continuous V norm f ==
- is_linearform V f \<and> (\<exists>c. \<forall>x \<in> V. |f x| <= c * norm x)"
+ "'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)"
-lemma continuousI [intro]:
- "[| is_linearform V f; !! x. x \<in> V ==> |f x| <= c * norm x |]
- ==> is_continuous V norm f"
+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"
proof (unfold is_continuous_def, intro exI conjI ballI)
- assume r: "!! x. x \<in> V ==> |f x| <= c * norm x"
- fix x assume "x \<in> V" show "|f x| <= c * norm x" by (rule r)
+ assume r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * norm x"
+ fix x assume "x \<in> V" show "\<bar>f x\<bar> \<le> c * norm x" by (rule r)
qed
-
-lemma continuous_linearform [intro?]:
- "is_continuous V norm f ==> is_linearform V f"
- by (unfold is_continuous_def) force
+
+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
- ==> \<exists>c. \<forall>x \<in> V. |f x| <= c * norm x"
- by (unfold is_continuous_def) force
+ "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
subsection{* The norm of a linear form *}
-text{* The least real number $c$ for which holds
-\[\All {x\in V}{|f\ap x| \leq c \cdot \norm x}\]
-is called the \emph{norm} of $f$.
+text {*
+ The least real number @{text c} for which holds
+ \begin{center}
+ @{text "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+ \end{center}
+ is called the \emph{norm} of @{text f}.
-For non-trivial vector spaces $V \neq \{\zero\}$ the norm can be defined as
-\[\fnorm {f} =\sup_{x\neq\zero}\frac{|f\ap x|}{\norm x} \]
+ For non-trivial vector spaces @{text "V \<noteq> {0}"} the norm can be
+ defined as
+ \begin{center}
+ @{text "\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>"}
+ \end{center}
-For the case $V = \{\zero\}$ the supremum would be taken from an
-empty set. Since $\bbbR$ is unbounded, there would be no supremum. To
-avoid this situation it must be guaranteed that there is an element in
-this set. This element must be ${} \ge 0$ so that
-$\idt{function{\dsh}norm}$ has the norm properties. Furthermore it
-does not have to change the norm in all other cases, so it must be
-$0$, as all other elements of are ${} \ge 0$.
+ For the case @{text "V = {0}"} the supremum would be taken from an
+ empty set. Since @{text \<real>} is unbounded, there would be no supremum.
+ To avoid this situation it must be guaranteed that there is an
+ 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"}.
-Thus we define the set $B$ the supremum is taken from as
-\[
-\{ 0 \} \Union \left\{ \frac{|f\ap x|}{\norm x} \dt x\neq \zero \And x\in F\right\}
- \]
+ Thus we define the set @{text B} the supremum is taken from as
+ \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}.
*}
constdefs
- B :: "[ 'a set, 'a => real, 'a::{plus, minus, zero} => real ] => real set"
- "B V norm f ==
- {#0} \<union> {|f x| * inverse (norm x) | x. x \<noteq> 0 \<and> x \<in> V}"
+ 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{* $n$ is the function norm of $f$, iff
-$n$ is the supremum of $B$.
+text {*
+ @{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} => real, 'a set, 'a => real] => real => bool"
- "is_function_norm f V norm fn == is_Sup UNIV (B V norm f) fn"
+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)"
-text{* $\idt{function{\dsh}norm}$ is equal to the supremum of $B$,
-if the supremum exists. Otherwise it is undefined. *}
-
-constdefs
- function_norm :: " ['a::{minus,plus,zero} => real, 'a set, 'a => real] => real"
- "function_norm f V norm == Sup UNIV (B V norm f)"
-
-syntax
- function_norm :: " ['a => real, 'a set, 'a => real] => real" ("\<parallel>_\<parallel>_,_")
+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, force)
-
-text {* The following lemma states that every continuous linear form
-on a normed space $(V, \norm{\cdot})$ has a function norm. *}
+ by (unfold B_def) blast
-lemma ex_fnorm [intro?]:
- "[| is_normed_vectorspace V norm; is_continuous V norm f|]
- ==> is_function_norm f V norm \<parallel>f\<parallel>V,norm"
-proof (unfold function_norm_def is_function_norm_def
+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. |f x| <= c * norm x"
+ assume "is_linearform V f"
+ and e: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
- txt {* The existence of the supremum is shown using the
+ 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
+ every non-empty bounded set of reals has a
supremum. *}
- show "\<exists>a. is_Sup UNIV (B V norm f) a"
+ show "\<exists>a. is_Sup UNIV (B V norm f) a"
proof (unfold is_Sup_def, rule reals_complete)
- txt {* First we have to show that $B$ is non-empty: *}
+ txt {* First we have to show that @{text B} is non-empty: *}
- show "\<exists>X. X \<in> B V norm f"
- proof (intro exI)
- show "#0 \<in> (B V norm f)" by (unfold B_def, force)
+ show "\<exists>X. X \<in> B V norm f"
+ proof
+ show "#0 \<in> (B V norm f)" by (unfold B_def) blast
qed
- txt {* Then we have to show that $B$ is bounded: *}
+ txt {* Then we have to show that @{text B} is bounded: *}
from e show "\<exists>Y. isUb UNIV (B V norm f) Y"
proof
- txt {* We know that $f$ is bounded by some value $c$. *}
-
- fix c assume a: "\<forall>x \<in> V. |f x| <= c * norm x"
- def b == "max c #0"
+ 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"
show "?thesis"
- proof (intro exI isUbI setleI ballI, unfold B_def,
- elim UnE CollectE exE conjE singletonE)
+ 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 $b$, such that $y \leq b$ for all $y\in B$.
- Due to the definition of $B$ there are two cases for
- $y\in B$. If $y = 0$ then $y \leq \idt{max}\ap c\ap 0$: *}
+ 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 <= b" by (simp! add: le_maxI2)
+ fix y assume "y = (#0::real)"
+ show "y \<le> b" by (simp! add: le_maxI2)
- txt{* The second case is
- $y = {|f\ap x|}/{\norm x}$ for some
- $x\in V$ with $x \neq \zero$. *}
+ 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 y
- assume "x \<in> V" "x \<noteq> 0" (***
+ 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. *}
- have ge: "#0 <= inverse (norm x)";
- by (rule real_less_imp_le, rule real_inverse_gt_zero,
- rule normed_vs_norm_gt_zero); ( ***
- proof (rule real_less_imp_le);
- show "#0 < inverse (norm x)";
- proof (rule real_inverse_gt_zero);
- show "#0 < norm x"; ..;
- qed;
- qed; *** )
- have nz: "norm x \<noteq> #0"
- by (rule not_sym, rule lt_imp_not_eq,
- rule normed_vs_norm_gt_zero) (***
- proof (rule not_sym);
- show "#0 \<noteq> norm x";
- proof (rule lt_imp_not_eq);
- show "#0 < norm x"; ..;
- qed;
- qed; ***)***)
-
- txt {* The thesis follows by a short calculation using the
- fact that $f$ is bounded. *}
-
- assume "y = |f x| * inverse (norm x)"
- also have "... <= c * norm x * inverse (norm x)"
+ 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 <= inverse (norm x)"
- by (rule real_less_imp_le, rule real_inverse_gt_zero1,
+ show "#0 \<le> inverse (norm x)"
+ by (rule real_less_imp_le, rule real_inverse_gt_zero1,
rule normed_vs_norm_gt_zero)
- from a show "|f x| <= c * norm x" ..
+ from a show "\<bar>f x\<bar> \<le> c * norm x" ..
qed
- also have "... = c * (norm x * inverse (norm x))"
+ also have "... = c * (norm x * inverse (norm x))"
by (rule real_mult_assoc)
- also have "(norm x * inverse (norm x)) = (#1::real)"
+ 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,
+ 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 * ... <= b " by (simp! add: le_maxI1)
- finally show "y <= b" .
+ also have "c * ... \<le> b " by (simp! add: le_maxI1)
+ finally show "y \<le> b" .
qed simp
qed
qed
qed
-text {* The norm of a continuous function is always $\geq 0$. *}
+text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}
-lemma fnorm_ge_zero [intro?]:
- "[| is_continuous V norm f; is_normed_vectorspace V norm |]
- ==> #0 <= \<parallel>f\<parallel>V,norm"
+lemma fnorm_ge_zero [intro?]:
+ "is_continuous V norm f \<Longrightarrow> is_normed_vectorspace V norm
+ \<Longrightarrow> #0 \<le> \<parallel>f\<parallel>V,norm"
proof -
- assume c: "is_continuous V norm f"
+ assume c: "is_continuous V norm f"
and n: "is_normed_vectorspace V norm"
- txt {* The function norm is defined as the supremum of $B$.
- So it is $\geq 0$ if all elements in $B$ are $\geq 0$, provided
- the supremum exists and $B$ is not empty. *}
+ 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
+ show ?thesis
proof (unfold function_norm_def, rule sup_ub1)
- show "\<forall>x \<in> (B V norm f). #0 <= x"
+ show "\<forall>x \<in> (B V norm f). #0 \<le> x"
proof (intro ballI, unfold B_def,
- elim UnE singletonE CollectE exE conjE)
+ elim UnE singletonE CollectE exE conjE)
fix x r
- assume "x \<in> V" "x \<noteq> 0"
- and r: "r = |f x| * inverse (norm x)"
+ assume "x \<in> V" "x \<noteq> 0"
+ and r: "r = \<bar>f x\<bar> * inverse (norm x)"
- have ge: "#0 <= |f x|" by (simp! only: abs_ge_zero)
- have "#0 <= 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 real_less_imp_le, rule real_inverse_gt_zero1, rule)(***
proof (rule real_less_imp_le);
- show "#0 < inverse (norm x)";
+ show "#0 < inverse (norm x)";
proof (rule real_inverse_gt_zero);
show "#0 < norm x"; ..;
qed;
qed; ***)
- with ge show "#0 <= r"
+ with ge show "#0 \<le> r"
by (simp only: r, rule real_le_mult_order1a)
qed (simp!)
- txt {* Since $f$ is continuous the function norm exists: *}
+ 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))"
+ thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
by (unfold is_function_norm_def function_norm_def)
- txt {* $B$ is non-empty by construction: *}
+ txt {* @{text B} is non-empty by construction: *}
show "#0 \<in> B V norm f" by (rule B_not_empty)
qed
qed
-
-text{* \medskip The fundamental property of function norms is:
-\begin{matharray}{l}
-| f\ap x | \leq {\fnorm {f}} \cdot {\norm x}
-\end{matharray}
+
+text {*
+ \medskip The fundamental property of function norms is:
+ \begin{center}
+ @{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
+ \end{center}
*}
-lemma norm_fx_le_norm_f_norm_x:
- "[| is_continuous V norm f; is_normed_vectorspace V norm; x \<in> V |]
- ==> |f x| <= \<parallel>f\<parallel>V,norm * norm x"
-proof -
- assume "is_normed_vectorspace V norm" "x \<in> V"
+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 $x$. *}
-
+ txt{* The proof is by case analysis on @{text x}. *}
+
show ?thesis
proof cases
- txt {* For the case $x = \zero$ the thesis follows
- from the linearity of $f$: for every linear function
- holds $f\ap \zero = 0$. *}
+ 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 "|f x| = |f 0|" by (simp!)
+ 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 <= \<parallel>f\<parallel>V,norm * norm x"
+ also have "#0 \<le> \<parallel>f\<parallel>V,norm * norm x"
proof (rule real_le_mult_order1a)
- show "#0 <= \<parallel>f\<parallel>V,norm" ..
- show "#0 <= norm x" ..
+ show "#0 \<le> \<parallel>f\<parallel>V,norm" ..
+ show "#0 \<le> norm x" ..
qed
- finally
- show "|f x| <= \<parallel>f\<parallel>V,norm * norm x" .
+ 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"
+ hence nz: "norm x \<noteq> #0"
by (simp only: lt_imp_not_eq)
- txt {* For the case $x\neq \zero$ we derive the following
- fact from the definition of the function norm:*}
+ txt {* For the case @{text "x \<noteq> 0"} we derive the following fact
+ from the definition of the function norm:*}
- have l: "|f x| * inverse (norm x) <= \<parallel>f\<parallel>V,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 "|f x| * inverse (norm x) \<in> B V norm f"
+ 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 "|f x| = |f x| * #1" by (simp!)
- also from nz have "#1 = inverse (norm x) * norm x"
+ 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 "|f x| * ... = |f x| * inverse (norm x) * norm x"
+ 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 "... <= \<parallel>f\<parallel>V,norm * norm x"
+ also from n l have "... \<le> \<parallel>f\<parallel>V,norm * norm x"
by (simp add: real_mult_le_le_mono2)
- finally show "|f x| <= \<parallel>f\<parallel>V,norm * norm x" .
+ finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>V,norm * norm x" .
qed
qed
-text{* \medskip The function norm is the least positive real number for
-which the following inequation holds:
-\begin{matharray}{l}
-| f\ap x | \leq c \cdot {\norm x}
-\end{matharray}
+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>"}
+ \end{center}
*}
-lemma fnorm_le_ub:
- "[| is_continuous V norm f; is_normed_vectorspace V norm;
- \<forall>x \<in> V. |f x| <= c * norm x; #0 <= c |]
- ==> \<parallel>f\<parallel>V,norm <= c"
+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 "is_normed_vectorspace V norm"
assume c: "is_continuous V norm f"
- assume fb: "\<forall>x \<in> V. |f x| <= c * norm x"
- and "#0 <= c"
+ 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 $c\geq 0$.
- If $c$ is an upper bound of $B$, then $c$ is greater
- than the function norm since the function norm is the
- least upper bound.
- *}
+ 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) <= c"
+ 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 {* $c$ is an upper bound of $B$, i.e. every
- $y\in B$ is less than $c$. *}
+ 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 "isUb UNIV (B V norm f) c"
+ 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 <= c"
+ thus le: "y \<le> c"
proof (unfold B_def, elim UnE CollectE exE conjE singletonE)
- txt {* The first case for $y\in B$ is $y=0$. *}
+ txt {* The first case for @{text "y \<in> B"} is @{text "y = 0"}. *}
assume "y = #0"
- show "y <= c" by (force!)
+ show "y \<le> c" by (blast!)
- txt{* The second case is
- $y = {|f\ap x|}/{\norm x}$ for some
- $x\in V$ with $x \neq \zero$. *}
+ 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"
+ fix x
+ assume "x \<in> V" "x \<noteq> 0"
- have lz: "#0 < norm x"
+ have lz: "#0 < norm x"
by (simp! add: normed_vs_norm_gt_zero)
-
- have nz: "norm x \<noteq> #0"
+
+ 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_zero1)
- hence inverse_gez: "#0 <= inverse (norm x)"
+
+ from lz have "#0 < inverse (norm x)"
+ by (simp! add: real_inverse_gt_zero1)
+ hence inverse_gez: "#0 \<le> inverse (norm x)"
by (rule real_less_imp_le)
- assume "y = |f x| * inverse (norm x)"
- also from inverse_gez have "... <= c * norm x * inverse (norm x)"
- proof (rule real_mult_le_le_mono2)
- show "|f x| <= c * norm x" by (rule bspec)
- qed
- also have "... <= c" by (simp add: nz real_mult_assoc)
- finally show ?thesis .
+ 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 force
+ qed blast
qed
qed
-end
\ No newline at end of file
+end