The Riesz Representation Theorem

Michikazu Hirata 📧

June 4, 2024

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


We formalize the Riesz-Markov-Kakutani representation theorem following pp.37-47 of the book Real and Complex Analysis by Rudin. This entry also includes formalization of regular measures, tightness of measures, and Urysohn's lemma on locally compact Hausdorff spaces. Roughly speaking, the theorem states that if $\varphi$ is a positive linear functional from $C(X)$ (the space of continuous functions from $X$ to complex numbers which have compact supports) to complex numbers, then there exists a unique measure $\mu$ such that for all $f\in C(X)$, \[\varphi(f) = \int f \mathrm{d}\mu.\]


BSD License


Session Riesz_Representation