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 \<^theory>‹HOL-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