Page 1

Displaying 1 – 7 of 7

Showing per page

Integral of Complex-Valued Measurable Function

Keiko Narita, Noboru Endou, Yasunari Shidama (2008)

Formalized Mathematics

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

Integral of Real-Valued Measurable Function 1

Yasunari Shidama, Noboru Endou (2006)

Formalized Mathematics

Based on [16], authors formalized the integral of an extended real valued measurable function in [12] before. However, the integral argued in [12] cannot be applied to real-valued functions unconditionally. Therefore, in this article we have formalized the integral of a real-value function.

Currently displaying 1 – 7 of 7

Page 1