Product-space weak equation on finite Fourier tests

This module connects the finite Galerkin identities to the synchronized product-space limits.

@[instance_reducible]

noncomputable def weakLimitEquationMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem weakLimitEquationMeasureIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem weakLimitEquationProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.initialProjection_pairing (P : FrozenDriftProblem) (N : ℕ) (d : Coefficients (RealFourierDimension N)) : inner ℝ P.initialTorusL2 ((realFourierScalarMap N) d) = inner ℝ (P.galerkinData N).initial d

Pairing the initial datum with a cutoff Fourier test is the coefficient pairing with the Galerkin projection of the datum.