Topology

Motivation

Brouwer's fixed point theorem says that a continuous map of a closed simplex into itself has a fixed point. Many existence questions in game theory and mathematical economics produce instead a point-to-set mapping: to each point $x$ it assigns a whole set $\Phi(x)$ of admissible responses, for instance the set of best replies of a player to the others' strategies. Such a set need not be a single point, and no continuous single-valued selection need exist. Kakutani's 1941 note, A generalization of Brouwer's fixed point theorem, gives the fixed point theorem for this setting, and shows on the same three pages that it implies two results of J. von Neumann: an intersection theorem for two closed subsets of a product of convex sets, and the minimax theorem.

Timeline, as the paper records it:

• 1912–1929: Brouwer's theorem; the paper cites the proof of Knaster, Kuratowski and Mazurkiewicz (Fund. Math. 14, 1929).
• 1928: von Neumann proves the minimax theorem for matrix games (Math. Ann. 100).
• 1937: von Neumann proves the intersection theorem (Kakutani's Theorem 2) in his paper on an economic equilibrium system, "by using a notion of integral in Euclidean spaces".
• 1941: Kakutani proves Theorem 1 (simplex), the Corollary (bounded closed convex sets), and derives Theorems 2 and 3 from it.
• 1950: Nash's existence proof for equilibrium points of $n$-person games applies Kakutani's theorem (PNAS 36).

Setting

Let $E=\mathbb R^m$ with its Euclidean norm, and let $S\subseteq E$. Kakutani writes $\mathfrak R(S)$ for the family of all closed convex subsets of $S$; as printed, it contains the empty set. A point-to-set mapping of $S$ into $\mathfrak R(S)$ assigns to each $x\in S$ a closed convex set $\Phi(x)\subseteq S$.

$\Phi$ is upper semi-continuous (in the paper's sense) when

$$x_n\in S,\quad x_n\to x_0\in S,\quad y_n\in\Phi(x_n),\quad y_n\to y_0\quad\Longrightarrow\quad y_0\in\Phi(x_0).$$

This is a sequential closed-graph condition. The paper remarks that for a closed $S$ it is equivalent to the graph $\{(x,y):x\in S,\ y\in\Phi(x)\}$ being closed in $S\times S$.

An $r$-dimensional closed simplex is the convex hull of $r+1$ affinely independent points of $E$. A fixed point of $\Phi$ is a point $x_0\in S$ with $x_0\in\Phi(x_0)$.

Formalization targets

Goal: the Corollary (p. 458)

Let $S\subseteq\mathbb R^m$ be nonempty, bounded, closed and convex, and let $\Phi$ be upper semi-continuous on $S$ with every value $\Phi(x)$, $x\in S$, a nonempty closed convex subset of $S$. Then

$$\exists\,x_0\in S:\qquad x_0\in\Phi(x_0).$$

Milestones

1. Brouwer's fixed point theorem (§1, p. 457) — a published, proved platform theorem, referenced.
2. Approximation step of the proof of Theorem 1 (pp. 457–458): for every $\varepsilon>0$ there are a point $x$ of the simplex, points $x_0,\dots,x_r$ within $\varepsilon$ of $x$, selections $y_i\in\Phi(x_i)$ and weights $\lambda\in\Delta_r$ with $x=\sum_i\lambda_ix_i=\sum_i\lambda_iy_i$.
3. Limit step of the proof of Theorem 1 (p. 458): such data for every $\varepsilon>0$, on a compact $S$, force a fixed point.
4. Theorem 1 (p. 457): the fixed point statement for an $r$-dimensional closed simplex.
5. Enclosing simplex (proof of the Corollary, p. 458): every bounded subset of $\mathbb R^m$ lies in an $m$-dimensional closed simplex $S'$.
6. Retraction (proof of the Corollary, p. 458): a continuous map of $S'$ into $S$ fixing $S$.
7. Composition (proof of the Corollary, p. 458): $x\mapsto\Phi(\psi(x))$ is upper semi-continuous on $S'$ with values in $\mathfrak R(S)\subseteq\mathfrak R(S')$.
8. Closed-graph equivalence (§1, p. 457), for closed $S$ and $\Phi(x)\subseteq S$.
9. Theorem 2 (p. 458, von Neumann's intersection theorem): if $K\subseteq\mathbb R^m$, $L\subseteq\mathbb R^n$ are bounded closed convex, $K\neq\emptyset$, and $U,V\subseteq K\times L$ are closed with all sections $U_{x_0}\subseteq L$, $V_{y_0}\subseteq K$ nonempty, closed and convex, then $U\cap V\neq\emptyset$.

Milestones 8 and 9 stand off the goal's proof path: the paper proves Theorem 2 from the Corollary, using milestone 8 to check upper semi-continuity.

Significance

The Corollary is the form in which Kakutani's theorem is used: existence of equilibrium points in $n$-person games (Nash), of competitive equilibria (Arrow–Debreu), and of solutions of generalized games and variational inequalities all reduce to a fixed point of a point-to-set mapping with nonempty closed convex values on a compact convex set. Theorem 2 in turn gives the minimax theorem (the paper's Theorem 3) in a few lines.

The results are classical and their proofs are known; what is missing is a machine-checked version. Mathlib does not contain Kakutani's theorem, and on Prove2Me the theorem is not posed. Brouwer's theorem is proved on the platform (AGT.brouwer_fixed_point) and enters as a reference milestone. Theorem 3 is already proved on the platform as a special case of Sion's minimax theorem (FamousTheorems.sion_minimax_theorem, Mathlib's Sion.minimax) and is therefore not posed here. A related open platform statement, Debreu's 1952 fixed point lemma for a contractible polyhedron with contractible values and a closed graph (SocialEquilibrium.Existence.fixed_point_of_contractible_polyhedron), generalizes Theorem 1 on polyhedra but not the Corollary, since a bounded closed convex set need not be a polyhedron. Once proved, the goal is the standard entry point for formalized equilibrium existence results.

Difficulty

Brouwer's theorem needs a continuous single-valued map, and a point-to-set mapping with closed convex values need not admit a continuous selection: the mapping on $[-1,1]$ equal to $\{1\}$ for $x<0$, $[-1,1]$ at $0$ and $\{-1\}$ for $x>0$ is upper semi-continuous and has none. So the obvious route, select and apply Brouwer, fails; any proof must pass through approximations and a limit in which the graph condition and the convexity of the limiting value both enter. The approximation step needs a family of triangulations of the simplex with mesh tending to zero, which Mathlib does not provide. The transfer from a simplex to a general convex set needs a continuous retraction, which uses convexity and closedness of $S$ in Euclidean space.

Formalization scope

• The ambient space is EuclideanSpace ℝ (Fin m), $m=0$ included. A point-to-set mapping is a total function Φ : E → Set E; only its values on $S$ are constrained.
• IsClosedConvexSubset S A is the paper's $A\in\mathfrak R(S)$ ($A\subseteq S$, closed, convex) and admits $A=\emptyset$ as printed. Nonemptiness of the values (and of $S$, and of $K$ in Theorem 2) is a separate, labelled hypothesis: with $\Phi\equiv\emptyset$, or $S=\emptyset$, the printed hypotheses hold and there is no fixed point, while the paper's proof picks "an arbitrary point $y^n$ from $\Phi(x^n)$".
• IsUpperSemicontinuous S Φ is the paper's sequential condition, with sequences in $S$ and limit $x_0\in S$. It is not Berge's open-neighbourhood upper hemicontinuity.
• Explicit readings of loose phrases: "the $n$-th barycentric simplicial subdivision" becomes "for every $\varepsilon>0$" with the selected vertices within $\varepsilon$ of the point (no subdivision is built into the statement); "it is clear that … converges" becomes compactness of $S$ in the limit step; "take a closed simplex $S'$ which contains $S$" becomes an $m$-dimensional affinely independent hull; "a continuous retracting point-to-point mapping" becomes ContinuousOn ψ S', MapsTo ψ S' S and ψ x = x on $S$; "clearly an upper semi-continuous point-to-set mapping of $S'$ into $\mathfrak R(S)\subseteq\mathfrak R(S')$" is stated as three conclusions; "closed subset of $S\times S$" is closedness in $E\times E$ (the same for closed $S$); $U\cdot V$ is $U\cap V$; "$K\times L$ in $R^{m+n}$" is the product $\mathbb R^m\times\mathbb R^n$.
• A trivializing formalization would allow empty values, an empty domain, a degenerate simplex, or approximation data for a single coarse $\varepsilon$; each is excluded by the statements as written.
• Infrastructure a complete development needs: barycentric subdivisions or another construction of approximate fixed points; nearest-point projection onto closed convex sets in Euclidean space; transport of the Corollary to $\mathbb R^m\times\mathbb R^n$ for Theorem 2. The two definitions are generic and reusable for any later set-valued existence result. Proofs by any faithful route are welcome, including a route through Brouwer's theorem and a continuous approximate selection.

Selected references

• S. Kakutani, A generalization of Brouwer's fixed point theorem, Duke Math. J. 8 (1941), 457–459. https://doi.org/10.1215/s0012-7094-41-00838-4
• B. Knaster, C. Kuratowski, S. Mazurkiewicz, Ein Beweis des Fixpunktsatzes für n-dimensionale Simplexe, Fund. Math. 14 (1929), 132–137. https://doi.org/10.4064/fm-14-1-132-137
• J. von Neumann, Zur Theorie der Gesellschaftsspiele, Math. Ann. 100 (1928), 295–320. https://doi.org/10.1007/BF01448847
• J. von Neumann, Über ein ökonomisches Gleichungssystem und eine Verallgemeinerung des Brouwerschen Fixpunktsatzes, Ergebnisse eines Math. Kolloquiums 8 (1937), 73–83.
• J. F. Nash, Equilibrium points in n-person games, Proc. Natl. Acad. Sci. USA 36 (1950), 48–49. https://doi.org/10.1073/pnas.36.1.48
• M. Sion, On general minimax theorems, Pacific J. Math. 8 (1958), 171–176. https://doi.org/10.2140/pjm.1958.8.171

Motivation

A minimax theorem asserts that, for a function $f(\mu, \nu)$ of two variables,

$$\sup_{\mu \in M} \inf_{\nu \in N} f(\mu, \nu) = \inf_{\nu \in N} \sup_{\mu \in M} f(\mu, \nu).$$

Such equalities are the basis of zero-sum game theory, of Lagrangian duality in optimization, of robust optimization, and of minimax lower bounds in statistics and online learning. Maurice Sion's 1958 paper On general minimax theorems proved the version most often cited today: $M$ and $N$ convex subsets of topological vector spaces, one of them compact, $f$ quasi-concave and upper semicontinuous in $\mu$, quasi-convex and lower semicontinuous in $\nu$.

Sion's theorem itself is already machine-checked: Mathlib's Sion.minimax proves it, following the elementary argument of Komiya (1988), and the platform holds it as FamousTheorems.sion_minimax_theorem. Sion's own proof is different. It runs through an open-cover form of the Knaster–Kuratowski–Mazurkiewicz (KKM) theorem, a Helly-type fact about $n+1$ points in low dimension, and a lemma about minimal finite covers (Lemma 3.3). That route has not been formalized. This mission formalizes its ingredients, with Lemma 3.3 as the goal.

Timeline:

• 1928: von Neumann proves the minimax theorem for bilinear payoffs on simplices (mixed strategies of matrix games).
• 1929: Knaster, Kuratowski and Mazurkiewicz prove the KKM covering theorem for closed sets.
• 1952–1953: Kneser and Fan extend the minimax theorem to concave-convex and concavelike-convexlike functions on compact sets.
• 1958: Sion proves the quasi-concave-convex version with semicontinuity, by the KKM route.
• 1988: Komiya gives an elementary proof avoiding KKM; it is the proof formalized in Mathlib.

Setting

Let $E$ be a real topological vector space: a real vector space with a topology for which addition and scalar multiplication are continuous. A set $M \subseteq E$ is convex if it contains the segment between any two of its points. The convex hull $\ulcorner X \urcorner$ of a set $X$ is the smallest convex set containing it.

A real function $g$ on a convex set $M$ is quasi-concave on $M$ if every superlevel set $\{\mu \in M : g(\mu) \ge r\}$ is convex, and quasi-convex if every sublevel set $\{\mu \in M : g(\mu) \le r\}$ is convex. It is upper semicontinuous (u.s.c.) on $M$ if every strict sublevel set $\{\mu \in M : g(\mu) < r\}$ is open in the topology $M$ inherits from $E$; lower semicontinuous (l.s.c.) is the mirror notion.

Let $Y$ be a finite set, $c$ a real number, and $f$ a real function on $M \times Y$. Say that $Y$ has property P if for each $\mu \in M$ there is a $y \in Y$ with $f(\mu, y) < c$, and that $Y$ is minimal for P if no proper subset of $Y$ has P.

An $n$-dimensional simplex with vertices $a_0, \dots, a_n$ is the convex hull of $n+1$ affinely independent points.

Formalization targets

Goal: Lemma 3.3 (p. 173)

Let $M \subseteq E$ be nonempty and convex, $Y$ finite, and $f(\cdot, y)$ quasi-concave and u.s.c. on $M$ for each $y \in Y$. If $Y$ is minimal for P, then

$$\exists\, \mu_0 \in M \;\; \forall y \in Y: \quad f(\mu_0, y) < c.$$

The lemma makes no compactness or finite-dimensionality assumption on $M$; that generality is what lets Sion apply it on the convex hull of a finite set inside an arbitrary topological vector space.

Milestones

1. Theorem 3.2 (p. 173). If $\mathfrak A = \{a_0, \dots, a_n\}$ are $n+1$ points in a real vector space of dimension $k < n$, then $\bigcap_{i=0}^n \ulcorner \mathfrak A - \{a_i\} \urcorner \ne \emptyset$.
2. Theorem 3.1 (p. 173). If $S$ is an $n$-simplex with vertices $a_0, \dots, a_n$ and $A_0, \dots, A_n$ are open in the ambient space, $S \subseteq \bigcup_i A_i$, each $S - A_i$ is convex, and $a_i \notin A_j$ for $i \ne j$, then $\bigcap_{i} A_i \neq \emptyset$.
3. Lemma 3.3′ (p. 173). The dual of the goal: quasi-convex, l.s.c. in the second variable, with $>$ in place of $<$.
4. Remark 3.6 (p. 174). The explicit function on $[0,1]^2$, quasi-concave-convex and l.s.c. in $\nu$ but not u.s.c. in $\mu$, with $\sup\inf f = 0 < 1 = \inf\sup f$.

Sion's Theorem 3.4 and the Corollary on p. 174 (the minimax theorem) enter the mission as the existing, proved platform item FamousTheorems.sion_minimax_theorem.

Significance

Lemma 3.3 is a finite, one-sided statement that already contains the full strength of the quasi-concave case: a finite family of "threats" $y \in Y$, none of which can be dropped, can be beaten simultaneously by one point $\mu_0$. On p. 174 Sion derives the minimax theorem from Lemma 3.3 and Lemma 3.3′ by reducing open covers to minimal finite ones, alternately on each side. Theorem 3.1 is an open-set KKM theorem with a convexity condition on complements, a covering principle of independent use in fixed-point theory and equilibrium existence. Remark 3.6 shows that the semicontinuity hypotheses are not decorative.

On the formal side, the minimax theorem is proved in Mathlib by another route, so nothing in this mission is needed to know that Sion's theorem is true. What the mission adds is the infrastructure of the original proof: a KKM-type theorem (absent from Mathlib and from the platform), a Helly-type statement about $n+1$ points, and the minimal-cover lemma. None of these has a machine-checked proof today. A formalized open KKM theorem is reusable for Fan's lemma, for Gale–Nikaido–Debreu type existence results and for other covering arguments.

Difficulty

The obvious approach to Lemma 3.3 is induction on $|Y|$, using quasi-concavity to combine points that are good for subfamilies. It fails because quasi-concavity gives control over superlevel sets $\{f \ge c\}$ only, so the union of two "bad" sets is not controlled, and nothing forces two partial witnesses to have a common improvement on the segment between them. The lemma is genuinely topological: without upper semicontinuity it is false (Remark 3.6 exhibits the resulting failure of the minimax equality).

The topological content sits in Theorem 3.1. Neither Mathlib nor the platform has a KKM theorem (the platform has Brouwer's fixed-point theorem), and the passage from the classical closed-set KKM theorem to the open-set form, and from a simplex inside a possibly non-Hausdorff topological vector space to the standard simplex, both need care: the topology induced on a finite-dimensional subspace need not be the Euclidean one.

Formalization scope

• The ambient space is a real topological vector space: [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E], the class of Mathlib's Sion file. No Hausdorff or finite-dimensionality assumption is made. The paper never names the ambient space; "convex set" is read as a convex subset of such a space.
• Quasi-concavity, quasi-convexity and semicontinuity are Mathlib's QuasiconcaveOn, QuasiconvexOn, UpperSemicontinuousOn, LowerSemicontinuousOn, all relative to the set $M$ or $N$.
• $f$ is typed $E \to \iota \to \mathbb R$ (or $\iota \to E \to \mathbb R$) and $Y$ is a Finset ι; values off $M \times Y$ are irrelevant. Minimality is "no strict sub-Finset has property P".
• Added hypothesis $M \ne \emptyset$ in Lemma 3.3 and $N \neq \emptyset$ in Lemma 3.3′: with $M = Y = \emptyset$ the hypotheses hold vacuously and the conclusion fails.
• Theorem 3.1 uses the page's ambient openness hypothesis and nonempty intersection conclusion. In the application to Lemma 3.3, relatively open strict sublevel sets on $M$ must be represented by ambient open sets before restricting to the simplex.
• Theorem 3.2 takes the points as an injective family (encoding "$n+1$ points") and $\mathfrak A - \{a_i\}$ as a set difference; dimension is linear dimension (Module.finrank).
• Remark 3.6 formalizes only the checkable claims about the example, with $\sup\inf$ and $\inf\sup$ over the subtype $[0,1]$ in EReal; "cannot be removed nor appreciably weakened" is informal and omitted.
• Trivializing formalizations are ruled out: minimality is not defined in terms of the conclusion, and $M$ is neither finite-dimensional nor compact.

Contributions welcome: a formal KKM theorem (closed and open versions), Theorem 3.2 from Mathlib's Convex.helly_theorem, and proofs of the milestones in any order.

Selected references

• M. Sion, On general minimax theorems, Pacific Journal of Mathematics 8(1), 171–176, 1958. https://doi.org/10.2140/pjm.1958.8.171
• B. Knaster, C. Kuratowski, S. Mazurkiewicz, Ein Beweis des Fixpunktsatzes für n-dimensionale Simplexe, Fundamenta Mathematicae 14, 132–137, 1929. https://doi.org/10.4064/fm-14-1-132-137
• K. Fan, Minimax theorems, Proceedings of the National Academy of Sciences 39(1), 42–47, 1953. https://doi.org/10.1073/pnas.39.1.42
• H. Kneser, Sur un théorème fondamental de la théorie des jeux, Comptes Rendus de l'Académie des Sciences 234, 2418–2420, 1952.
• H. Komiya, Elementary proof for Sion's minimax theorem, Kodai Mathematical Journal 11(1), 5–7, 1988. https://doi.org/10.2996/kmj/1138038812
• J. von Neumann, Zur Theorie der Gesellschaftsspiele, Mathematische Annalen 100, 295–320, 1928. https://doi.org/10.1007/BF01448847

Motivation

Dynamic programming over uncountable state and control spaces needs two things at every stage: the optimal cost-to-go, obtained by minimizing over the control, must be a function that can be integrated against the next stage's transition probabilities, and a policy that nearly attains the minimum must be measurable, so that it defines a stochastic process. With Borel-measurable costs and Borel-measurable policies both requirements fail. Minimizing a Borel function of $(x,y)$ over $y$ produces a function whose level sets are projections of Borel sets, and such projections need not be Borel (Suslin, 1917). The repair, developed by Blackwell, Freedman and Orkin (1974), Shreve and Bertsekas, and set out in Chapter 7 of Bertsekas and Shreve's Stochastic Optimal Control: The Discrete-Time Case (1978), is to enlarge the class of costs to the lower semianalytic functions and the class of policies to the analytically or universally measurable ones. Sections 7.6–7.7 of the book establish that this class is closed under partial minimization and admits measurable ε-optimal selectors. Chapters 8–10 of the book, and much of the later literature on Borel-space Markov decision processes (Hernández-Lerma and Lasserre; Feinberg and coauthors), build on these results.

Timeline:

• 1917: Suslin shows that projections of Borel sets need not be Borel and introduces analytic sets; Lusin proves that analytic sets are universally measurable.
• 1941–1949: Jankov and von Neumann independently prove that an analytic subset of a product admits a selector measurable with respect to the σ-algebra generated by analytic sets.
• 1974: Blackwell, Freedman and Orkin use analytic sets to construct ε-optimal policies in Borel dynamic programming.
• 1978: Bertsekas and Shreve give the treatment used here (§7.6–7.7), including the selection theorem for lower semianalytic functions, Proposition 7.50.

Setting

A Borel space is a topological space homeomorphic to a Borel subset of a complete separable metric space (Definition 7.7); its Borel σ-algebra is $\mathscr B_X$. The Baire space is $\mathscr N=\mathbb N^{\mathbb N}$ with the product topology. A set $A\subseteq X$ is analytic if it is empty or the image of $\mathscr N$ under a continuous map; by Proposition 7.41 this is the book's Definition 7.16 (the Suslin operation applied to closed sets). Every Borel set is analytic, and the converse fails when $X$ is uncountable.

Three σ-algebras on $X$ are in play. The analytic σ-algebra $\mathscr A_X$ is generated by the analytic sets (Definition 7.19). The universal σ-algebra is $\mathscr U_X=\bigcap_{p}\mathscr B_X(p)$, the intersection over all probability measures $p$ on $(X,\mathscr B_X)$ of the $p$-completions of $\mathscr B_X$ (Definition 7.18). For a function $f$ from $D\subseteq X$ into a Borel space $Y$, $f$ is analytically measurable if $D\in\mathscr A_X$ and $f^{-1}(B)\in\mathscr A_X$ for every $B\in\mathscr B_Y$, and universally measurable if the same holds with $\mathscr U_X$ (Definition 7.20).

Let $R^*=[-\infty,\infty]$. A function $f:D\to R^*$ is lower semianalytic if $D$ is analytic and $\{x\in D\mid f(x)<c\}$ is analytic for every real $c$ (Definition 7.21). For $D\subseteq X\times Y$ write $D_x=\{y\mid (x,y)\in D\}$, $\mathrm{proj}_X(D)=\{x\mid D_x\neq\emptyset\}$, and define the partial infimum

$$f^*(x)=\inf_{y\in D_x}f(x,y),\qquad x\in\mathrm{proj}_X(D).$$

A selector is a function $\varphi:\mathrm{proj}_X(D)\to Y$ whose graph $\mathrm{Gr}(\varphi)$ lies in $D$.

Formalization targets

Goal: Proposition 7.50

Let $X,Y$ be Borel spaces, $D\subseteq X\times Y$ analytic, and $f:D\to R^*$ lower semianalytic.

(a) For every $\varepsilon>0$ there is an analytically measurable selector $\varphi$ with

$$f[x,\varphi(x)]\le\begin{cases}f^*(x)+\varepsilon&\text{if }f^*(x)>-\infty,\\-1/\varepsilon&\text{if }f^*(x)=-\infty.\end{cases}$$

(b) The set $I$ of points where the infimum is attained is universally measurable, and for every $\varepsilon>0$ there is a universally measurable selector $\varphi$ with $f[x,\varphi(x)]=f^*(x)$ on $I$ and the bounds of (a) off $I$.

The goal fixes no constant beyond the book's $\varepsilon$ and $-1/\varepsilon$.

Milestones

In attack order: Proposition 7.40 (Borel images and preimages of analytic sets are analytic), Corollary 7.42.1 ($\mathscr A_X\subseteq\mathscr U_X$), Corollary 7.44.2 (composites of analytically measurable maps are universally measurable), and Proposition 7.49, the Jankov–von Neumann theorem:

$$A\subseteq X\times Y\text{ analytic}\ \Longrightarrow\ \exists\,\varphi:\mathrm{proj}_X(A)\to Y\ \text{analytically measurable},\ \mathrm{Gr}(\varphi)\subseteq A.$$

Further items of the mission, on the same definitions: Proposition 7.39 (projections of analytic sets are analytic, and every analytic set is a projection of a Borel set), Lemma 7.30(1) (strict and non-strict, real and extended level sets give the same class) and Proposition 7.47 (lower semianalytic functions are exactly partial infima of Borel functions).

Significance

Proposition 7.50 is the selection theorem behind the existence of ε-optimal policies in Borel-space dynamic programming. In the finite-horizon model of Chapter 8 the optimal cost-to-go at each stage is lower semianalytic, by Propositions 7.47 and 7.48. Proposition 7.50 then turns the one-stage minimization into a measurable policy, analytically measurable when only ε-optimality is required and universally measurable when the minimum is attained. Chapters 8–9 of the book (the finite-horizon recursion $J^*_K=T^K(J_0)$ and the optimality equation under (P), (N), (D)) use it at every step. Downstream catalog papers on average-cost and stochastic shortest-path problems over Borel spaces cite these results.

All results here are proved in the book and in the descriptive set theory literature (Kechris, Classical Descriptive Set Theory, §18 and §29). None is formalized on Prove2Me. Mathlib has analytic sets in Polish-type settings, the Lusin separation theorem and Suslin's theorem, but it has no universal σ-algebra, no analytic σ-algebra, no lower semianalytic functions and no Jankov–von Neumann uniformization. The definitions in this mission are reusable by the later missions of the series (Chapters 8–10), which restate them locally until these are published.

Difficulty

The obvious route to a selector is to choose, for each $x$, a minimizing or near-minimizing $y$. The axiom of choice provides such a function, but nothing makes it measurable, and the conclusion of the theorem is exactly that measurability. The Borel route fails too: the set $\{x\mid f^*(x)<c\}$ is a projection of a Borel set, which is analytic but in general not Borel, so no Borel-measurable selector exists in general. The Jankov–von Neumann theorem needs a lexicographically least branch of a continuous parametrization of $A$ by $\mathscr N$, and an argument that the resulting map is measurable with respect to $\mathscr A_X$, which is generated by sets that are not closed under complementation. Part (b) adds a further obstacle: the composite of two analytically measurable maps need not be analytically measurable, so the exact selector is only universally measurable. Proving that requires Lusin's theorem that analytic sets are measurable for every completed probability measure.

Formalization scope

• A Borel space is a type with a topology satisfying the class IsBorelSpace (Definition 7.7, the ambient complete separable metric space taken in the same universe), together with Mathlib's [MeasurableSpace X] [BorelSpace X], so measurable sets are exactly the Borel sets. On $X\times Y$ the product σ-algebra is used; it coincides with $\mathscr B_{X\times Y}$ for separable metrizable spaces (Proposition 7.13).
• Analytic sets are Mathlib's MeasureTheory.AnalyticSet (empty or a continuous image of ℕ → ℕ).
• $R^*$ is EReal. The book uses $\infty-\infty=\infty$, and Mathlib's EReal uses $\bot+\top=\bot$. No statement of this mission adds infinities of opposite sign; $f^*(x)+\varepsilon$ adds a real number.
• Functions on $D$ and on $\mathrm{proj}_X(D)$ are functions on subtypes. The graph condition $\mathrm{Gr}(\varphi)\subseteq D$ is part of every selector statement.
• Universally measurable means NullMeasurableSet E p for every probability measure p.
• "Analytically measurable" refers to the σ-algebra generated by analytic sets. Replacing it by the power set, dropping the graph condition, or dropping the $-1/\varepsilon$ case would make the selection theorems a consequence of the axiom of choice. The statements rule all three out.

Not included: Lusin's theorem in Suslin-scheme form (Proposition 7.42, which needs the Suslin operation as a definition), Proposition 7.43 on $P(X)$, the integration results of Propositions 7.46 and 7.48, and Lemma 7.30(2)–(4). None is used in the proof of the goal. Contributions welcome: the bridge between IsBorelSpace and Mathlib's StandardBorelSpace, the universal σ-algebra API, and the Jankov–von Neumann theorem itself.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press 1978; Athena Scientific 1996, §7.6–7.7. https://web.mit.edu/dimitrib/www/soc.html
• D. Blackwell, D. Freedman and M. Orkin, The optimal reward operator in dynamic programming, Annals of Probability 2 (1974) 926–941. https://doi.org/10.1214/aop/1176996558
• A. S. Kechris, Classical Descriptive Set Theory, Graduate Texts in Mathematics 156, Springer 1995, §18 (Jankov–von Neumann uniformization), §29 (measurability of analytic sets). https://doi.org/10.1007/978-1-4612-4190-4
• S. E. Shreve and D. P. Bertsekas, Universally measurable policies in dynamic programming, Mathematics of Operations Research 4 (1979) 15–30. https://doi.org/10.1287/moor.4.1.15

Motivation

Every step of the dynamic programming algorithm on a general state space does three things: it takes a conditional expectation of the cost-to-go under a transition kernel, it minimizes the resulting function of state and control over the control, and, if a policy is to be produced, it picks a control for each state that attains or nearly attains that minimum. On a finite or countable state space all three are harmless. On an uncountable state space each can destroy the measurability needed to take the next expectation: the infimum over an uncountable family of measurable functions need not be measurable, and a minimizer chosen state by state need not be a measurable function of the state, so it does not define a policy at all.

Section 7.5 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (1978; Athena Scientific reprint 1996), settles the three operations for semicontinuous costs and continuous kernels. The results are the topological half of the book's measurability theory; the descriptive set theory half (lower semianalytic functions and analytically measurable selectors, §7.6–7.7) is a separate mission in this series. The semicontinuous results are what Propositions 8.6–8.7 and Corollaries 9.17.2–9.17.3 of the book use to obtain Borel-measurable optimal policies for finite-horizon and infinite-horizon models with lower semicontinuous costs and compact control sets.

Timeline. The exact selection theorem for lower semicontinuous functions (Proposition 7.33 below) is credited by the book's notes to Dubins and Savage, How to Gamble If You Must (1965). The Hausdorff metric on closed sets goes back to Hausdorff's Set Theory. Measurable selection in the closed-valued setting was later systematized by Kuratowski and Ryll-Nardzewski (1965), whose theorem gives a different route to results of this kind.

Setting

Throughout, $R^*=[-\infty,+\infty]$ is the extended real line. A function $f:X\to R^*$ on a metrizable space $X$ is lower semicontinuous if every sublevel set $\{x\mid f(x)\le c\}$, $c\in\mathbb R$, is closed, and upper semicontinuous if every superlevel set $\{x\mid f(x)\ge c\}$ is closed (Definition 7.13). $C(X)$ is the space of bounded continuous real-valued functions on $X$.

For a separable metrizable space $Y$, $P(Y)$ is the set of Borel probability measures on $Y$ with the weak topology (convergence of integrals of functions in $C(Y)$). A stochastic kernel $q(dy\mid x)$ on $Y$ given $X$ is a map $x\mapsto q(dy\mid x)$ from $X$ to $P(Y)$, and it is continuous if this map is continuous (Definition 7.12). The integral of a Borel-measurable $f:Y\to R^*$ is $\int f\,dp=\int f^+dp-\int f^-dp$ with the convention $-\infty+\infty=+\infty-\infty=+\infty$ (Eq. (43) of Chapter 7).

For a compact metric space $Y$, $2^Y$ is the collection of closed subsets of $Y$ with the topology of the Hausdorff metric (Appendix C). For $D\subseteq X\times Y$, the section at $x$ is $D_x=\{y\mid (x,y)\in D\}$, the projection is $\mathrm{proj}_X(D)=\{x\mid D_x\neq\emptyset\}$, and a function $\varphi:\mathrm{proj}_X(D)\to Y$ has its graph in $D$ if $(x,\varphi(x))\in D$ for every $x\in\mathrm{proj}_X(D)$. "Borel-measurable" refers to the Borel σ-algebras of the topologies in question; on $\mathrm{proj}_X(D)$ this is the Borel σ-algebra of the subspace topology.

Formalization targets

Goal: Proposition 7.33

Let $X$ be metrizable, $Y$ compact metrizable, $D\subseteq X\times Y$ closed, and $f:D\to R^*$ lower semicontinuous. Put

$$f^*(x)=\min_{y\in D_x}f(x,y),\qquad x\in\mathrm{proj}_X(D).$$

Then $\mathrm{proj}_X(D)$ is closed, $f^*$ is lower semicontinuous, and there is a Borel-measurable $\varphi:\mathrm{proj}_X(D)\to Y$ with graph in $D$ and

$$f\bigl(x,\varphi(x)\bigr)=f^*(x)\qquad\forall x\in\mathrm{proj}_X(D).$$

Milestones

• Proposition 7.32: for $f^*(x)=\inf_{y\in Y}f(x,y)$, lower semicontinuity of $f$ and compactness of $Y$ give lower semicontinuity of $f^*$ and attainment; upper semicontinuity of $f$ gives upper semicontinuity of $f^*$.
• Lemma 7.18: there is a Borel-measurable $\sigma:2^Y-\{\emptyset\}\to Y$ with $\sigma(A)\in A$.
• Lemma 7.20: for lower semicontinuous $f$ on a nonempty compact $Y$, the argmin map $x\mapsto\{y\mid f(x,y)\le f^*(x)\}$ is Borel-measurable into $2^Y$.
• Lemma 7.14: $f$ is lower semicontinuous and bounded below iff $f_n\uparrow f$ for some $f_n\in C(X)$ (and dually).
• Proposition 7.30: $x\mapsto\int f(x,y)\,q(dy\mid x)$ is continuous for $f\in C(X\times Y)$ and continuous $q$.
• Proposition 7.31: the same map is lower (upper) semicontinuous and bounded below (above) when $f$ is.
• Lemma 7.21: an open $G\subseteq X\times Y$, $Y$ separable, has open projection and a Borel-measurable selector with graph in $G$.
• Proposition 7.34: for open $D$ and upper semicontinuous $f$, $\mathrm{proj}_X(D)$ is open, $f^*=\inf_{D_x}f$ is upper semicontinuous, and for each $\varepsilon>0$ there is a Borel-measurable $\varphi_\varepsilon$ with graph in $D$ and

$$f\bigl(x,\varphi_\varepsilon(x)\bigr)\le\begin{cases}f^*(x)+\varepsilon&\text{if }f^*(x)>-\infty,\\-1/\varepsilon&\text{if }f^*(x)=-\infty.\end{cases}$$

Significance

The results. Propositions 7.31–7.33 are the closure properties that make the dynamic programming recursion stay inside the class of lower semicontinuous functions bounded below: the expectation step preserves the class (7.31), the minimization step preserves it (7.32, 7.33), and the minimization admits a Borel-measurable exact minimizer (7.33). This is why, in semicontinuous models, the optimal cost functions are lower semicontinuous and optimal policies can be taken Borel-measurable and nonrandomized. Proposition 7.34 gives the weaker, $\varepsilon$-optimal counterpart for upper semicontinuous costs, where the infimum need not be attained.

Formalizing them. All of these results are proved in the book; none is open. As far as is known, none has a machine-checked proof: Mathlib has semicontinuity, the Hausdorff extended metric on closed and on nonempty compact sets, and the weak topology on probability measures, but no theorem combining them into a measurable selection result of this kind. A formal development would supply measurable selectors for semicontinuous minimization in Lean and the Borel-measurability of set-valued maps into the hyperspace of closed sets, both reusable well beyond dynamic programming.

Difficulty

The obvious attempt at the goal is to pick, for each $x$, some minimizer $y$ of $f(x,\cdot)$ over the compact section $D_x$. The minimizer exists by compactness and lower semicontinuity, but the choice is made pointwise and gives no control on measurability: a minimizer chosen by the axiom of choice need not be Borel-measurable. The argmin sets $F^*(x)$ vary with $x$ only semicontinuously: they can jump from a single point to a large set, so a continuous selection generally does not exist, and continuity arguments cannot replace measurability. Lemma 7.18 isolates the hardest part: a choice of a point of each nonempty closed set that is measurable as a function of the set itself.

A second difficulty is bookkeeping at infinity. Values $\pm\infty$ are allowed throughout, so sublevel sets, minima, integrals and $\varepsilon$-bounds must all be handled in $R^*$; the integral in Proposition 7.31 uses the convention $\infty-\infty=+\infty$, which is not Mathlib's.

Formalization scope

• Extended reals. Values are in EReal. The only place where values of opposite infinite sign are combined is the integral, which is the published definition DupacovaWets.Consistency.expect (reused, not restated): $\int f^+-\int f^-$ with an explicit case returning $+\infty$ when $\int f^+=\infty$, exactly the book's convention (42). The $\varepsilon$-bound of Proposition 7.34 adds a real $\varepsilon$ to a value different from $-\infty$, which is safe in EReal.
• Semicontinuity is Mathlib's LowerSemicontinuous/UpperSemicontinuous, equivalent to Definition 7.13 for EReal-valued functions. Lemma 7.13 of the book (the sequential characterization) is Mathlib's lowerSemicontinuous_iff_le_liminf together with first countability of metrizable spaces, and is not restated here.
• Functions on $D$. Functions "on $D$" are functions on $X\times Y$ with LowerSemicontinuousOn f D (resp. UpperSemicontinuousOn); values off $D$ play no role. $\mathrm{proj}_X(D)$ is Prod.fst '' D, selectors are functions on that subtype, and its σ-algebra is the Borel σ-algebra of the subspace topology.
• Hyperspace. $2^Y$ is Closeds Y, and $2^Y-\{\emptyset\}$ for compact $Y$ is NonemptyCompacts Y, each with the Hausdorff extended metric and the Borel σ-algebra of its topology. This topology agrees with the book's (the exponential topology of Appendix C, independent of the metric).
• Boundedness. "Bounded below/above" is by a real constant. BddBelow in EReal would be vacuous and is not used.
• Edge cases. Proposition 7.32(a)'s attainment clause is stated for nonempty $Y$, since for $Y=\emptyset$ the infimum is $+\infty$ and nothing attains it.
• Argmin minimum. Lemma 7.20 assumes nonempty $Y$ because its defining formula uses a minimum; for empty $Y$ there is no minimizer.
• Ruling out trivial readings. The graph condition $(x,\varphi(x))\in D$ is part of every selection statement; without it the goal would follow from the unconstrained case. The selector must be Borel-measurable on $\mathrm{proj}_X(D)$ and must attain the minimum exactly, not up to $\varepsilon$.

A complete development needs the Borel structure of the hyperspace (measurability of maps into Closeds Y from upper semicontinuity in the sense of Kuratowski, Proposition C.4 of the book), the construction of a measurable choice function on NonemptyCompacts Y, and approximation of semicontinuous functions by monotone sequences in $C(X)$. Each of these is reusable on its own; proofs of individual milestones by any route are welcome.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific reprint, 1996, Section 7.5 and Appendix C. https://web.mit.edu/dimitrib/www/soc.html
• L. E. Dubins and L. J. Savage, How to Gamble If You Must: Inequalities for Stochastic Processes, McGraw-Hill, 1965.
• K. Kuratowski and C. Ryll-Nardzewski, "A general theorem on selectors," Bull. Acad. Polon. Sci. 13 (1965), 397–403.
• F. Hausdorff, Set Theory, Chelsea, New York, 1957.

Motivation

In 1998 Smale listed eighteen problems for the twenty-first century; the eighteenth asks: What are the limits of intelligence, both artificial and human? (Smale 1998). The paper of Acharjee and Gogoi (arXiv:2310.10792) proposes a mathematical model of a mind, the cognitive-consequence space, built from a Tarski consequence operator, and claims that two theorems about this model (its Theorems 3.3 and 3.4) show that "human intelligence is limitless" (Discussion, p. 22; Conclusion, p. 23).

This mission records that model and its results in Lean 4 exactly as stated, so that each claim becomes a checkable statement: proved, or refuted, by the verifier rather than by argument.

Setting

A cognitive-consequence space is a set $C$ of mental representations (thoughts) with a consequence operator $\mathrm{Cn} : \mathcal P(C) \to \mathcal P(C)$ and an implication connective $X \Rightarrow Y$ satisfying Tarski's axioms as listed in the paper (p. 5):

1. $C$ is countable;
2. $A \subseteq \mathrm{Cn}(A)$;
3. $A \subseteq B \Rightarrow \mathrm{Cn}(A) \subseteq \mathrm{Cn}(B)$;
4. $\mathrm{Cn}(\mathrm{Cn}(A)) = \mathrm{Cn}(A)$;
5. if $X \in \mathrm{Cn}(A)$ then $X \in \mathrm{Cn}(B)$ for some finite $B \subseteq A$;
6. if $Y \in \mathrm{Cn}(A \cup \{X\})$ then $(X \Rightarrow Y) \in \mathrm{Cn}(A)$;

together with the paper's standing assumption $\mathrm{Cn}(\varnothing) \neq \varnothing$ (p. 5, after Definition 3.2).

A set $A$ is deductive if $\mathrm{Cn}(A) = A$. The cognitive-consequence topology is

$$\tau = \{A \subseteq C : \mathrm{Cn}(C \setminus A) = C \setminus A\},$$

and members of $\tau$ are consequence-wise open (CWO). The cognitive closure $\mathrm{Cl}^{\square}(A)$ is the intersection of all deductive sets containing $A$.

Separately, a cognitive similarity distance is a function $\mathrm{Cog} : C \times C \to [0,1]$ together with a relation $x \approx y$ ("$x$ and $y$ cognitively coincide") such that $\mathrm{Cog}(x,y) = 0 \iff x \approx y$, $\mathrm{Cog}$ is symmetric, $x \approx z \Rightarrow \mathrm{Cog}(x,y) = \mathrm{Cog}(z,y)$, and the triangle inequality holds. A sequence of thoughts $(x_n)$ converges to $x$ if for every $\varepsilon \in (0,1)$ we have $\mathrm{Cog}(x, x_n) < \varepsilon$ for all large $n$.

Formalization targets

Goal: "human intelligence is limitless" (Theorems 3.3 and 3.4)

For every cognitive-consequence space,

$$\Bigl(\exists f \in C\ \forall A \in \tau,\ f \notin A\Bigr) \ \wedge\ \Bigl(\exists f \in C\ \exists A \in \tau,\ f \in A\Bigr).$$

Milestones

Theorems 3.1, 3.2, 3.3, 3.5, 3.6, 3.7 and Corollary 3.5 (the topology $\tau$ and the cognitive closure), Theorems 3.8 and 3.12 (cognitive limits), Theorem 4.3 (the filter $f_d$) and Theorem 5.1 (Gödel's incompleteness black hole).

Significance

The paper presents the goal as its answer to the human-intelligence half of Smale's eighteenth problem. A machine-checked verdict on the goal settles whether that conclusion follows from the paper's own axioms. The milestones are the paper's structural results about $\tau$, cognitive closure and cognitive limits.

Status: to the best of current knowledge none of these results has a published machine-checked proof. The first conjunct of the goal (Theorem 3.3) follows from the standing assumption $\mathrm{Cn}(\varnothing) \neq \varnothing$. The second conjunct (Theorem 3.4) is not implied by the listed axioms as formalized: the consequence operator with $\mathrm{Cn}(A) = C$ for every $A$, on a one-point language, satisfies all of them and has $\tau = \{\varnothing\}$. The goal is therefore expected to be resolved by a disproof.

Difficulty

The content of the goal is the existence of a nonempty CWO set, equivalently of a deductive set different from $C$ (a consistent theory). The paper's argument for Theorem 3.4 derives $\bigcap_i A_i = \varnothing$ and calls this a contradiction; nothing in the axioms forbids it.

Formalization scope

• CogCons.CognitiveConsequenceSpace C bundles $\mathrm{Cn}$, the connective imp, axioms (i)–(vi) and $\mathrm{Cn}(\varnothing) \neq \varnothing$. The syntax $\sigma$ and interpretation $I$ of the paper are not modelled beyond imp.
• The paper also asserts $\mathrm{Cn}(C) \neq C$ (p. 5). This contradicts axiom (ii), since $C \subseteq \mathrm{Cn}(C) \subseteq C$; including it would make every statement vacuously true, so it is omitted. For the same reason the second half of Corollary 3.4 ($\mathrm{Cl}^{\square}(C) \neq C$) is not included.
• Theorem 4.4 (the family $\{A : f \in \mathrm{Cn}(A)\}$ is a filter) is not included: closure under intersection fails in a four-element model satisfying all the axioms.
• Results relying on informal notions (the practical topology of Section 2, Theorems 3.9–3.11 and 3.13, Theorems 4.1–4.2, and the "solution space" of Section 5) are not formalized.
• CogCons.CognitiveSimilarityDistance C is independent of $\mathrm{Cn}$; sequences are indexed by $\mathbb N$ starting at $0$; $\approx$ is an arbitrary relation constrained only by the listed axioms.

Selected references

• S. Acharjee, U. Gogoi, The limit of human intelligence, arXiv:2310.10792v2 [math.GM], 2023. https://arxiv.org/abs/2310.10792
• S. Smale, Mathematical problems for the next century, The Mathematical Intelligencer 20(2), 7–15, 1998. https://doi.org/10.1007/BF03025291

Why the horseshoe

The Smale horseshoe is the standard example of a smooth invertible map of the plane with chaotic dynamics. Smale introduced it in the 1960s as the mechanism behind the complicated orbits near a transverse homoclinic point, and it became the basic model of hyperbolic invariant sets (Smale 1967). Its importance for differential equations is the Smale–Birkhoff theorem: whenever the stable and unstable manifolds of a hyperbolic fixed point intersect transversally, some iterate of the map contains a horseshoe. Melnikov's method then turns this into a checkable criterion for chaos in periodically forced planar systems such as Duffing's equation.

This mission formalizes the horseshoe as it is treated in Chapter 13 of G. Teschl, Ordinary Differential Equations and Dynamical Systems (author's preliminary version of AMS GSM 140, 2012). It takes along the one-dimensional results from §§11.4–11.5 that the chapter's argument reuses: the tent map's Cantor set, the one-sided shift, and the metric on two-sided sequences.

Setting

Fix parameters $\lambda$ and $\mu$ and let $D = [0,1]^2$. The two horizontal strips

$$J_0 = [0,1] \times [0, 1/\mu], \qquad J_1 = [0,1] \times [1 - 1/\mu, 1]$$

are mapped by

$$F(x,y) = (\lambda x, \mu y) \text{ on } J_0, \qquad F(x,y) = (1 - \lambda x, \mu(1-y)) \text{ on } J_1 .$$

Each strip is contracted horizontally by $\lambda$ and stretched vertically by $\mu$ into a vertical strip crossing $D$. The book specifies $F$ only on $J_0 \cup J_1$ and leaves the fold between them to a picture. A horseshoe map here is any $F : \mathbb{R}^2 \to \mathbb{R}^2$ given by these formulas on $J_0 \cup J_1$. On $K_0 = F(J_0) = [0, \lambda] \times [0,1]$ and $K_1 = F(J_1) = [1-\lambda, 1] \times [0,1]$ the inverse $g$ is given by explicit formulas.

The tent map $T_\nu(x) = \frac{\nu}{2}(1 - |2x-1|)$ on $\mathbb{R}$ has the invariant set

$$\Lambda(T_\nu) = \{x \in \mathbb{R} : T_\nu^n(x) \in [0,1] \text{ for all } n \ge 0\}.$$

The second coordinate of $F$ is $T_\mu(y)$ and the first coordinate of $g$ is $T_{1/\lambda}(x)$. The horseshoe's invariant set is

$$\Lambda = \Lambda(T_{1/\lambda}) \times \Lambda(T_\mu).$$

The two-sided shift space is $\Sigma_2 = \{0,1\}^{\mathbb{Z}}$. It carries the metric

$$d(s,t) = \tfrac12 \sum_{n \ge 0} \frac{|s_n - t_n| + |s_{-n} - t_{-n}|}{2^n}$$

and the shift $\sigma(s)_n = s_{n+1}$. The itinerary $\varphi(x,y) \in \Sigma_2$ of a point of $\Lambda$ records, for $n \ge 0$, which strip $J_{y_n}$ contains $F^n(x,y)$. For $n < 0$ it records which strip $K_{x_{-n-1}}$ contains $g^{-n-1}(x,y)$.

A system $(M, f)$ is chaotic in the book's sense (p. 296) under four conditions: $f$ is continuous, $M$ is infinite, $f$ is topologically transitive (for nonempty open $U, V$ some $f^n(U)$ meets $V$), and the periodic points are dense. A Cantor set is a compact, perfect, totally disconnected set.

Formalization targets

Goal: Theorem 13.1 (p. 333)

For $0 < \lambda < \tfrac12$, $\mu > 2$ and every horseshoe map $F$:

$$\Lambda \text{ is a Cantor set}, \quad F(\Lambda) = \Lambda, \quad \varphi : \Lambda \to \Sigma_2 \text{ is a homeomorphism with } \sigma \circ \varphi = \varphi \circ F \text{ on } \Lambda,$$ $$\text{and } (\Lambda, F|_\Lambda) \text{ is chaotic.}$$

The book's sentence is: "The Smale horseshoe map has an invariant Cantor set $\Lambda$ on which the dynamics is equivalent to the double sided shift on two symbols. In particular it is chaotic."

Milestones, in attack order

• Lemma 11.15 (p. 306). On two-sided sequences, $d(s,t) \le N^{-n}$ when $s, t$ agree on $|j| \le n$, and $d(s,t)$ is bounded below by a multiple of $N^{-n}$ when they differ at some $|j| \le n$.
• Lemma 11.8 (p. 303). The one-sided shift on $\Sigma_N = \{0, \dots, N-1\}^{\mathbb{N}_0}$ has countably many periodic points, and they are dense.
• Lemma 11.9 (p. 303). The one-sided shift has a dense forward orbit.
• Lemma 11.4 (p. 299). For $\nu > 2$, $\Lambda(T_\nu)$ is a Cantor set.
• Theorem 11.5 (p. 301). For $\nu > 2$, the itinerary map conjugates $(\Lambda(T_\nu), T_\nu)$ to the one-sided shift on $\{0,1\}^{\mathbb{N}_0}$ by a homeomorphism.

Significance

Theorem 13.1 exhibits a two-dimensional invertible system with an explicit invariant set on which the dynamics is exactly the two-sided shift. Every property of the shift is then inherited:

• infinitely many periodic orbits of every period;
• a dense orbit;
• sensitive dependence (Lemma 11.3);
• orbits with any prescribed forward and backward itinerary.

Theorem 13.1 is the model to which the Smale–Birkhoff theorem (13.2) reduces the dynamics near a transverse homoclinic point. It is therefore the terminal object of the book's route from Melnikov integrals to chaos in forced oscillators.

The results are classical and fully proved in the literature. Their proofs have not been formalized. Mathlib has Cantor-type sets (the middle-thirds set), totally disconnected and perfect sets, and product topologies. It has no tent-map invariant set, no two-sided symbolic dynamics with the book's metric, and no conjugacy theorem of this kind. A formal proof would supply a machine-checked conjugacy between a concrete planar map and a full shift, together with the symbolic-dynamics layer it rests on.

Difficulty

The book's own argument for Theorem 13.1 has two gaps that a formal proof must fill. First, it asserts that a product of two Cantor sets is again a Cantor set and leaves this as an exercise. Second, it treats continuity of the itinerary map and of its inverse as an exercise. It also leans on "all other results hold with no further modifications" to transfer the one-sided lemmas (11.7–11.9) to the two-sided shift.

The two-sided transfer is not literally a restatement. The metric (11.35) weights each off-centre index by $\tfrac12$, and so the one-sided closeness estimate does not carry over verbatim; see the correction to Lemma 11.15 below.

The inverse $g$ must also be tracked alongside $F$. The negative half of the itinerary is defined through $g$ rather than through $F$, so the conjugacy at index $-1$ couples the two halves.

Finally, the parameter endpoints need care. The book allows $\lambda = \tfrac12$ and $\mu = 2$. At $\mu = 2$ the defining formulas are inconsistent on $y = \tfrac12$, and at either endpoint one factor of $\Lambda$ is the whole interval $[0,1]$.

Formalization scope

• Parameters. The goal is stated for $0 < \lambda < \tfrac12$ and $\mu > 2$, a correction of the book's closed endpoints recorded in the statement.
• Lemma 11.15 is stated with the lower bound $\tfrac12 N^{-n}$ instead of the printed $N^{-n}$. The printed bound fails for the metric (11.35): for $N = 2$, $n = 1$ and sequences differing only at index $1$, $d = \tfrac14$. The first clause is as printed.
• The map. IsHorseshoeMap λ μ F is a predicate fixing $F$ only on $J_0 \cup J_1$, and the goal quantifies over all such $F$. Its conclusion therefore cannot depend on how the fold is drawn. The inverse horseshoeInv is the explicit formula (13.5)–(13.6).
• Spaces. $\mathbb{R}^2$ is ℝ × ℝ; its max-distance has the Euclidean topology. Sequence spaces are ℕ → Fin N and ℤ → Fin N. The metrics (11.28) and (11.35) are functions symDist and symDistZ, not type-class instances. Density and continuity are stated in $\varepsilon$–$\delta$ form against them, so no unmentioned product topology enters.
• Topological equivalence is spelled out: $F$ maps $\Lambda$ onto $\Lambda$, $\varphi$ is a bijection $\Lambda \to \Sigma_2$, $\sigma \circ \varphi = \varphi \circ F$ on $\Lambda$, and $\varphi$, $\varphi^{-1}$ are continuous.
• Chaos is the book's definition (continuous, infinite, transitive, dense periodic points), applied to $F$ restricted to the subtype $\Lambda$. It is not the three-axiom definition with sensitive dependence.
• Cantor set means compact, Preperfect and IsTotallySeparated, the last being the book's definition of total disconnectedness on p. 302.

$\Lambda$ is constructed as in (13.8) and $\varphi$ as in (13.9), not quantified over. The goal asserts the full conjunction, so it cannot be discharged by exhibiting some other invariant set or some other conjugacy. For $\mu > 2$ maps satisfying IsHorseshoeMap exist, so the hypothesis is not vacuous.

A complete development needs:

• the product of Cantor sets in a product of metric spaces;
• the tent-map coding (Theorem 11.5) for both $T_\mu$ and $T_{1/\lambda}$;
• the two-sided shift's Cantor, periodic-point and transitivity properties;
• transport of chaos along a conjugacy.

The tent-map and one-sided shift lemmas duplicate those of the interval-maps mission of this series and are reusable there. Contributions proving the two-sided analogues of Lemmas 11.7–11.9 as auxiliary lemmas are welcome.

Selected references

• G. Teschl, Ordinary Differential Equations and Dynamical Systems, Graduate Studies in Mathematics 140, AMS, 2012. Author's preliminary version: https://www.mat.univie.ac.at/~gerald/ftp/book-ode/ode.pdf
• S. Smale, Differentiable dynamical systems, Bull. Amer. Math. Soc. 73 (1967), 747–817. https://doi.org/10.1090/S0002-9904-1967-11798-1
• R. L. Devaney, An Introduction to Chaotic Dynamical Systems, 2nd ed., Addison-Wesley, 1989.
• C. Robinson, Dynamical Systems: Stability, Symbolic Dynamics, and Chaos, 2nd ed., CRC Press, 1999.

Motivation

Dynamic programming, as introduced by Bellman in the early 1950s, solves sequential decision problems through a functional equation: the value of a problem started in a given state equals the best one-stage return plus the value of the problem started in the state that decision leads to. In practice the argument usually runs backwards. One writes down the functional equation, finds or characterizes a solution, and reads off the structure of optimal decisions from that solution. This is legitimate only if two things hold: an optimal policy exists at all, and the solution of the functional equation that was found is the optimal value, not some other solution of the same equation.

Samuel Karlin's 1955 paper The Structure of Dynamic Programing Models (Naval Research Logistics Quarterly 2(4):285–294) gives an abstract deterministic model in which both questions can be posed precisely. It proves existence of optimal strategies by a compactness argument (Theorem 1), derives the functional equation, which it calls the Principle of Optimality, and identifies the condition under which a solution of that equation is the optimal return: a tail term must vanish. Later treatments of dynamic programming on general state spaces, such as Blackwell's discounted and positive programming (1965–1967) and the monographs of Bertsekas and Shreve, state their verification theorems in the same form, with a solution of the optimality equation plus a condition at infinity.

Setting

The model has a state space $\Omega$, a Hausdorff topological space, and a decision space $D$, a nonempty compact Hausdorff space. A strategy is a sequence $s = (\delta_1, \delta_2, \dots)$ of decisions, one per stage. The strategy space $S = D \times D \times \cdots$ carries the product topology and is compact by Tychonoff's theorem.

The data are:

• a return function $L : \Omega \times D \to \mathbb{R}$, continuous and non-negative, where $L(\omega, \delta)$ is the return for taking decision $\delta$ in state $\omega$;
• a transition $(\delta, \omega) \mapsto T_\delta\,\omega \in \Omega$, the state faced at the next stage after decision $\delta$ in state $\omega$;
• a normalization factor $P : D \to \mathbb{R}$, continuous and positive.

From an initial state $\omega$, a strategy $s$ generates the trajectory $\omega_1 = \omega$, $\omega_n = T_{\delta_{n-1}}\,\omega_{n-1}$, and the weights $P_n(s) = \prod_{i=1}^{n-1} P(\delta_i)$ with $P_1(s) = 1$. The total yield is

$$\Phi(\omega, s) = \sum_{n=1}^{\infty} L(\omega_n, \delta_n)\, P_n(s),$$

and the optimal return is $K(\omega) = \max_{s \in S} \Phi(\omega, s)$. The standing assumption of the paper, display (1), is that the partial sums $\sum_{n=1}^{k} L(\omega_n, \delta_n) P_n(s)$ converge uniformly in $s \in S$ for each $\omega$.

Formalization targets

Goal: uniqueness of solutions with vanishing tail

Let $M : \Omega \to \mathbb{R}$ solve the functional equation

$$M(\omega) = \max_{\delta \in D} \bigl\{ L(\omega, \delta) + P(\delta)\, M(T_\delta\,\omega) \bigr\} \quad \text{for all } \omega,$$

with the maximum attained, and suppose that for every $\omega$

$$\lim_{n \to \infty} \ \sup_{\delta_1, \dots, \delta_n} |M(\omega_n)| \prod_{i=1}^{n-1} P(\delta_i) = 0.$$

Then $M(\omega) = \max_{s \in S} \Phi(\omega, s)$ for every $\omega$, and the maximum is attained (pp. 290–291, §Uniqueness).

Milestones

1. Theorem 1 (p. 287). If the series (1) converges uniformly in $S$, an optimal strategy $s^*$ exists: $\Phi(\omega, s^*) = \max_S \Phi(\omega, s)$.
2. Shift identity (p. 290, first display). For a strategy $s$ with convergent yield series and the shift $s' = (\delta_2, \delta_3, \dots)$,

$$\Phi(\omega, s) = L(\omega, \delta_1) + P(\delta_1)\, \Phi(T_{\delta_1}\,\omega, s').$$

3. Principle of Optimality, eq. (2) (p. 290). $K(\omega) = \max_{\delta_1} \{ L(\omega, \delta_1) + P(\delta_1) K(T_{\delta_1}\,\omega) \}$.
4. n-step expansion (p. 291, first display). A solution $M$ of (2) satisfies, for every $n$,

$$M(\omega) = \max_{\delta_1, \dots, \delta_n} \Bigl\{ \sum_{m=1}^{n} L(\omega_m, \delta_m) P_m(s) + M(\omega_{n+1}) P_{n+1}(s) \Bigr\}.$$

Significance

Milestone 3 says that the optimal return solves the functional equation. The goal gives the converse on a class of candidate solutions: any solution with a vanishing tail is the optimal return. Together they justify solving a dynamic program by solving its functional equation. The paper's two examples, a two-operation allocation problem with discounting and a resource allocation model driving the state to the origin, obtain uniqueness among bounded solutions and among continuous solutions vanishing at the origin respectively, by checking the tail condition. Without the tail condition the conclusion fails; the paper notes that the limit term "need not be true in general for any solution to the functional equation".

All four milestones and the goal are classical results with published proofs. None of them has a machine-checked proof on this platform: its existing Bellman-equation theorems concern finite-state stochastic models with a constant discount factor, and this model has neither restriction. The mission produces a formal version of the general deterministic model on topological state spaces, with optimality characterized by a verification theorem, which later missions on the paper's examples can reuse.

Difficulty

Existence rests on continuity of $s \mapsto \Phi(\omega, s)$ on the product space. Each term $L(\omega_n, \delta_n) P_n(s)$ depends on the first $n$ decisions through the composite map $\omega_n = T_{\delta_{n-1}} \circ \cdots \circ T_{\delta_1}\,\omega$, and continuity of that composite in all decisions at once does not follow from separate continuity of $T_\delta\,\omega$ in $\delta$ and in $\omega$. The limit of the series is continuous only because the convergence is uniform.

For uniqueness, the paper's display "$M(\omega) = \max_S \Phi(\omega, s) + \lim_n \max M(\omega_n) \prod P(\delta_i)$" is not an identity: a maximum of a sum is not the sum of the maxima. A proof has to bound $M$ from above by the yield of every strategy and from below by the yield of one particular strategy, and the lower bound fails if the tail term is controlled only from above. Attainment of the maximum in the conclusion needs a strategy to be exhibited, not only a supremum computed.

Formalization scope

A strategy is a function s : ℕ → D, with the product topology. Lean's 0-based index $k$ is the paper's stage $k+1$: s 0 is $\delta_1$, trajectory T ω s 0 is $\omega_1 = \omega$, and weight P s k is $P_{k+1}(s)$, so weight P s 0 = 1. The total yield is a tsum and the optimal return a supremum over all strategies. "Maximum" is encoded as IsGreatest of a range, so every stated maximum is attained. Uniform convergence of (1) is TendstoUniformly of the partial sums to $\Phi(\omega, \cdot)$ along atTop.

The formalization commits to the following, relative to the page:

• The model's assumptions (1)–(3) of p. 286, non-negativity of $L$, and positivity and continuity of $P$ appear as hypotheses of every statement.
• A single return function $L$ is used, not stage-dependent $L_n$, as in display (1) and as the functional equation (2) requires. $P_n$ has the product form, which the paper adopts "unless stated to the contrary".
• Assumption (4), separate continuity of $T_\delta\,\omega$ in $\delta$ and in $\omega$, is strengthened to joint continuity of $(\delta, \omega) \mapsto T_\delta\,\omega$. This supports the paper's assertion (p. 287) that each term is a continuous function of $s$, which separate continuity does not give.
• $D$ is assumed nonempty. With $D$ empty there is no strategy and Theorem 1 is false.
• The paper leaves the class of admissible solutions open ("an appropriate class of M's for which the lim = 0"). The goal fixes it as the two-sided condition: for every $\omega$ and $\varepsilon > 0$ there is $N$ with $|M(\omega_n)|\,P_n(s) \le \varepsilon$ for all $n \ge N$ and all $s$. Both of the paper's examples verify this form.

Lean's tsum of a non-summable series is $0$, and a supremum of an unbounded family is $0$. Neither default can make a statement trivially true. The uniform-convergence hypothesis forces the series to converge, and under Theorem 1's hypotheses $\Phi(\omega, \cdot)$ is continuous on a compact space, so the supremum is a maximum. The goal's conclusion is stated without a supremum. A sorry-free check confirms that all hypotheses of the goal hold on a concrete instance with non-zero return: two decisions, constant return $1$, $P \equiv 1/2$, and $M \equiv 2$.

Needed infrastructure: Tychonoff's theorem, continuity of uniform limits, and attainment of maxima on compact spaces, all in Mathlib. The mission's own definitions are the trajectory, weights, partial and total yield, and the optimal return. Contributions of intermediate lemmas are welcome, for example continuity of $s \mapsto \omega_n$, summability from uniform convergence, and the upper and lower tail estimates for $M$. So are formalizations of the paper's Remarks 1 and 3 (Dini's theorem and convergence of the $k$-stage optimal returns).

Selected references

• S. Karlin, The Structure of Dynamic Programing Models, Naval Research Logistics Quarterly 2(4):285–294, 1955. https://doi.org/10.1002/nav.3800020408
• R. Bellman, Dynamic Programming, Princeton University Press, 1957. https://press.princeton.edu/books/paperback/9780691146683/dynamic-programming
• D. Blackwell, Discounted Dynamic Programming, Annals of Mathematical Statistics 36(1):226–235, 1965. https://doi.org/10.1214/aoms/1177700285
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978. https://web.mit.edu/dimitrib/www/soc.html