The Measurability of Complex-Valued Functional Sequences

Narita, Keiko; Endou, Noboru; Shidama, Yasunari

doi:10.2478/v10037-009-0010-1

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

The Measurability of Complex-Valued Functional Sequences

Abstract

Paradigm

My account