A copy of this issue can also be found on the
MetaPress server (with DOI names of articles).
Karol P\k{a}k.
Eigenvalues of a Linear Transformation,
Formalized Mathematics 16(4),
pages 289-295, 2008. MML Identifier:
VECTSP11 Summary:
The article presents well known facts about eigenvalues of
linear transformation of a vector space (see
\cite{HerstenWinter}).
I formalize main dependencies between eigenvalues and the diagram of
the matrix of a linear transformation over a finite-dimensional
vector space. Finally, I formalize the
subspace $\displaystyle\bigcup_{i=0}^\infty {\rm Ker}(f-\lambda I)^i$
called a generalized eigenspace for the eigenvalue $\lambda$ and
show its basic properties.
Karol P\k{a}k.
Jordan Matrix Decomposition,
Formalized Mathematics 16(4),
pages 297-303, 2008. MML Identifier:
MATRIXJ2 Summary:
In this paper I present the Jordan Matrix Decomposition Theorem
which states that an arbitrary square matrix $M$ over an algebraically
closed field can be decomposed into the
form $$M=SJS^{-1}$$ where $S$ is an invertible matrix
and $J$ is a matrix in a Jordan canonical form, i.e. a special
type of block diagonal matrix in which each block consists of
Jordan blocks (see \cite{GolubWilkinson}).
Noboru Endou, Keiko Narita, Yasunari Shidama.
Fatou's Lemma and the {L}ebesgue's Convergence Theorem,
Formalized Mathematics 16(4),
pages 305-309, 2008. MML Identifier:
MESFUN10 Summary:
In this article we prove the Fatou's Lemma and Lebesgue's Convergence Theorem
\cite{Halmos74}.
Masahiko Yamazaki, Hiroshi Yamazaki, Yasunari Shidama.
Extended {R}iemann Integral of Functions
of Real Variable and One-sided {L}aplace Transform,
Formalized Mathematics 16(4),
pages 311-317, 2008. MML Identifier:
INTEGR10 Summary:
In this article, we defined a variety of extended Riemann integrals
and proved that such integration is linear. Furthermore, we defined
the one-sided Laplace transform and proved the linearity of that operator.
Keiko Narita, Noboru Endou, Yasunari Shidama.
Integral of Complex-Valued Measurable Function,
Formalized Mathematics 16(4),
pages 319-324, 2008. MML Identifier:
MESFUN6C Summary:
In this article, we formalized the notion of the integral of a
complex-valued function considered as a sum of its real and
imaginary parts. Then we defined the measurability and integrability
in this context, and proved the linearity and several other basic
properties of complex-valued measurable functions. The set of
properties showed in this paper is based on
\cite{MESFUNC6.ABS},
where the case of real-valued measurable functions is considered.
Grzegorz Bancerek, Yasunari Shidama.
Introduction to Matroids,
Formalized Mathematics 16(4),
pages 325-332, 2008. MML Identifier:
MATROID0 Summary:
The paper includes elements of the theory of matroids
\cite{Welsh:1976}.
The formalization is done according to
\cite{Lipski}.
Bing Xie, Xiquan Liang, Hongwei Li.
Partial Differentiation of Real Binary Functions,
Formalized Mathematics 16(4),
pages 333-338, 2008. MML Identifier:
PDIFF_2 Summary:
In this article, we define two single-variable functions SVF1 and SVF2,
then discuss partial differentiation of real binary functions by
dint of one variable function SVF1 and SVF2. The main properties of
partial differentiation are shown
\cite{PDIFF_1.ABS}.
Kazuhisa Ishida, Yasunari Shidama.
Model Checking. {P}art {III},
Formalized Mathematics 16(4),
pages 339-353, 2008. MML Identifier:
MODELC_3 Summary:
This text includes verification of the basic algorithm in Simple
On-the-fly Automatic Verification of Linear Temporal Logic (LTL).
LTL formula can be transformed to Buchi automaton, and this
transforming algorithm is mainly used at Simple On-the-fly Automatic
Verification. In this article, we verified the transforming algorithm
itself. At first, we prepared some definitions and operations for transforming.
And then, we defined the Buchi automaton and verified the transforming algorithm.
Xiaopeng Yue, Xiquan Liang.
Basic Properties of Circulant Matrices
and Anti-Circular Matrices,
Formalized Mathematics 16(4),
pages 355-360, 2008. MML Identifier:
MATRIX16 Summary:
This article introduces definitions of circulant matrices,
line- and column-circulant matrices as well as anti-circular
matrices and describes their main properties.
Yasushige Watase, Noboru Endou, Yasunari Shidama.
On ${L}^1$ Space Formed by
Real-Valued Partial Functions,
Formalized Mathematics 16(4),
pages 361-369, 2008. MML Identifier:
LPSPACE1 Summary:
This article contains some definitions and properties refering
to function spaces formed by partial functions defined over a
measurable space. We formalized a function space, the so-called $L^1$
space and proved that the space turns out to be a normed space.
The formalization of a real function space was given in
\cite{FUNCSDOM.ABS}.
The set of all function forms additive group. Here addition is defined by
point-wise addition of two functions. However it is not true for partial
functions. The set of partial functions does not form an additive group
due to lack of right zeroed condition. Therefore, firstly we introduced
a kind of a quasi-linear space, then, we introduced the definition of an
equivalent relation of two functions which are almost everywhere
equal ($=_{\rm a.e.}$), thirdly we formalized a linear space by taking
the quotient of a quasi-linear space by the relation ($=_{\rm a.e.}$).
Yuzhong Ding, Fuguo Ge, Chenglong Wu.
{BCI}-homomorphisms,
Formalized Mathematics 16(4),
pages 371-376, 2008. MML Identifier:
BCIALG_6 Summary:
In this article the notion of the power of an element of BCI-algebra
and its period in the book
\cite{BCIAlgebras},
sections 1.4 to 1.5
are firstly given. Then the definition of BCI-homomorphism is defined
and the fundamental theorem of homomorphism, the first isomorphism
theorem and the second isomorphism theorem are proved following the
book \cite{BCIAlgebras2},
section 1.6.
Katsumi Wasaki.
Stability of the 4-2 Binary Addition
Circuit Cells. {P}art {I},
Formalized Mathematics 16(4),
pages 377-387, 2008. MML Identifier:
FTACELL1 Summary:
To evaluate our formal verification method on a real-size
calculation circuit, in this article, we continue to formalize
the concept of the 4-2 Binary Addition Cell primitives (FTAs)
to define the structures of calculation units for a very fast
multiplication algorithm for VLSI implementation
\cite{Vuillemin1983}.
We define the circuit structure of four-types FTAs, TYPE-0 to TYPE-3,
using the series constructions of the Generalized Full Adder Circuits
(GFAs) that generalized adder to have for each positive and negative
weights to inputs and outputs
\cite{GFACIRC1.ABS}.
We then successfully
prove its circuit stability of the calculation outputs after four-steps.
The motivation for this research is to establish a technique based on
formalized mathematics and its applications for calculation circuits
with high reliability.
Fuguo Ge, Bing Xie.
Several Differentiation Formulas
of Special Functions. {P}art {VII},
Formalized Mathematics 16(4),
pages 389-399, 2008. MML Identifier:
FDIFF_11 Summary:
In this article, we prove a series of differentiation identities
\cite{Chemnitius:1956}
involving the arctan and arccot functions
and specific combinations of special functions including
trigonometric and exponential functions.
Hideki Sakurai, Hisayoshi Kunimune, Yasunari Shidama.
Open Mapping Theorem,
Formalized Mathematics 16(4),
pages 401-403, 2008. MML Identifier:
LOPBAN_6 Summary:
In this article we formalize one of the most important theorems
of linear operator theory the Open Mapping Theorem commonly used
in a standard book such as
\cite{miyadera:1972}
in chapter 2.4.2.
It states that a surjective continuous linear operator between
Banach spaces is an open map.