Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/Analysis/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 8 kB

Quelle Operator_Norm.thy Sprache: Isabelle

(*  Title:      HOL/Analysis/Operator_Norm.thy
    Author:     Amine Chaieb, University of Cambridge
    Author:     Brian Huffman
*)

section \<open>Operator Norm\<close>

theory Operator_Norm
imports Complex_Main
begin

text \<open>This formulation yields zero if \<open>'a\<close> is the trivial vector space.\<close>

text\<^marker>\<open>tag important\<close> \<open>%whitespace\<close>
definition\<^marker>\<open>tag important\<close>
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 \<open>In non-trivial vector spaces, the first assumption is redundant.\<close>

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 \<open>a \<noteq> 0\<close> show "0 \<le> 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 \<open>x \<noteq> 0\<close>)
  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 *\<^sub>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 *\<^sub>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 *\<^sub>R f x) = \r\ * onorm f"
proof (cases "r = 0")
  assume "r \ 0"
  show ?thesis
  proof (rule order_antisym)
    show "onorm (\x. r *\<^sub>R f x) \ \r\ * onorm f"
      using f by (rule onorm_scaleR_lemma)
  next
    have "bounded_linear (\x. r *\<^sub>R f x)"
      using bounded_linear_scaleR_right f by (rule bounded_linear_compose)
    then have "onorm (\x. inverse r *\<^sub>R r *\<^sub>R f x) \ \inverse r\ * onorm (\x. r *\<^sub>R f x)"
      by (rule onorm_scaleR_lemma)
    with \<open>r \<noteq> 0\<close> show "\<bar>r\<bar> * onorm f \<le> onorm (\<lambda>x. r *\<^sub>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 *\<^sub>R f) \ onorm r * norm f"
proof (rule onorm_bound)
  fix x
  have "norm (r x *\<^sub>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 *\<^sub>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 *\<^sub>R f) = onorm r * norm f"
proof (cases "f = 0")
  assume "f \ 0"
  show ?thesis
  proof (rule order_antisym)
    show "onorm (\x. r x *\<^sub>R f) \ onorm r * norm f"
      using f by (rule onorm_scaleR_left_lemma)
  next
    have bl1: "bounded_linear (\x. r x *\<^sub>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 \<open>f \<noteq> 0\<close>
      by (simp add: inverse_eq_divide)
    also have "onorm (\x. r x * norm f) \ onorm (\x. r x *\<^sub>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 *\<^sub>R f)"
      using \<open>f \<noteq> 0\<close>
      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

quality100%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.