Formalization of a Stochastic Approximation Theorem

We first introduce pre_events ✿ which are just subsets of a type T i.e., maps T $\rightarrow\;$ Prop. Then we define $\sigma$-algebras, SigmaAlgebra(T) ✿, as collections of pre_events which are closed under countable union and complement and include the full subset of all elements in T:

Then, we label pre_events which are members of a $\sigma$-algebra as events ✿. Special $\sigma$-algebras, like that generated by a set of pre_events ✿ and the Borel $\sigma$-algebra ✿, are constructed as usual.

One interesting feature of the formalization of both of these is that they are both provided with alternative characterizations, which is useful for using the definitions. For the borel $\sigma$-algebra, we define two variants: borel_sa ✿, defined as the $\sigma$-algebra generated by the half-open intervals, and open_borel_sa ✿, defined as the $\sigma$-algebra generated by the open sets. After proving that the definitions yield the same $\sigma$-algebra ✿, we can choose which definition is simpler to work with in a given context, simplifying some proofs.

For the definition of $\sigma(X)$, the $\sigma$-algebra generated by a set $X$, we start with the standard definition ✿: the intersection ✿ of the set of $\sigma$-algebras that contain $X$ ✿. This is useful, but as it is non-constructive, it lacks a convenient induction principle. As an alternative, we define the explicit closure of a set of events ✿, built by starting with the set (augmented by $\Omega$), and repeatedly adding in complements and countable unions. In Coq, this is naturally defined using an inductive data type. This closure is then shown to be (a $\sigma$-algebra ✿ and) equivalent to $\sigma(X)$ ✿.

While definitions generally use the standard definition of $\sigma(X)$, some theorems are more easily proven by switching to the equivalent closure-based characterization. This enables induction, providing an easy way to extend a property on the generating set to the generated $\sigma$-algebra, by showing that complements and countable unions preserve the property in question.

Next, we introduce probability spaces ✿ over a $\sigma$-algebra, equipped with a measure mapping each event to a real number $r$, such that $0\leq r\leq 1$.

The usual properties of probability spaces, such as monotonicity ✿, complements ✿, and non-disjoint unions ✿, are verified.

Having defined probability spaces, we can introduce a commonly used assertion in probabilistic proofs: that a certain property holds almost everywhere on a probability space. By this we mean the set of points where the property holds includes a measurable event of measure 1. We define a predicate almost ✿ to indicate propositions which hold almost everywhere. It is parameterized by a probability space and proposition on that space.

We have introduced machinery to make it more convenient to reason about almost propositions. For example, if we want to show that almost P $\rightarrow\;$ almost Q $\rightarrow\;$ almost R, we reduce the proof to showing that almost (P $\rightarrow\;$ Q $\rightarrow\;$ R) ✿, which itself is implied by P $\rightarrow\;$ Q $\rightarrow\;$ R ✿. Usual theorem proving tools can then be used.

On top of the basic almost definition, we defined almostR2 ✿, which says that a binary relation holds almost everywhere.

This is useful, since it inherits many properties from the base relation (e.g. it is a preorder if the base relation is ✿), and simplifies definitions.

We next introduce the concept of measurable functions with respect to two $\sigma$-algebras. Since we are focusing on probability spaces, we call these measurable functions RandomVariables ✿.

In order to define the Expectation of a RandomVariable, we follow the usual technique of first treating the case of finite range functions ✿, then extending to nonnegative functions ✿ (resulting in an extended real) and then to general random variables. In the general case, the expectation is the difference of the expectation of the positive and negative parts of a random variable. ✿ Exceptions are handled using the Coq option type. For example, the difference of the expectations of the positive and negative parts of a random variable is not defined if they are both the same infinity. This exception is captured by allowing the difference to be None in that case. A well defined Expectation yields Some r, for some value in Coquelicot’s Rbar type [16]. This represents a value in the extended reals: either a Finite real value, or positive or negative infinity (p_infty or m_infty).

Originally our results about Expectation were for random variables taking images in the reals, but as we introduced limiting processes we needed to extend our definition to random variables taking values in the extended reals (Rbar).

This requires extending the support for limits in Coquelicot, allowing for sequences of functions over the extended reals ✿. The approach we took was to copy over all the definitions and lemmas in Coquelicot’s Lim_seq module, extending them as appropriate, and re-proving them. A few changes were made, such as defining the extended version of is_lim_seq ✿ to hold when the inf and sup sequence limits coincide. The original definition uses filters, and is problematic to extend to the extended reals, since they do not form a uniform space. Pleasantly, however, almost all of the lemmas continue to hold with minor modification.

The above construction of Expectation and its properties (including linearity ✿✿, the monotone convergence theorem ✿, and other standard results) are then generalized and proven for this generalization to functions whose image is the extended reals ✿.

On top of our general definition of Expectation, we define the IsFiniteExpectation property, which asserts that a function has a well-defined, finite expectation ✿✿. For functions that satisfy this property, we can define their FiniteExpectation ✿✿, which returns their (real) expectation. This simplifies working with such functions, and avoids otherwise necessary side-conditions on properties such as linearity ✿✿.

Using these building blocks, we can define $L^{p}$ spaces, which are the space of measurable functions where the $p$-th power of its absolute value has finite expectation ✿.

This space is then quotiented, identifying functions that are equal almost everywhere (see Section 3.2) ✿. We use a quotient construction ✿ that avoids needing axioms beyond those already proposed in Coq’s standard libraries⁶⁶6Specifically, we use functional and propositional extensionality as well as constructive definite description (also known as the axiom of unique choice).. This quotienting operation is required in order to define a norm on the space (defined as the $p$-th root of the Expectation of the absolute value of the $p$-th power of the function), as having a zero Expectation only implies that a non-negative function is zero almost everywhere.

For nonnegative $p$, $L^{p}$ is shown to be a module space ✿. For $1\leq p\leq\infty$, it is shown to be a Banach space (complete normed module space) ✿ ✿.

Furthermore, the important special case of $L^{2}$ is proven to be a Hilbert space ✿, where the inner product of $x$ and $y$ is defined as the Expectation of the product of $x$ and $y$.

Building on top of this work, we turn to the definition of conditional expectation, defining it with respect to a general $\sigma$-algebra dom2 (the ambient $\sigma$-algebra being dom). We first postulate a relational definition ✿, characterized by the universal property of conditional expectations: for any event $P$ that is in the sub $\sigma$-algebra dom2, if we multiply the original function and its conditional expectation by that event’s associated indicator function, we get equal expectations.

Using this definition, we can show uniqueness (where equality is almost everywhere) ✿, and many standard properties of conditional expectation, such as linearity ✿✿, preservation of Expectation ✿, (almost) monotonicity ✿, and the tower law ✿. We also show the “factor out” property ✿, which enables factoring out of a conditional expectation a random variable that is measurable with respect to the sub $\sigma$-algebra. In addition, we verify its interactions with limits (e.g. the conditional version of the monotone convergence theorem ✿), and prove Jensen’s lemma ✿, bounding how convex functions affect the conditional expectation.

After having proven these properties for the is_conditional_expectation relation, we still need to show that the conditional expectation generally exists (at least for functions that are non-negative or have finite expectation).

To do this, we build on our work on $L^{p}$ spaces (Section 3.4), and in particular our proof that that $L^{2}$ is a Hilbert space. Given an $L^{2}$ function, this implies that the subset of functions which are measurable with respect to a smaller $\sigma$-algebra dom2 forms a linear subspace.

The $L^{2}$ conditional expectation ✿ of an $L^{2}$ random variable $X$ with respect to dom2 is then defined as the orthogonal projection ✿ of $X$ onto that subspace. For this construction and definitions of Hilbert spaces we use the library from the formal development of the Lax-Milgram theorem [14]. Note that this definition is for a function in the quotiented space (recall that $L^{2}$ is quotiented to identify functions that are equal almost everywhere).

We can then define conditional expectation on the unquotiented space by injecting the inputs into the quotiented space, using the conditional expectation operator just defined on $L^{2}$ functions, and then choosing a representative from the equivalence class of functions it returns ✿. This unquotienting gives insight into why most theorems about conditional expectations only almost hold, as it is defined on equivalence classes of almost equal functions.

Next, we extend our notion of conditional expectation to nonnegative functions whose usual expectation is finite using the property that $L^{2}$ functions are dense in $L^{1}$. In particular, given a nonnegative $L^{1}$ function $f$, we can define an $L^{2}$ sequence $g_{n}=\min(f,n)$. The conditional expectation of $f$ is defined as the limit of the conditional expectation of the $g_{n}$ ✿.

Using this definition directly has some disadvantages: it forces essentially all theorems, including simple ones such as the result being non-negative, or that the conditional expectation is the identity operation on functions that are already measurable with respect to the sub $\sigma$-algebra dom2, be only almost valid. To address this, we wrap this definition in a wrapper ✿ that takes the function returned by the original (limit based) definition and tweaks it slightly, producing a “fixed” function almost equivalent to the original, but where such simple properties hold unconditionally.

Finally, we extend this to all measurable functions by taking the difference of the nonnegative conditional expectation of its positive and negative parts ✿. While this function is defined for all measurable functions, it can only be shown to be a conditional expectation (the is_conditional_expectation relation defined above) for functions that are either non-negative ✿ or have finite expectation ✿. Using this property, we now lift all of the properties proven above for the relational version to our explicitly defined version, verifying that it satisfies all the expected properties. For convenience, we also provide a wrapper definition FiniteConditionalExpectation ✿, which assumes that the function has finite expectation, and returns a function whose image is in $\mathbb{R}$ (insted of the extended reals), and lift all the expected properties to it.

Connecting back to $L^{p}$ spaces, we can use Jensen’s lemma about convex functions to show that if a function is in $L^{p}$ then its conditional expectation is as well ✿, allowing us to view conditional expectation as a (contractive ✿) operation on $L^{p}$ spaces. Furthermore, we show that it minimizes the $L^{2}$-loss for an $L^{2}$ function  ✿.

We chose this approach to defining conditional expectation (via an orthonormal projection on $L^{2}$) since we could rely on an existing library of Hilbert space theory [14], thus avoiding other tedious constructions involving Radon-Nikodym derivatives etc.

We next introduce a notion of $\sigma$-algebra filtrations ✿, which are an increasing sequence of $\sigma$-algebras. We say that a sequence of random variables $X_{n}$ IsAdapted ✿ to a filtration $F_{n}$, if each random variable of the sequence is measurable with respect the corresponding $\sigma$-algebra.

Building on these definitions and our development of conditional expectation, we started developing the basics of martingale theory ✿.

Additionally, the language of filtrations and adapted processes enables us to represent the history of a stochastic process, which is critical for stating and verifying properties of stochastic approximation methods.

There are many other results proven in the library; here we highlight two that are used in the Derman-Sacks proof: Chebyshev’s inequality and the Borel-Cantelli lemma.

Chebyshev’s inequality ✿ which states that given a random variable $X$ and a positive constant $a$, the probability of $\|X\|\geq a$ is less that or equal to the expectation of $X^{2}/a^{2}$.

Another is the Borel-Cantelli lemma ✿ which states that if the sum of probabilities of a sequence of events is finite, then the probability of all but finitely many of them occuring is 0.

In this theorem statement, ex_series f, defined in Coquelicot, assert that the infinite series of partial sums $\lim_{n\to\infty}\sum_{0\leq i\leq n}f(i)$ converges to a finite limit.

In this section we discuss some of the design choices we made (and revisited), and our retrospective opinion on their impact. This may be of benefit to those seeking to pursue similar projects.

Initially, we modeled events as sets (now called pre_events), accompanying them with proofs that the set was in a given $\sigma$-algebra. This resulted in a lot of code threading and transforming these proofs, which was particularly painful when reasoning about lists. Revisiting that decision, we built up events as a subset type: a dependent pair of a pre_event and a proof that it belongs in a relevant $\sigma$-algebra ✿. For many simple uses, this obviates the need for reasoning explicitly about being in a $\sigma$-algebra. There are still cases where explicit reasoning is required, but this change definitely simplified the code.

We support general random variables using a typeclass which specifies the sigma algebras for the domain and range along with the function ✿. An initial version of our probability library developed expectation and properties of random variables whose codomain was the reals ✿. However as we proved more properties, especially limiting and convergence properties, it became clear that we needed to allow infinite values, thus to allow random variables with $\bar{\mathbb{R}}$ (the extended real numbers) as codomain ✿. However the native support for limits in the Coquelicot package allows the limiting value to be infinite, but restricts to sequences taking values in $\mathbb{R}$. In order to be able to take limits of random variables to $\bar{\mathbb{R}}$, we developed our own limit package extending the Coquelicot definitions and lemmas to sequences taking values in $\bar{\mathbb{R}}$ ✿. In the end, some results about $\bar{\mathbb{R}}$ valued random variables become simpler since one doesn’t need to make unnatural finiteness restrictions, but on the other hand, one needs to be extra careful, since $\bar{\mathbb{R}}$ is not a field as sums and products are not always defined and operations are not associative.

As in the standard development of expectation, we first defined it for functions whose range is a finite subset of $\mathbb{R}$ (or $\bar{\mathbb{R}}$). We decided to represent them as a typeclass which includes a field containing a finite list of values which includes all the values in the range of the function ✿.

We decided to allow this list to have duplicates and to contain additional values not in the range. This made several definitions more convenient, for example when defining the sum of two finite range functions, the new list of values is just the sum of all pairs of values, which is guaranteed to contain all the actual values, but can contain values which are not in the image of the sum and can contain duplicated values ✿.

One simplification our code makes is that we deal only with probability spaces, rather then general measures. This was a pragmatic decision, as it simplifies some of the proofs (since, for example, measures must be finite). As our intended use is probability theory, this mostly sufficed. In order to define (dependent) product spaces, we did define the rudiments of measure theory (measures, outer measures, and inner measures) ✿, but the final construction of the product is defined only for probability spaces, since the proof crucially relies on the monotone convergence theorem, which we have not proven for general measure spaces. It would clearly have been nicer to define things more generally, and we may go back and change things in the future, however this simplification allowed us to use our limited resources to greater effect.

The Derman-Sacks proof relies on a number of prerequisites in Probability Theory and Real Analysis. For example, the proof begins by stating that we may replace the series $\sum_{n}\mathbb{E}W_{n}^{2}<\infty$ by the series $\sum_{n}\frac{\mathbb{E}W_{n}^{2}}{\alpha_{n}^{2}}<\infty$ where $\alpha_{n}\to 0$. This statement invokes a classical theorem of du Bois-Reymond [13] which states:

In other words, this theorem states that no worst convergent series exists (see [5]). This elementary theorem did require some effort to formalize, in part because existing proofs such as the one in [5] require the sequence $(a_{n})$ to consist only of positive terms, while our application (Dvoretzky’s theorem) needed them to be non-negative. Additionally, we had to prove convergence of the product series without using the integral test (as used in [5]), because it was unavailable in our library. Our final proof of Theorem 4.1 involved a case analysis in which we case on whether the sequence $(a_{n})$ was eventually positive or not ✿, and we bypassed the need to use the integral test by using an exercise from Rudin’s Principles of Mathematical Analysis [31].

The main workhorse of the Derman-Sacks proof is the sequence $Z_{n}:=W_{n}\ \mathrm{sgn}\ T_{n}$. First, they apply the following theorem⁷⁷7the proof of this theorem is a modification of Theorem 6.2.1 in Ash’s Probability and Measure Theory [6] to the sequence of random variables $(Z_{n})$:

to conclude that the series $\sum_{n}Z_{n}$ converges almost surely. To apply this theorem we need to prove that $(Z_{n})$ is adapted to the filtration $\mathcal{F}$, which critically uses the fact that $T_{n}:\mathcal{H}^{n}\to\mathcal{H}$ is a measurable function. (Here we take $\mathcal{H}=\mathbb{R}$.) The proof of the theorem uses $\mathbb{E}[X_{n+1}\ |\ \mathcal{F}_{n}]=0$ to show that since the sequence is adapted, we have $\mathbb{E}[X_{i}X_{j}]=0$ for all $i\neq j$. This depends on the “factor out” property of conditional expectation ✿ (see Section 3.5).

Next, it is shown that $|Z_{n}|\leq\alpha_{n}$ almost surely for sufficiently large $n$. This argument uses the Borel-Cantelli lemma ✿ and the Chebyshev inequality ✿, both of which needed a significant amount of probability theory to be set up (see Section 3.7). Using this bound for $Z_{n}$ and the bound for $|T_{n}|$ in the hypothesis, an elementary argument shows that

almost surely for sufficiently large $n$.

Now, the conclusion $X_{n+1}\to 0$ almost surely follows by applying the following lemma:

The proof of the lemma is somewhat unusual since it involves running an iteration backwards: the property (3) is applied repeatedly to derive an inequality between $\xi_{n+1}$ and $\xi_{N}$ for $n>N>N_{0}$ ✿. Besides using several properties of infinite products and list maximums, the final convergence result is an application of Abel’s descending convergence criterion ✿ which says if the series $\sum_{n}b_{n}$ converges, and $a_{n}$ is a bounded descending sequence, then the series $\sum_{n}a_{n}b_{n}$ also converges.

We note that our formalization is firmly within the Classical territory for a number of reasons: first of all, the theory of Real numbers within the Coq standard library (which we use) uses non-computable axioms [23]. Secondly, while constructive measure theory and constructive analysis are both actively researched topics (see [19, 18, 11]) we are unaware if our main result (Dvoretzky’s theorem) is constructively valid. Thirdly, as we remarked above, our proof of Theorem 4.1 requires a case split on whether a particular sequence of real numbers is eventually zero or not, for which we use the axiom of constructive indefinite description.

While Dvoretzky’s theorem admits generalizations in many different ways, we chose to focus on formalizing the ones most suited for applications.

1. 1.

   As already mentioned, we prove Theorem 2.2 which is a generalization of Theorem 2.1 in which the sequences of numbers $\alpha_{n},\ \beta_{n},\ \gamma_{n}$ are replaced by sequences of functions on the probability space. This generalization is called the extended Dvoretzky theorem ✿. All conditions on the sequences $\alpha_{n},\ \beta_{n},\ \gamma_{n}$ now hold pointwise, almost everywhere.

2. 2.

   To apply Theorem 4.2 in the proof of Theorem 2.1 we needed to prove that $(Z_{n})$ is adapted to the filtration $\mathcal{F}$, which needed us to make assumptions on the functions $T_{n}$. These assumptions on $T_{n}$ can be modified and generalized as:

   1. (a)

      in the regular (non-extended) case, $T_{n}:\mathbb{R}^{n}\to\mathbb{R}$ are deterministic and measurable. ✿

   2. (b)

      in the extended case, $T_{n}:\mathbb{R}^{n}\times\Omega\to\mathbb{R}$ are stochastic and $\mathcal{F}_{n}$-adapted. ✿

   Since Derman-Sacks do not explicitly state either assumption, we formalized Dvoretzky’s theorem under both assumptions. It should be noted that Dvoretzky’s original paper [21] and his revisited paper [22] treat both the above cases.

3. 3.

   We have also formalized a corollary of the extended Dvoretzky’s theorem ✿ which proves that the theorem holds in the context where the bound on $T$ in (14) is assumed as follows with all other assumptions intact:

   $$|T_{n}(x_{1},\dots,x_{n})-x_{*}|\leq\max(\alpha_{n},(1+\beta_{n}-\gamma_{n})|x_{n}-x_{*}|)$$

   While this formulation is weaker compared to the original, it is convenient to have it for several applications of stochastic approximation theorems. A proof of this corollary used a classical analysis result of Abel [1] on the fact that the terms in a divergent sum-series could be multiplied by infinitesimally small series and the sum-series would still diverge ✿. This was addressed in Dvoretzky’s paper [21, (5.1)].