All a b c d e f g h i j k l m n o p q r s t u v w x y z Other

Previous Page 2 Next

Displaying 21 – 40 of 163

Showing per page

Compactness in Metric Spaces

Kazuhisa Nakasho, Keiko Narita, Yasunari Shidama (2016)

Formalized Mathematics

In this article, we mainly formalize in Mizar [2] the equivalence among a few compactness definitions of metric spaces, norm spaces, and the real line. In the first section, we formalized general topological properties of metric spaces. We discussed openness and closedness of subsets in metric spaces in terms of convergence of element sequences. In the second section, we firstly formalize the definition of sequentially compact, and then discuss the equivalence of compactness, countable compactness,...

Conservation Rules of Direct Sum Decomposition of Groups

Kazuhisa Nakasho, Hiroshi Yamazaki, Hiroyuki Okazaki, Yasunari Shidama (2016)

Formalized Mathematics

In this article, conservation rules of the direct sum decomposition of groups are mainly discussed. In the first section, we prepare miscellaneous definitions and theorems for further formalization in Mizar [5]. In the next three sections, we formalized the fact that the property of direct sum decomposition is preserved against the substitutions of the subscript set, flattening of direct sum, and layering of direct sum, respectively. We referred to [14], [13] [6] and [11] in the formalization.

Constructing Binary Huffman Tree

Hiroyuki Okazaki, Yuichi Futa, Yasunari Shidama (2013)

Formalized Mathematics

Huffman coding is one of a most famous entropy encoding methods for lossless data compression [16]. JPEG and ZIP formats employ variants of Huffman encoding as lossless compression algorithms. Huffman coding is a bijective map from source letters into leaves of the Huffman tree constructed by the algorithm. In this article we formalize an algorithm constructing a binary code tree, Huffman tree.

Construction of Measure from Semialgebra of Sets1

Noboru Endou (2015)

Formalized Mathematics

In our previous article [22], we showed complete additivity as a condition for extension of a measure. However, this condition premised the existence of a σ-field and the measure on it. In general, the existence of the measure on σ-field is not obvious. On the other hand, the proof of existence of a measure on a semialgebra is easier than in the case of a σ-field. Therefore, in this article we define a measure (pre-measure) on a semialgebra and extend it to a measure on a σ-field. Furthermore, we...

Convergent Filter Bases

Roland Coghetto (2015)

Formalized Mathematics

We are inspired by the work of Henri Cartan [16], Bourbaki [10] (TG. I Filtres) and Claude Wagschal [34]. We define the base of filter, image filter, convergent filter bases, limit filter and the filter base of tails (fr: filtre des sections).

Definition and Properties of Direct Sum Decomposition of Groups1

Kazuhisa Nakasho, Hiroshi Yamazaki, Hiroyuki Okazaki, Yasunari Shidama (2015)

Formalized Mathematics

In this article, direct sum decomposition of group is mainly discussed. In the second section, support of element of direct product group is defined and its properties are formalized. It is formalized here that an element of direct product group belongs to its direct sum if and only if support of the element is finite. In the third section, product map and sum map are prepared. In the fourth section, internal and external direct sum are defined. In the last section, an equivalent form of internal...

Definition of First Order Language with Arbitrary Alphabet. Syntax of Terms, Atomic Formulas and their Subterms

Marco Caminati (2011)

Formalized Mathematics

Second of a series of articles laying down the bases for classical first order model theory. A language is defined basically as a tuple made of an integer-valued function (adicity), a symbol of equality and a symbol for the NOR logical connective. The only requests for this tuple to be a language is that the value of the adicity in = is -2 and that its preimage (i.e. the variables set) in 0 is infinite. Existential quantification will be rendered (see [11]) by mere prefixing a formula with a letter....

Definition of Flat Poset and Existence Theorems for Recursive Call

Kazuhisa Ishida, Yasunari Shidama, Adam Grabowski (2014)

Formalized Mathematics

This text includes the definition and basic notions of product of posets, chain-complete and flat posets, flattening operation, and the existence theorems of recursive call using the flattening operator. First part of the article, devoted to product and flat posets has a purely mathematical quality. Definition 3 allows to construct a flat poset from arbitrary non-empty set [12] in order to provide formal apparatus which eanbles to work with recursive calls within the Mizar langauge. To achieve this...

Difference of Function on Vector Space over F

Kenichi Arai, Ken Wakabayashi, Hiroyuki Okazaki (2014)

Formalized Mathematics

In [11], the definitions of forward difference, backward difference, and central difference as difference operations for functions on R were formalized. However, the definitions of forward difference, backward difference, and central difference for functions on vector spaces over F have not been formalized. In cryptology, these definitions are very important in evaluating the security of cryptographic systems [3], [10]. Differential cryptanalysis [4] that undertakes a general purpose attack against...

Differentiability of Polynomials over Reals

Artur Korniłowicz (2017)

Formalized Mathematics

In this article, we formalize in the Mizar system [3] the notion of the derivative of polynomials over the field of real numbers [4]. To define it, we use the derivative of functions between reals and reals [9].

Differential Equations on Functions from R into Real Banach Space

Keiko Narita, Noboru Endou, Yasunari Shidama (2013)

Formalized Mathematics

In this article, we describe the differential equations on functions from R into real Banach space. The descriptions are based on the article [20]. As preliminary to the proof of these theorems, we proved some properties of differentiable functions on real normed space. For the proof we referred to descriptions and theorems in the article [21] and the article [32]. And applying the theorems of Riemann integral introduced in the article [22], we proved the ordinary differential equations on real...

Differentiation in Normed Spaces

Noboru Endou, Yasunari Shidama (2013)

Formalized Mathematics

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].

Divisible ℤ-modules

Yuichi Futa, Yasunari Shidama (2016)

Formalized Mathematics

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].

Double Sequences and Iterated Limits in Regular Space

Roland Coghetto (2016)

Formalized Mathematics

First, we define in Mizar [5], the Cartesian product of two filters bases and the Cartesian product of two filters. After comparing the product of two Fréchet filters on ℕ (F1) with the Fréchet filter on ℕ × ℕ (F2), we compare limF₁ and limF₂ for all double sequences in a non empty topological space. Endou, Okazaki and Shidama formalized in [14] the “convergence in Pringsheim’s sense” for double sequence of real numbers. We show some basic correspondences between the p-convergence and the filter...

Double Sequences and Limits

Noboru Endou, Hiroyuki Okazaki, Yasunari Shidama (2013)

Formalized Mathematics

Double sequences are important extension of the ordinary notion of a sequence. In this article we formalized three types of limits of double sequences and the theory of these limits.

Double Series and Sums

Noboru Endou (2014)

Formalized Mathematics

In this paper the author constructs several properties for double series and its convergence. The notions of convergence of double sequence have already been introduced in our previous paper [18]. In section 1 we introduce double series and their convergence. Then we show the relationship between Pringsheim-type convergence and iterated convergence. In section 2 we study double series having non-negative terms. As a result, we have equality of three type sums of non-negative double sequence. In...

Currently displaying 21 – 40 of 163