src/HOL/Multivariate_Analysis/Operator_Norm.thy

a few new lemmas

(*  Title:      HOL/Multivariate_Analysis/Operator_Norm.thy
    Author:     Amine Chaieb, University of Cambridge
*)

header {* Operator Norm *}

theory Operator_Norm
imports Linear_Algebra
begin

definition "onorm f = (SUP x:{x. norm x = 1}. norm (f x))"

lemma norm_bound_generalize:
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  assumes lf: "linear f"
  shows "(\<forall>x. norm x = 1 \<longrightarrow> norm (f x) \<le> b) \<longleftrightarrow> (\<forall>x. norm (f x) \<le> b * norm x)"
  (is "?lhs \<longleftrightarrow> ?rhs")
proof
  assume H: ?rhs
  {
    fix x :: "'a"
    assume x: "norm x = 1"
    from H[rule_format, of x] x have "norm (f x) \<le> b"
      by simp
  }
  then show ?lhs by blast
next
  assume H: ?lhs
  have bp: "b \<ge> 0"
    apply -
    apply (rule order_trans [OF norm_ge_zero])
    apply (rule H[rule_format, of "SOME x::'a. x \<in> Basis"])
    apply (auto intro: SOME_Basis norm_Basis)
    done
  {
    fix x :: "'a"
    {
      assume "x = 0"
      then have "norm (f x) \<le> b * norm x"
        by (simp add: linear_0[OF lf] bp)
    }
    moreover
    {
      assume x0: "x \<noteq> 0"
      then have n0: "norm x \<noteq> 0"
        by (metis norm_eq_zero)
      let ?c = "1/ norm x"
      have "norm (?c *\<^sub>R x) = 1"
        using x0 by (simp add: n0)
      with H have "norm (f (?c *\<^sub>R x)) \<le> b"
        by blast
      then have "?c * norm (f x) \<le> b"
        by (simp add: linear_cmul[OF lf])
      then have "norm (f x) \<le> b * norm x"
        using n0 norm_ge_zero[of x]
        by (auto simp add: field_simps)
    }
    ultimately have "norm (f x) \<le> b * norm x"
      by blast
  }
  then show ?rhs by blast
qed

lemma onorm:
  fixes f:: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  assumes lf: "linear f"
  shows "norm (f x) \<le> onorm f * norm x"
    and "\<forall>x. norm (f x) \<le> b * norm x \<Longrightarrow> onorm f \<le> b"
proof -
  let ?S = "(\<lambda>x. norm (f x))`{x. norm x = 1}"
  have "norm (f (SOME i. i \<in> Basis)) \<in> ?S"
    by (auto intro!: exI[of _ "SOME i. i \<in> Basis"] norm_Basis SOME_Basis)
  then have Se: "?S \<noteq> {}"
    by auto
  from linear_bounded[OF lf] have b: "bdd_above ?S"
    unfolding norm_bound_generalize[OF lf, symmetric] by auto
  then show "norm (f x) \<le> onorm f * norm x"
    apply -
    apply (rule spec[where x = x])
    unfolding norm_bound_generalize[OF lf, symmetric]
    apply (auto simp: onorm_def intro!: cSUP_upper)
    done
  show "\<forall>x. norm (f x) \<le> b * norm x \<Longrightarrow> onorm f \<le> b"
    unfolding norm_bound_generalize[OF lf, symmetric]
    using Se by (auto simp: onorm_def intro!: cSUP_least b)
qed

lemma onorm_pos_le:
  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
  assumes lf: "linear f"
  shows "0 \<le> onorm f"
  using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "SOME i. i \<in> Basis"]]
  by (simp add: SOME_Basis)

lemma onorm_eq_0:
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  assumes lf: "linear f"
  shows "onorm f = 0 \<longleftrightarrow> (\<forall>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
  done

lemma onorm_const: "onorm (\<lambda>x::'a::euclidean_space. y::'b::euclidean_space) = norm y"
  using SOME_Basis by (auto simp add: onorm_def intro!: cSUP_const norm_Basis)

lemma onorm_pos_lt:
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  assumes lf: "linear f"
  shows "0 < onorm f \<longleftrightarrow> \<not> (\<forall>x. f x = 0)"
  unfolding onorm_eq_0[OF lf, symmetric]
  using onorm_pos_le[OF lf] by arith

lemma onorm_compose:
  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
    and g :: "'k::euclidean_space \<Rightarrow> 'n::euclidean_space"
  assumes lf: "linear f"
    and lg: "linear g"
  shows "onorm (f \<circ> g) \<le> 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])
    done

lemma onorm_neg_lemma:
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  assumes lf: "linear f"
  shows "onorm (\<lambda>x. - f x) \<le> onorm f"
  using onorm[OF linear_compose_neg[OF lf]] onorm[OF lf]
  unfolding norm_minus_cancel by metis

lemma onorm_neg:
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  assumes lf: "linear f"
  shows "onorm (\<lambda>x. - f x) = onorm f"
  using onorm_neg_lemma[OF lf] onorm_neg_lemma[OF linear_compose_neg[OF lf]]
  by simp

lemma onorm_triangle:
  fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
  assumes lf: "linear f"
    and lg: "linear g"
  shows "onorm (\<lambda>x. f x + g x) \<le> 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])
  done

lemma onorm_triangle_le:
  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
  assumes "linear f"
    and "linear g"
    and "onorm f + onorm g \<le> e"
  shows "onorm (\<lambda>x. f x + g x) \<le> e"
  apply (rule order_trans)
  apply (rule onorm_triangle)
  apply (rule assms)+
  done

lemma onorm_triangle_lt:
  fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
  assumes "linear f"
    and "linear g"
    and "onorm f + onorm g < e"
  shows "onorm (\<lambda>x. f x + g x) < e"
  apply (rule order_le_less_trans)
  apply (rule onorm_triangle)
  apply (rule assms)+
  done

end