On L p Space Formed by Real-Valued Partial Functions

Yasushige Watase; Noboru Endou; Yasunari Shidama

Formalized Mathematics (2010)

  • Volume: 18, Issue: 3, page 159-169
  • ISSN: 1426-2630

Abstract

top
This article is the continuation of [31]. We define the set of Lp integrable functions - the set of all partial functions whose absolute value raised to the p-th power is integrable. We show that Lp integrable functions form the Lp space. We also prove Minkowski's inequality, Hölder's inequality and that Lp space is Banach space ([15], [27]).

How to cite

top

Yasushige Watase, Noboru Endou, and Yasunari Shidama. " On L p Space Formed by Real-Valued Partial Functions ." Formalized Mathematics 18.3 (2010): 159-169. <http://eudml.org/doc/266976>.

@article{YasushigeWatase2010,
abstract = {This article is the continuation of [31]. We define the set of Lp integrable functions - the set of all partial functions whose absolute value raised to the p-th power is integrable. We show that Lp integrable functions form the Lp space. We also prove Minkowski's inequality, Hölder's inequality and that Lp space is Banach space ([15], [27]).},
author = {Yasushige Watase, Noboru Endou, Yasunari Shidama},
journal = {Formalized Mathematics},
language = {eng},
number = {3},
pages = {159-169},
title = { On L p Space Formed by Real-Valued Partial Functions },
url = {http://eudml.org/doc/266976},
volume = {18},
year = {2010},
}

TY - JOUR
AU - Yasushige Watase
AU - Noboru Endou
AU - Yasunari Shidama
TI - On L p Space Formed by Real-Valued Partial Functions
JO - Formalized Mathematics
PY - 2010
VL - 18
IS - 3
SP - 159
EP - 169
AB - This article is the continuation of [31]. We define the set of Lp integrable functions - the set of all partial functions whose absolute value raised to the p-th power is integrable. We show that Lp integrable functions form the Lp space. We also prove Minkowski's inequality, Hölder's inequality and that Lp space is Banach space ([15], [27]).
LA - eng
UR - http://eudml.org/doc/266976
ER -

References

top
  1. [1] Jonathan Backer, Piotr Rudnicki, and Christoph Schwarzweller. Ring ideals. Formalized Mathematics, 9(3):565-582, 2001. 
  2. [2] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990. Zbl06213858
  3. [3] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990. 
  4. [4] Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Formalized Mathematics, 5(4):485-492, 1996. 
  5. [5] Józef Białas. Series of positive real numbers. Measure theory. Formalized Mathematics, 2(1):173-183, 1991. 
  6. [6] Józef Białas. The s-additive measure theory. Formalized Mathematics, 2(2):263-270, 1991. 
  7. [7] Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175-180, 1990. 
  8. [8] Czesław Byliński. The complex numbers. Formalized Mathematics, 1(3):507-513, 1990. 
  9. [9] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990. 
  10. [10] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990. 
  11. [11] Czesław Byliński. Partial functions. Formalized Mathematics, 1(2):357-367, 1990. 
  12. [12] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990. 
  13. [13] Noboru Endou and Yasunari Shidama. Integral of measurable function. Formalized Mathematics, 14(2):53-70, 2006, doi:10.2478/v10037-006-0008-x.[Crossref] 
  14. [14] Noboru Endou, Yasunari Shidama, and Keiko Narita. Egoroff's theorem. Formalized Mathematics, 16(1):57-63, 2008, doi:10.2478/v10037-008-0009-z.[Crossref] Zbl1298.46005
  15. [15] P. R. Halmos. Measure Theory. Springer-Verlag, 1987. 
  16. [16] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35-40, 1990. 
  17. [17] Jarosław Kotowicz. Convergent sequences and the limit of sequences. Formalized Mathematics, 1(2):273-275, 1990. 
  18. [18] Jarosław Kotowicz. Real sequences and basic operations on them. Formalized Mathematics, 1(2):269-272, 1990. 
  19. [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.[Crossref] Zbl1298.26030
  20. [20] Keiko Narita, Noboru Endou, and Yasunari Shidama. Lebesgue's convergence theorem of complex-valued function. Formalized Mathematics, 17(2):137-145, 2009, doi: 10.2478/v10037-009-0015-9.[Crossref] Zbl1298.26030
  21. [21] Andrzej Nędzusiak. s-fields and probability. Formalized Mathematics, 1(2):401-407, 1990. 
  22. [22] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223-230, 1990. 
  23. [23] Beata Perkowska. Functional sequence from a domain to a domain. Formalized Mathematics, 3(1):17-21, 1992. 
  24. [24] Jan Popiołek. Real normed space. Formalized Mathematics, 2(1):111-115, 1991. 
  25. [25] Konrad Raczkowski and Andrzej Nędzusiak. Real exponents and logarithms. Formalized Mathematics, 2(2):213-216, 1991. 
  26. [26] Konrad Raczkowski and Andrzej Nędzusiak. Series. Formalized Mathematics, 2(4):449-452, 1991. 
  27. [27] Walter Rudin. Real and Complex Analysis. Mc Graw-Hill, Inc., 1974. 
  28. [28] 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.[Crossref] Zbl1298.26030
  29. [29] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296, 1990. 
  30. [30] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990. 
  31. [31] 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
  32. [32] 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.