The Orthogonal Projection and the Riesz Representation Theorem

Keiko Narita; Noboru Endou; Yasunari Shidama

Formalized Mathematics (2015)

  • Volume: 23, Issue: 3, page 243-252
  • ISSN: 1426-2630

Abstract

top
In this article, the orthogonal projection and the Riesz representation theorem are mainly formalized. In the first section, we defined the norm of elements on real Hilbert spaces, and defined Mizar functor RUSp2RNSp, real normed spaces as real Hilbert spaces. By this definition, we regarded sequences of real Hilbert spaces as sequences of real normed spaces, and proved some properties of real Hilbert spaces. Furthermore, we defined the continuity and the Lipschitz the continuity of functionals on real Hilbert spaces. Referring to the article [15], we also defined some definitions on real Hilbert spaces and proved some theorems for defining dual spaces of real Hilbert spaces. As to the properties of all definitions, we proved that they are equivalent properties of functionals on real normed spaces. In Sec. 2, by the definitions [11], we showed properties of the orthogonal complement. Then we proved theorems on the orthogonal decomposition of elements of real Hilbert spaces. They are the last two theorems of existence and uniqueness. In the third and final section, we defined the kernel of linear functionals on real Hilbert spaces. By the last three theorems, we showed the Riesz representation theorem, existence, uniqueness, and the property of the norm of bounded linear functionals on real Hilbert spaces. We referred to [36], [9], [24] and [3] in the formalization.

How to cite

top

Keiko Narita, Noboru Endou, and Yasunari Shidama. "The Orthogonal Projection and the Riesz Representation Theorem." Formalized Mathematics 23.3 (2015): 243-252. <http://eudml.org/doc/276402>.

@article{KeikoNarita2015,
abstract = {In this article, the orthogonal projection and the Riesz representation theorem are mainly formalized. In the first section, we defined the norm of elements on real Hilbert spaces, and defined Mizar functor RUSp2RNSp, real normed spaces as real Hilbert spaces. By this definition, we regarded sequences of real Hilbert spaces as sequences of real normed spaces, and proved some properties of real Hilbert spaces. Furthermore, we defined the continuity and the Lipschitz the continuity of functionals on real Hilbert spaces. Referring to the article [15], we also defined some definitions on real Hilbert spaces and proved some theorems for defining dual spaces of real Hilbert spaces. As to the properties of all definitions, we proved that they are equivalent properties of functionals on real normed spaces. In Sec. 2, by the definitions [11], we showed properties of the orthogonal complement. Then we proved theorems on the orthogonal decomposition of elements of real Hilbert spaces. They are the last two theorems of existence and uniqueness. In the third and final section, we defined the kernel of linear functionals on real Hilbert spaces. By the last three theorems, we showed the Riesz representation theorem, existence, uniqueness, and the property of the norm of bounded linear functionals on real Hilbert spaces. We referred to [36], [9], [24] and [3] in the formalization.},
author = {Keiko Narita, Noboru Endou, Yasunari Shidama},
journal = {Formalized Mathematics},
keywords = {normed linear spaces; Banach spaces; duality; orthogonal projection; Riesz representation},
language = {eng},
number = {3},
pages = {243-252},
title = {The Orthogonal Projection and the Riesz Representation Theorem},
url = {http://eudml.org/doc/276402},
volume = {23},
year = {2015},
}

TY - JOUR
AU - Keiko Narita
AU - Noboru Endou
AU - Yasunari Shidama
TI - The Orthogonal Projection and the Riesz Representation Theorem
JO - Formalized Mathematics
PY - 2015
VL - 23
IS - 3
SP - 243
EP - 252
AB - In this article, the orthogonal projection and the Riesz representation theorem are mainly formalized. In the first section, we defined the norm of elements on real Hilbert spaces, and defined Mizar functor RUSp2RNSp, real normed spaces as real Hilbert spaces. By this definition, we regarded sequences of real Hilbert spaces as sequences of real normed spaces, and proved some properties of real Hilbert spaces. Furthermore, we defined the continuity and the Lipschitz the continuity of functionals on real Hilbert spaces. Referring to the article [15], we also defined some definitions on real Hilbert spaces and proved some theorems for defining dual spaces of real Hilbert spaces. As to the properties of all definitions, we proved that they are equivalent properties of functionals on real normed spaces. In Sec. 2, by the definitions [11], we showed properties of the orthogonal complement. Then we proved theorems on the orthogonal decomposition of elements of real Hilbert spaces. They are the last two theorems of existence and uniqueness. In the third and final section, we defined the kernel of linear functionals on real Hilbert spaces. By the last three theorems, we showed the Riesz representation theorem, existence, uniqueness, and the property of the norm of bounded linear functionals on real Hilbert spaces. We referred to [36], [9], [24] and [3] in the formalization.
LA - eng
KW - normed linear spaces; Banach spaces; duality; orthogonal projection; Riesz representation
UR - http://eudml.org/doc/276402
ER -

References

top
  1. [1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990. Zbl06213858
  2. [2] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990. 
  3. [3] Haim Brezis. Functional Analysis, Sobolev Spaces and Partial Differential Equations. Springer, 2011. 
  4. [4] Czesław Bylinski. The complex numbers. Formalized Mathematics, 1(3):507-513, 1990. 
  5. [5] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990. 
  6. [6] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990. 
  7. [7] Czesław Bylinski. Partial functions. Formalized Mathematics, 1(2):357-367, 1990. 
  8. [8] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990. 
  9. [9] Peter D. Dax. Functional Analysis. Pure and Applied Mathematics: A Wiley Series of Texts, Monographs and Tracts. Wiley Interscience, 2002. 
  10. [10] Noboru Endou, Takashi Mitsuishi, and Yasunari Shidama. Subspaces and cosets of subspace of real unitary space. Formalized Mathematics, 11(1):1-7, 2003. 
  11. [11] Noboru Endou, Takashi Mitsuishi, and Yasunari Shidama. Topology of real unitary space. Formalized Mathematics, 11(1):33-38, 2003. 
  12. [12] Noboru Endou, Yasumasa Suzuki, and Yasunari Shidama. Real linear space of real sequences. Formalized Mathematics, 11(3):249-253, 2003. 
  13. [13] Jarosław Kotowicz. Convergent sequences and the limit of sequences. Formalized Mathematics, 1(2):273-275, 1990. 
  14. [14] Jarosław Kotowicz. Convergent real sequences. Upper and lower bound of sets of real numbers. Formalized Mathematics, 1(3):477-481, 1990. 
  15. [15] Keiko Narita, Noboru Endou, and Yasunari Shidama. Dual spaces and Hahn-Banach theorem. Formalized Mathematics, 22(1):69-77, 2014. doi:10.2478/forma-2014-0007.[Crossref] Zbl1298.46005
  16. [16] Adam Naumowicz. Conjugate sequences, bounded complex sequences and convergent complex sequences. Formalized Mathematics, 6(2):265-268, 1997. 
  17. [17] Takaya Nishiyama, Keiji Ohkubo, and Yasunari Shidama. The continuous functions on normed linear spaces. Formalized Mathematics, 12(3):269-275, 2004. 
  18. [18] Bogdan Nowak and Andrzej Trybulec. Hahn-Banach theorem. Formalized Mathematics, 4(1):29-34, 1993. 
  19. [19] Jan Popiołek. Some properties of functions modul and signum. Formalized Mathematics, 1(2):263-264, 1990. 
  20. [20] Jan Popiołek. Introduction to Banach and Hilbert spaces - part I. Formalized Mathematics, 2(4):511-516, 1991. 
  21. [21] Jan Popiołek. Introduction to Banach and Hilbert spaces - part II. Formalized Mathematics, 2(4):517-521, 1991. 
  22. [22] Jan Popiołek. Introduction to Banach and Hilbert spaces - part III. Formalized Mathematics, 2(4):523-526, 1991. 
  23. [23] Jan Popiołek. Real normed space. Formalized Mathematics, 2(1):111-115, 1991. 
  24. [24] Walter Rudin. Functional Analysis. New York, McGraw-Hill, 2nd edition, 1991. 
  25. [25] Yasunari Shidama. Banach space of bounded linear operators. Formalized Mathematics, 12(1):39-48, 2004. 
  26. [26] Yasumasa Suzuki, Noboru Endou, and Yasunari Shidama. Banach space of absolute summable real sequences. Formalized Mathematics, 11(4):377-380, 2003. 
  27. [27] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1 (2):329-334, 1990. 
  28. [28] Andrzej Trybulec. On the sets inhabited by numbers. Formalized Mathematics, 11(4): 341-347, 2003. 
  29. [29] Andrzej Trybulec and Czesław Bylinski. Some properties of real numbers. Formalized Mathematics, 1(3):445-449, 1990. 
  30. [30] Wojciech A. Trybulec. Subspaces and cosets of subspaces in real linear space. Formalized Mathematics, 1(2):297-301, 1990. 
  31. [31] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296, 1990. 
  32. [32] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990. 
  33. [33] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990. 
  34. [34] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181-186, 1990. 
  35. [35] Hiroshi Yamazaki, Yasumasa Suzuki, Takao Inou´e, and Yasunari Shidama. On some properties of real Hilbert space. Part I. Formalized Mathematics, 11(3):225-229, 2003. 
  36. [36] Kosaku Yoshida. Functional Analysis. Springer, 1980. 

NotesEmbed ?

top

You must be logged in to post comments.