Smoothness of slices of a map on a product

If a map H on a product is smooth near every point of s ×ˢ I, then each of its slices H (·, t) with t ∈ I is smooth on s (TauCeti.contDiffOn_comp_prodMk_left). For instance, the time slices of a homotopy smooth near s × [0, 1] are smooth on s.

For a family F : P × E → X smooth at (p, x), the spatial differential (q, y) ↦ fderiv (F (q, ·)) y is smooth jointly (ContDiffAt.fderiv_slice), smoothness persists along a graph over the parameter (ContDiffAt.eventually_contDiffAt_graph), and the vertical part of the derivative of a C¹ map is continuous along a continuous graph (ContDiffAt.continuousAt_fderiv_comp_inr). The partial derivative in the second variable, applied to a fixed vector, is then C^m jointly whenever m + 1 ≤ n (ContDiffAt.fderiv_snd_apply).

A compactly supported C³ function on E × ℝ has compactly supported spatial first and second derivative fields and a time derivative field of lower smoothness, computing its slice derivatives at every point (ContDiff.exists_derivative_fields_of_hasCompactSupport).

theorem TauCeti.contDiffOn_comp_prodMk_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {s : Set E} {I : Set G} {H : E × G → F} (hH : ∀ p ∈ s ×ˢ I, ContDiffAt 𝕜 n H p) {t : G} (ht : t ∈ I) : ContDiffOn 𝕜 n (fun (x : E) => H (x, t)) s

Slices of a map smooth near s ×ˢ I are smooth: for t ∈ I, the slice H (·, t) is smooth on s.

theorem ContDiffAt.fderiv_slice {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {P : Type u_2} [NormedAddCommGroup P] [NormedSpace 𝕜 P] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X : Type u_4} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {p : P} {x : E} {n m : WithTop ℕ∞} {F : P × E → X} (hF : ContDiffAt 𝕜 n F (p, x)) (hmn : m + 1 ≤ n) : ContDiffAt 𝕜 m (fun (q : P × E) => fderiv 𝕜 (fun (y : E) => F (q.1, y)) q.2) (p, x)

The spatial differential of a C^n family is C^m jointly in the parameter and the spatial variable, for m + 1 ≤ n.

theorem ContDiffAt.eventually_contDiffAt_graph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {P : Type u_2} [NormedAddCommGroup P] [NormedSpace 𝕜 P] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X : Type u_4} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {p : P} {f : P × E → X} {ψ : P → E} {n : ℕ} (hf : ContDiffAt 𝕜 (↑n) f (p, ψ p)) (hψ : ContinuousAt ψ p) : ∀ᶠ (q : P) in nhds p, ContDiffAt 𝕜 (↑n) f (q, ψ q)

A function that is C^n at (p, ψ p) is C^n at (q, ψ q) for q near p, when ψ is continuous at p.

theorem ContDiffAt.continuousAt_fderiv_comp_inr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {P : Type u_2} [NormedAddCommGroup P] [NormedSpace 𝕜 P] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X : Type u_4} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {p : P} {G : P × E → X} {ψ : P → E} (hG : ContDiffAt 𝕜 1 G (p, ψ p)) (hψ : ContinuousAt ψ p) : ContinuousAt (fun (q : P) => fderiv 𝕜 G (q, ψ q) ∘SL ContinuousLinearMap.inr 𝕜 P E) p

The vertical part of the derivative of a C¹ map is continuous along a continuous graph.

theorem ContDiffAt.fderiv_snd_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {P : Type u_2} [NormedAddCommGroup P] [NormedSpace 𝕜 P] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {X : Type u_4} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {n m : WithTop ℕ∞} {f : P × E → X} {r : P × E} (hf : ContDiffAt 𝕜 n f r) (hmn : m + 1 ≤ n) (v : E) : ContDiffAt 𝕜 m (fun (r : P × E) => (fderiv 𝕜 (fun (z : E) => f (r.1, z)) r.2) v) r

The partial derivative in the second variable of a function of (r.1, z), applied to a fixed vector, is as differentiable in r as the function allows.

theorem ContDiff.exists_derivative_fields_of_hasCompactSupport {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E × ℝ → F} (hf : ContDiff ℝ 3 f) (hs : HasCompactSupport f) : ∃ (fx : E × ℝ → E →L[ℝ] F) (fxx : E × ℝ → E →L[ℝ] E →L[ℝ] F) (ft : E × ℝ → F), ContDiff ℝ 2 fx ∧ HasCompactSupport fx ∧ ContDiff ℝ 1 fxx ∧ HasCompactSupport fxx ∧ ContDiff ℝ 2 ft ∧ HasCompactSupport ft ∧ (∀ (p : E × ℝ), HasFDerivAt (fun (y : E) => f (y, p.2)) (fx p) p.1) ∧ (∀ (p : E × ℝ), HasFDerivAt (fun (y : E) => fx (y, p.2)) (fxx p) p.1) ∧ ∀ (p : E × ℝ), HasDerivAt (fun (s : ℝ) => f (p.1, s)) (ft p) p.2

The spatial first and second derivative fields and the time derivative field of a compactly supported C³ function on a product with a real second factor are compactly supported, of the expected smoothness, and compute its slice derivatives at every point.