Continuous finite-mode time derivatives for the smooth Galerkin sequence.

noncomputable def AVenhance.Infra.Classical.classicalGalerkinFiniteFourierDerivativePath (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (N : ℕ) (k : Fin 2 → ℤ) : C(↑(Set.Icc 0 1), ℂ)

The ODE right-hand side projected to one Fourier coefficient is continuous through the closed unit slab.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Classical.classicalGalerkinFiniteFourierCoeffPath_hasDerivAt (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (N : ℕ) (k : Fin 2 → ℤ) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : HasDerivAt (fun (s : ℝ) => (classicalComplexFourierCoeffCLM k) ((Parabolic.FourierGalerkin.realFourierScalarMap N) (ODE.extendCurve classicalGalerkinFiniteFourierCoeffPath_hasDerivAt._proof_1 (classicalGalerkinCoefficientPath φ hφ κ hκ F hF θ₀ hθ₀ N) s))) ((classicalGalerkinFiniteFourierDerivativePath φ hφ κ hκ F hF θ₀ hθ₀ N k) ⟨t, ⋯⟩) t