A copy of this issue can also be found on the
MetaPress server (with DOI names of articles).
Peng Wang, Bo Li.
Several Differentiation Formulas of Special Functions. {P}art {V},
Formalized Mathematics 15(3),
pages 73-79, 2007. MML Identifier: FDIFF_9 Summary: In this article, we give several differentiation formulas of special and composite functions including trigonometric, polynomial and logarithmic functions.
Noboru Endou, Yasunari Shidama, Keiichi Miyajima.
The Product Space of Real Normed Spaces and its Properties,
Formalized Mathematics 15(3),
pages 81-85, 2007. MML Identifier: PRVECT_2 Summary: In this article, we define the product space of real linear spaces and real normed spaces. We also describe properties of these spaces.
Grzegorz Bancerek.
Mizar Analysis of Algorithms: {P}reliminaries,
Formalized Mathematics 15(3),
pages 87-110, 2007. MML Identifier: AOFA_000 Summary: Algorithms and its parts -- instructions -- are formalized as elements of if-while algebras. An if-while algebra is a (1-sorted) universal algebra which has 4 operations: a constant -- the empty instruction, a binary catenation of instructions, a ternary conditional instruction, and a binary while instruction. An execution function is defined on pairs $(s,I)$, where $s$ is a state (an element of certain set of states) and $I$ is an instruction, and results in states. The execution
function obeys control structures using the set of distinguished true states, i.e. a condition instruction is executed and the continuation of execution depends on if the resulting state is in true states or not. Termination is also defined for pairs $(s,I)$ and depends on the execution function. The existence of execution function determined on elementary instructions and its uniqueness for terminating instructions are shown.
Bo Zhang, Yatsuka Nakamura.
Definition and some Properties of Information Entropy,
Formalized Mathematics 15(3),
pages 111-119, 2007. MML Identifier: ENTROPY1 Summary: In this article we mainly define the information entropy \cite{Billingsley:1964}, \cite{Hirasawa:1996} and prove some its basic properties. First, we discuss some properties on four kinds of transformation functions between vector and matrix. The transformation functions are LineVec2Mx, ColVec2Mx, Vec2DiagMx and Mx2FinS. Mx2FinS is a horizontal concatenation operator for a given matrix, treating rows of the given matrix as finite sequences,
yielding a new finite sequence by horizontally joining each row of the given matrix in order to index. Then we define each concept of information entropy for a probability sequence and two kinds of probability matrices, joint and conditional, that are defined in article \cite{MATRPROB.ABS}. Further, we discuss some properties of information entropy including
Shannon's lemma, maximum property, additivity and super-additivity properties.
Micha{\l} ~Trybulec.
String Rewriting Systems,
Formalized Mathematics 15(3),
pages 121-126, 2007. MML Identifier: REWRITE2 Summary: Basing on the definitions from \cite{WAITE-GOOS:1984}, semi-Thue systems, Thue systems, and direct derivations are introduced. Next, the standard reduction relation is defined that, in turn, is used to introduce derivations using the theory from \cite{REWRITE1.ABS}. Finally, languages generated by rewriting systems are defined as all strings reachable from an initial word. This is followed by the introduction of the equivalence of semi-Thue systems with respect to the initial word.
Nobuyuki Tamura, Yatsuka Nakamura.
Determinant and Inverse of Matrices of Real Elements,
Formalized Mathematics 15(3),
pages 127-136, 2007. MML Identifier: MATRIXR2 Summary: In this paper the classic theory of matrices of real elements (see e.g. \cite{Furuya:57}, \cite{Gantmacher:59}) is developed. We prove selected equations that have been proved previously for matrices of field elements. Similarly, we introduce in this special context the determinant of a matrix, the identity and zero matrices, and the inverse matrix. The new concept discussed in the case of matrices of real numbers is the property of matrices as operators acting on finite sequences of real numbers from both sides. The relations of invertibility of matrices and the ``onto" property of matrices as operators are discussed.
Jesse ~Alama.
The Rank+Nullity Theorem,
Formalized Mathematics 15(3),
pages 137-142, 2007. MML Identifier: RANKNULL Summary: The rank+nullity theorem states that, if $T$ is a linear transformation from a finite-dimensional vector space $V$ to a finite-dimensional vector space $W$, then $\dim(V) = \mathrm{rank}(T) + \mathrm{nullity}(T)$, where $\mathrm{rank}(T) = \dim(\mathrm{im}(T))$ and $\mathrm{nullity}(T) = \dim(\mathrm{ker}(T))$. The proof treated here is standard; see, for example,~\cite{lang-algebra}: take a basis $A$ of $\mathrm{ker}(T)$ and extend it to a basis $B$ of $V$, and then show that $\dim(\mathrm{im}(T))$ is equal to $|B - A|$, and that $T$ is one-to-one on $B - A$.
Karol P\c{a}k, Andrzej Trybulec.
Laplace Expansion,
Formalized Mathematics 15(3),
pages 143-150, 2007. MML Identifier: LAPLACE Summary: In the article the formula for Laplace expansion is proved.
Xiquan Liang, Tao Sun, Dahai Hu.
Some Properties of Line and Column Operations on Matrices,
Formalized Mathematics 15(3),
pages 151-157, 2007. MML Identifier: MATRIX12 Summary: This article describes definitions of elementary operations about matrix and their main properties.
Marco Riccardi.
The {S}ylow Theorems,
Formalized Mathematics 15(3),
pages 159-165, 2007. MML Identifier: GROUP_10 Summary: The goal of this article is to formalize the Sylow theorems closely following the book \cite{BourbakiAlgI}. Accordingly, the article introduces the group operating on a set, the stabilizer, the orbits, the $p$-groups and the Sylow subgroups.