  This thesis presents a formalization of martingales in arbitrary Banach
spaces using Isabelle/HOL. We begin by examining formalizations in prominent
proof repositories and extend the definition of the conditional expectation
operator from the real numbers to general Banach spaces. The current
formalization of conditional expectation in the Isabelle library is limited to
real-valued functions. To overcome this limitation, we use measure theoretic
arguments to construct the conditional expectation in Banach spaces using
suitable limits of simple functions. Subsequently, we define stochastic
processes and introduce the concepts of adapted, progressively measurable and
predictable processes using suitable locale definitions. We show the relation
$$\text{adapted} \supseteq \text{progressive} \supseteq \text{predictable}$$
Furthermore, we show that progressive measurability and adaptedness are
equivalent when the indexing set is discrete. We pay special attention to
predictable processes in discrete-time, showing that $(X_n)_{n \in \mathbb{N}}$
is predictable if and only if $(X_{n + 1})_{n \in \mathbb{N}}$ is adapted.
  We rigorously define martingales, submartingales, and supermartingales,
presenting their first consequences and corollaries. Discrete-time martingales
are given special attention in the formalization. In every step of our
formalization, we make extensive use of the powerful locale system of Isabelle.
  The formalization further contributes by generalizing concepts in Bochner
integration by extending their application from the real numbers to arbitrary
Banach spaces equipped with a second-countable topology. Induction schemes for
integrable simple functions on Banach spaces are introduced. Additionally, we
formalize a powerful result called the "Averaging Theorem" which allows us to
show that densities are unique in Banach spaces.
