Exhaustion limits for the symmetric torus Fourier cutoffs

The finite frequency boxes exhaust the full integer lattice. This file records the unconditional sum convergence needed to turn the landed torus Fourier basis expansion into cutoff convergence.

@[instance_reducible]

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.fourierLimitMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.fourierLimitMeasureIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem AVenhance.Infra.Parabolic.FourierGalerkin.fourierLimitProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.two_le_fact : Fact (1 ≤ 2)

@[reducible, inline]

noncomputable abbrev AVenhance.Infra.Parabolic.FourierGalerkin.ComplexScalarTorusL2 : AddSubgroup (Torus →ₘ[MeasureTheory.volume] ℂ)

Complex-valued scalar L² on the unit torus.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.ComplexScalarTorusL2 = MeasureTheory.Lp ℂ 2 MeasureTheory.volume

def AVenhance.Infra.Parabolic.FourierGalerkin.pairFrequencyEquiv : ℤ × ℤ ≃ (Fin 2 → ℤ)

Pair-frequency indexing is equivalent to the two-coordinate integer lattice.

Equations

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.tendsto_symmetricFrequencyBox_atTop : Filter.Tendsto symmetricFrequencyBox Filter.atTop Filter.atTop

The symmetric frequency boxes tend to the at-top filter on finite frequency sets.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.tendsto_pairBox_sum_of_hasSum {F : Type u_1} [AddCommMonoid F] [TopologicalSpace F] {f : (Fin 2 → ℤ) → F} {z : F} (hsum : HasSum f z) : Filter.Tendsto (fun (N : ℕ) => ∑ p ∈ symmetricFrequencyBox N, f (pairFrequency p)) Filter.atTop (nhds z)

Unconditional Fourier series sums over the symmetric frequency boxes converge to the full sum.

@[irreducible]

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.complexFourierPartialSumLp (N : ℕ) (f : ↥ComplexScalarTorusL2) : ↥ComplexScalarTorusL2

The finite complex Fourier partial sum as an L² class.

Equations

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

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

Pointwise complex Fourier partial sum for an arbitrary complex-valued function.

Equations

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.complexFourierPartialSumLp_coeFn (N : ℕ) (f : ↥ComplexScalarTorusL2) : (fun (x : Torus) => ↑↑(complexFourierPartialSumLp N f) x) =ᵐ[MeasureTheory.volume] complexFourierPartialSumFunction N fun (x : Torus) => ↑↑f x

The L² Fourier partial sum has the expected pointwise representative a.e.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.tendsto_complexFourierPartialSumLp (f : ↥ComplexScalarTorusL2) : Filter.Tendsto (fun (N : ℕ) => complexFourierPartialSumLp N f) Filter.atTop (nhds f)

Complex Fourier partial sums over the positive symmetric cutoff converge in L².

theorem AVenhance.Infra.Parabolic.FourierGalerkin.tendsto_realPartFourierPartialSumLp (f : ↥ComplexScalarTorusL2) : Filter.Tendsto (fun (N : ℕ) => Complex.reCLM.compLp (complexFourierPartialSumLp N f)) Filter.atTop (nhds (Complex.reCLM.compLp f))

Taking real parts preserves the Fourier cutoff convergence.