| This thesis investigates aspects of functional analysis and measure theory, as well as the mean and pointwise ergodic theorems in the foundational context of subsystems of second-order arithmetic. The chapter on functional analysis discusses some properties of Banach and Hilbert spaces, such as existence of orthogonal projections and properties of bounded linear functionals. The chapter on measure theory contains a development of the theory L p spaces, while special attention is paid to the space L1(X), of integrable functions over a compact metric space. Using the results from these chapters, we show that the mean ergodic theorem is equivalent to arithmetic comprehension over the base theory RCA0. We consider three distinct proofs of the pointwise ergodic theorem, each of which raises different issues in formalization. We show that the pointwise ergodic theorem is also equivalent to arithmetic comprehension over RCA0. |
