Theory HOL-Analysis.Operator_Norm

(*  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.›

texttag important› ‹%whitespace›
definitiontag 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