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