arXiv subjects

Mitchell A. Taylor

Publications and source records attributed to Mitchell A. Taylor.

At least 19 recordsLinked to original sources

arXiv2026

Phase retrieval from a uniformly discrete point set

We prove that for every window $w$ of the form $w(x) = e^{-π|x|^2} h(x)$, where $h$ is a polynomial, there exists a uniformly discrete set of points $\mathcal{S} \subset \mathbb R^{2d}$ such that the magnitude of the short-time Fourier transform $V_w f$ on $\mathcal{S}$ determines every $f \in L^2(\mathbb R^d)$ up to a constant phase factor. The separation distance can be chosen independent of the degree of $h$ and proportional to the square root of the dimension. The proof combines a discrete norming inequality, based on a multidimensional Remez inequality and VC-dimension bounds, with tail estimates for the reproducing kernel. A formalization of our main result in Lean 4 is also provided.

math.CA↗

arXiv2026

Counterexamples to Grad's conjecture

For each sufficiently large $N$, we construct smooth solutions of the magnetohydrostatic equations on embedded solid tori whose regular pressure levels are nested tori, whose magnetic field vanishes exactly on a round magnetic axis, and whose group of Euclidean symmetries, even when isometries reversing the sign of the field are admitted, is exactly the cyclic group $C_N$ of rotations through multiples of $2π/N$. For each such $N$, these equilibria form a smooth one-parameter family which is locally nontrivial in the moduli space of embedded configurations and have none of the plane-reflection, axial, or helical symmetries conjectured by Grad. A Lean 4 certification of the above results is also provided.

math.AP↗

arXiv2026

Energy minimization for eight points on the sphere

We study the energy minimization problem for eight points on the unit sphere. For the logarithmic and Coulomb energies, we show that the unique global minimizer up to congruence is a square antiprism with height characterized by a unique stationarity equation. The proof is computer-assisted and fully verified in Lean. After this, we consider generalizations of the result to other important energies. For the Riesz $s$-energies, we provide a Lean-verified, non-computer-assisted proof that the square antiprism with height depending on $s$ is the unique global minimizer for all sufficiently large $s$, and a computer-assisted proof that this in fact holds for all $s\geq 0$. We also give examples of energies arising from completely monotonic potentials for which the square antiprism is not a global minimizer, answering in the negative a universality question of Cohn and Woo.

math.MG↗

arXiv2026

Universal completeness of exponentials

We consider generalizations of the classical Fourier uniqueness theorem. First, we construct a family of uniformly discrete sets $Λ\subset \mathbb{R}$, of uniform density one, such that the exponential system $\{e^{2πiλx} : λ\in Λ\}$ is complete in $L^p(S)$ for every $1 \leq p < \infty$ and every measurable set $S \subset \mathbb{R}$ with $|S| < 1$. We also show that no set that is asymptotically integer can have this universality property. Additionally, for every $v \in (0,1)$, we construct a set of integer frequencies and uniform density $v$ whose exponential system is complete in $L^p(S)$ for every $1 \leq p < \infty$ and every measurable set $S \subset [0,1]$ with $|S| < v$. Finally, we prove that the Sobolev regularity condition $α> \frac12$ for the existence of uniformly discrete uniqueness sets for spectra with periodic weak gaps, considered by Olevskii and Ulanovskii, is sharp. Our findings admit extensions to higher dimensions and are verified in Lean.

math.CA↗

arXiv2026

Derivatives of Theta Functions and a Problem of Lyubarskii and Nes

We characterize all lattices $Λ\subset \mathbb{R}^2$ of rational density for which the Gabor system generated by the first Hermite function along $Λ$ is a frame for $L^2(\mathbb{R})$. We prove that these are precisely the lattices whose density satisfies $D(Λ) = \frac{q}{p} $ where $p,q \in \mathbb{N}$ are coprime with $q \geq p+2$, thereby confirming a conjecture of Lyubarskii and Nes. A formalization of our main result in Lean $4$ is also included.

math.CA↗

arXiv2026

Aliprantis's questions on locally solid topologies

In 1974, C. D. Aliprantis posed several questions concerning topological completions of locally solid vector lattices. We answer all of them in the negative. We construct Hausdorff locally convex-solid vector lattices showing that, without metrizability, neither the $σ$-Lebesgue property nor property (B, i) need pass to the completion; a positive element of the completion need not be the limit of a decreasing sequence of upper elements; the generalized (A, 0) property need not make the canonical image a regular sublattice; and regularity of this image need not imply order density. All five counterexamples have been formalized in Lean 4 using the Banach lattice Lean library.

math.FA↗

arXiv2026

Grothendieck's theorem for Bessel sequences

We establish a sharp version of Grothendieck's theorem for Bessel sequences. Precisely, given a Bessel sequence $\{ x_j \}_{j\in\mathbb{N}}$ with Bessel bound $1$ in a Hilbert space, we show that there exists functions $\{ f_j \}_{j\in\mathbb{N}}$ belonging to the unit ball of $L^\infty([0,1])$ such that for all $j,k \in \mathbb{N}$ one has $$ \langle x_j,x_k\rangle = \int_0^1 f_j(x)\overline{f_k(x)}\,dx.$$ As an application, we give an affirmative answer to an extension problem of Olevskii: if $E \subset [0,1]$ is a Lebesgue measurable set such that $[0,1]\setminus E$ has positive measure, then every Bessel sequence in $L^2(E)$ with Bessel bound $1$ extends to an orthonormal system in $L^2([0,1])$ that is bounded by the (optimal) constant $λ([0,1]\setminus E)^{-1/2}$ on $[0,1]\setminus E$. A formalization of our main result in Lean 4 accompanies the paper.

math.FA↗

arXiv2026

Banach lattices and phase retrieval: A case study for the use of AI in mathematics

The ability of large language models to assist professional mathematicians has been progressing rapidly. Earlier this year, a group of researchers in Banach lattice theory and phase retrieval began incorporating this technology into their research workflows. Facing challenges about the reliability of these models, they also decided to couple the discovery process with Lean verification. Here, we present a case study of how this has led to a more united community and a deeper understanding of our field.

math.FA↗

arXiv2026

Gabor Frames of Totally Positive Functions: A Complete Characterization

We prove that the set of time-frequency shifts $\{e^{2πi βl t} g(t-αk) : k,l \in \mathbb{Z}\}$ with a continuous, integrable totally positive function $g$ and lattice parameters $α,β>0$ generates a frame for $L^2(\mathbb{R})$ if and only if $αβ<1$. This fully settles the so-called frame set problem for the class of totally positive functions. As a closely related result we prove a sharp Kadets-type theorem for every shift-invariant space generated by a continuous totally positive function. The proofs are based on Fredholm theory and limit-operator theory. A formalization of our main result in Lean 4 is also provided.

math.FA↗

arXiv2026

Cantor measures with odd base do not admit Fourier frames

We prove that the Cantor measure with base $b$ does not admit a Fourier frame whenever $b > 1$ is an odd integer. In particular, this answers a question of Strichartz on the existence of a Fourier frame for the middle third Cantor measure. A formalization of our main result in Lean 4 is also provided.

math.FA↗

arXiv2026

Stable Phase Retrieval for Spans of Independent Random Variables

We prove that, after $L^2$ normalization, stable phase retrieval holds over the $L^2$-spans of independent real-valued centered random variables if and only if all but possibly one coordinate satisfies a uniform two-sided $L^1$ bound. This provides a complete characterization of stable phase retrieval for such subspaces, building upon the pioneering work of Calderbank--Daubechies--Freeman--Freeman and confirming the conjectured characterization communicated to us by those authors. We provide two different proofs of this fact, both based on a decomposition of the $\ell^2$-coefficients of each random variable. The first is a compactness proof, which makes use of the infinite divisibility of limit laws of tail sums. The second is a quantitative proof, which substitutes the compactness step with an explicit dichotomy based on anticoncentration estimates of Sperner type. This latter proof was partially LLM generated based on the ideas in the first proof and a considerable amount of guidance by the authors. An autoformalization of our main result in Lean 4 is also provided, following the ideas in the quantitative proof.

math.FA↗

arXiv2026

On the existence problem of regular Gabor frames

For every dimension $d > 1$, we establish explicit criteria on lattices $Λ\subset \mathbb{R}^{2d}$ with density $D(Λ) > 1$ such that no function with a continuous Zak transform generates a Gabor frame along $Λ$. In particular, this gives a negative answer to the existence problem of Gabor frames with window functions in the Schwartz space, the Feichtinger algebra, and the Fourier-invariant Wiener space. Our result is based on a characterization of when a collection of quasiperiodic functions admits a common zero, which may be of independent interest. We also include a formalization of our main result in Lean 4.

math.FA↗

arXiv2026

$L^2$-Stability for STFT phase retrieval

We prove that the short-time Fourier transform with Gaussian window performs $L^2$-local stable phase retrieval at the constant function. The proof involved significant interplay between mathematicians and LLMs. An autoformalization in Lean 4 of an extension of our result to $L^2$-local stable phase retrieval for all Hermite windows and all elements in the finite span of the canonical basis vectors is also presented.

math.FA↗

arXiv2026

Coordinate systems in Banach spaces and lattices

Using methods of descriptive set theory, in particular, the determinacy of infinite games of perfect information, we answer several questions from the literature regarding different notions of bases in Banach spaces and lattices. For the case of Banach lattices, our results follow from a general theorem stating that (under the assumption of analytic determinacy), every $σ$-order basis $(e_n)$ for a Banach lattice $X=[e_n]$ is a uniform basis, and every uniform basis is Schauder. Moreover, the notions of order and $σ$-order bases coincide when $X=[e_n].$ Regarding Banach spaces, we address two problems concerning filter Schauder bases for Banach spaces, i.e., in which the norm convergence of partial sums is replaced by norm convergence along some appropriate filter on $\mathbb N$. We first provide an example of a Banach space admitting such a filter Schauder basis, but no ordinary Schauder basis. Secondly, we show that every filter Schauder basis with respect to an analytic filter is also a filter Schauder basis with respect to a Borel filter.

math.FA↗

arXiv2026

A Classification of Order Convergence via a Transfinite Fatou Hierarchy

We investigate the descriptive complexity of order convergence in separable Banach lattices. While uniform convergence is Borel and $σ$-order convergence is known to be ${\bf Δ}^1_2$, it is unclear in general when $σ$-order convergence is analytic. We introduce a transfinite hierarchy of weakenings of the classical Fatou property, indexed by countable ordinals, and show that it provides a complete structural classification of this definability problem. For a separable Banach lattice $X$, we prove that the following are equivalent: (i) the set of decreasing positive sequences with infimum zero is Borel; (ii) $σ$-order convergence is analytic; and (iii) $X$ satisfies the $α$-Fatou property for some countable ordinal $α$. We further establish that the hierarchy is proper: for every countable ordinal $α$ there exists a separable Banach lattice with a countable $π$-basis that fails to be $α$-Fatou, but is $β$-Fatou for some $β>α$. Thus the Borel definability of order convergence is governed by a canonical ordinal invariant intrinsic to the lattice, and the descriptive complexity can be arbitrarily high below $ω_1$. These results identify projective complexity as a genuine structural invariant in Banach lattice theory.

math.FA↗

arXiv2026

Banach lattices with upper $p$-estimates: Renorming and factorization

The notions of $p$-convexity and concavity are fundamental tools for studying Banach lattices, as they partition the class of Banach lattices into a scale of spaces with $L_p$-like properties. Upper and lower $p$-estimates provide a refinement of this scale, modeled by the Lorentz spaces $L_{p,\infty}$ and $L_{p,1}$, respectively. In this article, we provide a comprehensive treatment of Banach lattices with upper $p$-estimates. In particular, we show that many well-known theorems about $p$-convex Banach lattices have analogues in the upper $p$-estimate setting, including the ability to represent all such spaces inside of infinity sums of model spaces, to canonically factor the convex operators and identify their associated operator ideals, as well as to give a precise description of the free objects and push-outs. Proving these results is far from straightforward and will require the development of a variety of new tools that avoid convexification and concavification procedures. In fact, we will identify many fundamental differences between the theories of $p$-convexity and upper $p$-estimates, particularly with regards to isometric problems and renormings.

math.FA↗

arXiv2025

Cheeger's Constant for the Gabor Transform and Ripples

We discover a new instability mechanism for short-time Fourier transform phase retrieval which yields that for any reasonable window function $ϕ$ in any dimension $d$, the local stability constant $c(f)$ defined via \begin{equation*} \inf_{|λ|=1}\|f- λg\|_{M^p(\mathbb{R}^{d})}\leq c(f)\| |V_ϕf|-|V_ϕ g|\|_\mathcal{D}, \hspace{5mm} \forall g\in M^p(\mathbb{R}^d), \end{equation*} is infinite on a dense set of vectors for all weighted fractional Sobolev norms $\mathcal{D}$, up to the sharp maximal regularity level ensuring that the problem is well-defined. This, in particular, answers an open problem of Rathmair, who asked whether exponential concentration of the Gabor transform on $\mathbb{R}^2$ guaranteed a finite local stability constant. For the specific case of Gabor phase retrieval, we further show that there is a complementary dense set where the local stability constant on $\mathbb{R}^{2d}$ is finite. Our results extend and complement a series of fundamental stability theorems for Gabor phase retrieval which have been proven over the last ten years. Of particular note is the work of Grohs and Rathmair, who showed that for sufficiently strong weighted Sobolev norms $\mathcal{D}$ on $\mathbb{R}^{2d}$, the local stability constant for Gabor phase retrieval is bounded by the inverse of the Cheeger constant of the flat metric conformally multiplied by $|V_ϕf|$. As a consequence of our analysis, we determine two dense families of functions, one of which has associated Cheeger constant zero and the other strictly positive. We also revisit the stability problem for STFT phase retrieval on bounded subsets of the time-frequency plane, for more general windows, and for restricted signal classes, extending and simplifying many influential results in the literature.

math.CA↗

arXiv2025

The Cahill-Casazza-Daubechies problem on Hölder stable phase retrieval

Phase retrieval using a frame for a finite-dimensional Hilbert space is known to always be Lipschitz stable. However, phase retrieval using a frame or a continuous frame for an infinite-dimensional Hilbert space is always unstable. In order to bridge the gap between the finite and infinite dimensional phenomena, Cahill-Casazza-Daubechies (Trans.Amer.Math.Soc. 2016) gave a construction of a family of nonlinear subsets of an infinite-dimensional Hilbert space where phase retrieval could be performed with a Hölder stability estimate. They then posed the question of whether these subsets satisfied Lipschitz stable phase retrieval. We solve this problem both by giving examples which fail Lipschitz stability and by giving examples which satisfy Lipschitz stability.

math.FA↗