Search Results

You are looking at 1 - 10 of 12 items for

  • Author: Hiroshi Yamazaki x
Clear All Modify Search
Open access

Masahiko Yamazaki, Hiroshi Yamazaki and Yasunari Shidama

Extended Riemann Integral of Functions of Real Variable and One-sided Laplace Transform

In this article, we defined a variety of extended Riemann integrals and proved that such integration is linear. Furthermore, we defined the one-sided Laplace transform and proved the linearity of that operator.

MML identifier: INTEGR10, version: 7.9.01 4.101.1015

Open access

Masahiko Yamazaki, Hiroshi Yamazaki, Yasunari Shidama and Katsumi Wasaki

Complex Integral

In this article, we defined complex curve and complex integral. Then we have proved the linearity for the complex integral. Furthermore, we have proved complex integral of complex curve's connection is the sum of each complex integral of individual complex curve.

Open access

Hiroyuki Okazaki, Hiroshi Yamazaki and Yasunari Shidama

Summary

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

Open access

Bo Zhang, Hiroshi Yamazaki and Yatsuka Nakamura

The Relevance of Measure and Probability, and Definition of Completeness of Probability

In this article, we first discuss the relation between measure defined using extended real numbers and probability defined using real numbers. Further, we define completeness of probability, and its completion method, and also show that they coincide with those of measure.

Open access

Hiroshi Yamazaki, Czesław Byliński and Katsumi Wasaki

Morphology for Image Processing. Part I

In this article we defined mathematical morphology image processing with set operations. First, we defined Minkowski set operations and proved their properties. Next, we defined basic image processing, dilation and erosion proving basic fact about them [5], [8].

Open access

Kazuhisa Nakasho, Hiroshi Yamazaki, Hiroyuki Okazaki and Yasunari Shidama

Summary

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.

Open access

Kazuhisa Nakasho, Hiroyuki Okazaki, Hiroshi Yamazaki and Yasunari Shidama

Summary

In this article, the equivalent expressions of the direct sum decomposition of groups are mainly discussed. In the first section, we formalize the fact that the internal direct sum decomposition can be defined as normal subgroups and some of their properties. In the second section, we formalize an equivalent form of internal direct sum of commutative groups. In the last section, we formalize that the external direct sum leads an internal direct sum. We referred to [19], [18] [8] and [14] in the formalization.

Open access

Hiroshi Yamazaki, Yasunari Shidama, Yatsuka Nakamura and Chanapat Pacharapokin

The Cauchy-Riemann Differential Equations of Complex Functions

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

Open access

Kazuhisa Nakasho, Hiroshi Yamazaki, Hiroyuki Okazaki and Yasunari Shidama

Summary

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 direct sum is proved. We referred to [23], [22], [8] and [18] in the formalization.

Open access

Hiroshi Yamazaki, Hiroyuki Okazaki, Kazuhisa Nakasho and Yasunari Shidama

Summary

In this paper we formalized some theorems concerning the cyclic groups of prime power order. We formalize that every commutative cyclic group of prime power order is isomorphic to a direct product of family of cyclic groups [1], [18].