Fourier coefficient identities for differences of nested Galerkin cutoffs.

@[instance_reducible]

noncomputable def classicalResidualTailMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem classicalResidualTailMeasureIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem classicalResidualTailProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

def AVenhance.Infra.Classical.GalerkinResidualTail.classicalResidualFrequencyBox (N : ℕ) : Finset (Fin 2 → ℤ)

Integer frequencies retained by the symmetric Galerkin cutoff.

Equations

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

theorem AVenhance.Infra.Classical.GalerkinResidualTail.pairBox_sum_single (N : ℕ) (f : ↥Parabolic.FourierGalerkin.ComplexScalarTorusL2) (k : Fin 2 → ℤ) : (∑ p ∈ Parabolic.FourierGalerkin.symmetricFrequencyBox N, UnitAddTorus.mFourierCoeff (↑↑f) (Parabolic.FourierGalerkin.pairFrequency p) * if k = Parabolic.FourierGalerkin.pairFrequency p then 1 else 0) = if k ∈ classicalResidualFrequencyBox N then UnitAddTorus.mFourierCoeff (↑↑f) k else 0

theorem AVenhance.Infra.Classical.mFourierBasis_repr_complexFourierPartialSumLp (N : ℕ) (f : ↥Parabolic.FourierGalerkin.ComplexScalarTorusL2) (k : Fin 2 → ℤ) : ↑(UnitAddTorus.mFourierBasis.repr (Parabolic.FourierGalerkin.complexFourierPartialSumLp N f)) k = if k ∈ GalerkinResidualTail.classicalResidualFrequencyBox N then UnitAddTorus.mFourierCoeff (↑↑f) k else 0

The Hilbert basis coordinates of a finite complex Fourier partial sum are exactly the retained Fourier coefficients.

theorem AVenhance.Infra.Classical.GalerkinResidualTail.classicalResidualFrequencyBox_subset {M N : ℕ} (hMN : M ≤ N) : classicalResidualFrequencyBox M ⊆ classicalResidualFrequencyBox N

theorem AVenhance.Infra.Classical.GalerkinResidualTail.frequencySq_ge_of_not_mem_box (N : ℕ) (k : Fin 2 → ℤ) (hk : k ∉ classicalResidualFrequencyBox N) : ↑(N + 1) ^ 2 ≤ Heat.frequencySq k

theorem AVenhance.Infra.Classical.GalerkinResidualTail.realPart_compLp_sub (f g : ↥Parabolic.FourierGalerkin.ComplexScalarTorusL2) : Complex.reCLM.compLp (f - g) = Complex.reCLM.compLp f - Complex.reCLM.compLp g

theorem AVenhance.Infra.Classical.GalerkinResidualTail.mFourierCoeff_complexFourierPartialSumLp_tail (M N : ℕ) (hMN : M ≤ N) (f : ↥Parabolic.FourierGalerkin.ComplexScalarTorusL2) (k : Fin 2 → ℤ) : UnitAddTorus.mFourierCoeff (↑↑(Parabolic.FourierGalerkin.complexFourierPartialSumLp N f - Parabolic.FourierGalerkin.complexFourierPartialSumLp M f)) k = if k ∈ classicalResidualFrequencyBox N \ classicalResidualFrequencyBox M then UnitAddTorus.mFourierCoeff (↑↑f) k else 0

theorem AVenhance.Infra.Classical.complexFourierPartialSumLp_tail_norm_sq_le (M N : ℕ) (hMN : M ≤ N) (f : ↥Parabolic.FourierGalerkin.ComplexScalarTorusL2) (hE : Heat.HasFiniteFourierEnergy f) : ‖Parabolic.FourierGalerkin.complexFourierPartialSumLp N f - Parabolic.FourierGalerkin.complexFourierPartialSumLp M f‖ ^ 2 ≤ (4 * Real.pi ^ 2 * ↑(M + 1) ^ 2)⁻¹ * Heat.fourierEnergy f

The L² tail of the complex Fourier cutoff is bounded by the high-frequency part of the Dirichlet energy.

theorem AVenhance.Infra.Classical.realFourierProjectionCoefficients_tail_norm_sq_le (M N : ℕ) (hMN : M ≤ N) (v : ↥Parabolic.FourierGalerkin.ScalarTorusL2) (hE : Heat.HasFiniteFourierEnergy (Complex.ofRealCLM.compLp v)) : ‖Parabolic.FourierGalerkin.realFourierProjectionCoefficients N v - Parabolic.FourierGalerkin.realFourierCoefficientsLift hMN (Parabolic.FourierGalerkin.realFourierProjectionCoefficients M v)‖ ^ 2 ≤ (4 * Real.pi ^ 2 * ↑(M + 1) ^ 2)⁻¹ * Heat.fourierEnergy (Complex.ofRealCLM.compLp v)

The nested real Galerkin projection tail is controlled by the Fourier H¹ energy of its complexification.