In this article, we formalize differentiability of functions on normed linear spaces. Partial derivative, mean value theorem for vector-valued functions, continuous differentiability, etc. are formalized. As it is well known, there is no exact analog of the mean value theorem for vector-valued functions. However a certain type of generalization of the mean value theorem for vector-valued functions is obtained as follows: If ||ƒ'(x + t · h)|| is bounded for t between 0 and 1 by some constant M, then...
In this article we formalized the Fréchet differentiation. It is defined as a generalization of the differentiation of a real-valued function of a single real variable to more general functions whose domain and range are subsets of normed spaces [14].
We have been working on the formalization of the probability and the randomness. In [15] and [16], we formalized some theorems concerning the real-valued random variables and the product of two probability spaces. In this article, we present the generalized formalization of [15] and [16]. First, we formalize the random variables of arbitrary set and prove the equivalence between random variable on Σ, Borel sets and a real-valued random variable on Σ. Next, we formalize the product of countably infinite...
In this paper we construct integral of measurable function.
Based on [16], authors formalized the integral of an extended real valued measurable function in [12] before. However, the integral argued in [12] cannot be applied to real-valued functions unconditionally. Therefore, in this article we have formalized the integral of a real-value function.
In this article, we define the Riemann Integral of functions from R into Rn, and prove the linearity of this operator. The presented method is based on [21].
This text includes the definition of chain-complete poset, fix-point theorem on it, and the definition of the function space of continuous functions on chain-complete posets [10].
In the [20], it had been proven that the Integers modulo p, in this article we shall refer as Z/pZ, constitutes a field if and only if Z/pZ is a prime. Then the prime modulo Z/pZ is an additive cyclic group and Z/pZ* = Z/pZ{0is a multiplicative cyclic group, too. The former has been proven in the [23]. However, the latter had not been proven yet. In this article, first, we prove a theorem concerning the LCM to prove the existence of primitive elements of Z/pZ*. Moreover we prove the uniqueness of...
The paper includes elements of the theory of matroids [23]. The formalization is done according to [12].MML identifier: MATROID0, version: 7.9.03 4.108.1028
In this article we continue formalizing probability and randomness started in [13], where we formalized some theorems concerning the probability and real-valued random variables. In this paper we formalize the variance of a random variable and prove Chebyshev's inequality. Next we formalize the product probability measure on the Cartesian product of discrete spaces. In the final part of this article we define the algebra of real-valued random variables.
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.MML identifier:...
In this article we formalize DES (the Data Encryption Standard), that was the most widely used symmetric cryptosystem in the world. DES is a block cipher which was selected by the National Bureau of Standards as an official Federal Information Processing Standard for the United States in 1976 [15].
In the various branches of science, probability and randomness provide us with useful theoretical frameworks. The Formalized Mathematics has already published some articles concerning the probability: [23], [24], [25], and [30]. 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.
In this article, we formalize in the Mizar system [1, 4] some properties of vector spaces over a ring. We formally prove the first isomorphism theorem of vector spaces over a ring. We also formalize the product space of vector spaces. ℤ-modules are useful for lattice problems such as LLL (Lenstra, Lenstra and Lovász) [5] base reduction algorithm and cryptographic systems [6, 2].
In this article, we formalize in Mizar [5] the definition of dual lattice and their properties. We formally prove that a set of all dual vectors in a rational lattice has the construction of a lattice. We show that a dual basis can be calculated by elements of an inverse of the Gram Matrix. We also formalize a summation of inner products and their properties. Lattice of ℤ-module is necessary for lattice problems, LLL(Lenstra, Lenstra and Lovász) base reduction algorithm and cryptographic systems...
In this article, we formalize in Mizar [14] the definition of embedding of lattice and its properties. We formally define an inner product on an embedded module. We also formalize properties of Gram matrix. We formally prove that an inverse of Gram matrix for a rational lattice exists. Lattice of Z-module is necessary for lattice problems, LLL (Lenstra, Lenstra and Lov´asz) base reduction algorithm [16] and cryptographic systems with lattice [17].
In this article, we formalize the definition of divisible ℤ-module and its properties in the Mizar system [3]. We formally prove that any non-trivial divisible ℤ-modules are not finitely-generated.We introduce a divisible ℤ-module, equivalent to a vector space of a torsion-free ℤ-module with a coefficient ring ℚ. ℤ-modules are important for lattice problems, LLL (Lenstra, Lenstra and Lovász) base reduction algorithm [15], cryptographic systems with lattices [16] and coding theory [8].
In this article, we formalize the definition of lattice of ℤ-module and its properties in the Mizar system [5].We formally prove that scalar products in lattices are bilinear forms over the field of real numbers ℝ. We also formalize the definitions of positive definite and integral lattices and their properties. Lattice of ℤ-module is necessary for lattice problems, LLL (Lenstra, Lenstra and Lovász) base reduction algorithm [14], and cryptographic systems with lattices [15] and coding theory [9]....
We have been working on the formalization of groups. In [1], we encoded some theorems concerning the product of cyclic groups. In this article, we present the generalized formalization of [1]. First, we show that every finite commutative group which order is composite number is isomorphic to a direct product of finite commutative groups which orders are relatively prime. Next, we describe finite direct products of finite commutative groups
Download Results (CSV)