(*  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 (‹∥_∥&hyphen_› [0, 1000] 999)
  defines "∥f∥&hyphenV ≡ ⊔(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∥&hyphenV)"
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∥&hyphenV"
proof -
  interpret continuous V f norm by fact
  have "lub (B V f) (∥f∥&hyphenV)"
    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∥&hyphenV ≤ y"
proof -
  interpret continuous V f norm by fact
  have "lub (B V f) (∥f∥&hyphenV)"
    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∥&hyphenV"
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›, provided the supremum exists and ‹B› is not empty.›
  have "lub (B V f) (∥f∥&hyphenV)"
    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∥&hyphenV * ∥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∥&hyphenV"
      using ‹continuous V f norm› by (rule fn_norm_ge_zero)
    from x have "0 ≤ norm x" ..
    with a have "0 ≤ ∥f∥&hyphenV * ∥x∥" by (simp add: zero_le_mult_iff)
    finally show "∣f x∣ ≤ ∥f∥&hyphenV * ∥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∥&hyphenV * ∥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∥&hyphenV"
        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∥&hyphenV ≤ 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