Search Results

You are looking at 1 - 10 of 21 items for

  • Author: Keiko Narita x
Clear All Modify Search
Open access

Keiko Narita, Kazuhisa Nakasho and Yasunari Shidama

Summary

In this article, we formalize in the Mizar system [1, 4] the F. Riesz theorem. In the first section, we defined Mizar functor ClstoCmp, compact topological spaces as closed interval subset of real numbers. Then using the former definition and referring to the article [10] and the article [5], we defined the normed spaces of continuous functions on closed interval subset of real numbers, and defined the normed spaces of bounded functions on closed interval subset of real numbers. We also proved some related properties.

In Sec.2, we proved some lemmas for the proof of F. Riesz theorem. In Sec.3, we proved F. Riesz theorem, about the dual space of the space of continuous functions on closed interval subset of real numbers, finally. We applied Hahn-Banach theorem (36) in [7], to the proof of the last theorem. For the description of theorems of this section, we also referred to the article [8] and the article [6]. These formalizations are based on [2], [3], [9], and [11].

Open access

Keiko Narita, Artur Kornilowicz and Yasunari Shidama

More on the Continuity of Real Functions

In this article we demonstrate basic properties of the continuous functions from R to Rn which correspond to state space equations in control engineering.

Open access

Keiko Narita, Noboru Endou and Yasunari Shidama

Summary

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

Open access

Keiko Narita, Noboru Endou and Yasunari Shidama

Summary

In this article, we described basic properties of Riemann integral on functions from R into Real Banach Space. We proved mainly the linearity of integral operator about the integral of continuous functions on closed interval of the set of real numbers. These theorems were based on the article [10] and we referred to the former articles about Riemann integral. We applied definitions and theorems introduced in the article [9] and the article [11] to the proof. Using the definition of the article [10], we also proved some theorems on bounded functions.

Open access

Keiko Narita, Noboru Endou and Yasunari Shidama

The First Mean Value Theorem for Integrals

In this article, we prove the first mean value theorem for integrals [16]. The formalization of various theorems about the properties of the Lebesgue integral is also presented.

MML identifier: MESFUNC7, version: 7.8.09 4.97.1001

Open access

Noboru Endou, Keiko Narita and Yasunari Shidama

The Lebesgue Monotone Convergence Theorem

In this article we prove the Monotone Convergence Theorem [16].

MML identifier: MESFUNC9, version: 7.8.10 4.100.1011

Open access

Keiko Narita, Kazuhisa Nakasho and Yasunari Shidama

Abstract

In this article, the definitions and basic properties of Riemann-Stieltjes integral are formalized in Mizar [1]. In the first section, we showed the preliminary definition. We proved also some properties of finite sequences of real numbers. In Sec. 2, we defined variation. Using the definition, we also defined bounded variation and total variation, and proved theorems about related properties.

In Sec. 3, we defined Riemann-Stieltjes integral. Referring to the way of the article [7], we described the definitions. In the last section, we proved theorems about linearity of Riemann-Stieltjes integral. Because there are two types of linearity in Riemann-Stieltjes integral, we proved linearity in two ways. We showed the proof of theorems based on the description of the article [7]. These formalizations are based on [8], [5], [3], and [4].

Open access

Keiko Narita, Artur Korniłowicz and Yasunari Shidama

The Differentiable Functions from R into R n

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

Open access

Keiko Narita, Noboru Endou and Yasunari Shidama

The Measurability of Complex-Valued Functional Sequences

In this article, we formalized the measurability of complex-valued functional sequences. First, we proved the measurability of the limits of real-valued functional sequences. Next, we defined complex-valued functional sequences dividing real part into imaginary part. Then using the former theorems, we proved the measurability of each part. Lastly, we proved the measurability of the limits of complex-valued functional sequences. We also showed several properties of complex-valued measurable functions. In addition, we proved properties of complex-valued simple functions.

Open access

Keiko Narita, Noboru Endou and Yasunari Shidama

Summary

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