Closed-slab smoothness criteria for mixed time/spatial derivative families.

theorem AVenhance.Infra.Classical.classicalHasDerivAt_of_within_Iic_Ici {f : ℝ → ℝ} {f' x : ℝ} (hleft : HasDerivWithinAt f f' (Set.Iic x) x) (hright : HasDerivWithinAt f f' (Set.Ici x) x) : HasDerivAt f f' x

Two compatible one-sided derivatives determine the ordinary derivative.

def AVenhance.Infra.Classical.classicalSpatialWordDerivativeLinearMap (f q : List (Fin 2) → ℝ × Homogenization.Vec 2 → ℝ) (w : List (Fin 2)) (p : ℝ × Homogenization.Vec 2) : ℝ × Homogenization.Vec 2 →L[ℝ] ℝ

The full derivative map for a spatial word: its time component is the equation right-hand side, and its spatial components are the coordinate derivatives.

Equations

• AVenhance.Infra.Classical.classicalSpatialWordDerivativeLinearMap f q w p = (ContinuousLinearMap.toSpanSingleton ℝ (q w p)).coprod (∑ i : Fin 2, f (i :: w) p • ContinuousLinearMap.proj i)

theorem AVenhance.Infra.Classical.classicalSpatialWordFamily_contDiffOn (S : Set (ℝ × Homogenization.Vec 2)) (hS : UniqueDiffOn ℝ S) (f q : List (Fin 2) → ℝ × Homogenization.Vec 2 → ℝ) (hcontinuous : ∀ (w : List (Fin 2)), ContinuousOn (f w) S) (hderivative : ∀ (w : List (Fin 2)), ∀ p ∈ S, HasFDerivWithinAt (f w) (classicalSpatialWordDerivativeLinearMap f q w p) S p) (hRhsRegular : ∀ (k : ℕ), (∀ (w : List (Fin 2)), ContDiffOn ℝ (↑k) (f w) S) → ∀ (w : List (Fin 2)), ContDiffOn ℝ (↑k) (q w) S) (w : List (Fin 2)) : ContDiffOn ℝ (↑⊤) (f w) S

A continuous spatial-word family is smooth to every finite order once each word has its equation and coordinate derivatives, and the equation right-hand sides inherit finite regularity from the word family.