Finite symmetric Fourier cutoffs on the two-torus

The frequency box is indexed by integer pairs and is invariant under negation. The Fourier partial sum of a real-valued function is therefore real-valued; the real projection below is its real part, with a theorem identifying its complexification with the partial sum itself.

@[instance_reducible]

noncomputable def basisMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

Use normalized Haar measure on the unit circle for periodic integrals.

Equations

• basisMeasureSpaceUnitAddCircle = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }

theorem basisMeasureIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem basisProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

@[reducible, inline]

abbrev AVenhance.Infra.Parabolic.FourierGalerkin.Torus : Type

Two-dimensional unit torus carrying the periodic Galerkin equation.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.Torus = UnitAddTorus (Fin 2)

def AVenhance.Infra.Parabolic.FourierGalerkin.pairFrequency (p : ℤ × ℤ) : Fin 2 → ℤ

The integer frequency represented by an ordered pair.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.pairFrequency p i = if i = 0 then p.1 else p.2

@[simp]

theorem AVenhance.Infra.Parabolic.FourierGalerkin.pairFrequency_neg (p : ℤ × ℤ) : pairFrequency (-p) = -pairFrequency p

def AVenhance.Infra.Parabolic.FourierGalerkin.symmetricFrequencyBox (N : ℕ) : Finset (ℤ × ℤ)

The finite symmetric cutoff [-N,N]² in frequency space.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.symmetricFrequencyBox N = Finset.Icc (-↑N) ↑N ×ˢ Finset.Icc (-↑N) ↑N

theorem AVenhance.Infra.Parabolic.FourierGalerkin.neg_mem_symmetricFrequencyBox {N : ℕ} {p : ℤ × ℤ} (hp : p ∈ symmetricFrequencyBox N) : -p ∈ symmetricFrequencyBox N

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.complexFourierPartialSum (N : ℕ) (f : Torus → ℝ) (x : Torus) : ℂ

The complex Fourier partial sum over a finite symmetric box.

Equations

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

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.realFourierProjection (N : ℕ) (f : Torus → ℝ) (x : Torus) : ℝ

The real-valued Fourier projection associated with the symmetric frequency box.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.realFourierProjection N f x = (AVenhance.Infra.Parabolic.FourierGalerkin.complexFourierPartialSum N f x).re

theorem AVenhance.Infra.Parabolic.FourierGalerkin.Basis.mFourierCoeff_conj (f : Torus → ℂ) (k : Fin 2 → ℤ) : UnitAddTorus.mFourierCoeff (fun (x : UnitAddTorus (Fin 2)) => star (f x)) k = star (UnitAddTorus.mFourierCoeff f (-k))

theorem AVenhance.Infra.Parabolic.FourierGalerkin.mFourierCoeff_real_neg (f : Torus → ℝ) (k : Fin 2 → ℤ) : UnitAddTorus.mFourierCoeff (fun (x : UnitAddTorus (Fin 2)) => ↑(f x)) (-k) = star (UnitAddTorus.mFourierCoeff (fun (x : UnitAddTorus (Fin 2)) => ↑(f x)) k)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.complexFourierPartialSum_real (N : ℕ) (f : Torus → ℝ) (x : Torus) : star (complexFourierPartialSum N f x) = complexFourierPartialSum N f x

theorem AVenhance.Infra.Parabolic.FourierGalerkin.complexFourierPartialSum_eq_ofReal (N : ℕ) (f : Torus → ℝ) (x : Torus) : ↑(realFourierProjection N f x) = complexFourierPartialSum N f x

theorem AVenhance.Infra.Parabolic.FourierGalerkin.realFourierProjection_complexification (N : ℕ) (f : Torus → ℝ) : (fun (x : Torus) => ↑(realFourierProjection N f x)) = complexFourierPartialSum N f

The finite Fourier sum is a real-valued trigonometric polynomial for real input.