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: 47

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

Wyniki wyszukiwania

help Sortuj według:

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

Integral of Non Positive Functions

100%
Endou N.
Formalized Mathematics
|
2017
|
tom 25
|
nr 3
227-240
EN
In this article, we formalize in the Mizar system [1, 7] the Lebesgue type integral and convergence theorems for non positive functions [8],[2]. Many theorems are based on our previous results [5], [6].
2
Content available remote

Fubini’s Theorem on Measure

100%
Endou N.
Formalized Mathematics
|
2017
|
tom 25
|
nr 1
1-29
EN
The purpose of this article is to show Fubini’s theorem on measure [16], [4], [7], [15], [18]. Some theorems have the possibility of slight generalization, but we have priority to avoid the complexity of the description. First of all, for the product measure constructed in [14], we show some theorems. Then we introduce the section which plays an important role in Fubini’s theorem, and prove the relevant proposition. Finally we show Fubini’s theorem on measure.
3
Content available remote

Product Pre-Measure

100%
Endou N.
Formalized Mathematics
|
2016
|
tom 24
|
nr 1
69-79
EN
In this article we formalize in Mizar [5] product pre-measure on product sets of measurable sets. Although there are some approaches to construct product measure [22], [6], [9], [21], [25], we start it from σ-measure because existence of σ-measure on any semialgebras has been proved in [15]. In this approach, we use some theorems for integrals.
4
Content available remote

Double Series and Sums

100%
Endou N.
Formalized Mathematics
|
2014
|
tom 22
|
nr 1
57-68
EN
In this paper the author constructs several properties for double series and its convergence. The notions of convergence of double sequence have already been introduced in our previous paper [18]. In section 1 we introduce double series and their convergence. Then we show the relationship between Pringsheim-type convergence and iterated convergence. In section 2 we study double series having non-negative terms. As a result, we have equality of three type sums of non-negative double sequence. In section 3 we show that if a non-negative sequence is summable, then the sequence of rearrangement of terms is summable and it has the same sums. In the last section two basic relations between double sequences and matrices are introduced.
5
Content available remote

Construction of Measure from Semialgebra of Sets1

100%
Endou N.
Formalized Mathematics
|
2015
|
tom 23
|
nr 4
309-323
EN
In our previous article [22], we showed complete additivity as a condition for extension of a measure. However, this condition premised the existence of a σ-field and the measure on it. In general, the existence of the measure on σ-field is not obvious. On the other hand, the proof of existence of a measure on a semialgebra is easier than in the case of a σ-field. Therefore, in this article we define a measure (pre-measure) on a semialgebra and extend it to a measure on a σ-field. Furthermore, we give a σ-measure as an extension of the measure on a σ-field. We follow [24], [10], and [31].
6
Content available remote

Extended Real-Valued Double Sequence and Its Convergence

100%
Endou N.
Formalized Mathematics
|
2015
|
tom 23
|
nr 3
253-277
EN
In this article we introduce the convergence of extended realvalued double sequences [16], [17]. It is similar to our previous articles [15], [10]. In addition, we also prove Fatou’s lemma and the monotone convergence theorem for double sequences.
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

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.
9
Content available remote

Separability of Real Normed Spaces and Its Basic Properties

64%
Nakasho K., Endou N.
Formalized Mathematics
|
2015
|
tom 23
|
nr 1
59-65
EN
In this article, the separability of real normed spaces and its properties are mainly formalized. In the first section, it is proved that a real normed subspace is separable if it is generated by a countable subset. We used here the fact that the rational numbers form a dense subset of the real numbers. In the second section, the basic properties of the separable normed spaces are discussed. It is applied to isomorphic spaces via bounded linear operators and double dual spaces. In the last section, it is proved that the completeness and reflexivity are transferred to sublinear normed spaces. The formalization is based on [34], and also referred to [7], [14] and [16].
10
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].
11
Content available remote

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

52%
Yamazaki H., Endou N., Shidama Y., Okazaki H.
Formalized Mathematics
|
2007
|
tom 15
|
nr 4
231-235
EN
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.
12
Content available remote

Fatou's Lemma and the Lebesgue's Convergence Theorem

52%
Endou N., Narita K., Shidama Y.
Formalized Mathematics
|
2008
|
tom 16
|
nr 4
305-309
EN
In this article we prove the Fatou's Lemma and Lebesgue's Convergence Theorem [10].MML identifier: MESFUN10, version: 7.9.01 4.101.1015
13
Content available remote

Integral of Complex-Valued Measurable Function

52%
Narita K., Endou N., Shidama Y.
Formalized Mathematics
|
2008
|
tom 16
|
nr 4
319-324
EN
In this article, we formalized the notion of the integral of a complex-valued function considered as a sum of its real and imaginary parts. Then we defined the measurability and integrability in this context, and proved the linearity and several other basic properties of complex-valued measurable functions. The set of properties showed in this paper is based on [15], where the case of real-valued measurable functions is considered.MML identifier: MESFUN6C, version: 7.9.01 4.101.1015
14
Content available remote

Banach Algebra of Continuous Functionals and the Space of Real-Valued Continuous Functionals with Bounded Support

52%
Kanazashi K., Endou N., Shidama Y.
Formalized Mathematics
|
2010
|
tom 18
|
nr 1
11-16
EN
In this article, we give a definition of a functional space which is constructed from all 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 real-valued continuous functions with bounded support. We prove that this function space is a real normed space.
15
Content available remote

The Product Space of Real Normed Spaces and its Properties

52%
Endou N., Shidama Y., Miyajima K.
Formalized Mathematics
|
2007
|
tom 15
|
nr 3
81-85
EN
In this article, we define the product space of real linear spaces and real normed spaces. We also describe properties of these spaces.
16
Content available remote

Differentiation of Vector-Valued Functions onn-Dimensional Real Normed Linear Spaces

52%
Inoué T., Endou N., Shidama Y.
Formalized Mathematics
|
2010
|
tom 18
|
nr 4
207-212
EN
In this article, we define and develop differentiation of vector-valued functions on n-dimensional real normed linear spaces (refer to [16] and [17]).
17
Content available remote

Hopf Extension Theorem of Measure

52%
Endou N., Okazaki H., Shidama Y.
Formalized Mathematics
|
2009
|
tom 17
|
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].
18
Content available remote

Dual Spaces and Hahn-Banach Theorem

52%
Narita K., Endou N., Shidama Y.
Formalized Mathematics
|
2014
|
tom 22
|
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].
19
Content available remote

Bidual Spaces and Reflexivity of Real Normed Spaces

52%
Narita K., Endou N., Shidama Y.
Formalized Mathematics
|
2014
|
tom 22
|
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].
20
Content available remote

Higher-Order Partial Differentiation

52%
Endou N., Okazaki H., Shidama Y.
Formalized Mathematics
|
2012
|
tom 20
|
nr 2
113-124
EN
In this article, we shall extend the formalization of [10] to discuss higher-order partial differentiation of real valued functions. The linearity of this operator is also proved (refer to [10], [12] and [13] for partial differentiation).
first rewind previous Strona / 3 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ć.