The orthogonal projection and the Riesz representation theorem

DOI10.1515/forma-2015-0020zbMath1321.46022OpenAlexW2294649372MaRDI QIDQ500027

Noboru Endou, Yasunari Shidama, Keiko Narita

Publication date: 7 October 2015

Published in: Formalized Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1515/forma-2015-0020

zbMATH Keywords

Banach spacesdualitynormed linear spacesorthogonal projectionRiesz representation

Mathematics Subject Classification ID

Hilbert and pre-Hilbert spaces: geometry and topology (including spaces with semidefinite inner product) (46C05) Mechanization of proofs and logical operations (03B35) Hilbert spaces of continuous, differentiable or analytic functions (46E20)

Related Items (6)

Construction of measure from semialgebra of sets ⋮ Product pre-measure ⋮ Integral of non positive functions ⋮ Double sequences and limits ⋮ Double series and sums ⋮ Extended real-valued double sequence and its convergence

Uses Software

• Mizar

Cites Work

• Dual spaces and Hahn-Banach theorem
• Functional analysis, Sobolev spaces and partial differential equations
• Semantics of MML Query - Ordering
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: The orthogonal projection and the Riesz representation theorem