Fuglede's conjecture in dimensions 1 and 2

References:

• Fuglede's conjecture

def Fuglede.FugledeConjectureFor (n : ℕ) : Prop

Fuglede's conjecture in dimension n: A bounded subset of ℝ^n with positive Lebesgue measure is spectral iff it tiles ℝ^n by translation.

Equations

• Fuglede.FugledeConjectureFor n = ∀ (Ω : Set (Fin n → ℝ)), Bornology.IsBounded Ω → MeasurableSet Ω → 0 < MeasureTheory.volume Ω → (isSpectral Ω ↔ tilesByTranslation Ω)

theorem Fuglede.FugledeConjecture.variants.dim_1 : True ↔ FugledeConjectureFor 1

Fuglede's conjecture in one dimension: A bounded subset of ℝ with positive Lebesgue measure is spectral iff it tiles ℝ by translation.

theorem Fuglede.FugledeConjecture.variants.dim_2 : True ↔ FugledeConjectureFor 2

Fuglede's conjecture in two dimensions: A bounded subset of ℝ^2 with positive Lebesgue measure is spectral iff it tiles ℝ^2 by translation.

theorem Fuglede.FugledeConjecture.variants.dim_3_or_higher : False ↔ ∀ (n : ℕ), 3 ≤ n → FugledeConjectureFor n

Fuglede's conjecture in three or higher dimensions has been disproven. (Note that counterexamples in lower dimensions would also disprove the conjecture in higher dimensions.)