Mixed space-time partial derivatives

Let u : E → ℝ → F be a function of a space variable y in a real normed space E and of a time variable t in a convex set s ⊆ ℝ, such as a closed interval [a, b]. Time derivatives are taken within s, so that at an endpoint of an interval they are one-sided. This file proves the theorem of Schwarz and Peano on mixed partial derivatives in this setting: if one of the two iterated partial derivatives ∂ₜ D_y u and D_y ∂ₜ u exists and is jointly continuous, then the other one exists and the two agree. Only the existence of the first partial derivatives and the joint continuity of the given mixed derivative at the point are assumed; no joint differentiability of u is needed.

• TauCeti.hasFDerivAt_timeDeriv_of_continuousWithinAt: if ∂ₜ D_y u is jointly continuous at (x, t) and u(y, ·) has a time derivative g y at t for y near x, then g is differentiable at x, with derivative ∂ₜ D_y u (x, t).
• TauCeti.hasDerivWithinAt_spatialDeriv_of_continuousWithinAt: if D_y ∂ₜ u is jointly continuous at (x, t), then the spatial derivative D_y u (x, ·) has time derivative D_y ∂ₜ u (x, t) within s at t.

Iterating these one-step statements shows that all orders of a family of mixed derivatives agree. Index the candidate mixed derivatives by a family Q r y t, where Q r y t n stands for the n-multilinear map ∂ₜ^r D_y^n u (y, t), and the admissible orders (r, n) by a lower set I ⊆ ℕ × ℕ; for parabolic problems of order k this is {(r, n) | 2 r + n ≤ k}. Spatial derivatives are related as in HasFTaylorSeriesUpTo, through curryLeft.

• TauCeti.hasFDerivAt_mixedDeriv_of_isLowerSet: if Q 0 is related to itself by spatial derivatives, each Q (r + 1) is the time derivative of Q r, and the mixed derivatives are jointly continuous, then every Q r is related to itself by spatial derivatives.
• TauCeti.hasDerivWithinAt_mixedDeriv_of_isLowerSet: conversely, if every Q r is related to itself by spatial derivatives, Q (r + 1) y t 0 is the time derivative of Q r y t 0, and the mixed derivatives are jointly continuous, then Q (r + 1) y t n is the time derivative of Q r y t n for every admissible n.

In either case the family Q satisfies both the spatial and the temporal derivative relations at every admissible order, so every ordering of r time derivatives and n spatial derivatives exists and equals Q r y t n, including the one-sided time derivatives at the endpoints of an interval. This is the form in which spaces of functions with continuous mixed space-time derivatives, such as parabolic Hölder spaces, are described independently of the order of differentiation.

References

• W. Rudin, Principles of Mathematical Analysis, 3rd ed., Theorem 9.41 (the two-variable form with the classical proof).

theorem TauCeti.hasFDerivAt_timeDeriv_of_continuousWithinAt {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {u : E → ℝ → F} {v w : E → ℝ → E →L[ℝ] F} {g : E → F} {s : Set ℝ} {x : E} {t : ℝ} (hs : Convex ℝ s) (ht : t ∈ s) (hst : UniqueDiffWithinAt ℝ s t) (hv : ∀ᶠ (p : E × ℝ) in nhds x ×ˢ nhdsWithin t s, HasFDerivAt (fun (x : E) => u x p.2) (v p.1 p.2) p.1) (hw : ∀ᶠ (p : E × ℝ) in nhds x ×ˢ nhdsWithin t s, HasDerivWithinAt (v p.1) (w p.1 p.2) s p.2) (hwc : ContinuousWithinAt (fun (p : E × ℝ) => w p.1 p.2) (Set.univ ×ˢ s) (x, t)) (hg : ∀ᶠ (y : E) in nhds x, HasDerivWithinAt (u y) (g y) s t) : HasFDerivAt g (w x t) x

Peano's theorem on mixed partial derivatives, differentiating a time derivative in space. Let u : E → ℝ → F, let s ⊆ ℝ be convex, and let t ∈ s be a point at which derivatives within s are unique. Suppose that near x in space and near t within s, the spatial derivative of u(·, τ) at y is v(y, τ), and that v(y, ·) has time derivative w(y, τ) within s, with w jointly continuous at (x, t). If g y is the time derivative of u(y, ·) within s at t for every y near x, then g is differentiable at x with derivative w(x, t): the spatial derivative of ∂ₜu exists and equals ∂ₜ D_y u.

theorem TauCeti.hasDerivWithinAt_spatialDeriv_of_continuousWithinAt {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {u : E → ℝ → F} {v : ℝ → E →L[ℝ] F} {g : E → ℝ → F} {w : E → ℝ → E →L[ℝ] F} {s : Set ℝ} {x : E} {t : ℝ} (hs : Convex ℝ s) (ht : t ∈ s) (hv : ∀ᶠ (τ : ℝ) in nhdsWithin t s, HasFDerivAt (fun (x : E) => u x τ) (v τ) x) (hg : ∀ᶠ (p : E × ℝ) in nhds x ×ˢ nhdsWithin t s, HasDerivWithinAt (u p.1) (g p.1 p.2) s p.2) (hw : ∀ᶠ (p : E × ℝ) in nhds x ×ˢ nhdsWithin t s, HasFDerivAt (fun (x : E) => g x p.2) (w p.1 p.2) p.1) (hwc : ContinuousWithinAt (fun (p : E × ℝ) => w p.1 p.2) (Set.univ ×ˢ s) (x, t)) : HasDerivWithinAt v (w x t) s t

Peano's theorem on mixed partial derivatives, differentiating a spatial derivative in time. Let u : E → ℝ → F, let s ⊆ ℝ be convex, and let t ∈ s. Suppose that v τ is the spatial derivative of u(·, τ) at x for τ ∈ s near t, and that near x in space and near t within s, u(y, ·) has time derivative g(y, τ) within s, whose spatial derivative is w(y, τ), with w jointly continuous at (x, t). Then v has time derivative w(x, t) within s at t: the time derivative of D_y u exists and equals D_y ∂ₜu.

theorem TauCeti.hasFDerivAt_mixedDeriv_of_isLowerSet {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Q : ℕ → E → ℝ → FormalMultilinearSeries ℝ E F} {s : Set ℝ} {I : Set (ℕ × ℕ)} (hI : IsLowerSet I) (hs : Convex ℝ s) (hs' : UniqueDiffOn ℝ s) (hx : ∀ (n : ℕ), (0, n + 1) ∈ I → ∀ t ∈ s, ∀ (y : E), HasFDerivAt (fun (x : E) => Q 0 x t n) (Q 0 y t (n + 1)).curryLeft y) (ht : ∀ (r n : ℕ), (r + 1, n) ∈ I → ∀ (y : E), ∀ t ∈ s, HasDerivWithinAt (fun (x : ℝ) => Q r y x n) (Q (r + 1) y t n) s t) (hc : ∀ (r n : ℕ), (r + 1, n + 1) ∈ I → ContinuousOn (fun (p : E × ℝ) => Q (r + 1) p.1 p.2 (n + 1)) (Set.univ ×ˢ s)) {r n : ℕ} (hrn : (r, n + 1) ∈ I) {t : ℝ} (hts : t ∈ s) (y : E) : HasFDerivAt (fun (x : E) => Q r x t n) (Q r y t (n + 1)).curryLeft y

Mixed derivatives with time derivatives taken last. Let I ⊆ ℕ × ℕ be a lower set of orders, and let s ⊆ ℝ be a convex set on which derivatives within s are unique, such as a nondegenerate closed interval. Suppose that

• Q 0 y t (n + 1) is the spatial derivative of Q 0 · t n whenever (0, n + 1) ∈ I;
• Q (r + 1) y t n is the time derivative within s of Q r y · n whenever (r + 1, n) ∈ I;
• the mixed derivatives Q (r + 1) · · (n + 1) are jointly continuous on univ ×ˢ s.

Then Q r y t (n + 1) is the spatial derivative of Q r · t n whenever (r, n + 1) ∈ I. Thus if Q r y t n is ∂ₜ^r D_y^n u, it is also D_y^n ∂ₜ^r u.

theorem TauCeti.hasDerivWithinAt_mixedDeriv_of_isLowerSet {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Q : ℕ → E → ℝ → FormalMultilinearSeries ℝ E F} {s : Set ℝ} {I : Set (ℕ × ℕ)} (hI : IsLowerSet I) (hs : Convex ℝ s) (hx : ∀ (r n : ℕ), (r, n + 1) ∈ I → ∀ t ∈ s, ∀ (y : E), HasFDerivAt (fun (x : E) => Q r x t n) (Q r y t (n + 1)).curryLeft y) (ht : ∀ (r : ℕ), (r + 1, 0) ∈ I → ∀ (y : E), ∀ t ∈ s, HasDerivWithinAt (fun (x : ℝ) => Q r y x 0) (Q (r + 1) y t 0) s t) (hc : ∀ (r n : ℕ), (r + 1, n + 1) ∈ I → ContinuousOn (fun (p : E × ℝ) => Q (r + 1) p.1 p.2 (n + 1)) (Set.univ ×ˢ s)) {r n : ℕ} (hrn : (r + 1, n) ∈ I) (y : E) {t : ℝ} (hts : t ∈ s) : HasDerivWithinAt (fun (x : ℝ) => Q r y x n) (Q (r + 1) y t n) s t

Mixed derivatives with spatial derivatives taken last. Let I ⊆ ℕ × ℕ be a lower set of orders, and let s ⊆ ℝ be convex. Suppose that

• Q r y t (n + 1) is the spatial derivative of Q r · t n whenever (r, n + 1) ∈ I;
• Q (r + 1) y t 0 is the time derivative within s of Q r y · 0 whenever (r + 1, 0) ∈ I;
• the mixed derivatives Q (r + 1) · · (n + 1) are jointly continuous on univ ×ˢ s.

Then Q (r + 1) y t n is the time derivative within s of Q r y · n whenever (r + 1, n) ∈ I. Thus if Q r y t n is D_y^n ∂ₜ^r u, it is also ∂ₜ^r D_y^n u.