Iterated derivatives in one variable of a product

The iterated derivative of a slice x ↦ f (p, x) is the total iterated derivative of f restricted to directions in the second factor. Consequently these partial derivatives vary continuously in both variables when f is sufficiently differentiable. This gives the joint derivative continuity needed for smooth families in function spaces.

The within-set versions require unique derivatives only on the product, so they also handle coordinate domains of manifolds with boundary or corners.

theorem ContDiffOn.iteratedFDerivWithin_prod_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {P : Type u_2} [NormedAddCommGroup P] [NormedSpace 𝕜 P] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : P × E → F} {s : Set P} {t : Set E} (hf : ContDiffOn 𝕜 n f (s ×ˢ t)) (hst : UniqueDiffOn 𝕜 (s ×ˢ t)) (m : ℕ) (hm : ↑m ≤ n) {p : P} (hp : p ∈ s) {x : E} (hx : x ∈ t) : iteratedFDerivWithin 𝕜 m (fun (y : E) => f (p, y)) t x = (iteratedFDerivWithin 𝕜 m f (s ×ˢ t) (p, x)).compContinuousLinearMap fun (x : Fin m) => ContinuousLinearMap.inr 𝕜 P E

When the product has unique derivatives, differentiation in the second variable restricts the total derivative to directions with zero first component.

theorem ContDiffOn.continuousOn_iteratedFDerivWithin_prod_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {P : Type u_2} [NormedAddCommGroup P] [NormedSpace 𝕜 P] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : P × E → F} {s : Set P} {t : Set E} (hf : ContDiffOn 𝕜 n f (s ×ˢ t)) (hst : UniqueDiffOn 𝕜 (s ×ˢ t)) (m : ℕ) (hm : ↑m ≤ n) : ContinuousOn (fun (z : P × E) => iteratedFDerivWithin 𝕜 m (fun (y : E) => f (z.1, y)) t z.2) (s ×ˢ t)

When the product has unique derivatives, partial iterated derivatives vary jointly continuously, including at boundary points of either set.