<abstract xml:lang="en" xmlns="http://www.w3.org/1999/xhtml"><p>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.</p></abstract>

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.

Lebesgue's Convergence Theorem of Complex-Valued Function

Gifu National College of Technology, Japan

Formalized Mathematics

{"article-title":"Lebesgue's Convergence Theorem of Complex-Valued Function"}

In this article, we formalized Lebesgue's Convergence theorem of complex-valued function. We proved Lebesgue's Convergence Theorem of realvalued function using...

Lebesgue's Convergence Theorem of Complex-Valued Function

Data publikacji: 14 lip 2009

Zakres stron: 137 - 145

DOI: https://doi.org/10.2478/v10037-009-0015-9

This content is open access.