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

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

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, Noboru Endou, Yasunari Shidama and Hiroyuki Okazaki

Inferior Limit, Superior Limit and Convergence of Sequences of Extended Real Numbers

In this article, we extended properties of sequences of real numbers to sequences of extended real numbers. We also introduced basic properties of the inferior limit, superior limit and convergence of sequences of extended real numbers.

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

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

Chanapat Pacharapokin, Hiroshi Yamazaki, Yasunari Shidama and Yatsuka Nakamura

Complex Function Differentiability

For a complex valued function defined on its domain in complex numbers the differentiability in a single point and on a subset of the domain is presented. The main elements of differential calculus are developed. The algebraic properties of differential complex functions are shown.

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.