Time-tested finite Galerkin equation

The measurable-coefficient ODE yields the weak equation against a fixed finite Fourier test with an arbitrary smooth time factor vanishing at the terminal time. This is the finite test identity used before passing to the space-time weak limit.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.finite_time_test_identity (P : FrozenDriftProblem) (N : ℕ) (d : Coefficients (RealFourierDimension N)) (η : ℝ → ℝ) (hη : ContDiff ℝ 1 η) (hη₁ : η 1 = 0) : ∫ (t : ℝ) in 0..1, -inner ℝ (ODE.extendCurve finite_time_test_identity._proof_1 (P.coefficientPath N) t) d * deriv η t - η t * inner ℝ (((P.galerkinData N).coefficient t) (ODE.extendCurve finite_time_test_identity._proof_1 (P.coefficientPath N) t)) d = η 0 * inner ℝ (P.galerkinData N).initial d

The coefficient ODE, integrated against a smooth time test and a fixed real Fourier vector, has the expected initial trace.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.finite_fourier_test_weak_identity (P : FrozenDriftProblem) (N : ℕ) (d : Coefficients (RealFourierDimension N)) (η : ℝ → ℝ) (hη : ContDiff ℝ 1 η) (hη₁ : η 1 = 0) : have y := ODE.extendCurve finite_time_test_identity._proof_1 (P.coefficientPath N); ∫ (t : ℝ) in 0..1, -inner ℝ ((realFourierScalarMap N) (y t)) ((realFourierScalarMap N) d) * deriv η t + η t * (realFourierDriftBilinearForm N (fun (s : ℝ) => Torus.periodicToTorus (P.b s)) t (y t) d + P.κ * inner ℝ ((realFourierGradientMap N) (y t)) ((realFourierGradientMap N) d)) = η 0 * inner ℝ (P.galerkinData N).initial d

The concrete weak form holds after time integration against every fixed real Fourier test and smooth scalar time factor vanishing at t = 1.