Joint smoothness from continuous partial derivatives

lem:lps-Bochner-joint-smooth: a family of functions on ℝ³ × [a,b] closed under the spatial derivatives and the time derivative, all jointly continuous, is C^∞ on the closed slab, with one-sided time derivatives at the endpoints.

def ESS.lpsSlabDeriv (w : ℕ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (j : ℕ) (α : List (Fin 3)) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.Foundation.Parabolic.Vec3 × ℝ →L[ℝ] ℝ

The candidate Fréchet derivative of w j α on the slab: coordinate derivatives in space and the time derivative.

Equations

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

theorem ESS.lpsSlabDeriv_continuousOn {w : ℕ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {S : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} (hc : ∀ (j : ℕ) (α : List (Fin 3)), ContinuousOn (w j α) S) (j : ℕ) (α : List (Fin 3)) : ContinuousOn (lpsSlabDeriv w j α) S

theorem ESS.lpsSlabDeriv_contDiffOn {w : ℕ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {S : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {n : ℕ} (hc : ∀ (j : ℕ) (α : List (Fin 3)), ContDiffOn ℝ (↑n) (w j α) S) (j : ℕ) (α : List (Fin 3)) : ContDiffOn ℝ (↑n) (lpsSlabDeriv w j α) S

theorem ESS.lps_slab_hasFDerivAt {a b : ℝ} {w : ℕ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hc : ∀ (j : ℕ) (α : List (Fin 3)), ContinuousOn (w j α) (Set.univ ×ˢ Set.Icc a b)) (hx : ∀ (j : ℕ) (α : List (Fin 3)), ∀ t ∈ Set.Icc a b, ∀ (x : CKN.Foundation.Parabolic.Vec3), HasFDerivAt (fun (y : CKN.Foundation.Parabolic.Vec3) => w j α (y, t)) (∑ i : Fin 3, w j (α ++ [i]) (x, t) • ContinuousLinearMap.proj i) x) (ht : ∀ (j : ℕ) (α : List (Fin 3)) (x : CKN.Foundation.Parabolic.Vec3), ∀ t ∈ Set.Icc a b, HasDerivWithinAt (fun (s : ℝ) => w j α (x, s)) (w (j + 1) α (x, t)) (Set.Icc a b) t) (j : ℕ) (α : List (Fin 3)) {z : CKN.Foundation.Parabolic.Vec3 × ℝ} (hz : z ∈ Set.univ ×ˢ Set.Ioo a b) : HasFDerivAt (w j α) (lpsSlabDeriv w j α z) z

Fréchet differentiability at interior points of the slab from the continuous partial derivatives.

theorem ESS.lps_slab_hasFDerivWithinAt {a b : ℝ} (hab : a < b) {w : ℕ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hc : ∀ (j : ℕ) (α : List (Fin 3)), ContinuousOn (w j α) (Set.univ ×ˢ Set.Icc a b)) (hx : ∀ (j : ℕ) (α : List (Fin 3)), ∀ t ∈ Set.Icc a b, ∀ (x : CKN.Foundation.Parabolic.Vec3), HasFDerivAt (fun (y : CKN.Foundation.Parabolic.Vec3) => w j α (y, t)) (∑ i : Fin 3, w j (α ++ [i]) (x, t) • ContinuousLinearMap.proj i) x) (ht : ∀ (j : ℕ) (α : List (Fin 3)) (x : CKN.Foundation.Parabolic.Vec3), ∀ t ∈ Set.Icc a b, HasDerivWithinAt (fun (s : ℝ) => w j α (x, s)) (w (j + 1) α (x, t)) (Set.Icc a b) t) (j : ℕ) (α : List (Fin 3)) {z : CKN.Foundation.Parabolic.Vec3 × ℝ} (hz : z ∈ Set.univ ×ˢ Set.Icc a b) : HasFDerivWithinAt (w j α) (lpsSlabDeriv w j α z) (Set.univ ×ˢ Set.Icc a b) z

Fréchet differentiability within the closed slab, including the endpoints.

theorem ESS.lps_slab_contDiffOn {a b : ℝ} (hab : a < b) {w : ℕ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hc : ∀ (j : ℕ) (α : List (Fin 3)), ContinuousOn (w j α) (Set.univ ×ˢ Set.Icc a b)) (hx : ∀ (j : ℕ) (α : List (Fin 3)), ∀ t ∈ Set.Icc a b, ∀ (x : CKN.Foundation.Parabolic.Vec3), HasFDerivAt (fun (y : CKN.Foundation.Parabolic.Vec3) => w j α (y, t)) (∑ i : Fin 3, w j (α ++ [i]) (x, t) • ContinuousLinearMap.proj i) x) (ht : ∀ (j : ℕ) (α : List (Fin 3)) (x : CKN.Foundation.Parabolic.Vec3), ∀ t ∈ Set.Icc a b, HasDerivWithinAt (fun (s : ℝ) => w j α (x, s)) (w (j + 1) α (x, t)) (Set.Icc a b) t) (j : ℕ) (α : List (Fin 3)) : ContDiffOn ℝ (↑⊤) (w j α) (Set.univ ×ˢ Set.Icc a b)

Joint smoothness on the closed slab from continuous partial derivatives of all orders (lem:lps-Bochner-joint-smooth).