Almost-everywhere periodic H¹ slices

The common Fourier derivative identities identify the synchronized limit's Euclidean weak gradient on almost every slice.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.synchronized_limit_isPeriodicH1With_ae (Uprod : ↥ScalarProductTimeL2) (Gprod : ↥GradientProductTimeL2) (u : ↑(Set.Icc 0 1) → ↥ScalarTorusL2) (S : Set ℝ) (B : ℝ) (hB : 0 ≤ B) (hbound : ∀ (t : ↑(Set.Icc 0 1)), ‖u t‖ ≤ B) (hS : ∀ t ∈ S, synchronizedScalarSliceGood Uprod u t) (hmode : ∀ᵐ (t : ℝ) ∂GalerkinTimeMeasure, ∀ (i : Fin 2) (N : ℕ) (j : Fin (RealFourierDimension N)), ∫ (x : Homogenization.Vec 2) in unitCube, synchronizedScalarRepresentative Uprod u S t x * spaceGrad (realFourierModeAmbient N ((realFourierIndexEquivFin N).symm j)) x i = -∫ (x : Homogenization.Vec 2) in unitCube, synchronizedGradientRepresentative Gprod t x i * realFourierModeAmbient N ((realFourierIndexEquivFin N).symm j) x) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 1), IsPeriodicH1With (synchronizedScalarRepresentative Uprod u S t) (synchronizedGradientRepresentative Gprod t)

The synchronized scalar and gradient representatives form the exact periodic H¹ pair on almost every open time slice.