Theory Function_Norm
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∥ = \<sup>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
assume "y = 0"
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›.›
assume "y ≠ 0"
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 [iff?]:
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›, provided the supremum exists and ‹B› is not empty.›
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
assume "x = 0"
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
assume "x ≠ 0"
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
assume "b = 0"
with ge show ?thesis by simp
next
assume "b ≠ 0"
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 (insert ‹continuous V f norm›, simp_all add: continuous_def)
qed
end