Cutoff tails of smooth real periodic residuals.

@[instance_reducible]

noncomputable def classicalResidualMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem classicalResidualMeasureIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem classicalResidualProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Classical.GalerkinResidual.continuous_spaceGrad_component {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (i : Fin 2) : Continuous fun (x : Homogenization.Vec 2) => spaceGrad f x i

theorem AVenhance.Infra.Classical.classicalSmoothProjection_tail_norm_sq_le (M N : ℕ) (hMN : M ≤ N) (f : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ 1 f) (hper : IsZ2Periodic f) : ‖Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) (Torus.periodicToTorus f) - Parabolic.FourierGalerkin.realFourierCoefficientsLift hMN (Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension M) (Parabolic.FourierGalerkin.realFourierModeFin M) (Torus.periodicToTorus f))‖ ^ 2 ≤ (4 * Real.pi ^ 2 * ↑(M + 1) ^ 2)⁻¹ * gradNormSq (spaceGrad f)

For a smooth periodic real source, the difference between nested Galerkin projections is bounded by the source's spatial Dirichlet energy, with the expected inverse-cutoff factor.

theorem AVenhance.Infra.Classical.classicalSmoothProjection_tail_norm_le (M N : ℕ) (hMN : M ≤ N) (f : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ 1 f) (hper : IsZ2Periodic f) : ‖Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension N) (Parabolic.FourierGalerkin.realFourierModeFin N) (Torus.periodicToTorus f) - Parabolic.FourierGalerkin.realFourierCoefficientsLift hMN (Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension M) (Parabolic.FourierGalerkin.realFourierModeFin M) (Torus.periodicToTorus f))‖ ≤ √((4 * Real.pi ^ 2 * ↑(M + 1) ^ 2)⁻¹ * gradNormSq (spaceGrad f))

A smooth projection tail has norm bounded by the square root of its Dirichlet-energy tail.

theorem AVenhance.Infra.Classical.classicalL2_norm_le_of_all_projection_bounds (v : ↥Parabolic.FourierGalerkin.ScalarTorusL2) {B : ℝ} (hproj : ∀ (N : ℕ), ‖Parabolic.FourierGalerkin.realFourierProjectionCoefficients N v‖ ≤ B) : ‖v‖ ≤ B

Uniform bounds for all finite Fourier projections pass to the full torus L² norm.

theorem AVenhance.Infra.Classical.classicalSmoothSource_gradient_energy_le_of_projection_bounds (f : Homogenization.Vec 2 → ℝ) (hf : ContDiff ℝ 1 f) (hper : IsZ2Periodic f) {B : ℝ} (hB : 0 ≤ B) (hproj : ∀ (i : Fin 2) (K : ℕ), ‖Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension K) (Parabolic.FourierGalerkin.realFourierModeFin K) (Torus.periodicToTorus fun (x : Homogenization.Vec 2) => spaceGrad f x i)‖ ≤ B) : gradNormSq (spaceGrad f) ≤ 2 * B ^ 2

Uniform bounds for all scalar Fourier projections of each derivative component bound the full Dirichlet energy of a smooth periodic function.

theorem AVenhance.Infra.Classical.classicalRealFourierProduct_projection_norm_le (K N : ℕ) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) (f : Homogenization.Vec 2 → ℝ) (hf : Continuous f) {_B : ℝ} (_hB : 0 ≤ _B) (hbound : ∀ (x : Homogenization.Vec 2), ‖f x‖ ≤ _B) : ‖Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension K) (Parabolic.FourierGalerkin.realFourierModeFin K) (Torus.periodicToTorus fun (x : Homogenization.Vec 2) => f x * realFourierModeAmbientExpansion N c x)‖ ≤ _B * ‖c‖

Projection of a bounded multiplier times a finite Fourier synthesis is controlled for every target cutoff, including cutoffs larger than the synthesis space.

theorem AVenhance.Infra.Classical.GalerkinResidual.classicalWordDerivative_periodic_for_residual (w : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) (hper : IsZ2Periodic f) : IsZ2Periodic (classicalWordDerivative w f)

theorem AVenhance.Infra.Classical.classicalTransportDerivative_projection_norm_le (K N : ℕ) (b : Homogenization.Vec 2 → Homogenization.Vec 2) (c : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) (i : Fin 2) {B : ℝ} (hB : 0 ≤ B) (hb : ContDiff ℝ (↑⊤) b) (hbp : IsZ2Periodic b) (hDb : ∀ (w : List (Fin 2)), w.length ≤ 1 → ∀ (j : Fin 2) (x : Homogenization.Vec 2), ‖classicalWordDerivative w (fun (y : Homogenization.Vec 2) => b y j) x‖ ≤ B) : ‖Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension K) (Parabolic.FourierGalerkin.realFourierModeFin K) (Torus.periodicToTorus (classicalWordDerivative [i] (classicalTransport b (realFourierModeAmbientExpansion N c))))‖ ≤ B * (‖(realFourierWordDerivativeMap N [0, i]) c‖ + ‖(realFourierWordDerivativeMap N [1, i]) c‖ + ‖(realFourierWordDerivativeMap N [0]) c‖ + ‖(realFourierWordDerivativeMap N [1]) c‖)

The first spatial derivative of the finite-dimensional transport term has a uniform projection bound controlled by the first two derivative levels of the coefficient vector.