Theory Extra_Operator_Norm

section Extra_Operator_Norm› -- Additional facts bout the operator norm›

theory Extra_Operator_Norm
  imports "HOL-Analysis.Operator_Norm"
    Extra_General
    "HOL-Analysis.Bounded_Linear_Function"
    Extra_Vector_Spaces
begin


text ‹This theorem complements theoryHOL-Analysis.Operator_Norm
      additional useful facts about operator norms.›

lemma onorm_sphere:
  fixes f :: "'a::{real_normed_vector, not_singleton}  'b::real_normed_vector"
  assumes a1: "bounded_linear f"
  shows onorm f = Sup {norm (f x) | x. norm x = 1}
proof(cases f = (λ _. 0))
  case True
  have (UNIV::'a set)  {0}
    by simp
  hence x::'a. norm x = 1
    using  ex_norm1
    by blast
  have norm (f x) = 0
    for x
    by (simp add: True)
  hence {norm (f x) | x. norm x = 1} = {0}
    using x. norm x = 1 by auto
  hence v1: Sup {norm (f x) | x. norm x = 1} = 0
    by simp
  have onorm f = 0
    by (simp add: True onorm_eq_0)
  thus ?thesis using v1 by simp
next
  case False
  have y  {norm (f x) |x. norm x = 1}  {0}
    if "y  {norm (f x) / norm x |x. True}"
    for y
  proof(cases y = 0)
    case True
    thus ?thesis
      by simp
  next
    case False
    have  x. y = norm (f x) / norm x
      using y  {norm (f x) / norm x |x. True} by auto
    then obtain x where y = norm (f x) / norm x
      by blast
    hence y = ¦(1/norm x)¦ * norm ( f x )
      by simp
    hence y = norm ( (1/norm x) *R f x )
      by simp
    hence y = norm ( f ((1/norm x) *R x) )
      apply (subst linear_cmul[of f])
      by (simp_all add: assms bounded_linear.linear)
    moreover have norm ((1/norm x) *R x) = 1
      using False y = norm (f x) / norm x by auto
    ultimately have y  {norm (f x) |x. norm x = 1}
      by blast
    thus ?thesis by blast
  qed
  moreover have "y  {norm (f x) / norm x |x. True}"
    if y  {norm (f x) |x. norm x = 1}  {0}
    for y
  proof(cases y = 0)
    case True
    thus ?thesis
      by auto
  next
    case False
    hence y  {0}
      by simp
    hence y  {norm (f x) |x. norm x = 1}
      using that by auto
    hence  x. norm x = 1  y = norm (f x)
      by auto
    then obtain x where norm x = 1 and y = norm (f x)
      by auto
    have y = norm (f x) / norm x using  norm x = 1  y = norm (f x)
      by simp
    thus ?thesis
      by auto
  qed
  ultimately have {norm (f x) / norm x |x. True} = {norm (f x) |x. norm x = 1}  {0}
    by blast
  hence Sup {norm (f x) / norm x |x. True} = Sup ({norm (f x) |x. norm x = 1}  {0})
    by simp
  moreover have Sup {norm (f x) |x. norm x = 1}  0
  proof-
    have  x::'a. norm x = 1
      by (metis (full_types) False assms linear_simps(3) norm_sgn)
    then obtain x::'a where norm x = 1
      by blast
    have norm (f x)  0
      by simp
    hence  x::'a. norm x = 1  norm (f x)  0
      using norm x = 1 by blast
    hence  y  {norm (f x) |x. norm x = 1}. y  0
      by blast
    then obtain y::real where y  {norm (f x) |x. norm x = 1}
      and y  0
      by auto
    have {norm (f x) |x. norm x = 1}  {}
      using y  {norm (f x) |x. norm x = 1} by blast
    moreover have bdd_above {norm (f x) |x. norm x = 1}
      using bdd_above_norm_f
      by (metis (mono_tags, lifting) a1)
    ultimately have y  Sup {norm (f x) |x. norm x = 1}
      using y  {norm (f x) |x. norm x = 1}
      by (simp add: cSup_upper)
    thus ?thesis using y  0 by simp
  qed
  moreover have Sup ({norm (f x) |x. norm x = 1}  {0}) = Sup {norm (f x) |x. norm x = 1}
  proof-
    have {norm (f x) |x. norm x = 1}  {}
      by (simp add: assms(1) ex_norm1)
    moreover have bdd_above {norm (f x) |x. norm x = 1}
      using a1 bdd_above_norm_f by force
    have {0::real}  {}
      by simp
    moreover have bdd_above {0::real}
      by simp
    ultimately have Sup ({norm (f x) |x. norm x = 1}  {(0::real)})
             = max (Sup {norm (f x) |x. norm x = 1}) (Sup {0::real})
      by (metis (lifting) 0  Sup {norm (f x) |x. norm x = 1} bdd_above {0} bdd_above {norm (f x) |x. norm x = 1} {0}  {} {norm (f x) |x. norm x = 1}  {} cSup_singleton cSup_union_distrib max.absorb_iff1 sup.absorb_iff1)
    moreover have Sup {(0::real)} = (0::real)
      by simp
    moreover have Sup {norm (f x) |x. norm x = 1}  0
      by (simp add: 0  Sup {norm (f x) |x. norm x = 1})
    ultimately show ?thesis
      by simp
  qed
  moreover have Sup ( {norm (f x) |x. norm x = 1}  {0})
           = max (Sup {norm (f x) |x. norm x = 1}) (Sup {0})
    using calculation(2) calculation(3) by auto
  ultimately have w1: "Sup {norm (f x) / norm x | x. True} = Sup {norm (f x) | x. norm x = 1}"
    by simp

  have (SUP x. norm (f x) / (norm x)) = Sup {norm (f x) / norm x | x. True}
    by (simp add: full_SetCompr_eq)
  also have ... = Sup {norm (f x) | x. norm x = 1}
    using w1 by auto
  ultimately  have (SUP x. norm (f x) / (norm x)) = Sup {norm (f x) | x. norm x = 1}
    by linarith
  thus ?thesis unfolding onorm_def by blast
qed

lemma onormI:
  assumes "x. norm (f x)  b * norm x"
    and "x  0" and "norm (f x) = b * norm x"
  shows "onorm f = b"
  apply (unfold onorm_def, rule cSup_eq_maximum)
   apply (smt (verit) UNIV_I assms(2) assms(3) image_iff nonzero_mult_div_cancel_right norm_eq_zero)
  by (smt (verit, del_insts) assms(1) assms(2) divide_nonneg_nonpos norm_ge_zero norm_le_zero_iff pos_divide_le_eq rangeE zero_le_mult_iff)

end