(* Title: HOL/Analysis/Operator_Norm.thy
Author: Amine Chaieb, University of Cambridge
Author: Brian Huffman
*)
section \<open>Operator Norm\<close>
theory Operator_Norm
imports Complex_Main
begin
text \<open>This formulation yields zero if \<open>'a\<close> is the trivial vector space.\<close>
text\<^marker>\<open>tag important\<close> \<open>%whitespace\<close>
definition\<^marker>\<open>tag important\<close>
onorm :: "('a::real_normed_vector \ 'b::real_normed_vector) \ real" where
"onorm f = (SUP x. norm (f x) / norm x)"
proposition onorm_bound:
assumes "0 \ b" and "\x. norm (f x) \ b * norm x"
shows "onorm f \ b"
unfolding onorm_def
proof (rule cSUP_least)
fix x
show "norm (f x) / norm x \ b"
using assms by (cases "x = 0") (simp_all add: pos_divide_le_eq)
qed simp
text \<open>In non-trivial vector spaces, the first assumption is redundant.\<close>
lemma onorm_le:
fixes f :: "'a::{real_normed_vector, perfect_space} \ 'b::real_normed_vector"
assumes "\x. norm (f x) \ b * norm x"
shows "onorm f \ b"
proof (rule onorm_bound [OF _ assms])
have "{0::'a} \ UNIV" by (metis not_open_singleton open_UNIV)
then obtain a :: 'a where "a \ 0" by fast
have "0 \ b * norm a"
by (rule order_trans [OF norm_ge_zero assms])
with \<open>a \<noteq> 0\<close> show "0 \<le> b"
by (simp add: zero_le_mult_iff)
qed
lemma le_onorm:
assumes "bounded_linear f"
shows "norm (f x) / norm x \ onorm f"
proof -
interpret f: bounded_linear f by fact
obtain b where "0 \ b" and "\x. norm (f x) \ norm x * b"
using f.nonneg_bounded by auto
then have "\x. norm (f x) / norm x \ b"
by (clarify, case_tac "x = 0",
simp_all add: f.zero pos_divide_le_eq mult.commute)
then have "bdd_above (range (\x. norm (f x) / norm x))"
unfolding bdd_above_def by fast
with UNIV_I show ?thesis
unfolding onorm_def by (rule cSUP_upper)
qed
lemma onorm:
assumes "bounded_linear f"
shows "norm (f x) \ onorm f * norm x"
proof -
interpret f: bounded_linear f by fact
show ?thesis
proof (cases)
assume "x = 0"
then show ?thesis by (simp add: f.zero)
next
assume "x \ 0"
have "norm (f x) / norm x \ onorm f"
by (rule le_onorm [OF assms])
then show "norm (f x) \ onorm f * norm x"
by (simp add: pos_divide_le_eq \<open>x \<noteq> 0\<close>)
qed
qed
lemma onorm_pos_le:
assumes f: "bounded_linear f"
shows "0 \ onorm f"
using le_onorm [OF f, where x=0] by simp
lemma onorm_zero: "onorm (\x. 0) = 0"
proof (rule order_antisym)
show "onorm (\x. 0) \ 0"
by (simp add: onorm_bound)
show "0 \ onorm (\x. 0)"
using bounded_linear_zero by (rule onorm_pos_le)
qed
lemma onorm_eq_0:
assumes f: "bounded_linear f"
shows "onorm f = 0 \ (\x. f x = 0)"
using onorm [OF f] by (auto simp: fun_eq_iff [symmetric] onorm_zero)
lemma onorm_pos_lt:
assumes f: "bounded_linear f"
shows "0 < onorm f \ \ (\x. f x = 0)"
by (simp add: less_le onorm_pos_le [OF f] onorm_eq_0 [OF f])
lemma onorm_id_le: "onorm (\x. x) \ 1"
by (rule onorm_bound) simp_all
lemma onorm_id: "onorm (\x. x::'a::{real_normed_vector, perfect_space}) = 1"
proof (rule antisym[OF onorm_id_le])
have "{0::'a} \ UNIV" by (metis not_open_singleton open_UNIV)
then obtain x :: 'a where "x \ 0" by fast
hence "1 \ norm x / norm x"
by simp
also have "\ \ onorm (\x::'a. x)"
by (rule le_onorm) (rule bounded_linear_ident)
finally show "1 \ onorm (\x::'a. x)" .
qed
lemma onorm_compose:
assumes f: "bounded_linear f"
assumes g: "bounded_linear g"
shows "onorm (f \ g) \ onorm f * onorm g"
proof (rule onorm_bound)
show "0 \ onorm f * onorm g"
by (intro mult_nonneg_nonneg onorm_pos_le f g)
next
fix x
have "norm (f (g x)) \ onorm f * norm (g x)"
by (rule onorm [OF f])
also have "onorm f * norm (g x) \ onorm f * (onorm g * norm x)"
by (rule mult_left_mono [OF onorm [OF g] onorm_pos_le [OF f]])
finally show "norm ((f \ g) x) \ onorm f * onorm g * norm x"
by (simp add: mult.assoc)
qed
lemma onorm_scaleR_lemma:
assumes f: "bounded_linear f"
shows "onorm (\x. r *\<^sub>R f x) \ \r\ * onorm f"
proof (rule onorm_bound)
show "0 \ \r\ * onorm f"
by (intro mult_nonneg_nonneg onorm_pos_le abs_ge_zero f)
next
fix x
have "\r\ * norm (f x) \ \r\ * (onorm f * norm x)"
by (intro mult_left_mono onorm abs_ge_zero f)
then show "norm (r *\<^sub>R f x) \ \r\ * onorm f * norm x"
by (simp only: norm_scaleR mult.assoc)
qed
lemma onorm_scaleR:
assumes f: "bounded_linear f"
shows "onorm (\x. r *\<^sub>R f x) = \r\ * onorm f"
proof (cases "r = 0")
assume "r \ 0"
show ?thesis
proof (rule order_antisym)
show "onorm (\x. r *\<^sub>R f x) \ \r\ * onorm f"
using f by (rule onorm_scaleR_lemma)
next
have "bounded_linear (\x. r *\<^sub>R f x)"
using bounded_linear_scaleR_right f by (rule bounded_linear_compose)
then have "onorm (\x. inverse r *\<^sub>R r *\<^sub>R f x) \ \inverse r\ * onorm (\x. r *\<^sub>R f x)"
by (rule onorm_scaleR_lemma)
with \<open>r \<noteq> 0\<close> show "\<bar>r\<bar> * onorm f \<le> onorm (\<lambda>x. r *\<^sub>R f x)"
by (simp add: inverse_eq_divide pos_le_divide_eq mult.commute)
qed
qed (simp add: onorm_zero)
lemma onorm_scaleR_left_lemma:
assumes r: "bounded_linear r"
shows "onorm (\x. r x *\<^sub>R f) \ onorm r * norm f"
proof (rule onorm_bound)
fix x
have "norm (r x *\<^sub>R f) = norm (r x) * norm f"
by simp
also have "\ \ onorm r * norm x * norm f"
by (intro mult_right_mono onorm r norm_ge_zero)
finally show "norm (r x *\<^sub>R f) \ onorm r * norm f * norm x"
by (simp add: ac_simps)
qed (intro mult_nonneg_nonneg norm_ge_zero onorm_pos_le r)
lemma onorm_scaleR_left:
assumes f: "bounded_linear r"
shows "onorm (\x. r x *\<^sub>R f) = onorm r * norm f"
proof (cases "f = 0")
assume "f \ 0"
show ?thesis
proof (rule order_antisym)
show "onorm (\x. r x *\<^sub>R f) \ onorm r * norm f"
using f by (rule onorm_scaleR_left_lemma)
next
have bl1: "bounded_linear (\x. r x *\<^sub>R f)"
by (metis bounded_linear_scaleR_const f)
have "bounded_linear (\x. r x * norm f)"
by (metis bounded_linear_mult_const f)
from onorm_scaleR_left_lemma[OF this, of "inverse (norm f)"]
have "onorm r \ onorm (\x. r x * norm f) * inverse (norm f)"
using \<open>f \<noteq> 0\<close>
by (simp add: inverse_eq_divide)
also have "onorm (\x. r x * norm f) \ onorm (\x. r x *\<^sub>R f)"
by (rule onorm_bound)
(auto simp: abs_mult bl1 onorm_pos_le intro!: order_trans[OF _ onorm])
finally show "onorm r * norm f \ onorm (\x. r x *\<^sub>R f)"
using \<open>f \<noteq> 0\<close>
by (simp add: inverse_eq_divide pos_le_divide_eq mult.commute)
qed
qed (simp add: onorm_zero)
lemma onorm_neg:
shows "onorm (\x. - f x) = onorm f"
unfolding onorm_def by simp
lemma onorm_triangle:
assumes f: "bounded_linear f"
assumes g: "bounded_linear g"
shows "onorm (\x. f x + g x) \ onorm f + onorm g"
proof (rule onorm_bound)
show "0 \ onorm f + onorm g"
by (intro add_nonneg_nonneg onorm_pos_le f g)
next
fix x
have "norm (f x + g x) \ norm (f x) + norm (g x)"
by (rule norm_triangle_ineq)
also have "norm (f x) + norm (g x) \ onorm f * norm x + onorm g * norm x"
by (intro add_mono onorm f g)
finally show "norm (f x + g x) \ (onorm f + onorm g) * norm x"
by (simp only: distrib_right)
qed
lemma onorm_triangle_le:
assumes "bounded_linear f"
assumes "bounded_linear g"
assumes "onorm f + onorm g \ e"
shows "onorm (\x. f x + g x) \ e"
using assms by (rule onorm_triangle [THEN order_trans])
lemma onorm_triangle_lt:
assumes "bounded_linear f"
assumes "bounded_linear g"
assumes "onorm f + onorm g < e"
shows "onorm (\x. f x + g x) < e"
using assms by (rule onorm_triangle [THEN order_le_less_trans])
lemma onorm_sum:
assumes "finite S"
assumes "\s. s \ S \ bounded_linear (f s)"
shows "onorm (\x. sum (\s. f s x) S) \ sum (\s. onorm (f s)) S"
using assms
by (induction) (auto simp: onorm_zero intro!: onorm_triangle_le bounded_linear_sum)
lemmas onorm_sum_le = onorm_sum[THEN order_trans]
end
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
