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

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

Wyniki wyszukiwania

help Sortuj według:

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

The Differentiable Functions from R intoR n

100%
Narita K., Korniłowicz A., Shidama Y.
Formalized Mathematics
|
2012
|
tom 20
|
nr 1
65-71
EN
In control engineering, differentiable partial functions from R into Rn play a very important role. In this article, we formalized basic properties of such functions.
2
Content available remote

More on the Continuity of Real Functions

100%
Narita K., Kornilowicz A., Shidama Y.
Formalized Mathematics
|
2011
|
tom 19
|
nr 4
233-239
EN
In this article we demonstrate basic properties of the continuous functions from R to Rn which correspond to state space equations in control engineering.
3
Content available remote

F. Riesz Theorem

100%
Narita K., Nakasho K., Shidama Y.
Formalized Mathematics
|
2017
|
tom 25
|
nr 3
179-184
EN
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].
4
Content available remote

Fatou's Lemma and the Lebesgue's Convergence Theorem

100%
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
5
Content available remote

Integral of Complex-Valued Measurable Function

100%
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
6
Content available remote

Compactness in Metric Spaces

100%
Nakasho K., Narita K., Shidama Y.
Formalized Mathematics
|
2016
|
tom 24
|
nr 3
167-172
EN
In this article, we mainly formalize in Mizar [2] the equivalence among a few compactness definitions of metric spaces, norm spaces, and the real line. In the first section, we formalized general topological properties of metric spaces. We discussed openness and closedness of subsets in metric spaces in terms of convergence of element sequences. In the second section, we firstly formalize the definition of sequentially compact, and then discuss the equivalence of compactness, countable compactness, sequential compactness, and totally boundedness with completeness in metric spaces. In the third section, we discuss compactness in norm spaces. We formalize the equivalence of compactness and sequential compactness in norm space. In the fourth section, we formalize topological properties of the real line in terms of convergence of real number sequences. In the last section, we formalize the equivalence of compactness and sequential compactness in the real line. These formalizations are based on [20], [5], [17], [14], and [4].
7
Content available remote

Dual Spaces and Hahn-Banach Theorem

100%
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].
8
Content available remote

Bidual Spaces and Reflexivity of Real Normed Spaces

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

The Basic Existence Theorem of Riemann-Stieltjes Integral

100%
Nakasho K., Narita K., Shidama Y.
Formalized Mathematics
|
2016
|
tom 24
|
nr 4
253-259
EN
In this article, the basic existence theorem of Riemann-Stieltjes integral is formalized. This theorem states that if f is a continuous function and ρ is a function of bounded variation in a closed interval of real line, f is Riemann-Stieltjes integrable with respect to ρ. In the first section, basic properties of real finite sequences are formalized as preliminaries. In the second section, we formalized the existence theorem of the Riemann-Stieltjes integral. These formalizations are based on [15], [12], [10], and [11].
10
Content available remote

Lebesgue's Convergence Theorem of Complex-Valued Function

100%
Narita K., Endou N., Shidama Y.
Formalized Mathematics
|
2009
|
tom 17
|
nr 2
137-145
EN
In this article, we formalized Lebesgue's Convergence theorem of complex-valued function. We proved Lebesgue's Convergence Theorem of realvalued function using the theorem of extensional real-valued function. Then applying the former theorem to real part and imaginary part of complex-valued functional sequences, we proved Lebesgue's Convergence Theorem of complex-valued function. We also defined partial sums of real-valued functional sequences and complex-valued functional sequences and showed their properties. In addition, we proved properties of complex-valued simple functions.
11
Content available remote

The Measurability of Complex-Valued Functional Sequences

100%
Narita K., Endou N., Shidama Y.
Formalized Mathematics
|
2009
|
tom 17
|
nr 2
89-97
EN
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.
12
Content available remote

Riemann-Stieltjes Integral

100%
Narita K., Nakasho K., Shidama Y.
Formalized Mathematics
|
2016
|
tom 24
|
nr 3
199-204
EN
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].
13
Content available remote

The First Mean Value Theorem for Integrals

100%
Narita K., Endou N., Shidama Y.
Formalized Mathematics
|
2008
|
tom 16
|
nr 1
51-55
EN
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
14
Content available remote

Egoroff's Theorem

100%
Endou N., Shidama Y., Narita K.
Formalized Mathematics
|
2008
|
tom 16
|
nr 1
57-63
EN
The goal of this article is to prove Egoroff's Theorem [13]. However, there are not enough theorems related to sequence of measurable functions in Mizar Mathematical Library. So we proved many theorems about them. At the end of this article, we showed Egoroff's theorem.MML identifier: MESFUNC8, version: 7.8.10 4.100.1011
15
Content available remote

Differentiable Functions into Real Normed Spaces

100%
Okazaki H., Endou N., Narita K., Shidama Y.
Formalized Mathematics
|
2011
|
tom 19
|
nr 2
69-72
EN
In this article, we formalize the differentiability of functions from the set of real numbers into a normed vector space [14].
16
Content available remote

The Orthogonal Projection and the Riesz Representation Theorem

100%
Narita K., Endou N., Shidama Y.
Formalized Mathematics
|
2015
|
tom 23
|
nr 3
243-252
EN
In this article, the orthogonal projection and the Riesz representation theorem are mainly formalized. In the first section, we defined the norm of elements on real Hilbert spaces, and defined Mizar functor RUSp2RNSp, real normed spaces as real Hilbert spaces. By this definition, we regarded sequences of real Hilbert spaces as sequences of real normed spaces, and proved some properties of real Hilbert spaces. Furthermore, we defined the continuity and the Lipschitz the continuity of functionals on real Hilbert spaces. Referring to the article [15], we also defined some definitions on real Hilbert spaces and proved some theorems for defining dual spaces of real Hilbert spaces. As to the properties of all definitions, we proved that they are equivalent properties of functionals on real normed spaces. In Sec. 2, by the definitions [11], we showed properties of the orthogonal complement. Then we proved theorems on the orthogonal decomposition of elements of real Hilbert spaces. They are the last two theorems of existence and uniqueness. In the third and final section, we defined the kernel of linear functionals on real Hilbert spaces. By the last three theorems, we showed the Riesz representation theorem, existence, uniqueness, and the property of the norm of bounded linear functionals on real Hilbert spaces. We referred to [36], [9], [24] and [3] in the formalization.
17
Content available remote

The Lebesgue Monotone Convergence Theorem

100%
Endou N., Narita K., Shidama Y.
Formalized Mathematics
|
2008
|
tom 16
|
nr 2
167-175
EN
In this article we prove the Monotone Convergence Theorem [16].MML identifier: MESFUNC9, version: 7.8.10 4.100.1011
18
Content available remote

Differential Equations on Functions from R into Real Banach Space

100%
Narita K., Endou N., Shidama Y.
Formalized Mathematics
|
2013
|
tom 21
|
nr 4
261-272
EN
In this article, we describe the differential equations on functions from R into real Banach space. The descriptions are based on the article [20]. As preliminary to the proof of these theorems, we proved some properties of differentiable functions on real normed space. For the proof we referred to descriptions and theorems in the article [21] and the article [32]. And applying the theorems of Riemann integral introduced in the article [22], we proved the ordinary differential equations on real Banach space. We referred to the methods of proof in [30].
19
Content available remote

The Linearity of Riemann Integral on Functions from ℝ into Real Banach Space

100%
Narita K., Endou N., Shidama Y.
Formalized Mathematics
|
2013
|
tom 21
|
nr 3
185-191
EN
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.
20
Content available remote

Riemann Integral of Functions from ℝ into Real Banach Space

100%
Narita K., Endou N., Shidama Y.
Formalized Mathematics
|
2013
|
tom 21
|
nr 2
145-152
EN
In this article we deal with the Riemann integral of functions from R into a real Banach space. The last theorem establishes the integrability of continuous functions on the closed interval of reals. To prove the integrability we defined uniform continuity for functions from R into a real normed space, and proved related theorems. We also stated some properties of finite sequences of elements of a real normed space and finite sequences of real numbers. In addition we proved some theorems about the convergence of sequences. We applied definitions introduced in the previous article [21] to the proof of integrability.
first rewind previous Strona / 2 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ć.