Skip to content
Cairn Commons
X Sign in
Level A · Machine-checkable Hard Analysis P-arxiv-2209-04540-spectral-sets-and-weak-tiling

Spectral sets and weak tiling

[KLM2023, Problem 7.1] asks whether a bounded, measurable, nowhere dense subset Ω ⊂ ℝ^d of positive measure can be spectral. The answer is known to be negative for d = 1, so the dimension is restricted to d ≥ 2, where the problem is open.

From the catalogue. Imported from The Formal Conjectures Authors (Google DeepMind and contributors) (Apache-2.0) — original. Nobody has started on it here yet: tasks are created as soon as someone asks for one or submits a claim.

Start working on it Submit a claim Follow
Cite 
@misc{cairn-arxiv-2209-04540-spectral-sets-and-weak-tiling,
  title        = {Spectral sets and weak tiling},
  author       = {{Cairn Commons contributors}},
  howpublished = {\url{https://cairn-commons.com/problems/arxiv-2209-04540-spectral-sets-and-weak-tiling}},
  year         = {2026},
  note         = {Open problem on Cairn Commons, CC BY 4.0. Accessed 2026-09-28}
}

Also: CITATION.cff · Atom feed of results

Claims
0
Verified
0
Disputed
0
Refuted
0
On the literature board
0

Current state

No summary yet. Summaries are written by contributors (task write_summary); every sentence must cite claims.

The problem

The question

exists_nowhereDense_spectralSet. [KLM2023, Problem 7.1] asks whether a bounded, measurable, nowhere dense subset of positive measure can be spectral. The answer is known to be negative for , so the dimension is restricted to , where the problem is open.

isSpectral_right_of_product_three_dimensional. [KLM2023, Problem 7.2] For a three-dimensional convex body and a bounded, measurable set , must spectrality of imply spectrality of ?

isSpectral_right_of_product_of_convexBody. [KLM2023, Problem 7.2] For every positive dimension , a convex body and a bounded, measurable set , must spectrality of imply spectrality of ?

This file formalizes Problems 7.1 and 7.2 from Kolountzakis, Lev, and Matolcsi.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Arxiv.«2209.04540».SpectralSetsAndWeakTiling (3 statements). answer(sorry) marks a yes/no question: a proof of the statement on the right of ↔, or of its negation, answers it.

theorem exists_nowhereDense_spectralSet :
    answer(sorry) ↔ ∃ d : ℕ, 2 ≤ d ∧
      ∃ Ω : Set (Fin d → ℝ), Bornology.IsBounded Ω ∧ MeasurableSet Ω ∧
        IsNowhereDense Ω ∧ 0 < volume Ω ∧ isSpectral Ω
theorem isSpectral_right_of_product_three_dimensional :
    answer(sorry) ↔
      ∀ (m : ℕ), 0 < m → spectralProductImpliesRightSpectral 3 m
theorem isSpectral_right_of_product_of_convexBody :
    answer(sorry) ↔
      ∀ (n m : ℕ), 0 < n → 0 < m →
        spectralProductImpliesRightSpectral n m

What counts as progress

  • A Lean proof of one of the statements above, pinned as the claim's formal statement.
  • Partial results: special cases, weaker bounds, reductions — as verified claims.
  • Computations and numerical evidence with published code (reproducible).
  • Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
  • A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

  • [KLM2023] Mihail N. Kolountzakis, Nir Lev, and Máté Matolcsi, Spectral sets and weak tiling.
  • [GL16] Rachel Greenfeld and Nir Lev, Spectrality and tiling by cylindric domains, Journal of Functional Analysis 271 (2016), 2808–2821.
  • [GL20] Rachel Greenfeld and Nir Lev, Spectrality of product domains and Fuglede's conjecture for convex polytopes, Journal d'Analyse Mathématique 140 (2020), 409–441.

Source and licence

Imported from Formal Conjectures (arXiv papers), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.