# Theory Operator_Norm

Up to index of Isabelle/HOL/HOL-Multivariate_Analysis

theory Operator_Norm
imports Linear_Algebra
`(*  Title:      HOL/Multivariate_Analysis/Operator_Norm.thy    Author:     Amine Chaieb, University of Cambridge*)header {* Operator Norm *}theory Operator_Normimports Linear_Algebrabegindefinition "onorm f = Sup {norm (f x)| x. norm x = 1}"lemma norm_bound_generalize:  fixes f:: "'a::euclidean_space => 'b::euclidean_space"  assumes lf: "linear f"  shows "(∀x. norm x = 1 --> norm (f x) ≤ b) <-> (∀x. norm (f x) ≤ b * norm x)" (is "?lhs <-> ?rhs")proof-  {assume H: ?rhs    {fix x :: "'a" assume x: "norm x = 1"      from H[rule_format, of x] x have "norm (f x) ≤ b" by simp}    then have ?lhs by blast }  moreover  {assume H: ?lhs    have bp: "b ≥ 0"      apply -      apply(rule order_trans [OF norm_ge_zero])      apply(rule H[rule_format, of "SOME x::'a. x ∈ Basis"])      by (auto intro: SOME_Basis norm_Basis)    {fix x :: "'a"      {assume "x = 0"        then have "norm (f x) ≤ b * norm x" by (simp add: linear_0[OF lf] bp)}      moreover      {assume x0: "x ≠ 0"        hence n0: "norm x ≠ 0" by (metis norm_eq_zero)        let ?c = "1/ norm x"        have "norm (?c *⇩R x) = 1" using x0 by (simp add: n0)        with H have "norm (f (?c *⇩R x)) ≤ b" by blast        hence "?c * norm (f x) ≤ b"          by (simp add: linear_cmul[OF lf])        hence "norm (f x) ≤ b * norm x"          using n0 norm_ge_zero[of x] by (auto simp add: field_simps)}      ultimately have "norm (f x) ≤ b * norm x" by blast}    then have ?rhs by blast}  ultimately show ?thesis by blastqed lemma onorm:  fixes f:: "'a::euclidean_space => 'b::euclidean_space"  assumes lf: "linear f"  shows "norm (f x) <= onorm f * norm x"  and "∀x. norm (f x) <= b * norm x ==> onorm f <= b"proof-  {    let ?S = "{norm (f x) |x. norm x = 1}"    have "norm (f (SOME i. i ∈ Basis)) ∈ ?S"      by (auto intro!: exI[of _ "SOME i. i ∈ Basis"] norm_Basis SOME_Basis)    hence Se: "?S ≠ {}" by auto    from linear_bounded[OF lf] have b: "∃ b. ?S *<= b"      unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: setle_def)    {from Sup[OF Se b, unfolded onorm_def[symmetric]]      show "norm (f x) <= onorm f * norm x"        apply -        apply (rule spec[where x = x])        unfolding norm_bound_generalize[OF lf, symmetric]        by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)}    {      show "∀x. norm (f x) <= b * norm x ==> onorm f <= b"        using Sup[OF Se b, unfolded onorm_def[symmetric]]        unfolding norm_bound_generalize[OF lf, symmetric]        by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)}  }qedlemma onorm_pos_le: assumes lf: "linear (f::'n::euclidean_space => 'm::euclidean_space)" shows "0 <= onorm f"  using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "SOME i. i ∈ Basis"]]   by (simp add: SOME_Basis)lemma onorm_eq_0: assumes lf: "linear (f::'a::euclidean_space => 'b::euclidean_space)"  shows "onorm f = 0 <-> (∀x. f x = 0)"  using onorm[OF lf]  apply (auto simp add: onorm_pos_le)  apply atomize  apply (erule allE[where x="0::real"])  using onorm_pos_le[OF lf]  apply arith  donelemma onorm_const: "onorm(λx::'a::euclidean_space. (y::'b::euclidean_space)) = norm y"proof-  let ?f = "λx::'a. (y::'b)"  have th: "{norm (?f x)| x. norm x = 1} = {norm y}"    by (auto simp: SOME_Basis intro!: exI[of _ "SOME i. i ∈ Basis"])  show ?thesis    unfolding onorm_def th    apply (rule Sup_unique) by (simp_all  add: setle_def)qedlemma onorm_pos_lt: assumes lf: "linear (f::'a::euclidean_space => 'b::euclidean_space)"  shows "0 < onorm f <-> ~(∀x. f x = 0)"  unfolding onorm_eq_0[OF lf, symmetric]  using onorm_pos_le[OF lf] by arithlemma onorm_compose:  assumes lf: "linear (f::'n::euclidean_space => 'm::euclidean_space)"  and lg: "linear (g::'k::euclidean_space => 'n::euclidean_space)"  shows "onorm (f o g) <= onorm f * onorm g"  apply (rule onorm(2)[OF linear_compose[OF lg lf], rule_format])  unfolding o_def  apply (subst mult_assoc)  apply (rule order_trans)  apply (rule onorm(1)[OF lf])  apply (rule mult_left_mono)  apply (rule onorm(1)[OF lg])  apply (rule onorm_pos_le[OF lf])  donelemma onorm_neg_lemma: assumes lf: "linear (f::'a::euclidean_space => 'b::euclidean_space)"  shows "onorm (λx. - f x) ≤ onorm f"  using onorm[OF linear_compose_neg[OF lf]] onorm[OF lf]  unfolding norm_minus_cancel by metislemma onorm_neg: assumes lf: "linear (f::'a::euclidean_space => 'b::euclidean_space)"  shows "onorm (λx. - f x) = onorm f"  using onorm_neg_lemma[OF lf] onorm_neg_lemma[OF linear_compose_neg[OF lf]]  by simplemma onorm_triangle:  assumes lf: "linear (f::'n::euclidean_space => 'm::euclidean_space)" and lg: "linear g"  shows "onorm (λx. f x + g x) <= onorm f + onorm g"  apply(rule onorm(2)[OF linear_compose_add[OF lf lg], rule_format])  apply (rule order_trans)  apply (rule norm_triangle_ineq)  apply (simp add: distrib)  apply (rule add_mono)  apply (rule onorm(1)[OF lf])  apply (rule onorm(1)[OF lg])  donelemma onorm_triangle_le: "linear (f::'n::euclidean_space => 'm::euclidean_space) ==> linear g ==> onorm(f) + onorm(g) <= e  ==> onorm(λx. f x + g x) <= e"  apply (rule order_trans)  apply (rule onorm_triangle)  apply assumption+  donelemma onorm_triangle_lt: "linear (f::'n::euclidean_space => 'm::euclidean_space) ==> linear g ==> onorm(f) + onorm(g) < e  ==> onorm(λx. f x + g x) < e"  apply (rule order_le_less_trans)  apply (rule onorm_triangle)  by assumption+end`