# 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›

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
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›
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])
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}›
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} ≠ {}›
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}›
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
```