Finite Laplacian coefficients in terms of the Galerkin second derivative paths.

@[instance_reducible]

noncomputable def laplacianFourierMeasureSpace : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem laplacianFourierMeasureHaar : MeasureTheory.volume.IsAddHaarMeasure

theorem laplacianFourierProbability : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem laplacianFourierTorusProbability : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Classical.classicalFrequencyPair_mem_symmetricFrequencyBox_eventually (k : Fin 2 → ℤ) : ∃ (K : ℕ), ∀ (N : ℕ), K ≤ N → Parabolic.FourierGalerkin.frequencyPair k ∈ Parabolic.FourierGalerkin.symmetricFrequencyBox N

theorem AVenhance.Infra.Classical.classicalGalerkinFiniteLaplacian_fourierCoeff_eq_sum (N : ℕ) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) (k : Fin 2 → ℤ) : UnitAddTorus.mFourierCoeff (fun (x : Parabolic.FourierGalerkin.Torus) => ↑(Torus.periodicToTorus (spaceLap (realFourierModeAmbientExpansion N c)) x)) k = ∑ i : Fin 2, (classicalComplexFourierCoeffCLM k) ((Parabolic.FourierGalerkin.realFourierScalarMap N) ((realFourierWordDerivativeMap N [i, i]) c))

The Fourier coefficient of the Laplacian of a finite Fourier synthesis is the sum of the Fourier coefficients of its two second derivative paths.