Spectral sets

This file defines the basic notions used in problems related to spectral sets and Fuglede's conjecture: translations, exponential characters, spectral pairs, spectral sets, and translational tilings in Euclidean space.

def translateSet {d : ℕ} (Ω : Set (Fin d → ℝ)) (t : Fin d → ℝ) : Set (Fin d → ℝ)

The translate of a set Ω by a vector t.

Equations

• translateSet Ω t = {x : Fin d → ℝ | x - t ∈ Ω}

noncomputable def exponentialCharacter {d : ℕ} (ξ x : Fin d → ℝ) : ℂ

The exponential character x ↦ exp(2π i ⟪ξ, x⟫).

Equations

• exponentialCharacter ξ x = Complex.exp (2 * ↑Real.pi * Complex.I * ↑(∑ i : Fin d, ξ i * x i))

theorem continuous_exponentialCharacter {d : ℕ} (ξ : Fin d → ℝ) : Continuous (exponentialCharacter ξ)

The exponential character is continuous.

theorem norm_exponentialCharacter {d : ℕ} (ξ x : Fin d → ℝ) : ‖exponentialCharacter ξ x‖ = 1

The exponential character has norm one.

theorem exponentialCharacter_memLp {d : ℕ} {Ω : Set (Fin d → ℝ)} (hΩ_finite : MeasureTheory.volume Ω ≠ ⊤) (ξ : Fin d → ℝ) : MeasureTheory.MemLp (exponentialCharacter ξ) 2 (MeasureTheory.volume.restrict Ω)

On a finite-measure set, every exponential character belongs to L^2.

def spectralPair {d : ℕ} (Ω Λ : Set (Fin d → ℝ)) : Prop

(Ω, Λ) is called a spectral pair if Λ is a spectrum for Ω, i.e. a set Λ of frequencies such that the associated exponential characters form an orthogonal basis of L^2(Ω).

Equations

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

def isSpectral {d : ℕ} (Ω : Set (Fin d → ℝ)) : Prop

A set is spectral if it belongs to a spectral pair.

Equations

• isSpectral Ω = ∃ (Λ : Set (Fin d → ℝ)), spectralPair Ω Λ

def tilesByTranslation {d : ℕ} (Ω : Set (Fin d → ℝ)) : Prop

A set Ω tiles ℝ^d by translation if there exists a set T of translation vectors such that the translates of Ω by T cover ℝ^d without overlap.

Equations

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