The auxiliary kernel and Bessel lower bound

This file proves the kernel calculation (8) and the lower bound (14) in the proof of Theorem 1.4. All sums are finite and the normalization is made explicit.

noncomputable def Chvatal.auxiliaryKernel {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : Family ι) (q : Finset ι → ℝ) (y x : Finset ι) : ℝ

The function H_y from Section 3.1, with a general spectral multiplier q. The paper takes q = g - t.

Equations

• Chvatal.auxiliaryKernel F q y x = if x ∈ F then ↑(Fintype.card (Finset ι)) * Chvatal.fourier q (symmDiff x y) else 0

theorem Chvatal.sum_mul_fourier_translate {ι : Type u_1} [Fintype ι] [DecidableEq ι] (h q : Finset ι → ℝ) (y : Finset ι) : ∑ x : Finset ι, h x * fourier q (symmDiff x y) = ∑ S : Finset ι, q S * fourier h S * walsh S y

The convolution calculation preceding equation (8), before imposing the physical support condition on the auxiliary function.

theorem Chvatal.auxiliaryKernel_inner_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : Family ι) (q h : Finset ι → ℝ) (y : Finset ι) (hh : ∀ x ∉ F, h x = 0) : uniformInner h (auxiliaryKernel F q y) = ∑ x : Finset ι, h x * fourier q (symmDiff x y)

The physical support restriction cancels the indicator and the normalization in the inner product with H_y, as in the first line preceding equation (8).

theorem Chvatal.auxiliaryKernel_inner_fourier {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : Family ι) (q h : Finset ι → ℝ) (y : Finset ι) (hh : ∀ x ∉ F, h x = 0) : uniformInner h (auxiliaryKernel F q y) = ∑ S : Finset ι, q S * fourier h S * walsh S y

The spectral form of the inner product calculation in Section 3.1.

theorem Chvatal.auxiliaryKernel_inner_eigenvalue {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : Family ι) (q h : Finset ι → ℝ) (y : Finset ι) (hh : ∀ x ∉ F, h x = 0) (c : ℝ) (hc : ∀ (S : Finset ι), q S * fourier h S = c * fourier h S) : uniformInner h (auxiliaryKernel F q y) = c * h y

Equation (8) in its general form: a constant spectral multiplier on the Fourier support of h makes h an eigenfunction of the kernel.

theorem Chvatal.auxiliaryKernel_inner_outside {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F G : Family ι) (h : Finset ι → ℝ) (y : Finset ι) (t : ℝ) (hh : h ∈ supportSubspace F Gᶜ) : uniformInner h (auxiliaryKernel F (fun (S : Finset ι) => G.indicator S - t) y) = -t * h y

Equation (8), first case: Fourier support outside G gives eigenvalue -t.

theorem Chvatal.auxiliaryKernel_inner_inside {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F G : Family ι) (h : Finset ι → ℝ) (y : Finset ι) (t : ℝ) (hh : h ∈ supportSubspace F G) : uniformInner h (auxiliaryKernel F (fun (S : Finset ι) => G.indicator S - t) y) = (1 - t) * h y

Equation (8), second case: Fourier support inside G gives eigenvalue 1-t.

theorem Chvatal.auxiliaryKernel_norm_sq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : Family ι) (q : Finset ι → ℝ) (y : Finset ι) : uniformInner (auxiliaryKernel F q y) (auxiliaryKernel F q y) = ↑(Fintype.card (Finset ι)) * ∑ x ∈ F, fourier q (symmDiff x y) ^ 2

Equation (7), pointwise norm calculation for the auxiliary kernel.

theorem Chvatal.auxiliaryKernel_energy_identity {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : Family ι) (q : Finset ι → ℝ) : ∑ x ∈ F, ∑ y ∈ F, fourier q (symmDiff x y) ^ 2 = (∑ y ∈ F, uniformInner (auxiliaryKernel F q y) (auxiliaryKernel F q y)) / ↑(Fintype.card (Finset ι))

Equation (7): the squared Fourier kernel on F × F is the average, with factor 2^{-n}, of the squared norms of the auxiliary kernels.

theorem Chvatal.sum_sq_of_supported_unit {ι : Type u_1} [Fintype ι] (F : Family ι) (h : Finset ι → ℝ) (hh : ∀ x ∉ F, h x = 0) (hunit : uniformInner h h = 1) : ∑ x ∈ F, h x ^ 2 = ↑(Fintype.card (Finset ι))

A probability-unit function supported on F has unnormalized squared sum 2^n on F, as used immediately before equation (14).

theorem Chvatal.auxiliaryKernel_bessel_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F G : Family ι) (hF : F.IsIncreasing) (hG : G.IsIncreasing) (t : ℝ) : t ^ 2 * ↑(Finset.card (F \ G)) + (1 - t) ^ 2 * ↑(Finset.card (F \ G.dual)) ≤ ∑ x ∈ F, ∑ y ∈ F, fourier (fun (S : Finset ι) => G.indicator S - t) (symmDiff x y) ^ 2

Equation (14): Bessel's inequality applied to the two auxiliary families gives the sharp lower bound on the squared Fourier kernel restricted to F × F. No positivity assumptions on t or nonemptiness assumptions on the families are needed.