Pointwise advection-diffusion equation for the unit-slab Galerkin limit.

theorem AVenhance.Infra.Classical.classicalGalerkinUnitLimit_advDiffOp (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (x : Homogenization.Vec 2) : advDiffOp (streamVel φ) κ (fun (s : ℝ) (y : Homogenization.Vec 2) => classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per (classicalGalerkinUnitSlabClamp s) y) t x = F t x

The real smooth Galerkin limit solves the advection-diffusion equation in the open unit time slab.