Commit dd33ba7b authored by Michael Kohlhase's avatar Michael Kohlhase

adding inner product spaces and vievws

parent c3144597
\begin{mhmodnl}[creators=miko]{inner-product-space}{en}
\begin{definition}
Let $F$ be the \trefi[field]{field} of \atrefii[realnumbers]{real}{real}{number} or
\trefiis[complexnumbers]{complex}{numbers}, $V$ a \trefii[vector-space]{vector}{space}
over $F$, and $\fun\innerproductOp{V,V}F$ a function with
\begin{enumerate}
\item $\innerproduct{x}y=\compconjugate{\innerproduct{y}x}$
(\defii{conjugate}{symmetry})
\item $\innerproduct{\smul{a}x}y=\comptimes{a{\innerproduct{x}y}}$ and
$\innerproduct{\vadd{x,y}}z=\vadd{\innerproduct{x}z,\innerproduct{y}z}$
(\mtrefi[linear-map?linear]{linearity} in the first argument)
\item $\realmethan{\innerproduct{x}x}0$ and $\eq{\innerproduct{x}x,0}$ iff $x=0$,
(\defii{positive}{definiteness}),
\end{enumerate}
then $\mvstructure{V,\innerproductOp}$ is called an \defiii{inner}{product}{space}
\end{definition}
\end{mhmodnl}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
\begin{modsig}[creators=miko]{inner-product-space}
\gimport[smglom/arithmetics]{comparith}
\gimport[smglom/linear-algebra]{linear-map}
\symdef[name=inner-product]{innerproduct}[2]{\mixfixii[nobrackets]\langle{#1},{#2}\rangle}
\symdef[name=inner-product]{innerproductOp}{\innerproduct\cdot\cdot}
\symtest{innerproduct}{\innerproduct{x}y}
\end{modsig}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
\begin{mhmodnl}[creators=miko]{innerproduct-induced-norm}{en}
\begin{definition}
\inlineass[type=obligation,id=obl.norm-metric.en]{Let $\mvstructure{V,\innerproductOp}$
be a \trefiii[inner-product-space]{inner}{product}{space}, then
$\fundefeq{x}{\anorm{x}}{\compsqrt{\innerproduct{x}x}}$ is a \trefi[norm]{norm}.} It
is called the \adefii{norm induced}{induced}{norm} by $\innerproductOp$.
\end{definition}
\end{mhmodnl}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
\begin{modsig}[creators=miko]{innerproduct-induced-norm}
\gimport*{inner-product-space}
\gimport{norm}
\symii{induced}{norm}
\end{modsig}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
\begin{gviewnl}[creators=miko]{innerproduct-norm}{en}
{norm}{innerproduct-induced-norm}
Given a \trefiii[inner-product-space]{inner}{product}{space} with base set $V$ and
\trefii[innerproduct-induced-norm]{induced}{norm} $\anormOp$, then
$\mvstructure{V,\anormOp}$ is a \trefiii[norm]{normed}{vector}{space}.
\end{gviewnl}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
% LocalWords: gve miko defeq trefii sproof spfstep
\begin{gviewsig}[creators=miko]{innerproduct-norm}{norm}{innerproduct-induced-norm}
\tassign{base-set}{base-set}
\tassign{norm}{induced-norm}
\end{gviewsig}
\hypernym[by=norm-metric]{normed-vector-space}{inner-product-space}
\hypernym[by=norm-metric]{norm}{inner-product}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment