DSpace Kolekcja:http://hdl.handle.net/11320/47992020-11-29T07:27:03Z2020-11-29T07:27:03ZExtended Real-Valued Double Sequence and Its ConvergenceEndou, Noboruhttp://hdl.handle.net/11320/48992017-10-05T22:59:29Z2015-01-01T00:00:00ZTytuł: Extended Real-Valued Double Sequence and Its Convergence
Autorzy: Endou, Noboru
Abstrakt: AbstractIn 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.2015-01-01T00:00:00ZThe Orthogonal Projection and the Riesz Representation TheoremNarita, KeikoEndou, NoboruShidama, Yasunarihttp://hdl.handle.net/11320/48982017-10-05T22:59:30Z2015-01-01T00:00:00ZTytuł: The Orthogonal Projection and the Riesz Representation Theorem
Autorzy: Narita, Keiko; Endou, Noboru; Shidama, Yasunari
Abstrakt: AbstractIn 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.2015-01-01T00:00:00ZConvergent Filter BasesCoghetto, Rolandhttp://hdl.handle.net/11320/48942017-10-05T22:59:25Z2015-01-01T00:00:00ZTytuł: Convergent Filter Bases
Autorzy: Coghetto, Roland
Abstrakt: AbstractWe are inspired by the work of Henri Cartan [16], Bourbaki [10] (TG. I Filtres) and Claude Wagschal [34]. We define the base of filter, image filter, convergent filter bases, limit filter and the filter base of tails (fr: filtre des sections).2015-01-01T00:00:00ZPolynomially Bounded Sequences and Polynomial SequencesOkazaki, HiroyukiFuta, Yuichihttp://hdl.handle.net/11320/48952017-10-05T22:59:26Z2015-01-01T00:00:00ZTytuł: Polynomially Bounded Sequences and Polynomial Sequences
Autorzy: Okazaki, Hiroyuki; Futa, Yuichi
Abstrakt: AbstractIn this article, we formalize polynomially bounded sequences that plays an important role in computational complexity theory. Class P is a fundamental computational complexity class that contains all polynomial-time decision problems [11], [12]. It takes polynomially bounded amount of computation time to solve polynomial-time decision problems by the deterministic Turing machine. Moreover we formalize polynomial sequences [5].2015-01-01T00:00:00Z