A copy of this issue can also be found on the
MetaPress server (with DOI names of articles).
Bo Li, Pan Wang, Xiquan Liang, Yanping Zhuang.
Some Operations on Quaternion Numbers,
Formalized Mathematics 17(2),
pages 61-65, 2009. MML Identifier:
QUATERN3 Summary:
In this article, we give some equality and basic theorems about quaternion numbers, and some special operations.
Chanapat Pacharapokin, Hiroshi Yamazaki, Yasunari Shidama, Yatsuka Nakamura.
Complex Function Differentiability,
Formalized Mathematics 17(2),
pages 67-72, 2009. MML Identifier:
CFDIFF_1 Summary:
For a complex valued function defined on its domain in complex numbers the differentiability
in a single point and on a subset of the domain is presented. The main elements of differential
calculus are developed. The algebraic properties of differential complex functions are shown.
Agnes Doll.
Kolmogorov's Zero-One Law,
Formalized Mathematics 17(2),
pages 73-77, 2009. MML Identifier:
KOLMOG01 Summary:
This article presents the proof of Kolmogorov's zero-one law
in probability theory. The independence of a family of $\sigma$-fields
is defined and basic theorems on it are given.
Bing Xie, Xiquan Liang, Xiuzhuan Shen.
Second-Order Partial Differentiation of Real Binary Functions,
Formalized Mathematics 17(2),
pages 79-87, 2009. MML Identifier:
PDIFF_3 Summary:
In this article we define second-order partial differentiation of real binary functions and discuss
the relation of
second-order partial derivatives and partial derivatives defined
in \cite{PDIFF_2.ABS}.
Keiko Narita, Noboru Endou, Yasunari Shidama.
The Measurability of Complex-Valued Functional Sequences,
Formalized Mathematics 17(2),
pages 89-97, 2009. MML Identifier:
MESFUN7C Summary:
In this article, we formalized the measurability of complex-valued functional sequences.
First, we proved the measurability of the limits of real-valued functional sequences.
Next, we defined complex-valued functional sequences dividing real part into imaginary part.
Then using the former theorems, we proved the measurability of each part.
Lastly, we proved the measurability of the limits of complex-valued functional sequences.
We also showed several properties of complex-valued measurable functions.
In addition, we proved properties of complex-valued simple functions.
Artur Korni{\l}owicz.
Collective Operations on Number-Membered Sets,
Formalized Mathematics 17(2),
pages 99-115, 2009. MML Identifier:
MEMBER_1 Summary:
The article starts with definitions of sets of opposite and inverse numbers of a given number membered set. Next,
collective addition, subtraction, multiplication and division of two sets are defined. Complex numbers cases and
extended real numbers ones are introduced separately and unified for reals. Shortcuts for singletons cases are also
defined.
Marco Riccardi.
Solution of Cubic and Quartic Equations,
Formalized Mathematics 17(2),
pages 117-122, 2009. MML Identifier:
POLYEQ_5 Summary:
In this article, the principal $n$-th root of a complex number is defined, the Vieta's
formulas for polynomial equations of degree 2, 3 and 4 are formalized. The solution of
quadratic equations, the Cardan's solution of cubic equations and the Descartes-Euler
solution of quartic equations in terms of their complex coefficients are also
presented \cite{Korn}.
Marco Riccardi.
The Perfect Number Theorem and {W}ilson's Theorem,
Formalized Mathematics 17(2),
pages 123-128, 2009. MML Identifier:
NAT_5 Summary:
This article formalizes proofs of some elementary theorems of number theory
(see \cite{PFTB,
LeVeque}): Wilson's theorem
(that $n$ is prime iff $n > 1$ and $(n-1)! \cong -1$ (mod $n$)),
that all primes (1 mod 4) equal the sum of two squares, and two basic theorems of
Euclid and Euler about perfect numbers. The article also formally defines Euler's sum
of divisors function $\phi$, proves that $\phi$ is multiplicative
and that $\sum_{k|n} \phi (k) = n$.
Hiroyuki Okazaki, Yasunari Shidama.
Probability on Finite Set and Real-Valued Random Variables,
Formalized Mathematics 17(2),
pages 129-136, 2009. MML Identifier:
RANDOM_1 Summary:
In the various branches of science, probability and randomness provide
us with useful theoretical frameworks. The {\it Formalized Mathematics}
has already published some articles concerning the
probability: \cite{PROB_2.ABS},
\cite{PROB_1.ABS},
\cite{RPR_1.ABS},
and \cite{PROB_4.ABS}.
In order to apply those articles,
we shall give some theorems concerning the probability and the
real-valued random variables to prepare for further studies.
Keiko Narita, Noboru Endou, Yasunari Shidama.
Lebesgue's Convergence Theorem
of Complex-Valued Function,
Formalized Mathematics 17(2),
pages 137-145, 2009. MML Identifier:
MESFUN9C Summary:
In this article, we formalized Lebesgue's Convergence theorem of complex-valued function.
We proved Lebesgue's Convergence Theorem of real-valued function using the theorem of
extensional real-valued function. Then applying the former theorem to real part and
imaginary part of complex-valued functional sequences, we proved Lebesgue's Convergence
Theorem of complex-valued function. We also defined partial sums of real-valued functional
sequences and complex-valued functional sequences and showed their properties.
In addition, we proved properties of complex-valued simple functions.
Hiroshi Yamazaki, Yasunari Shidama, Chanapat Pacharapokin, Yatsuka Nakamura.
The {C}auchy-{R}iemann Differential
Equations of Complex Functions,
Formalized Mathematics 17(2),
pages 147-149, 2009. MML Identifier:
CFDIFF_2 Summary:
In this article we prove Cauchy-Riemann differential equations of complex functions.
These theorems give necessary and sufficient condition for differentiable function.
Kenichi Arai, Hiroyuki Okazaki.
Properties of Primes and Multiplicative Group of a Field,
Formalized Mathematics 17(2),
pages 151-155, 2009. MML Identifier:
GR_CY_3 Summary:
In the \cite{INT_7.ABS} has been
proven that the multiplicative
group ${\mathbb Z}/p{{\mathbb Z}^\ast}$
is a cyclic group. Likewise, finite subgroup of the multiplicative group of a field
is a cyclic group. However, finite subgroup of the multiplicative group of a field
being a cyclic group has not yet been proven. Therefore, it is of importance to
prove that finite subgroup of the multiplicative group of a field is a cyclic group.
Meanwhile, in cryptographic system like RSA, in which security basis depends upon the
difficulty of factorization of given numbers into prime factors, it is important to
employ integers that are difficult to be factorized into prime factors.
If both $p$ and $2p+1$ are prime numbers, we call $p$ as Sophie Germain prime,
and $2p+1$ as safe prime. It is known that the product of two safe primes is a
composite number that is difficult for some factoring algorithms to factorize
into prime factors. In addition,
safe primes are also important in cryptography system because of their use in
discrete logarithm based techniques like Diffie-Hellman key exchange. If $p$ is a safe prime,
the multiplicative group of numbers modulo $p$ has a subgroup of large prime order.
However, no definitions have not been established yet with the safe prime
and Sophie Germain prime. So it is important to give definitions of the Sophie
Germain prime and safe prime.
In this article, we prove finite subgroup of the multiplicative group of a field is a
cyclic group, and, further, define the safe prime and Sophie Germain prime,
and prove several facts about them. In addition, we define Mersenne
number (${M}_{n}$), and some facts about Mersenne numbers and prime numbers are proven.
Noboru Endou, Hiroyuki Okazaki, Yasunari Shidama.
Hopf Extension Theorem of Measure,
Formalized Mathematics 17(2),
pages 157-162, 2009. MML Identifier:
MEASURE8 Summary:
The authors have presented some articles about Lebesgue type integration theory.
In our previous articles \cite{MESFUNC9.ABS,
MESFUNC5.ABS,
RINFSUP2.ABS},
we assumed that some $\sigma$-additive measure existed and that a function
was measurable on that measure. However the existence of such a measure is not trivial.
In general, because the construction of a finite additive measure is comparatively easy,
to induce a $\sigma$-additive measure a finite additive measure is used.
This is known as an E.~Hopf's extension theorem of
measure \cite{Halmos74}.
Micha{\l} Trybulec.
Labelled State Transition Systems,
Formalized Mathematics 17(2),
pages 163-171, 2009. MML Identifier:
REWRITE3 Summary:
This article introduces labelled state transition systems, where transitions may be
labelled by words from a given alphabet. Reduction relations
from \cite{REWRITE1.ABS}
are used to define transitions between states, acceptance of words, and reachable states.
Deterministic transition systems are also defined.
Hiroyuki Okazaki.
Probability on Finite and Discrete Set
and Uniform Distribution,
Formalized Mathematics 17(2),
pages 173-178, 2009. MML Identifier:
DIST_1 Summary:
A pseudorandom number generator plays an important role in practice in computer science.
For example: computer simulations, cryptology, and so on. A pseudorandom number generator
is an algorithm to generate a sequence of numbers that is indistinguishable from the
true random number sequence. In this article, we shall formalize the ``Uniform Distribution"
that is the idealized set of true random number sequences. The basic idea of our formalization
is due to \cite{CINTA}.
Keiichi Miyajima, Yasunari Shidama.
Riemann Integral of Functions
from $\mathbb{R}$ into $\calR^n$,
Formalized Mathematics 17(2),
pages 179-185, 2009. MML Identifier:
INTEGR15 Summary:
In this article, we define the Riemann Integral of functions from $\mathbb{R}$ into $\calR^n$,
and prove the linearity of this operator. The presented method is based
on \cite{Murray:1974}.
Bo Li, Yanhong Men.
Basic Properties of Even and Odd Functions,
Formalized Mathematics 17(2),
pages 187-192, 2009. MML Identifier:
FUNCT_8 Summary:
In this article we present definitions, basic properties and some examples of even
and odd functions \cite{Chen:1978}.
Micha{\l} Trybulec.
Equivalence of Deterministic and Nondeterministic
Epsilon Automata,
Formalized Mathematics 17(2),
pages 193-199, 2009. MML Identifier:
FSM_3 Summary:
Based on concepts introduced
in \cite{REWRITE3.ABS},
semiautomata and left-languages,
automata and right-languages, and langauges accepted by automata are defined.
The powerset construction is defined for transition systems, semiautomata and automata.
Finally, the equivalence of deterministic and nondeterministic epsilon automata is shown.