# Theory FunctionNorm

Up to index of Isabelle/HOL/HOL-Complex/HahnBanach

theory FunctionNorm
imports NormedSpace FunctionOrder
begin

    (*  Title:      HOL/Real/HahnBanach/FunctionNorm.thy
        ID:         $Id: FunctionNorm.thy,v 1.36 2005/06/17 14:13:09 haftmann Exp $
        Author:     Gertrud Bauer, TU Munich
    *)

    header {* The norm of a function *}

    theory FunctionNorm imports NormedSpace FunctionOrder begin

    subsection {* Continuous linear forms*}

    text {*
      A linear form @{text f} on a normed vector space @{text "(V, \<parallel>·\<parallel>)"}
      is \emph{continuous}, iff it is bounded, i.e.
      \begin{center}
      @{text "∃c ∈ R. ∀x ∈ V. ¦f x¦ ≤ c · \<parallel>x\<parallel>"}
      \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 = var V + norm_syntax + linearform +
      assumes bounded: "∃c. ∀x ∈ V. ¦f x¦ ≤ c * \<parallel>x\<parallel>"

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

    lemma continuousI [intro]:
      includes norm_syntax + linearform
      assumes r: "!!x. x ∈ V ==> ¦f x¦ ≤ c * \<parallel>x\<parallel>"
      shows "continuous V norm f"
    proof
      show "linearform V f" .
      from r have "∃c. ∀x∈V. ¦f x¦ ≤ c * \<parallel>x\<parallel>" by blast
      then show "continuous_axioms V norm f" ..
    qed

    subsection {* The norm of a linear form *}

    text {*
      The least real number @{text c} for which holds
      \begin{center}
      @{text "∀x ∈ V. ¦f x¦ ≤ c · \<parallel>x\<parallel>"}
      \end{center}
      is called the \emph{norm} of @{text f}.

      For non-trivial vector spaces @{text "V ≠ {0}"} the norm can be
      defined as
      \begin{center}
      @{text "\<parallel>f\<parallel> = \<sup>x ≠ 0. ¦f x¦ / \<parallel>x\<parallel>"}
      \end{center}

      For the case @{text "V = {0}"} the supremum would be taken from an
      empty set. Since @{text \<real>} 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 @{text "{} ≥ 0"} so that
      @{text fn_norm} has the norm properties. Furthermore it does not
      have to change the norm in all other cases, so it must be @{text 0},
      as all other elements are @{text "{} ≥ 0"}.

      Thus we define the set @{text B} where the supremum is taken from as
      follows:
      \begin{center}
      @{text "{0} ∪ {¦f x¦ / \<parallel>x\<parallel>. x ≠ 0 ∧ x ∈ F}"}
      \end{center}

      @{text fn_norm} is equal to the supremum of @{text B}, if the
      supremum exists (otherwise it is undefined).
    *}

    locale fn_norm = norm_syntax +
      fixes B defines "B V f ≡ {0} ∪ {¦f x¦ / \<parallel>x\<parallel> | x. x ≠ 0 ∧ x ∈ V}"
      fixes fn_norm ("\<parallel>_\<parallel>_" [0, 1000] 999)
      defines "\<parallel>f\<parallel>V ≡ \<Squnion>(B V f)"

    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 @{text "(V, \<parallel>·\<parallel>)"} has a function norm.
    *}

    (* Alternative statement of the lemma as
         lemma (in fn_norm)
           includes normed_vectorspace + continuous
           shows "lub (B V f) (\<parallel>f\<parallel>V)"
       is not possible:
       fn_norm contrains parameter norm to type "'a::zero => real",
       normed_vectorspace and continuous contrain this parameter to
       "'a::{minus, plus, zero} => real, which is less general.
    *)

    lemma (in normed_vectorspace) fn_norm_works:
      includes fn_norm + continuous
      shows "lub (B V f) (\<parallel>f\<parallel>V)"
    proof -
      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 @{text B} is non-empty: *}
        have "0 ∈ B V f" ..
        thus "∃x. x ∈ B V f" ..

        txt {* Then we have to show that @{text B} is bounded: *}
        show "∃c. ∀y ∈ B V f. y ≤ c"
        proof -
          txt {* We know that @{text f} is bounded by some value @{text c}. *}
          from bounded obtain c where c: "∀x ∈ V. ¦f x¦ ≤ c * \<parallel>x\<parallel>" ..

          txt {* To prove the thesis, we have to show that there is some
            @{text b}, such that @{text "y ≤ b"} for all @{text "y ∈
            B"}. Due to the definition of @{text B} there are two cases. *}

          def 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
              assume "y = 0"
              thus ?thesis by (unfold b_def) arith
            next
              txt {* The second case is @{text "y = ¦f x¦ / \<parallel>x\<parallel>"} for some
                @{text "x ∈ V"} with @{text "x ≠ 0"}. *}
              assume "y ≠ 0"
              with y obtain x where y_rep: "y = ¦f x¦ * inverse \<parallel>x\<parallel>"
                  and x: "x ∈ V" and neq: "x ≠ 0"
                by (auto simp add: B_def real_divide_def)
              from x neq have gt: "0 < \<parallel>x\<parallel>" ..

              txt {* The thesis follows by a short calculation using the
                fact that @{text f} is bounded. *}

              note y_rep
              also have "¦f x¦ * inverse \<parallel>x\<parallel> ≤ (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
              proof (rule mult_right_mono)
                from c show "¦f x¦ ≤ c * \<parallel>x\<parallel>" ..
                from gt have "0 < inverse \<parallel>x\<parallel>"
                  by (rule positive_imp_inverse_positive)
                thus "0 ≤ inverse \<parallel>x\<parallel>" by (rule order_less_imp_le)
              qed
              also have "… = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)"
                by (rule real_mult_assoc)
              also
              from gt have "\<parallel>x\<parallel> ≠ 0" by simp
              hence "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp
              also have "c * 1 ≤ b" by (simp add: b_def le_maxI1)
              finally show "y ≤ b" .
            qed
          qed
          thus ?thesis ..
        qed
      qed
      then show ?thesis by (unfold fn_norm_def) (rule the_lubI_ex)
    qed

    lemma (in normed_vectorspace) fn_norm_ub [iff?]:
      includes fn_norm + continuous
      assumes b: "b ∈ B V f"
      shows "b ≤ \<parallel>f\<parallel>V"
    proof -
      have "lub (B V f) (\<parallel>f\<parallel>V)"
        by (unfold B_def fn_norm_def) (rule fn_norm_works [OF continuous.intro])
      from this and b show ?thesis ..
    qed

    lemma (in normed_vectorspace) fn_norm_leastB:
      includes fn_norm + continuous
      assumes b: "!!b. b ∈ B V f ==> b ≤ y"
      shows "\<parallel>f\<parallel>V ≤ y"
    proof -
      have "lub (B V f) (\<parallel>f\<parallel>V)"
        by (unfold B_def fn_norm_def) (rule fn_norm_works [OF continuous.intro])
      from this and b show ?thesis ..
    qed

    text {* The norm of a continuous function is always @{text "≥ 0"}. *}

    lemma (in normed_vectorspace) fn_norm_ge_zero [iff]:
      includes fn_norm + continuous
      shows "0 ≤ \<parallel>f\<parallel>V"
    proof -
      txt {* The function norm is defined as the supremum of @{text B}.
        So it is @{text "≥ 0"} if all elements in @{text B} are @{text "≥
        0"}, provided the supremum exists and @{text B} is not empty. *}
      have "lub (B V f) (\<parallel>f\<parallel>V)"
        by (unfold B_def fn_norm_def) (rule fn_norm_works [OF continuous.intro])
      moreover have "0 ∈ B V f" ..
      ultimately show ?thesis ..
    qed

    text {*
      \medskip The fundamental property of function norms is:
      \begin{center}
      @{text "¦f x¦ ≤ \<parallel>f\<parallel> · \<parallel>x\<parallel>"}
      \end{center}
    *}

    lemma (in normed_vectorspace) fn_norm_le_cong:
      includes fn_norm + continuous + linearform
      assumes x: "x ∈ V"
      shows "¦f x¦ ≤ \<parallel>f\<parallel>V * \<parallel>x\<parallel>"
    proof cases
      assume "x = 0"
      then have "¦f x¦ = ¦f 0¦" by simp
      also have "f 0 = 0" ..
      also have "¦…¦ = 0" by simp
      also have a: "0 ≤ \<parallel>f\<parallel>V"
          by (unfold B_def fn_norm_def)
            (rule fn_norm_ge_zero [OF continuous.intro])
        have "0 ≤ norm x" ..
      with a have "0 ≤ \<parallel>f\<parallel>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff)
      finally show "¦f x¦ ≤ \<parallel>f\<parallel>V * \<parallel>x\<parallel>" .
    next
      assume "x ≠ 0"
      with x have neq: "\<parallel>x\<parallel> ≠ 0" by simp
      then have "¦f x¦ = (¦f x¦ * inverse \<parallel>x\<parallel>) * \<parallel>x\<parallel>" by simp
      also have "… ≤  \<parallel>f\<parallel>V * \<parallel>x\<parallel>"
      proof (rule mult_right_mono)
        from x show "0 ≤ \<parallel>x\<parallel>" ..
        from x and neq have "¦f x¦ * inverse \<parallel>x\<parallel> ∈ B V f"
          by (auto simp add: B_def real_divide_def)
        then show "¦f x¦ * inverse \<parallel>x\<parallel> ≤ \<parallel>f\<parallel>V"
          by (unfold B_def fn_norm_def) (rule fn_norm_ub [OF continuous.intro])
      qed
      finally show ?thesis .
    qed

    text {*
      \medskip The function norm is the least positive real number for
      which the following inequation holds:
      \begin{center}
        @{text "¦f x¦ ≤ c · \<parallel>x\<parallel>"}
      \end{center}
    *}

    lemma (in normed_vectorspace) fn_norm_least [intro?]:
      includes fn_norm + continuous
      assumes ineq: "∀x ∈ V. ¦f x¦ ≤ c * \<parallel>x\<parallel>" and ge: "0 ≤ c"
      shows "\<parallel>f\<parallel>V ≤ c"
    proof (rule fn_norm_leastB [folded B_def fn_norm_def])
      fix b assume b: "b ∈ B V f"
      show "b ≤ c"
      proof cases
        assume "b = 0"
        with ge show ?thesis by simp
      next
        assume "b ≠ 0"
        with b obtain x where b_rep: "b = ¦f x¦ * inverse \<parallel>x\<parallel>"
            and x_neq: "x ≠ 0" and x: "x ∈ V"
          by (auto simp add: B_def real_divide_def)
        note b_rep
        also have "¦f x¦ * inverse \<parallel>x\<parallel> ≤ (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
        proof (rule mult_right_mono)
          have "0 < \<parallel>x\<parallel>" ..
          then show "0 ≤ inverse \<parallel>x\<parallel>" by simp
          from ineq and x show "¦f x¦ ≤ c * \<parallel>x\<parallel>" ..
        qed
        also have "… = c"
        proof -
          from x_neq and x have "\<parallel>x\<parallel> ≠ 0" by simp
          then show ?thesis by simp
        qed
        finally show ?thesis .
      qed
    qed (simp_all! add: continuous_def)

    end

### Continuous linear forms

lemma continuousI:

      [| linearform V f; !!x. x ∈ V ==> ¦f x¦ ≤ c * norm x |] ==> continuous V norm f

### The norm of a linear form

lemma B_not_empty:

      0 ∈ {0} ∪ {¦f x¦ / norm x |x. x ≠ (0::'a) ∧ x ∈ V}

lemma fn_norm_works:

      [| normed_vectorspace V norm; continuous V norm f |]
      ==> lub ({0} ∪ {¦f x¦ / norm x |x. x ≠ (0::'a) ∧ x ∈ V})
           (the_lub ({0} ∪ {¦f x¦ / norm x |x. x ≠ (0::'a) ∧ x ∈ V}))

lemma fn_norm_ub:

      [| normed_vectorspace V norm; continuous V norm f;
         b ∈ {0} ∪ {¦f x¦ / norm x |x. x ≠ (0::'a) ∧ x ∈ V} |]
      ==> b ≤ the_lub ({0} ∪ {¦f x¦ / norm x |x. x ≠ (0::'a) ∧ x ∈ V})

lemma fn_norm_leastB:

      [| normed_vectorspace V norm; continuous V norm f;
         !!b. b ∈ {0} ∪ {¦f x¦ / norm x |x. x ≠ (0::'a) ∧ x ∈ V} ==> b ≤ y |]
      ==> the_lub ({0} ∪ {¦f x¦ / norm x |x. x ≠ (0::'a) ∧ x ∈ V}) ≤ y

lemma fn_norm_ge_zero:

      [| normed_vectorspace V norm; continuous V norm f |]
      ==> 0 ≤ the_lub ({0} ∪ {¦f x¦ / norm x |x. x ≠ (0::'a) ∧ x ∈ V})

lemma fn_norm_le_cong:

      [| normed_vectorspace V norm; continuous V norm f; x ∈ V |]
      ==> ¦f x¦ ≤ the_lub ({0} ∪ {¦f x¦ / norm x |x. x ≠ (0::'a) ∧ x ∈ V}) * norm x

lemma fn_norm_least:

      [| normed_vectorspace V norm; continuous V norm f; ∀x∈V. ¦f x¦ ≤ c * norm x;
         0 ≤ c |]
      ==> the_lub ({0} ∪ {¦f x¦ / norm x |x. x ≠ (0::'a) ∧ x ∈ V}) ≤ c