Weak tiling problems

Problems 4.1, 4.2, and 4.3 from arxiv/2506.23631.

Reference:

• Geometric implications of weak tiling

See also FormalConjectures.Wikipedia.Fuglede for Fuglede's spectral set conjecture, which motivates the study of weak tilings.

def WeakTiling.IsUnionOfNIntervals (n : ℕ) (A : Set ℝ) : Prop

A set $A \subseteq \mathbb{R}$ is a union of $n$ intervals if it can be written as $A = \bigcup_{i=1}^{n} (a_i, b_i)$ with $a_1 < b_1 < a_2 < b_2 < \dots < a_n < b_n$, i.e., as a disjoint union of $n$ nondegenerate open intervals in strict order with strict separation. This matches the convention of the paper (see e.g. Theorem 3.4 there).

Equations

• WeakTiling.IsUnionOfNIntervals n A = ∃ (a : Fin n → ℝ) (b : Fin n → ℝ), (∀ (i : Fin n), a i < b i) ∧ (∀ (i j : Fin n), i < j → b i < a j) ∧ A = ⋃ (i : Fin n), Set.Ioo (a i) (b i)

def WeakTiling.IsFiniteUnionOfIntervals (A : Set ℝ) : Prop

A set $A \subseteq \mathbb{R}$ is a finite union of intervals if it is a union of $n$ intervals for some $n$.

Equations

• WeakTiling.IsFiniteUnionOfIntervals A = ∃ (n : ℕ), WeakTiling.IsUnionOfNIntervals n A

def WeakTiling.IsWeakTilingMeasure (Ω : Set ℝ) (ν : MeasureTheory.Measure ℝ) : Prop

A positive, locally finite Borel measure $\nu$ on $\mathbb{R}$ is a weak tiling measure for a bounded measurable set $\Omega \subset \mathbb{R}$ if the convolution $1_\Omega \ast \nu = 1_{\Omega^c}$ holds almost everywhere, i.e., $\int 1_\Omega(x - t) \, d\nu(t) = 1_{\Omega^c}(x)$ for a.e. $x \in \mathbb{R}$.

This is Definition 1.1 from the paper.

Equations

• One or more equations did not get rendered due to their size.

def WeakTiling.IsProperTiling (Ω T : Set ℝ) : Prop

A proper tiling of $\Omega^c$ by translates of $\Omega$ is specified by a set of translation parameters $T \subseteq \mathbb{R}$ such that the sum of Dirac masses on $T$ is a weak tiling measure for $\Omega$.

Equations

• WeakTiling.IsProperTiling Ω T = WeakTiling.IsWeakTilingMeasure Ω (MeasureTheory.Measure.sum fun (t : ↑T) => MeasureTheory.Measure.dirac ↑t)

def WeakTiling.HasBoundedDensity (Λ : Set ℝ) : Prop

A set $\Lambda \subseteq \mathbb{R}$ has bounded density if the number of points of $\Lambda$ in any unit open interval is uniformly bounded: $\sup_{x \in \mathbb{R}} \#(\Lambda \cap (x, x + 1)) < \infty$.

Equations

• WeakTiling.HasBoundedDensity Λ = ∃ (C : ℕ), ∀ (x : ℝ), (Λ ∩ Set.Ioo x (x + 1)).Finite ∧ (Λ ∩ Set.Ioo x (x + 1)).ncard ≤ C

theorem WeakTiling.problem_4_1 : True ↔ ∀ (Ω : Set ℝ), IsFiniteUnionOfIntervals Ω → ∀ (ν : MeasureTheory.Measure ℝ), IsWeakTilingMeasure Ω ν → HasBoundedDensity ν.support

Problem 4.1. Let $\Omega \subset \mathbb{R}$ be a finite union of intervals and $\nu$ a weak tiling measure for $\Omega$. Must $\mathrm{supp}(\nu)$ have bounded density?

theorem WeakTiling.problem_4_2 : True ↔ ∀ (n : ℕ), 3 ≤ n → ∀ (Ω : Set ℝ), IsUnionOfNIntervals n Ω → ∀ (ν : MeasureTheory.Measure ℝ), IsWeakTilingMeasure Ω ν → ∃ (T : Set ℝ), IsProperTiling Ω T

Problem 4.2. Let $\Omega \subset \mathbb{R}$ be a finite union of three or more intervals. If $\Omega$ weakly tiles its complement, must it also tile its complement properly?

theorem WeakTiling.problem_4_3 : True ↔ ∀ (Ω : Set ℝ), IsFiniteUnionOfIntervals Ω → ∀ (ν : MeasureTheory.Measure ℝ), IsWeakTilingMeasure Ω ν → ∃ (T : ℕ → Set ℝ) (c : ℕ → NNReal), (∀ (i : ℕ), IsProperTiling Ω (T i)) ∧ ∑' (i : ℕ), c i = 1 ∧ ν = MeasureTheory.Measure.sum fun (i : ℕ) => ↑(c i) • MeasureTheory.Measure.sum fun (t : ↑(T i)) => MeasureTheory.Measure.dirac ↑t

Problem 4.3. Let $\Omega \subset \mathbb{R}$ be a finite union of intervals and $\nu$ a weak tiling measure for $\Omega$. Must $\nu$ be expressible as a convex combination of proper tiling measures?