Quelle  Function_Norm.thy

(*  Title:      HOL/Hahn_Banach/Function_Norm.thy
  Author: Gertrud Bauer, TU Munich
*)

section ‹The norm of a function›

theory Function_Norm
imports Normed_Space Function_Order
begin

subsection ‹Continuous linear forms›

text ‹
  A linear form ‹f› on a normed vector space ‹(V, ∥⋅∥)› is 🪙‹continuous›, iff
  it is bounded, i.e.
  \begin{center}
  ‹∃c ∈ R. ∀x ∈ V. ∣f x∣ ≤ c ⋅ ∥x∥›
  \end{center}
  In our application no other functions than linear forms are considered, so
  we can define continuous linear forms as bounded linear forms:
 ›

locale continuous = linearform +
  fixes norm :: "_ ==> real"    (‹∥_∥›)
  assumes bounded: "∃c. ∀x ∈ V. ∣f x∣ ≤ c * ∥x∥"

declare continuous.intro [intro?] continuous_axioms.intro [intro?]

lemma continuousI [intro]:
  fixes norm :: "_ ==> real"  (‹∥_∥›)
  assumes "linearform V f"
  assumes r: "∧x. x ∈ V ==> ∣f x∣ ≤ c * ∥x∥"
  shows "continuous V f norm"
proof
  show "linearform V f" by fact
  from r have "∃c. ∀x∈V. ∣f x∣ ≤ c * ∥x∥" by blast
  then show "continuous_axioms V f norm" ..
qed


subsection ‹The norm of a linear form›

text ‹
  The least real number ‹c› for which holds
  \begin{center}
  ‹∀x ∈ V. ∣f x∣ ≤ c ⋅ ∥x∥›
  \end{center}
  is called the 🪙‹norm› of ‹f›.
 
  For non-trivial vector spaces ‹V ≠ {0}› the norm can be defined as
  \begin{center}
  ‹∥f∥ = 🪙x ≠ 0. ∣f x∣ / ∥x∥›
  \end{center}
 
  For the case ‹V = {0}› the supremum would be taken from an empty set. Since
  ‹ℝ› is unbounded, there would be no supremum. To avoid this situation it
  must be guaranteed that there is an element in this set. This element must
  be ‹{} ≥ 0› so that ‹fn_norm› has the norm properties. Furthermore it does
  not have to change the norm in all other cases, so it must be ‹0›, as all
  other elements are ‹{} ≥ 0›.
 
  Thus we define the set ‹B› where the supremum is taken from as follows:
  \begin{center}
  ‹{0} ∪ {∣f x∣ / ∥x∥. x ≠ 0 ∧ x ∈ F}›
  \end{center}
 
  ‹fn_norm› is equal to the supremum of ‹B›, if the supremum exists (otherwise
  it is undefined).
 ›

locale fn_norm =
  fixes norm :: "_ ==> real"    (‹∥_∥›)
  fixes B defines "B V f ≡ {0} ∪ {∣f x∣ / ∥x∥ | x. x ≠ 0 ∧ x ∈ V}"
  fixes fn_norm (‹∥_∥🍋_› [0, 1000] 999)
  defines "∥f∥🍋V ≡ ⊔(B V f)"

locale normed_vectorspace_with_fn_norm = normed_vectorspace + fn_norm

lemma (in fn_norm) B_not_empty [intro]: "0 ∈ B V f"
  by (simp add: B_def)

text ‹
  The following lemma states that every continuous linear form on a normed
  space ‹(V, ∥⋅∥)› has a function norm.
 ›

lemma (in normed_vectorspace_with_fn_norm) fn_norm_works:
  assumes "continuous V f norm"
  shows "lub (B V f) (∥f∥🍋V)"
proof -
  interpret continuous V f norm by fact
  txt ‹The existence of the supremum is shown using the
  completeness of the reals. Completeness means, that every
  non-empty bounded set of reals has a supremum.›
  have "∃a. lub (B V f) a"
  proof (rule real_complete)
    txt ‹First we have to show that ‹B› is non-empty:›
    have "0 ∈ B V f" ..
    then show "∃x. x ∈ B V f" ..

    txt ‹Then we have to show that ‹B› is bounded:›
    show "∃c. ∀y ∈ B V f. y ≤ c"
    proof -
      txt ‹We know that ‹f› is bounded by some value ‹c›.›
      from bounded obtain c where c: "∀x ∈ V. ∣f x∣ ≤ c * ∥x∥" ..

      txt ‹To prove the thesis, we have to show that there is some ‹b›, such
  that ‹y ≤ b› for all ‹y ∈ B›. Due to the definition of ‹B› there are
  two cases.›

      define b where "b = max c 0"
      have "∀y ∈ B V f. y ≤ b"
      proof
        fix y assume y: "y ∈ B V f"
        show "y ≤ b"
        proof (cases "y = 0")
          case True
          then show ?thesis unfolding b_def by arith
        next
          txt ‹The second case is ‹y = ∣f x∣ / ∥x∥› for some
  ‹x ∈ V› with ‹x ≠ 0›.›
          case False
          with y obtain x where y_rep: "y = ∣f x∣ * inverse ∥x∥"
              and x: "x ∈ V" and neq: "x ≠ 0"
            by (auto simp add: B_def divide_inverse)
          from x neq have gt: "0 < ∥x∥" ..

          txt ‹The thesis follows by a short calculation using the
  fact that ‹f› is bounded.›

          note y_rep
          also have "∣f x∣ * inverse ∥x∥ ≤ (c * ∥x∥) * inverse ∥x∥"
          proof (rule mult_right_mono)
            from c x show "∣f x∣ ≤ c * ∥x∥" ..
            from gt have "0 < inverse ∥x∥"
              by (rule positive_imp_inverse_positive)
            then show "0 ≤ inverse ∥x∥" by (rule order_less_imp_le)
          qed
          also have "… = c * (∥x∥ * inverse ∥x∥)"
            by (rule Groups.mult.assoc)
          also
          from gt have "∥x∥ ≠ 0" by simp
          then have "∥x∥ * inverse ∥x∥ = 1" by simp
          also have "c * 1 ≤ b" by (simp add: b_def)
          finally show "y ≤ b" .
        qed
      qed
      then show ?thesis ..
    qed
  qed
  then show ?thesis unfolding fn_norm_def by (rule the_lubI_ex)
qed

lemma (in normed_vectorspace_with_fn_norm) fn_norm_ub [intro?]:
  assumes "continuous V f norm"
  assumes b: "b ∈ B V f"
  shows "b ≤ ∥f∥🍋V"
proof -
  interpret continuous V f norm by fact
  have "lub (B V f) (∥f∥🍋V)"
    using ‹continuous V f norm› by (rule fn_norm_works)
  from this and b show ?thesis ..
qed

lemma (in normed_vectorspace_with_fn_norm) fn_norm_leastB:
  assumes "continuous V f norm"
  assumes b: "∧b. b ∈ B V f ==> b ≤ y"
  shows "∥f∥🍋V ≤ y"
proof -
  interpret continuous V f norm by fact
  have "lub (B V f) (∥f∥🍋V)"
    using ‹continuous V f norm› by (rule fn_norm_works)
  from this and b show ?thesis ..
qed

text ‹The norm of a continuous function is always ‹≥ 0›.›

lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]:
  assumes "continuous V f norm"
  shows "0 ≤ ∥f∥🍋V"
proof -
  interpret continuous V f norm by fact
  txt ‹The function norm is defined as the supremum of ‹B›.
  So it is ‹≥ 0› if all elements in ‹B› are ‹≥
  0›,
  have "lub (B V f) (∥f∥🍋V)"
  using ‹continuous V f norm› by (rule fn_norm_works)
  moreover have "0 ∈ B V f" ..
  ultimately show ?thesis ..
 qed
 
 text ‹
  🪙
  The fundamental property of function norms is:
  \begin{center}
  ‹∣f x∣ ≤ ∥f∥ ⋅ ∥x∥›
  \end{center}
 ›
 
 lemma (in normed_vectorspace_with_fn_norm) fn_norm_le_cong:
  assumes "continuous V f norm" "linearform V f"
  assumes x: "x ∈ V"
  shows "∣f x∣ ≤ ∥f∥🍋V * ∥x∥"
 proof -
  interpret continuous V f norm by fact
  interpret linearform V f by fact
  show ?thesis
  proof (cases "x = 0")
  case True
  then have "∣f x∣ = ∣f 0∣" by simp
  also have "f 0 = 0" by rule unfold_locales
  also have "∣…∣ = 0" by simp
  also have a: "0 ≤ ∥f∥🍋V"
  using ‹continuous V f norm› by (rule fn_norm_ge_zero)
  from x have "0 ≤ norm x" ..
  with a have "0 ≤ ∥f∥🍋V * ∥x∥" by (simp add: zero_le_mult_iff)
  finally show "∣f x∣ ≤ ∥f∥🍋V * ∥x∥" .
  next
  case False
  with x have neq: "∥x∥ ≠ 0" by simp
  then have "∣f x∣ = (∣f x∣ * inverse ∥x∥) * ∥x∥" by simp
  also have "… ≤ ∥f∥🍋V * ∥x∥"
  proof (rule mult_right_mono)
  from x show "0 ≤ ∥x∥" ..
  from x and neq have "∣f x∣ * inverse ∥x∥ ∈ B V f"
  by (auto simp add: B_def divide_inverse)
  with ‹continuous V f norm› show "∣f x∣ * inverse ∥x∥ ≤ ∥f∥🍋V"
  by (rule fn_norm_ub)
  qed
  finally show ?thesis .
  qed
 qed
 
 text ‹
  🪙
  The function norm is the least positive real number for which the
  following inequality holds:
  \begin{center}
  ‹∣f x∣ ≤ c ⋅ ∥x∥›
  \end{center}
 ›
 
 lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]:
  assumes "continuous V f norm"
  assumes ineq: "∧x. x ∈ V ==> ∣f x∣ ≤ c * ∥x∥" and ge: "0 ≤ c"
  shows "∥f∥🍋V ≤ c"
 proof -
  interpret continuous V f norm by fact
  show ?thesis
  proof (rule fn_norm_leastB [folded B_def fn_norm_def])
  fix b assume b: "b ∈ B V f"
  show "b ≤ c"
  proof (cases "b = 0")
  case True
  with ge show ?thesis by simp
  next
  case False
  with b obtain x where b_rep: "b = ∣f x∣ * inverse ∥x∥"
  and x_neq: "x ≠ 0" and x: "x ∈ V"
  by (auto simp add: B_def divide_inverse)
  note b_rep
  also have "∣f x∣ * inverse ∥x∥ ≤ (c * ∥x∥) * inverse ∥x∥"
  proof (rule mult_right_mono)
  have "0 🚫∥x∥" using x x_neq ..
  then show "0 ≤ inverse ∥x∥" by simp
  from x show "∣f x∣ ≤ c * ∥x∥" by (rule ineq)
  qed
  also have "… = c"
  proof -
  from x_neq and x have "∥x∥ ≠ 0" by simp
  then show ?thesis by simp
  qed
  finally show ?thesis .
  qed
  qed (use ‹continuous V f norm› in ‹simp_all add: continuous_def›)
 qed
 
 end