Wyniki wyszukiwania - Biblioteka Nauki

1

Differentiable Functions on Normed Linear Spaces

100%

Shidama Y.

|

nr 1

31-40

EN

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

Preface

63%

Grabowski A. , Shidama Y.

|

nr 2

i-iv

3

Probability on Finite Set and Real-Valued Random Variables

63%

Okazaki H. , Shidama Y.

|

nr 2

129-136

EN

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.

4

Lattice of ℤ-module

63%

Futa Y. , Shidama Y.

|

nr 1

49-68

EN

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

5

Divisible ℤ-modules

63%

Futa Y. , Shidama Y.

|

nr 1

37-47

EN

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

6

Formalization of the Data Encryption Standard

63%

Okazaki H. , Shidama Y.

|

nr 2

125-146

EN

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

7

Riemann Integral of Functions from R into R n

63%

Miyajima K. , Shidama Y.

|

nr 2

179-185

EN

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

8

Bidual Spaces and Reflexivity of Real Normed Spaces

51%

Narita K. , Endou N. , Shidama Y.

|

nr 4

303-311

EN

In this article, we considered bidual spaces and reflexivity of real normed spaces. At first we proved some corollaries applying Hahn-Banach theorem and showed related theorems. In the second section, we proved the norm of dual spaces and defined the natural mapping, from real normed spaces to bidual spaces. We also proved some properties of this mapping. Next, we defined real normed space of R, real number spaces as real normed spaces and proved related theorems. We can regard linear functionals as linear operators by this definition. Accordingly we proved Uniform Boundedness Theorem for linear functionals using the theorem (5) from [21]. Finally, we defined reflexivity of real normed spaces and proved some theorems about isomorphism of linear operators. Using them, we proved some properties about reflexivity. These formalizations are based on [19], [20], [8] and [1].

9

Topological Properties of Real Normed Space

51%

Nakasho K. , Futa Y. , Shidama Y.

|

nr 3

209-223

EN

In this article, we formalize topological properties of real normed spaces. In the first part, open and closed, density, separability and sequence and its convergence are discussed. Then we argue properties of real normed subspace. Then we discuss linear functions between real normed speces. Several kinds of subspaces induced by linear functions such as kernel, image and inverse image are considered here. The fact that Lipschitz continuity operators preserve convergence of sequences is also refered here. Then we argue the condition when real normed subspaces become Banach’s spaces. We also formalize quotient vector space. In the last session, we argue the properties of the closure of real normed space. These formalizations are based on [19](p.3-41), [2] and [34](p.3-67).

10

Rank of Submodule, Linear Transformations and Linearly Independent Subsets of Z-module

51%

Nakasho K. , Futa Y. , Okazaki H. , Shidama Y.

|

nr 3

189-198

EN

In this article, we formalize some basic facts of Z-module. In the first section, we discuss the rank of submodule of Z-module and its properties. Especially, we formally prove that the rank of any Z-module is equal to or more than that of its submodules, and vice versa, and that there exists a submodule with any given rank that satisfies the above condition. In the next section, we mention basic facts of linear transformations between two Z-modules. In this section, we define homomorphism between two Z-modules and deal with kernel and image of homomorphism. In the last section, we formally prove some basic facts about linearly independent subsets and linear combinations. These formalizations are based on [9](p.191-242), [23](p.117-172) and [2](p.17-35).

11

Torsion Z-module and Torsion-free Z-module

51%

Futa Y. , Okazaki H. , Nakasho K. , Shidama Y.

|

nr 4

277-289

EN

In this article, we formalize a torsion Z-module and a torsionfree Z-module. Especially, we prove formally that finitely generated torsion-free Z-modules are finite rank free. We also formalize properties related to rank of finite rank free Z-modules. The notion of Z-module is necessary for solving lattice problems, LLL (Lenstra, Lenstra, and Lov´asz) base reduction algorithm [20], cryptographic systems with lattice [21], and coding theory [11].

12

Definition of Flat Poset and Existence Theorems for Recursive Call

51%

Ishida K. , Shidama Y. , Grabowski A.

|

nr 1

1-10

EN

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 we extensively use technical Mizar functors like BaseFunc or RecFunc. The remaining part builds the background for information engineering approach for lists, namely recursive call for posets [21].We formalized some facts from Chapter 8 of this book as an introduction to the next two sections where we concentrate on binary product of posets rather than on a more general case.

13

Dual Spaces and Hahn-Banach Theorem

51%

Narita K. , Endou N. , Shidama Y.

|

nr 1

69-77

EN

In this article, we deal with dual spaces and the Hahn-Banach Theorem. At the first, we defined dual spaces of real linear spaces and proved related basic properties. Next, we defined dual spaces of real normed spaces. We formed the definitions based on dual spaces of real linear spaces. In addition, we proved properties of the norm about elements of dual spaces. For the proof we referred to descriptions in the article [21]. Finally, applying theorems of the second section, we proved the Hahn-Banach extension theorem in real normed spaces. We have used extensively used [17].

14

The Cauchy-Riemann Differential Equations of Complex Functions

51%

Yamazaki H. , Shidama Y. , Nakamura Y. , Pacharapokin C.

|

nr 2

147-149

EN

In this article we prove Cauchy-Riemann differential equations of complex functions. These theorems give necessary and sufficient condition for differentiable function.

15

Lebesgue's Convergence Theorem of Complex-Valued Function

51%

Narita K. , Endou N. , Shidama Y.

|

nr 2

137-145

EN

In this article, we formalized Lebesgue's Convergence theorem of complex-valued function. We proved Lebesgue's Convergence Theorem of realvalued function using the theorem of extensional real-valued function. Then applying the former theorem to real part and imaginary part of complex-valued functional sequences, we proved Lebesgue's Convergence Theorem of complex-valued function. We also defined partial sums of real-valued functional sequences and complex-valued functional sequences and showed their properties. In addition, we proved properties of complex-valued simple functions.

16

Hopf Extension Theorem of Measure

51%

Endou N. , Okazaki H. , Shidama Y.

|

nr 2

157-162

EN

The authors have presented some articles about Lebesgue type integration theory. In our previous articles [12, 13, 26], we assumed that some σ-additive measure existed and that a function was measurable on that measure. However the existence of such a measure is not trivial. In general, because the construction of a finite additive measure is comparatively easy, to induce a σ-additive measure a finite additive measure is used. This is known as an E. Hopf's extension theorem of measure [15].

17

Functional SpaceC(ω),C0(ω)

51%

Kanazashi K. , Okazaki H. , Shidama Y.

|

nr 1

15-22

EN

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.

18

The Differentiable Functions from R intoR n

51%

Narita K. , Korniłowicz A. , Shidama Y.

|

nr 1

65-71

EN

In control engineering, differentiable partial functions from R into Rn play a very important role. In this article, we formalized basic properties of such functions.

19

Z-modules

51%

Futa Y. , Okazaki H. , Shidama Y.

|

nr 1

47-59

EN

In this article, we formalize Z-module, that is a module over integer ring. Z-module is necassary for lattice problems, LLL (Lenstra-Lenstra-Lovász) base reduction algorithm and cryptographic systems with lattices [11].

20

On L1Space Formed by Complex-Valued Partial Functions

51%

Watase Y. , Endou N. , Shidama Y.

|

nr 4

349-357

EN

In this article, we formalized L1 space formed by complexvalued partial functions [11], [15]. The real-valued case was formalized in [22] and this article is its generalization.