On L 1 Space Formed by Complex-Valued Partial Functions

Yasushige Watase; Noboru Endou; Yasunari Shidama

Formalized Mathematics (2012)

  • Volume: 20, Issue: 4, page 349-357
  • ISSN: 1426-2630

Abstract

top
In this article, we formalized L1 space formed by complexvalued partial functions [11], [15]. The real-valued case was formalized in [22] and this article is its generalization.

How to cite

top

Yasushige Watase, Noboru Endou, and Yasunari Shidama. " On L 1 Space Formed by Complex-Valued Partial Functions ." Formalized Mathematics 20.4 (2012): 349-357. <http://eudml.org/doc/267630>.

@article{YasushigeWatase2012,
abstract = {In this article, we formalized L1 space formed by complexvalued partial functions [11], [15]. The real-valued case was formalized in [22] and this article is its generalization.},
author = {Yasushige Watase, Noboru Endou, Yasunari Shidama},
journal = {Formalized Mathematics},
language = {eng},
number = {4},
pages = {349-357},
title = { On L 1 Space Formed by Complex-Valued Partial Functions },
url = {http://eudml.org/doc/267630},
volume = {20},
year = {2012},
}

TY - JOUR
AU - Yasushige Watase
AU - Noboru Endou
AU - Yasunari Shidama
TI - On L 1 Space Formed by Complex-Valued Partial Functions
JO - Formalized Mathematics
PY - 2012
VL - 20
IS - 4
SP - 349
EP - 357
AB - In this article, we formalized L1 space formed by complexvalued partial functions [11], [15]. The real-valued case was formalized in [22] and this article is its generalization.
LA - eng
UR - http://eudml.org/doc/267630
ER -

References

top
  1. [1] Jonathan Backer, Piotr Rudnicki, and Christoph Schwarzweller. Ring ideals. FormalizedMathematics, 9(3):565-582, 2001. 
  2. [2] Józef Białas. Series of positive real numbers. Measure theory. Formalized Mathematics, 2(1):173-183, 1991. 
  3. [3] Józef Białas. The _-additive measure theory. Formalized Mathematics, 2(2):263-270, 1991. 
  4. [4] Czesław Bylinski. Binary operations. Formalized Mathematics, 1(1):175-180, 1990. 
  5. [5] Czesław Bylinski. The complex numbers. Formalized Mathematics, 1(3):507-513, 1990. 
  6. [6] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990. 
  7. [7] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990. 
  8. [8] Czesław Bylinski. Partial functions. Formalized Mathematics, 1(2):357-367, 1990. 
  9. [9] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990. 
  10. [10] Noboru Endou. Complex linear space and complex normed space. Formalized Mathematics, 12(2):93-102, 2004. 
  11. [11] P. R. Halmos. Measure Theory. Springer-Verlag, 1974. Zbl0283.28001
  12. [12] 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. 
  13. [13] 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.[Crossref] Zbl1298.26030
  14. [14] Andrzej Nedzusiak. _-fields and probability. Formalized Mathematics, 1(2):401-407, 1990. 
  15. [15] Walter Rudin. Real and Complex Analysis. Mc Graw-Hill, Inc., 1974. 
  16. [16] Yasunari Shidama and Noboru Endou. Integral of real-valued measurable function. FormalizedMathematics, 14(4):143-152, 2006, doi:10.2478/v10037-006-0018-8.[Crossref] Zbl1298.26030
  17. [17] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1(2):329-334, 1990. 
  18. [18] Andrzej Trybulec. On the sets inhabited by numbers. Formalized Mathematics, 11(4):341-347, 2003. 
  19. [19] Andrzej Trybulec and Agata Darmochwał. Boolean domains. Formalized Mathematics, 1(1):187-190, 1990. 
  20. [20] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296, 1990. 
  21. [21] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990. 
  22. [22] Yasushige Watase, Noboru Endou, and Yasunari Shidama. On L1 space formed by real-valued partial functions. Formalized Mathematics, 16(4):361-369, 2008, doi:10.2478/v10037-008-0044-9.[Crossref] Zbl1283.46024
  23. [23] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73-83, 1990. 
  24. [24] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181-186, 1990. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.