Fourier energy of translation boundaries

The character basis diagonalizes translation. This file develops the finite sum identities used in the spectral growth estimate directly, without introducing a weighted graph or its eigenvalues.

theorem EGZ.Expansion.re_sum {ι : Type u_1} (I : Finset ι) (f : ι → ℂ) : (∑ i ∈ I, f i).re = ∑ i ∈ I, (f i).re

theorem EGZ.Expansion.wInner_sum_left {G : Type u_1} {ι : Type u_2} [Fintype G] (I : Finset ι) (w : G → ℝ) (f : ι → G → ℂ) (g : G → ℂ) : ⟪∑ i ∈ I, f i, g⟫_[ℂ, w] = ∑ i ∈ I, ⟪f i, g⟫_[ℂ, w]

theorem EGZ.Expansion.wInner_sum_right {G : Type u_1} {ι : Type u_2} [Fintype G] (I : Finset ι) (w : G → ℝ) (f : G → ℂ) (g : ι → G → ℂ) : ⟪f, ∑ i ∈ I, g i⟫_[ℂ, w] = ∑ i ∈ I, ⟪f, g i⟫_[ℂ, w]

noncomputable def EGZ.Expansion.fourierCoeff {G : Type u_1} [AddCommGroup G] [Fintype G] (f : G → ℂ) (χ : AddChar G ℂ) : ℂ

Coordinates in the normalized orthonormal character basis.

Equations

• EGZ.Expansion.fourierCoeff f χ = ((AddChar.complexBasis G).repr f) χ

theorem EGZ.Expansion.fourier_expansion {G : Type u_1} [AddCommGroup G] [Fintype G] (f : G → ℂ) : ∑ χ : AddChar G ℂ, fourierCoeff f χ • ⇑χ = f

theorem EGZ.Expansion.inner_character_sums {G : Type u_1} [AddCommGroup G] [Fintype G] (c d : AddChar G ℂ → ℂ) : ⟪∑ χ : AddChar G ℂ, c χ • ⇑χ, ∑ χ : AddChar G ℂ, d χ • ⇑χ⟫ₙ_[ℂ] = ∑ χ : AddChar G ℂ, (starRingEnd ℂ) (c χ) * d χ

theorem EGZ.Expansion.fourier_inner {G : Type u_1} [AddCommGroup G] [Fintype G] (f g : G → ℂ) : ⟪f, g⟫ₙ_[ℂ] = ∑ χ : AddChar G ℂ, (starRingEnd ℂ) (fourierCoeff f χ) * fourierCoeff g χ

Finite Parseval identity in normalized character coordinates.

theorem EGZ.Expansion.fourierCoeff_eq_inner {G : Type u_1} [AddCommGroup G] [Fintype G] (f : G → ℂ) (χ : AddChar G ℂ) : fourierCoeff f χ = ⟪⇑χ, f⟫ₙ_[ℂ]

theorem EGZ.Expansion.fourier_translation_inner {G : Type u_1} [AddCommGroup G] [Fintype G] (f : G → ℂ) (a : G) : ⟪f, fun (x : G) => f (x + a)⟫ₙ_[ℂ] = ∑ χ : AddChar G ℂ, (starRingEnd ℂ) (fourierCoeff f χ) * fourierCoeff f χ * χ a

noncomputable def EGZ.Expansion.setIndicator {G : Type u_1} [DecidableEq G] (Y : Finset G) (x : G) : ℂ

The complex-valued indicator of a finite subset of the group.

Equations

• EGZ.Expansion.setIndicator Y x = if x ∈ Y then 1 else 0

noncomputable def EGZ.Expansion.density {G : Type u_1} [Fintype G] (Y : Finset G) : ℝ

The proportion of group elements belonging to the finite subset.

Equations

• EGZ.Expansion.density Y = ↑Y.card / ↑(Fintype.card G)

theorem EGZ.Expansion.sum_setIndicator {G : Type u_1} [Fintype G] [DecidableEq G] (Y : Finset G) : ∑ x : G, setIndicator Y x = ↑Y.card

theorem EGZ.Expansion.inner_setIndicator_self {G : Type u_1} [Fintype G] [DecidableEq G] (Y : Finset G) : ⟪setIndicator Y, setIndicator Y⟫ₙ_[ℂ] = ↑(density Y)

theorem EGZ.Expansion.fourierCoeff_setIndicator_zero {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (Y : Finset G) : fourierCoeff (setIndicator Y) 0 = ↑(density Y)

theorem EGZ.Expansion.sum_fourierCoeff_normSq {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (Y : Finset G) : ∑ χ : AddChar G ℂ, Complex.normSq (fourierCoeff (setIndicator Y) χ) = density Y

theorem EGZ.Expansion.inner_setIndicator_translation {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (Y : Finset G) (a : G) : ⟪setIndicator Y, fun (x : G) => setIndicator Y (x - a)⟫ₙ_[ℂ] = ↑(translate Y a ∩ Y).card / ↑(Fintype.card G)

theorem EGZ.Expansion.boundary_fourier {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (Y : Finset G) (a : G) : ↑(boundary Y a) / ↑(Fintype.card G) = density Y - ∑ χ : AddChar G ℂ, Complex.normSq (fourierCoeff (setIndicator Y) χ) * (χ (-a)).re

The energy of one translation, expressed in character coordinates.

theorem EGZ.Expansion.translation_energy {G : Type u_1} {ι : Type u_2} [AddCommGroup G] [Fintype G] [DecidableEq G] [Fintype ι] (Y : Finset G) (w : ι → ℝ) (a : ι → G) : (∑ i : ι, w i * ↑(boundary Y (a i))) / ↑(Fintype.card G) = (∑ i : ι, w i) * density Y - ∑ χ : AddChar G ℂ, Complex.normSq (fourierCoeff (setIndicator Y) χ) * ∑ i : ι, w i * (χ (-a i)).re

Fourier identity for an arbitrary finite real-weighted family of translations, allowing repeated translation vectors.

theorem EGZ.Expansion.spectral_boundary_average {G : Type u_1} {ι : Type u_2} [AddCommGroup G] [Fintype G] [DecidableEq G] [Fintype ι] (Y : Finset G) (w : ι → ℝ) (a : ι → G) (hw : ∀ (i : ι), 0 ≤ w i) {η : ℝ} (hη : 0 ≤ η) (hhalf : 2 * Y.card ≤ Fintype.card G) (hgap : ∀ (χ : AddChar G ℂ), χ ≠ 0 → ∑ i : ι, w i * (χ (-a i)).re ≤ (1 - η) * ∑ i : ι, w i) : (η * ∑ i : ι, w i) * ↑Y.card ≤ 2 * ∑ i : ι, w i * ↑(boundary Y (a i))

A gap in every nontrivial character implies average boundary growth. This is the finite Cayley-graph spectral estimate in multiplicity form.

theorem EGZ.Expansion.exists_boundary_of_spectral_gap {G : Type u_1} {ι : Type u_2} [AddCommGroup G] [Fintype G] [DecidableEq G] [Fintype ι] (Y : Finset G) (w : ι → ℝ) (a : ι → G) (hw : ∀ (i : ι), 0 ≤ w i) (hW : 0 < ∑ i : ι, w i) {η : ℝ} (hη : 0 ≤ η) (hhalf : 2 * Y.card ≤ Fintype.card G) (hgap : ∀ (χ : AddChar G ℂ), χ ≠ 0 → ∑ i : ι, w i * (χ (-a i)).re ≤ (1 - η) * ∑ i : ι, w i) : ∃ (i : ι), 0 < w i ∧ η * ↑Y.card ≤ 2 * ↑(boundary Y (a i))

Some positive-weight translation achieves the spectral average bound.