Pełnotekstowe zasoby PLDML oraz innych baz dziedzinowych są już dostępne w nowej Bibliotece Nauki.
Zapraszamy na https://bibliotekanauki.pl
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 102

Liczba wyników na stronie
first rewind previous Strona / 6 next fast forward last

Wyniki wyszukiwania

help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 6 next fast forward last
1
Content available remote

Differentiable Functions on Normed Linear Spaces

100%
Shidama Y.
Formalized Mathematics
|
2012
|
tom 20
|
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
Content available remote

Dual Lattice of ℤ-module Lattice

64%
Futa Y., Shidama Y.
Formalized Mathematics
|
2017
|
tom 25
|
nr 2
157-169
EN
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
Content available remote

Fixpoint Theorem for Continuous Functions on Chain-Complete Posets

64%
Ishida K., Shidama Y.
Formalized Mathematics
|
2010
|
tom 18
|
nr 1
47-51
EN
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
Content available remote

Isomorphism Theorem on Vector Spaces over a Ring

64%
Futa Y., Shidama Y.
Formalized Mathematics
|
2017
|
tom 25
|
nr 3
171-178
EN
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
Content available remote

Embedded Lattice and Properties of Gram Matrix

64%
Futa Y., Shidama Y.
Formalized Mathematics
|
2017
|
tom 25
|
nr 1
73-86
EN
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
Content available remote

Probability Measure on Discrete Spaces and Algebra of Real-Valued Random Variables

64%
Okazaki H., Shidama Y.
Formalized Mathematics
|
2010
|
tom 18
|
nr 4
213-217
EN
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
Content available remote

Integral of Measurable Function1

64%
Endou N., Shidama Y.
Formalized Mathematics
|
2006
|
tom 14
|
nr 2
53-70
EN
In this paper we construct integral of measurable function.
8
Content available remote

Model Checking. Part III

64%
Ishida K., Shidama Y.
Formalized Mathematics
|
2008
|
tom 16
|
nr 4
339-353
EN
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
Content available remote

Formalization of the Data Encryption Standard

64%
Okazaki H., Shidama Y.
Formalized Mathematics
|
2012
|
tom 20
|
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].
10
Content available remote

Probability on Finite Set and Real-Valued Random Variables

64%
Okazaki H., Shidama Y.
Formalized Mathematics
|
2009
|
tom 17
|
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.
11
Content available remote

Introduction to Matroids

64%
Bancerek G., Shidama Y.
Formalized Mathematics
|
2008
|
tom 16
|
nr 4
325-332
EN
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
Content available remote

Preface

64%
Grabowski A., Shidama Y.
Formalized Mathematics
|
2014
|
tom 22
|
nr 2
i-iv
13
Content available remote

Divisible ℤ-modules

64%
Futa Y., Shidama Y.
Formalized Mathematics
|
2016
|
tom 24
|
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].
14
Content available remote

Lattice of ℤ-module

64%
Futa Y., Shidama Y.
Formalized Mathematics
|
2016
|
tom 24
|
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].
15
Content available remote

Integral of Real-Valued Measurable Function1

64%
Shidama Y., Endou N.
Formalized Mathematics
|
2006
|
tom 14
|
nr 4
143-152
EN
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
Content available remote

Riemann Integral of Functions from R into R n

64%
Miyajima K., Shidama Y.
Formalized Mathematics
|
2009
|
tom 17
|
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].
17
Content available remote

Uniqueness of Factoring an Integer and Multiplicative GroupZ/pZ*

64%
Okazaki H., Shidama Y.
Formalized Mathematics
|
2008
|
tom 16
|
nr 2
103-107
EN
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
Content available remote

Differentiation in Normed Spaces

64%
Endou N., Shidama Y.
Formalized Mathematics
|
2013
|
tom 21
|
nr 2
95-102
EN
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
Content available remote

Random Variables and Product of Probability Spaces

64%
Okazaki H., Shidama Y.
Formalized Mathematics
|
2013
|
tom 21
|
nr 1
33-39
EN
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
Content available remote

Functional SpaceC(ω),C0(ω)

52%
Kanazashi K., Okazaki H., Shidama Y.
Formalized Mathematics
|
2012
|
tom 20
|
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.
first rewind previous Strona / 6 next fast forward last
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ć.