Finite Galerkin weak form in product-space pairings

The finite ODE identity is expressed using the product-space Hilbert classes so that it can be passed directly through weak convergence.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.FrozenDriftProblem.finite_product_fourier_test_weak_identity (P : FrozenDriftProblem) (N : ℕ) (d : Coefficients (RealFourierDimension N)) (η : ℝ → ℝ) (hη : ContDiff ℝ 1 η) (hη₁ : η 1 = 0) (hηMem : MeasureTheory.MemLp η ⊤ GalerkinTimeMeasure) (hηDerivMem : MeasureTheory.MemLp (deriv η) ⊤ GalerkinTimeMeasure) : -inner ℝ (P.scalarProductLp N) (scalarProductTestLp (deriv η) ((realFourierScalarMap N) d) hηDerivMem) + inner ℝ (P.gradientProductLp N) (P.weightedDriftProductTestLp η N d hηMem) + P.κ * inner ℝ (P.gradientProductLp N) (gradientProductTestLp η ((realFourierGradientMap N) d) hηMem) = η 0 * inner ℝ P.initialTorusL2 ((realFourierScalarMap N) d)

The finite Galerkin equation tested by a separated smooth time/Fourier test, written as three pairings in the common product-space L² spaces.