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 ||ƒ(x + t · h) - ƒ(x)|| ≤ M · ||h||. This theorem is called the mean value theorem for vector-valued functions. By this theorem, the relation between the (total) derivative and the partial derivatives of a function is derived [23].
2
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
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 with lattice [20], [10] and [19].
3
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
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].
4
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
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].
5
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
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].
6
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
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.
7
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
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: MODELC 3, version: 7.9.03 4.108.1028
9
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
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].
10
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
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.
11
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
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
12
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
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].
14
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
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].
15
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
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.
16
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
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].
17
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
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\{0} is 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 factoring an integer. Next we define the multiplicative group Z/pZ* and prove it is cyclic.MML identifier: INT 7, version: 7.8.10 4.99.1005
18
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
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].
19
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
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 probability spaces.
20
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
In this article, first we give a definition of a functional space which is constructed from all complex-valued continuous functions defined on a compact topological space. We prove that this functional space is a Banach algebra. Next, we give a definition of a function space which is constructed from all complex-valued continuous functions with bounded support. We also prove that this function space is a complex normed space.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.