Coordinate systems and maximal order complexity in Banach lattices
A. Avilés, C. Rosendal, M. A. Taylor, P. Tradacete
math.FA
Oct 24, 2026 · v1
TL;DR
The paper's results on order bases and coanalytic complexity in Banach lattices are formalized in Lean 4 using Mathlib and the BanLat library, with LLM assistance.
Abstract
We resolve three questions arising from the study of coordinate systems and order convergence in Banach lattices. Firstly, every order (respectively, $σ$-order) basis $(e_n)$ for a Banach lattice $X=[e_n]$ is automatically a Schauder basis. In fact, the associated partial sum projections satisfy a maximal inequality, and hence every such basis is uniform. Secondly, we show that there is a separable Banach lattice $X$ in which the set $$ X_{\downarrow0}=\{(x_n)\in X^{\mathbb N}:x_1\geqslant x_2\geqslant\ldots\geqslant 0=\inf_nx_n\} $$ is $\mathbfΠ^1_1$-complete. Finally, we construct a separable Banach lattice $Y$ for which the set $Y^{\uparrow\infty}$ of increasing positive sequences which are not order bounded is $\mathbfΠ^1_1$-complete. It follows that neither $X_{\downarrow0}$ nor $Y^{\uparrow\infty}$ can be described in any simpler way than by the nonexistence of positive lower and upper bounds, respectively.
Problem
Three questions about Banach lattices were left open in earlier work. Are order and σ-order bases automatically Schauder bases without assuming analytic determinacy? And is there a separable Banach lattice in which the set of sequences decreasing to zero, or the set of increasing sequences that are not order bounded, is Π^1_1-complete?
Approach
A lattice analogue of Mazur's weak-basis argument defines a norm ρ from order bounds on the partial sums, shows the resulting space is complete, and derives a maximal inequality. For the complexity results, weighted tree constructions over N^{<N} build separable Banach lattices (with E=L_1[0,1] and E=R) into which trees are reduced. Large language models helped produce the proofs and the Lean code. The results are formalized in Lean 4 with Mathlib and the BanLat library, and each statement is linked to its Lean theorem names.
Results
Every order or σ-order basis of X=[e_n] is a uniform basis, and hence a Schauder basis, satisfying a maximal inequality, with no extra set-theoretic hypothesis. The paper constructs separable Banach lattices X and Y for which X_{↓0} and Y^{↑∞} are Π^1_1-complete.
