(* Title: HOL/Analysis/Operator_Norm.thy Author: Amine Chaieb, University of Cambridge Author: Brian Huffman *) section ‹Operator Norm› theory Operator_Norm imports Complex_Main begin text ‹This formulation yields zero if ‹'a› is the trivial vector space.› text✐‹tag important› ‹%whitespace› definition✐‹tag important› 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 ‹In non-trivial vector spaces, the first assumption is redundant.› 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 ‹a ≠ 0› show "0 ≤ 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 ‹x ≠ 0›) 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 *⇩_{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 *⇩_{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 *⇩_{R}f x) = ¦r¦ * onorm f" proof (cases "r = 0") assume "r ≠ 0" show ?thesis proof (rule order_antisym) show "onorm (λx. r *⇩_{R}f x) ≤ ¦r¦ * onorm f" using f by (rule onorm_scaleR_lemma) next have "bounded_linear (λx. r *⇩_{R}f x)" using bounded_linear_scaleR_right f by (rule bounded_linear_compose) then have "onorm (λx. inverse r *⇩_{R}r *⇩_{R}f x) ≤ ¦inverse r¦ * onorm (λx. r *⇩_{R}f x)" by (rule onorm_scaleR_lemma) with ‹r ≠ 0› show "¦r¦ * onorm f ≤ onorm (λx. r *⇩_{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 *⇩_{R}f) ≤ onorm r * norm f" proof (rule onorm_bound) fix x have "norm (r x *⇩_{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 *⇩_{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 *⇩_{R}f) = onorm r * norm f" proof (cases "f = 0") assume "f ≠ 0" show ?thesis proof (rule order_antisym) show "onorm (λx. r x *⇩_{R}f) ≤ onorm r * norm f" using f by (rule onorm_scaleR_left_lemma) next have bl1: "bounded_linear (λx. r x *⇩_{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 ‹f ≠ 0› by (simp add: inverse_eq_divide) also have "onorm (λx. r x * norm f) ≤ onorm (λx. r x *⇩_{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 *⇩_{R}f)" using ‹f ≠ 0› 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