Assemble time and spatial derivatives on the closed unit slab and rescale to physical horizons.

theorem AVenhance.Infra.Classical.GalerkinHorizonSmoothnessAssembly.classicalBoundarySpatialWord_hasFDerivAt (w : List (Fin 2)) (u : Homogenization.Vec 2 → ℝ) (hu : ContDiff ℝ (↑⊤) u) (x : Homogenization.Vec 2) : HasFDerivAt (classicalWordDerivative w u) (∑ i : Fin 2, classicalWordDerivative (i :: w) u x • ContinuousLinearMap.proj i) x

theorem AVenhance.Infra.Classical.classicalGalerkinUnitWordFamily_contDiffOn (φ : ℝ → 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 θ₀) (w : List (Fin 2)) : ContDiffOn ℝ (↑⊤) (classicalGalerkinUnitWordFamily φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w) (Set.Icc 0 1 ×ˢ Set.univ)

Every ordered spatial derivative of the unit-slab Galerkin limit is jointly smooth up to both time endpoints.

theorem AVenhance.Infra.Classical.classicalGalerkinHorizonLimit_contDiffOn (N : ℕ) (hN : 0 < N) (φ : ℝ → 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 θ₀) : ContDiffOn ℝ (↑⊤) (Function.uncurry (classicalGalerkinHorizonLimit N hN φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per)) (Set.Icc 0 ↑N ×ˢ Set.univ)

The horizon-rescaled Galerkin limit is jointly smooth on its closed physical-time slab.

theorem AVenhance.Infra.Classical.classicalGalerkinIntegerHorizonFamily_contDiffOn (φ : ℝ → 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 θ₀) (N : ℕ) : ContDiffOn ℝ (↑⊤) (Function.uncurry (classicalGalerkinIntegerHorizonFamily φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per N)) (Set.Icc 0 ↑N ×ˢ Set.univ)

The integer-horizon family is jointly smooth on every requested closed horizon.