Several Differentiation Formulas of Special Functions. Part V
In this article, we give several differentiation formulas of special and composite functions including trigonometric, polynomial and logarithmic functions.
Published Online: 09 Jun 2008 Page range: 87 - 110
Abstract
Mizar Analysis of Algorithms: Preliminaries
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.
Published Online: 09 Jun 2008 Page range: 111 - 119
Abstract
Definition and some Properties of Information Entropy
In this article we mainly define the information entropy [3], [11] 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 [25]. Further, we discuss some properties of information entropy including Shannon's lemma, maximum property, additivity and super-additivity properties.
Published Online: 09 Jun 2008 Page range: 121 - 126
Abstract
String Rewriting Systems
Basing on the definitions from [15], 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 [1]. 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.
Published Online: 09 Jun 2008 Page range: 127 - 136
Abstract
Determinant and Inverse of Matrices of Real Elements
In this paper the classic theory of matrices of real elements (see e.g. [12], [13]) 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.
Published Online: 09 Jun 2008 Page range: 137 - 142
Abstract
The Rank+Nullity Theorem
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) = rank(T) + nullity(T), where rank(T) = dim(im(T)) and nullity(T) = dim(ker(T)). The proof treated here is standard; see, for example, [14]: take a basis A of ker(T) and extend it to a basis B of V, and then show that dim(im(T)) is equal to |B - A|, and that T is one-to-one on B - A.
Published Online: 09 Jun 2008 Page range: 159 - 165
Abstract
The Sylow Theorems
The goal of this article is to formalize the Sylow theorems closely following the book [4]. Accordingly, the article introduces the group operating on a set, the stabilizer, the orbits, the p-groups and the Sylow subgroups.
Several Differentiation Formulas of Special Functions. Part V
In this article, we give several differentiation formulas of special and composite functions including trigonometric, polynomial and logarithmic functions.
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.
Definition and some Properties of Information Entropy
In this article we mainly define the information entropy [3], [11] 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 [25]. Further, we discuss some properties of information entropy including Shannon's lemma, maximum property, additivity and super-additivity properties.
Basing on the definitions from [15], 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 [1]. 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.
Determinant and Inverse of Matrices of Real Elements
In this paper the classic theory of matrices of real elements (see e.g. [12], [13]) 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.
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) = rank(T) + nullity(T), where rank(T) = dim(im(T)) and nullity(T) = dim(ker(T)). The proof treated here is standard; see, for example, [14]: take a basis A of ker(T) and extend it to a basis B of V, and then show that dim(im(T)) is equal to |B - A|, and that T is one-to-one on B - A.
The goal of this article is to formalize the Sylow theorems closely following the book [4]. Accordingly, the article introduces the group operating on a set, the stabilizer, the orbits, the p-groups and the Sylow subgroups.