Papers With

← All papers
First page of Cantor measures with odd base do not admit Fourier frames

Cantor measures with odd base do not admit Fourier frames

Jaume de Dios Pont, Lukas Liehr, Mitchell A. Taylor

math.FA Jul 9, 2026 · v1
formalization analysis
Read PDF arXiv abstract Code
TL;DR
The main theorem that odd-base Cantor measures admit no Fourier frame is formalized and verified in Lean 4 using Mathlib.
Abstract
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.
Problem

It is unknown whether certain Cantor measures, such as the middle-third Cantor measure, admit a Fourier frame, a question of Strichartz. Frame-spectrality generalizes the existence of an orthonormal Fourier basis.

Approach

The authors prove that the Cantor measure with base b does not admit a Fourier frame for any odd integer b>1. The argument uses Haar functions on Cantor sets, self-similarity of the measure, and a contradiction argument based on estimates of the Fourier transform modulus. The main result is additionally formalized in Lean 4, relying on Mathlib's measure-theoretic definitions, with the theorem statement curated by the authors and proof files partly generated by large language models.

Results

The Cantor measure with odd base b admits no Fourier frame, answering Strichartz's question for the middle-third Cantor measure. The main theorem was Lean-verified via the statement NoFourierFrameExists.