Skip to main content

The Measurability of Complex-Valued Functional Sequences Cover

.blurhash-client-img { display: none !important; }

The Measurability of Complex-Valued Functional Sequences

Formalized Mathematics

Volume 17 (2009): Issue 2 (June 2009)

By: Keiko Narita, Noboru Endou and Yasunari Shidama

Open Access

|Jul 2009

Abstract

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.

References

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990.
Search in Google Scholar
[2] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990.
Search in Google Scholar
[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990.
Search in Google Scholar
[4] Józef Białas. Infimum and supremum of the set of real numbers. Measure theory. Formalized Mathematics, 2(1):163-171, 1991.
Search in Google Scholar
[5] Józef Białas. Series of positive real numbers. Measure theory. Formalized Mathematics, 2(1):173-183, 1991.
Search in Google Scholar
[6] Józef Białas. The σ-additive measure theory. Formalized Mathematics, 2(2):263-270, 1991.
Search in Google Scholar
[7] Józef Białas. Some properties of the intervals. Formalized Mathematics, 5(1):21-26, 1996.
Search in Google Scholar
[8] Czesław Byliński. The complex numbers. Formalized Mathematics, 1(3):507-513, 1990.
Search in Google Scholar
[9] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990.
Search in Google Scholar
[10] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.
Search in Google Scholar
[11] Czesław Byliński. Partial functions. Formalized Mathematics, 1(2):357-367, 1990.
Search in Google Scholar
[12] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.
Search in Google Scholar
[13] Wenpai Chang, Hiroshi Yamazaki, and Yatsuka Nakamura. The inner product and conjugate of finite sequences of complex numbers. Formalized Mathematics, 13(3):367-373, 2005.
Search in Google Scholar
[14] Noboru Endou and Yasunari Shidama. Integral of measurable function. Formalized Mathematics, 14(2):53-70, 2006, doi:10.2478/v10037-006-0008-x.10.2478/v10037-006-0008-x
Search in Google Scholar
[15] Noboru Endou, Yasunari Shidama, and Keiko Narita. Egoroff's theorem. Formalized Mathematics, 16(1):57-63, 2008, doi:10.2478/v10037-008-0009-z.10.2478/v10037-008-0009-z
Search in Google Scholar
[16] Noboru Endou, Katsumi Wasaki, and Yasunari Shidama. Definitions and basic properties of measurable functions. Formalized Mathematics, 9(3):495-500, 2001.
Search in Google Scholar
[17] Jarosław Kotowicz. Convergent sequences and the limit of sequences. Formalized Mathematics, 1(2):273-275, 1990.
Search in Google Scholar
[18] Jarosław Kotowicz and Yuji Sakai. Properties of partial functions from a domain to the set of real numbers. Formalized Mathematics, 3(2):279-288, 1992.
Search in Google Scholar
[19] Keiko Narita, Noboru Endou, and Yasunari Shidama. Integral of complex-valued measurable function. Formalized Mathematics, 16(4):319-324, 2008, doi:10.2478/v10037-008-0039-6.10.2478/v10037-008-0039-6
Search in Google Scholar
[20] Adam Naumowicz. Conjugate sequences, bounded complex sequences and convergent complex sequences. Formalized Mathematics, 6(2):265-268, 1997.
Search in Google Scholar
[21] Andrzej Nędzusiak. σ-fields and probability. Formalized Mathematics, 1(2):401-407, 1990.
Search in Google Scholar
[22] Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147-152, 1990.
Search in Google Scholar
[23] Beata Perkowska. Functional sequence from a domain to a domain. Formalized Mathematics, 3(1):17-21, 1992.
Search in Google Scholar
[24] Yasunari Shidama and Noboru Endou. Integral of real-valued measurable function. Formalized Mathematics, 14(4):143-152, 2006, doi:10.2478/v10037-006-0018-8.10.2478/v10037-006-0018-8
Search in Google Scholar
[25] Yasunari Shidama and Artur Korniłowicz. Convergence and the limit of complex sequences. Series. Formalized Mathematics, 6(3):403-410, 1997.
Search in Google Scholar
[26] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.
Search in Google Scholar
[27] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73-83, 1990.
Search in Google Scholar
[28] Hiroshi Yamazaki, Noboru Endou, Yasunari Shidama, and Hiroyuki Okazaki. Inferior limit, superior limit and convergence of sequences of extended real numbers. Formalized Mathematics, 15(4):231-236, 2007, doi:10.2478/v10037-007-0026-3.10.2478/v10037-007-0026-3
Search in Google Scholar

Articles in this issue

DOI: https://doi.org/10.2478/v10037-009-0010-1 | Journal eISSN: 1898-9934 | Journal ISSN: 1426-2630

Journal RSS Feed

Language: English

Page range: 89 - 97

Published on: Jul 14, 2009

Published by: University of Białystok

In partnership with: Paradigm Publishing Services

Publication frequency: 1 issue per year

Related subjects:

Logic and set theory,

Computer sciences,

Artificial intelligence

© 2009 Keiko Narita, Noboru Endou, Yasunari Shidama, published by University of Białystok
This work is licensed under the Creative Commons License.

Volume 17 (2009): Issue 2 (June 2009)