A Formal Proof Of The Riesz Representation Theorem
DOI:
https://doi.org/10.6092/issn.1972-5787/1952Abstract
This paper presents a formal proof of the Riesz representation theorem in the PVS theorem prover. The Riemann Stieltjes integral was defined in PVS, and the theorem relies on this integral. In order to prove the Riesz representation theorem, it was necessary to prove that continuous functions on a closed interval are Riemann Stieltjes integrable with respect to any function of bounded variation. This result follows from the equivalence of the Riemann Stieltjes and Darboux Stieltjes integrals, which would have been a lengthy result to prove in PVS, so a simpler lemma was proved that captures the underlying concept of this integral equivalence. In order to prove the Riesz theorem, the Hahn Banach theorem was proved in the case where the normed linear spaces are the continuous and bounded functions on a closed interval. The proof of the Riesz theorem follows the proof in Haaser and Sullivan's book Real Analysis. The formal proof of this result in PVS revealed an error in textbook's proof. Indeed, the proof of the Riesz representation theorem is constructive, and the function contstructed in the textbook does not satsify a key property. This error illustrates the ability of formal verification to find logical errors. A specific counterexample is given to the proof in the textbook. Finally, a corrected proof of the Riesz representation theorem is presented.Downloads
Published
2011-04-14
How to Cite
Narkawicz, A. (2011). A Formal Proof Of The Riesz Representation Theorem. Journal of Formalized Reasoning, 4(1), 1–24. https://doi.org/10.6092/issn.1972-5787/1952
Issue
Section
Articles
License
Copyright (c) 2011 Anthony Narkawicz
Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.
This journal is licensed under a Creative Commons Attribution 3.0 Unported License (full legal code).
See also our Open Access policy