Weak equation for time-dependent finite Fourier tests

The separated Fourier-mode identities sum to the weak equation for the spatial Fourier cutoff of an arbitrary smooth periodic spacetime test.

@[instance_reducible]

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.timeWeakEquationMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.timeWeakEquationMeasureIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem AVenhance.Infra.Parabolic.FourierGalerkin.timeWeakEquationProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.timeWeakEquationProbabilityTorus : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.realFourierUnitCoefficient (N : ℕ) (j : Fin (RealFourierDimension N)) : Coefficients (RealFourierDimension N)

The coefficient vector selecting one real Fourier basis mode.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.realFourierUnitCoefficient N j = WithLp.toLp 2 (Pi.single j 1)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentWeakEquation.realFourierScalarMap_unit (N : ℕ) (j : Fin (RealFourierDimension N)) : (realFourierScalarMap N) (realFourierUnitCoefficient N j) = realFourierModeL2 N j

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TimeDependentWeakEquation.realFourierGradientMap_unit (N : ℕ) (j : Fin (RealFourierDimension N)) : (realFourierGradientMap N) (realFourierUnitCoefficient N j) = realFourierModeGradL2 N j

theorem AVenhance.Infra.Parabolic.FourierGalerkin.modeExpansion_unit (N : ℕ) (j : Fin (RealFourierDimension N)) (x : Torus) : modeExpansion (RealFourierDimension N) (realFourierModeFin N) (realFourierUnitCoefficient N j) x = realFourierModeFin N j x

Expansion of the coefficient vector selecting one real Fourier mode.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.synchronized_limit_spacetimeFourierCutoff_identity (P : FrozenDriftProblem) (σ : ℕ → ℕ) (hσ : StrictMono σ) (Uprod : ↥ScalarProductTimeL2) (Gprod : ↥GradientProductTimeL2) (hUweak : ∀ (v : ↥ScalarProductTimeL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ (P.scalarProductLp (σ n)) v) Filter.atTop (nhds (inner ℝ Uprod v))) (hGweak : ∀ (v : ↥GradientProductTimeL2), Filter.Tendsto (fun (n : ℕ) => inner ℝ (P.gradientProductLp (σ n)) v) Filter.atTop (nhds (inner ℝ Gprod v))) {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (_hperiodic : ∀ (t : ℝ), IsZ2Periodic (φ t)) (hterminal : ∀ (t : ℝ), 1 ≤ t → ∀ (x : Homogenization.Vec 2), φ t x = 0) (N : ℕ) : -∑ j : Fin (RealFourierDimension N), inner ℝ Uprod (scalarProductTestLp (deriv (spacetimeRealFourierCoefficient φ N j)) (realFourierModeL2 N j) ⋯) + ∑ j : Fin (RealFourierDimension N), inner ℝ Gprod (P.weightedDriftProductTestLp (spacetimeRealFourierCoefficient φ N j) N (realFourierUnitCoefficient N j) ⋯) + P.κ * ∑ j : Fin (RealFourierDimension N), inner ℝ Gprod (gradientProductTestLp (spacetimeRealFourierCoefficient φ N j) (realFourierModeGradL2 N j) ⋯) = ∑ j : Fin (RealFourierDimension N), spacetimeRealFourierCoefficient φ N j 0 * inner ℝ P.initialTorusL2 (realFourierModeL2 N j)

The synchronized product limits satisfy the weak equation for every finite spatial Fourier cutoff of a smooth periodic spacetime test.