Nested-cutoff coefficient maps for the classical Galerkin sequence.

@[instance_reducible]

noncomputable def classicalConvergenceMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem classicalConvergenceMeasureIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem classicalConvergenceProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

noncomputable def AVenhance.Infra.Classical.classicalGalerkinCoefficientsRestrict {M N : ℕ} (hMN : M ≤ N) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension M)

Restrict a coefficient vector from a larger symmetric Fourier box to a smaller one.

Equations

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

@[simp]

theorem AVenhance.Infra.Classical.classicalGalerkinCoefficientsRestrict_apply {M N : ℕ} (hMN : M ≤ N) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) (i : Fin (Parabolic.FourierGalerkin.RealFourierDimension M)) : (classicalGalerkinCoefficientsRestrict hMN c).ofLp i = c.ofLp (Parabolic.FourierGalerkin.realFourierIndexLiftFin hMN i)