Fourier coefficients and the lowest-shell witness

TheoremFourier coefficients of a Fourier monomial on the 2-torus#✓fully proved

For frequencies \(m, n \in \mathbb{Z}^2\), the \(n\)-th Fourier coefficient, taken with respect to normalized Haar measure on \((\mathbb{R}/\mathbb{Z})^2\), of the monomial \(e_m(x) = e^{2\pi i\, m \cdot x}\) is \(1\) if \(n = m\) and \(0\) otherwise.

theorem mFourierCoeff_monomial (m n : Frequency) :
    UnitAddTorus.mFourierCoeff (UnitAddTorus.mFourier m) n = if n = m then 1 else 0

Uses 1 · Used by 2

Statement usesInteger frequencies

Used byFourier coefficients of the lowest-shell witness · The lowest-shell witness has mean zero

TheoremIntegrability of Fourier integrands on the 2-torus#✓fully proved

For every continuous function \(f : (\mathbb{R}/\mathbb{Z})^2 \to \mathbb{C}\) and every frequency \(n \in \mathbb{Z}^2\), the function \(x \mapsto e^{-2\pi i\, n \cdot x} f(x)\) is integrable with respect to normalized Haar measure.

theorem mFourierCoeff_integrable (f : C(UnitAddTorus (Fin 2), ℂ)) (n : Frequency) :
    Integrable (fun x ↦ UnitAddTorus.mFourier (-n) x * f x)

Uses 1 · Used by 2

Statement usesInteger frequencies

Used byAdditivity of Fourier coefficients on the 2-torus · The mean is the real part of the zeroth Fourier coefficient

TheoremAdditivity of Fourier coefficients on the 2-torus#✓fully proved

For continuous functions \(f, g : (\mathbb{R}/\mathbb{Z})^2 \to \mathbb{C}\) and every frequency \(n \in \mathbb{Z}^2\), the \(n\)-th Fourier coefficient \(\hat h(n) = \int e^{-2\pi i\, n \cdot x} h(x)\,dx\) (normalized Haar measure) satisfies \(\widehat{f + g}(n) = \hat f(n) + \hat g(n)\).

theorem mFourierCoeff_add (f g : C(UnitAddTorus (Fin 2), ℂ)) (n : Frequency) :
    UnitAddTorus.mFourierCoeff (f + g) n =
      UnitAddTorus.mFourierCoeff f n + UnitAddTorus.mFourierCoeff g n

Uses 2 · Used by 2

Statement usesInteger frequencies

Proof usesIntegrability of Fourier integrands on the 2-torus

Used byFourier coefficients of the lowest-shell witness · The lowest-shell witness has mean zero

TheoremHomogeneity of Fourier coefficients on the 2-torus#✓fully proved

For every \(c \in \mathbb{C}\), every continuous function \(f : (\mathbb{R}/\mathbb{Z})^2 \to \mathbb{C}\) and every frequency \(n \in \mathbb{Z}^2\), the \(n\)-th Fourier coefficient (normalized Haar measure) satisfies \(\widehat{c f}(n) = c\, \hat f(n)\).

theorem mFourierCoeff_smul (c : ℂ) (f : C(UnitAddTorus (Fin 2), ℂ)) (n : Frequency) :
    UnitAddTorus.mFourierCoeff (c • f) n = c * UnitAddTorus.mFourierCoeff f n

Uses 1 · Used by 2

Statement usesInteger frequencies

Used byFourier coefficients of the lowest-shell witness · The lowest-shell witness has mean zero

DefinitionAxis frequency#✓fully proved

For \(i \in \{0, 1\}\), the axis frequency \(e_i\) is the frequency in \(\mathbb{Z}^2\) whose \(i\)-th coordinate is \(1\) and whose other coordinate is \(0\).

def axisFrequency (i : Fin 2) : Frequency := Pi.single i 1

Uses 1 · Used by 8

Statement usesInteger frequencies

Used byFourier coefficients of the lowest-shell witness · Gradient energy of the lowest-shell witness · Laplacian energy of the lowest-shell witness · Lowest frequency shell · Lowest-shell unit polynomial · The lowest-shell unit polynomial is real-valued · Value of the lowest-shell witness at the origin · The lowest-shell witness has mean zero

DefinitionLowest-shell unit polynomial#✓fully proved

For \(n \in \mathbb{Z}^2\) let \(e_n(y) = e^{2\pi i\, n \cdot y}\) be the Fourier monomial on the unit torus \((\mathbb{R}/\mathbb{Z})^2\). The lowest-shell unit polynomial is the continuous function \(P : (\mathbb{R}/\mathbb{Z})^2 \to \mathbb{C}\) given by \(P = (4\pi)^{-1}\bigl(e_{(1,0)} + e_{(-1,0)} + e_{(0,1)} + e_{(0,-1)}\bigr)\), the normalized sum of the Fourier monomials of the four nonzero frequencies of smallest length.

def lowestShellUnit : C(UnitAddTorus (Fin 2), ℂ) :=
  (((4 * Real.pi)⁻¹ : ℝ) : ℂ) •
    ((UnitAddTorus.mFourier (axisFrequency 0) + UnitAddTorus.mFourier (-axisFrequency 0)) +
      (UnitAddTorus.mFourier (axisFrequency 1) + UnitAddTorus.mFourier (-axisFrequency 1)))

Uses 2 · Used by 6

Statement usesInteger frequencies · Axis frequency

Used byFourier coefficients of the lowest-shell witness · The lowest-shell unit polynomial is real-valued · Lowest-shell witness · Value of the lowest-shell witness at the origin · The lowest-shell witness has mean zero · Unit representative of the lowest-shell witness

DefinitionLowest-shell witness#✓fully proved

The lowest-shell witness is the continuous real function \(u\) on the torus \((\mathbb{R}/2\pi\mathbb{Z})^2\) given by \(u(x_1, x_2) = \frac{1}{4\pi}(e^{i x_1} + e^{-i x_1} + e^{i x_2} + e^{-i x_2}) = \frac{\cos x_1 + \cos x_2}{2\pi}\), the normalized sum of the four lowest nonzero Fourier modes.

def lowestShellWitness : C(Torus, ℝ) where
  toFun x := (lowestShellUnit (unitRescaling x)).re
  continuous_toFun := Complex.continuous_re.comp
    (lowestShellUnit.continuous.comp unitRescaling.continuous)

Uses 3 · Used by 9

Statement usesThe torus of period \(2\pi\) · Lowest-shell unit polynomial · Rescaling the torus to unit period

Used byFourier coefficients of the lowest-shell witness · Gradient energy of the lowest-shell witness · Laplacian energy of the lowest-shell witness · The lowest-shell witness is admissible at \(\delta = 1\) · Value of the lowest-shell witness at the origin · The lowest-shell witness is in \(H^2\) · The lowest-shell witness is a zero-mean \(H^2\) function · The lowest-shell witness has mean zero · Unit representative of the lowest-shell witness

TheoremThe lowest-shell unit polynomial is real-valued#✓fully proved

For every point \(y\) of the unit torus \((\mathbb{R}/\mathbb{Z})^2\), the lowest-shell unit polynomial \(P\) satisfies \(\operatorname{Im} P(y) = 0\).

Its Fourier modes come in opposite pairs \(\pm k\) with equal coefficients.

theorem lowestShellUnit_im_zero (x : UnitAddTorus (Fin 2)) : (lowestShellUnit x).im = 0

Uses 3 · Used by 1

Statement usesLowest-shell unit polynomial

Proof usesInteger frequencies · Axis frequency

Used byUnit representative of the lowest-shell witness

TheoremUnit representative of the lowest-shell witness#✓fully proved

The unit representative of the lowest-shell witness is the lowest-shell polynomial \((4\pi)^{-1}\bigl(e_{(1,0)} + e_{(-1,0)} + e_{(0,1)} + e_{(0,-1)}\bigr)\) on the unit torus \((\mathbb{R}/\mathbb{Z})^2\), where \(e_n(y) = e^{2\pi i\, n \cdot y}\) for \(n \in \mathbb{Z}^2\).

theorem unitRepresentative_lowestShellWitness :
    unitRepresentative lowestShellWitness = lowestShellUnit

Uses 6 · Used by 2

Statement usesLowest-shell unit polynomial · Lowest-shell witness · A function on the torus as a function on the unit torus

Proof usesThe torus of period \(2\pi\) · The lowest-shell unit polynomial is real-valued · Rescaling the torus to unit period

Used byFourier coefficients of the lowest-shell witness · The lowest-shell witness has mean zero

DefinitionLowest frequency shell#✓fully proved

The lowest shell is the set \(\{e_1, -e_1, e_2, -e_2\}\) of frequencies in \(\mathbb{Z}^2\), where \(e_1 = (1, 0)\) and \(e_2 = (0, 1)\); these are the four nonzero frequencies of smallest length.

def lowestShell : Finset Frequency := by
  classical
  exact {axisFrequency 0, -axisFrequency 0, axisFrequency 1, -axisFrequency 1}

Uses 2 · Used by 4

Statement usesInteger frequencies · Axis frequency

Used byFourier coefficients of the lowest-shell witness · Gradient energy of the lowest-shell witness · Laplacian energy of the lowest-shell witness · The lowest-shell witness is in \(H^2\)

TheoremFourier coefficients of the lowest-shell witness#✓fully proved

For every frequency \(k \in \mathbb{Z}^2\), the Fourier coefficient of the lowest-shell witness at \(k\) equals \(1/2\) if \(k\) lies in the lowest shell, that is, \(k\) is one of \((1, 0)\), \((-1, 0)\), \((0, 1)\), \((0, -1)\), and equals \(0\) otherwise.

theorem fourierCoefficient_lowestShellWitness (k : Frequency) :
    fourierCoefficient lowestShellWitness k = if k ∈ lowestShell then (1 / 2 : ℂ) else 0

Uses 12 · Used by 3

Statement usesInteger frequencies · Fourier coefficients on the torus · Lowest frequency shell · Lowest-shell witness

Proof usesThe torus of period \(2\pi\) · Axis frequency · Lowest-shell unit polynomial · Additivity of Fourier coefficients on the 2-torus · Fourier coefficients of a Fourier monomial on the 2-torus · Homogeneity of Fourier coefficients on the 2-torus · A function on the torus as a function on the unit torus · Unit representative of the lowest-shell witness

Used byGradient energy of the lowest-shell witness · Laplacian energy of the lowest-shell witness · The lowest-shell witness is in \(H^2\)

TheoremThe lowest-shell witness is in \(H^2\)#✓fully proved

The lowest-shell witness \(u\) belongs to the spectral Sobolev space \(H^2\): if \(a_k(u)\) denotes its Fourier coefficients, the series \(\sum_{k \in \mathbb{Z}^2} (1 + |k|^2)^2 |a_k(u)|^2\) converges.

theorem lowestShellWitness_isH2 : IsH2 lowestShellWitness

Uses 7 · Used by 1

Statement usesFunctions in \(H^2\) · Lowest-shell witness

Proof usesInteger frequencies · Fourier coefficients on the torus · Fourier coefficients of the lowest-shell witness · Squared frequency · Lowest frequency shell

Used byThe lowest-shell witness is a zero-mean \(H^2\) function

TheoremGradient energy of the lowest-shell witness#✓fully proved

The gradient energy of the lowest-shell witness equals \(1\).

theorem gradientEnergy_lowestShellWitness : gradientEnergy lowestShellWitness = 1

Uses 8 · Used by 1

Statement usesGradient energy · Lowest-shell witness

Proof usesInteger frequencies · Axis frequency · Fourier coefficients on the torus · Fourier coefficients of the lowest-shell witness · Squared frequency · Lowest frequency shell

Used byThe lowest-shell witness is admissible at \(\delta = 1\)

TheoremLaplacian energy of the lowest-shell witness#✓fully proved

The Laplacian energy of the lowest-shell witness equals \(1\).

theorem laplaceEnergy_lowestShellWitness : laplaceEnergy lowestShellWitness = 1

Uses 8 · Used by 1

Statement usesLaplacian energy · Lowest-shell witness

Proof usesInteger frequencies · Axis frequency · Fourier coefficients on the torus · Fourier coefficients of the lowest-shell witness · Squared frequency · Lowest frequency shell

Used byThe lowest-shell witness is admissible at \(\delta = 1\)

TheoremThe mean is the real part of the zeroth Fourier coefficient#✓fully proved

For every continuous function \(u : \mathbb{T} \to \mathbb{R}\) on the torus \(\mathbb{T} = (\mathbb{R}/2\pi\mathbb{Z})^2\), the mean of \(u\) equals the real part of the zeroth Fourier coefficient \(\int_{(\mathbb{R}/\mathbb{Z})^2} \tilde u(y)\,dy\), taken with respect to normalized Haar measure, of the unit representative \(\tilde u\) of \(u\) (the function \(u\), viewed as complex-valued and transported to the unit-period torus \((\mathbb{R}/\mathbb{Z})^2\)).

theorem mean_eq_mFourierCoeff_zero_re (u : C(Torus, ℝ)) :
    mean u = (UnitAddTorus.mFourierCoeff (unitRepresentative u) 0).re

Uses 7 · Used by 1

Statement usesThe torus of period \(2\pi\) · Mean of a function on the torus · A function on the torus as a function on the unit torus

Proof usesInteger frequencies · Integrability of Fourier integrands on the 2-torus · Normalized Haar measure on the unit torus · Rescaling the torus to unit period

Used byThe lowest-shell witness has mean zero

TheoremThe lowest-shell witness has mean zero#✓fully proved

The lowest-shell witness, the function \(w(x_1, x_2) = (\cos x_1 + \cos x_2)/(2\pi)\) on the torus \((\mathbb{R}/2\pi\mathbb{Z})^2\), has mean \(0\).

theorem mean_lowestShellWitness : mean lowestShellWitness = 0

Uses 11 · Used by 1

Statement usesLowest-shell witness · Mean of a function on the torus

Proof usesInteger frequencies · Axis frequency · Lowest-shell unit polynomial · Additivity of Fourier coefficients on the 2-torus · Fourier coefficients of a Fourier monomial on the 2-torus · Homogeneity of Fourier coefficients on the 2-torus · The mean is the real part of the zeroth Fourier coefficient · A function on the torus as a function on the unit torus · Unit representative of the lowest-shell witness

Used byThe lowest-shell witness is a zero-mean \(H^2\) function

TheoremThe unit rescaling fixes the origin#✓fully proved

The coordinate rescaling from the torus \((\mathbb{R}/2\pi\mathbb{Z})^2\) to the unit torus \((\mathbb{R}/\mathbb{Z})^2\) maps \(0\) to \(0\).

theorem unitRescaling_zero : unitRescaling (0 : Torus) = 0

Uses 2 · Used by 1

Statement usesThe torus of period \(2\pi\) · Rescaling the torus to unit period

Used byValue of the lowest-shell witness at the origin

TheoremValue of the lowest-shell witness at the origin#✓fully proved

The lowest-shell witness \(u\) takes the value \(u(0) = 1/\pi\) at the origin of the torus.

theorem lowestShellWitness_at_zero : lowestShellWitness 0 = 1 / Real.pi

Uses 7

Statement usesThe torus of period \(2\pi\) · Lowest-shell witness

Proof usesInteger frequencies · Axis frequency · Lowest-shell unit polynomial · Rescaling the torus to unit period · The unit rescaling fixes the origin

TheoremThe lowest-shell witness is a zero-mean \(H^2\) function#✓fully proved

The lowest-shell witness \(u\) belongs to the spectral Sobolev space \(H^2\) and has mean \(0\).

theorem lowestShellWitness_isZeroMeanH2 : IsZeroMeanH2 lowestShellWitness

Uses 6 · Used by 1

Statement usesZero-mean \(H^2\) functions · Lowest-shell witness

Proof usesFunctions in \(H^2\) · The lowest-shell witness is in \(H^2\) · Mean of a function on the torus · The lowest-shell witness has mean zero

Used byThe lowest-shell witness is admissible at \(\delta = 1\)

TheoremThe lowest-shell witness is admissible at \(\delta = 1\)#✓fully proved

The lowest-shell witness \(u\) satisfies the conditional constraints with \(\delta = 1\): it is a zero-mean \(H^2\) function on the torus, its gradient energy is \(1\), and its Laplacian energy is \(1\).

theorem lowestShellWitness_admissible : ConditionalAdmissible lowestShellWitness 1

Uses 8

Statement usesConditionally admissible functions · Lowest-shell witness

Proof usesZero-mean \(H^2\) functions · Gradient energy · Gradient energy of the lowest-shell witness · Laplacian energy · Laplacian energy of the lowest-shell witness · The lowest-shell witness is a zero-mean \(H^2\) function

TheoremUpper bounds for the conditional supremum#✓fully proved

Let \(\mathbb{T} = (\mathbb{R}/2\pi\mathbb{Z})^2\). For every real \(\delta\), let \(\theta(\delta)\), the conditional supremum, be the supremum in the extended reals of \(u(0)^2\) over all continuous functions \(u : \mathbb{T} \to \mathbb{R}\) that are conditionally admissible at \(\delta\), that is, zero-mean \(H^2\) functions with gradient energy \(1\) and Laplacian energy \(\delta\). Then for every extended real number \(b\), \(\theta(\delta) \le b\) if and only if \(u(0)^2 \le b\) for every such \(u\).

theorem theta_le_iff (δ : ℝ) (b : EReal) :
    theta δ ≤ b ↔ ∀ u : C(Torus, ℝ), ConditionalAdmissible u δ → ((u 0) ^ 2 : ℝ) ≤ b

Uses 4

Statement usesConditionally admissible functions · The torus of period \(2\pi\) · Conditional supremum of the squared value at the origin

Proof usesSquared values at the origin of admissible functions

TheoremUpper bounds for the sharp remainder#✓fully proved

Let \(\mathbb{T} = (\mathbb{R}/2\pi\mathbb{Z})^2\). For real \(\delta\), let \(\theta(\delta)\) be the supremum in the extended reals of \(u(0)^2\) over all continuous functions \(u : \mathbb{T} \to \mathbb{R}\) that are zero-mean \(H^2\) functions with gradient energy \(1\) and Laplacian energy \(\delta\), and let \(R(\delta) = 4\pi\,\theta(\delta) - \log\delta - \log(1 + \log\delta)\), computed in the extended reals. For every extended real number \(b\), the sharp remainder value \(\sup_{\delta \ge 1} R(\delta)\), a supremum in the extended reals, is at most \(b\) if and only if \(R(\delta) \le b\) for every real \(\delta \ge 1\).

theorem sharpRemainderValue_le_iff (b : EReal) :
    sharpRemainderValue ≤ b ↔ ∀ δ : ℝ, 1 ≤ δ → remainder δ ≤ b

Uses 2

Statement usesLogarithmic remainder · Sharp logarithmic remainder

TheoremFrequency weights are nonnegative#✓fully proved

For every frequency \(k = (k_0, k_1) \in \mathbb{Z}^2\), the frequency weight \(k_0^2 + k_1^2\) is nonnegative.

theorem frequencyWeight_nonneg (k : Frequency) : 0 ≤ frequencyWeight k

Uses 2 · Used by 2

Statement usesInteger frequencies · Squared frequency

Used by\(H^2\) functions have a summable gradient energy series · \(H^2\) functions have a summable Laplacian energy series

Theorem\(H^2\) functions have a summable gradient energy series#✓fully proved

If \(u\) is a continuous real function on the torus of period \(2\pi\) that lies in \(H^2\), with Fourier coefficients \(a_k\), then the family \(\left((k_0^2 + k_1^2) \, |a_k|^2\right)_{k \in \mathbb{Z}^2}\) is summable.

theorem IsH2.gradient_summable {u : C(Torus, ℝ)} (h : IsH2 u) :
    Summable fun k ↦ frequencyWeight k * ‖fourierCoefficient u k‖ ^ 2

Uses 6

Statement usesInteger frequencies · Functions in \(H^2\) · The torus of period \(2\pi\) · Fourier coefficients on the torus · Squared frequency

Proof usesFrequency weights are nonnegative

Theorem\(H^2\) functions have a summable Laplacian energy series#✓fully proved

If \(u\) is a continuous real function on the torus of period \(2\pi\) that lies in \(H^2\), with Fourier coefficients \(a_k\), then the family \(\left((k_0^2 + k_1^2)^2 \, |a_k|^2\right)_{k \in \mathbb{Z}^2}\) is summable.

theorem IsH2.laplace_summable {u : C(Torus, ℝ)} (h : IsH2 u) :
    Summable fun k ↦ frequencyWeight k ^ 2 * ‖fourierCoefficient u k‖ ^ 2

Uses 6

Statement usesInteger frequencies · Functions in \(H^2\) · The torus of period \(2\pi\) · Fourier coefficients on the torus · Squared frequency

Proof usesFrequency weights are nonnegative

TheoremFourier reconstruction#✓fully proved

Let \(u\) be a continuous real function on the torus of period \(2\pi\) in each coordinate, let \(a_k\) (\(k \in \mathbb{Z}^2\)) be its Fourier coefficients, and let \(c_k = a_k / (2\pi)\) be the Fourier coefficients, with respect to normalized Haar measure, of its unit representative on \((\mathbb{R}/\mathbb{Z})^2\). If the family \((c_k)_{k \in \mathbb{Z}^2}\) is summable, then for every point \(x\) of the torus, with unit rescaling \(y \in (\mathbb{R}/\mathbb{Z})^2\), the series \(\sum_{k \in \mathbb{Z}^2} (2\pi)^{-1} a_k \, e^{2\pi i (k_0 y_0 + k_1 y_1)}\) converges unconditionally to \(u(x)\).

theorem fourierReconstruction (u : C(Torus, ℝ))
    (h : Summable (UnitAddTorus.mFourierCoeff (unitRepresentative u))) (x : Torus) :
    HasSum (fun k ↦ (2 * Real.pi : ℂ)⁻¹ * fourierCoefficient u k *
      UnitAddTorus.mFourier k (unitRescaling x)) (u x : ℂ)

Uses 5

Statement usesInteger frequencies · The torus of period \(2\pi\) · Fourier coefficients on the torus · A function on the torus as a function on the unit torus · Rescaling the torus to unit period

26 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.