Mixed derivatives of a parametric map

For a map F : 𝕜 × E → F' with the minimum smoothness needed for symmetric second derivatives, differentiating its spatial Jacobian in the parameter direction at t₀ is the spatial derivative of its parameter velocity at t₀. This is the mixed-partial identity needed to identify the derivative of a parametric-family pullback with a Lie bracket. Over ℝ or ℂ, the required smoothness is C²; over a general nontrivially normed field, it is analyticity.

This supplies a prerequisite for Deliverable A, Layer 1 of TauCetiRoadmap/RepresentationTheory/LieGroups/README.md.

Main definitions

• spatialFDeriv: the spatial Jacobian of a parametric map.
• timeFDeriv: the parameter velocity at a specified parameter value.

Main results

• hasDerivAt_parameterCurve: the parameter velocity differentiates the corresponding parameter curve.
• hasFDerivAt_timeSlice: the spatial Jacobian differentiates the corresponding fixed-parameter slice.
• fderiv_timeSlice: the derivative of a fixed-parameter slice is its spatial Jacobian.
• ContDiffAt.deriv_parameterCurve_eventuallyEq_timeFDeriv: near a point, the derivatives of the parameter curves are the parameter-velocity field.
• hasDerivAt_spatialFDeriv: the spatial Jacobian differentiates to the spatial derivative of the parameter velocity.
• deriv_spatialFDeriv_apply: the parameter derivative of the spatial Jacobian equals the derivative of the parameter-velocity field.
• deriv_deriv_comm: for a map of two scalar variables, the two iterated partial derivatives agree.

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 1, "The infinitesimal adjoint".
• Sébastien Gouëzel, Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean, theorem ContDiffAt.isSymmSndFDerivAt.

noncomputable def spatialFDeriv {𝕜 : Type u_1} {E : Type u_2} {F' : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] (F : 𝕜 × E → F') (x : E) (t : 𝕜) : E →L[𝕜] F'

The spatial Jacobian of a parametric map at x, as a function of the parameter. If F is not differentiable at (t, x), its value at t is the junk value 0.

Equations

• spatialFDeriv F x t = fderiv 𝕜 F (t, x) ∘SL ContinuousLinearMap.inr 𝕜 𝕜 E

theorem spatialFDeriv_def {𝕜 : Type u_1} {E : Type u_2} {F' : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] (F : 𝕜 × E → F') (x : E) (t : 𝕜) : spatialFDeriv F x t = fderiv 𝕜 F (t, x) ∘SL ContinuousLinearMap.inr 𝕜 𝕜 E

The spatial derivative as the restriction of the full derivative to the spatial factor.

theorem spatialFDeriv_eq {𝕜 : Type u_1} {E : Type u_2} {F' : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] (F : 𝕜 × E → F') (x : E) : spatialFDeriv F x = fun (t : 𝕜) => fderiv 𝕜 F (t, x) ∘SL ContinuousLinearMap.inr 𝕜 𝕜 E

The spatial derivative, as a function of the parameter.

@[simp]

theorem spatialFDeriv_apply {𝕜 : Type u_1} {E : Type u_2} {F' : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] (F : 𝕜 × E → F') (x : E) (t : 𝕜) (w : E) : (spatialFDeriv F x t) w = (fderiv 𝕜 F (t, x)) (0, w)

noncomputable def timeFDeriv {𝕜 : Type u_1} {E : Type u_2} {F' : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] (F : 𝕜 × E → F') (t : 𝕜) (x : E) : F'

The parameter velocity of a parametric map at (t, x). If F is not differentiable there, this is the junk value 0.

Equations

• timeFDeriv F t x = (fderiv 𝕜 F (t, x)) (1, 0)

@[simp]

theorem timeFDeriv_apply {𝕜 : Type u_1} {E : Type u_2} {F' : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] (F : 𝕜 × E → F') (t : 𝕜) (x : E) : timeFDeriv F t x = (fderiv 𝕜 F (t, x)) (1, 0)

theorem timeFDeriv_eq {𝕜 : Type u_1} {E : Type u_2} {F' : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] (F : 𝕜 × E → F') (t : 𝕜) : timeFDeriv F t = fun (x : E) => (fderiv 𝕜 F (t, x)) (1, 0)

The parameter velocity, as a function of the spatial variable.

theorem hasDerivAt_parameterCurve {𝕜 : Type u_1} {E : Type u_2} {F' : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {F : 𝕜 × E → F'} {t : 𝕜} {x : E} (hF : DifferentiableAt 𝕜 F (t, x)) : HasDerivAt (fun (s : 𝕜) => F (s, x)) (timeFDeriv F t x) t

The parameter velocity is the derivative of the parameter curve fun s ↦ F (s, x).

theorem hasFDerivAt_timeSlice {𝕜 : Type u_1} {E : Type u_2} {F' : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {F : 𝕜 × E → F'} {t : 𝕜} {x : E} (hF : DifferentiableAt 𝕜 F (t, x)) : HasFDerivAt (fun (y : E) => F (t, y)) (spatialFDeriv F x t) x

The spatial Jacobian is the derivative of the fixed-parameter slice fun y ↦ F (t, y).

theorem fderiv_timeSlice {𝕜 : Type u_1} {E : Type u_2} {F' : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {F : 𝕜 × E → F'} {t : 𝕜} {x : E} (hF : DifferentiableAt 𝕜 F (t, x)) : fderiv 𝕜 (fun (y : E) => F (t, y)) x = spatialFDeriv F x t

The derivative of the fixed-parameter slice fun y ↦ F (t, y) is its spatial Jacobian.

theorem ContDiffAt.deriv_parameterCurve_eventuallyEq_timeFDeriv {𝕜 : Type u_1} {E : Type u_2} {F' : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {F : 𝕜 × E → F'} {t : 𝕜} {x : E} (hF : ContDiffAt 𝕜 1 F (t, x)) : (fun (y : E) => deriv (fun (s : 𝕜) => F (s, y)) t) =ᶠ[nhds x] timeFDeriv F t

Near x, the derivative of each parameter curve is the parameter-velocity field.

theorem hasDerivAt_spatialFDeriv {𝕜 : Type u_1} {E : Type u_2} {F' : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {F : 𝕜 × E → F'} {t : 𝕜} {x : E} (hF : ContDiffAt 𝕜 (minSmoothness 𝕜 2) F (t, x)) : HasDerivAt (spatialFDeriv F x) (fderiv 𝕜 (timeFDeriv F t) x) t

At t, the spatial Jacobian has derivative the spatial derivative of the parameter velocity.

theorem deriv_spatialFDeriv_apply {𝕜 : Type u_1} {E : Type u_2} {F' : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {F : 𝕜 × E → F'} {t : 𝕜} {x w : E} (hF : ContDiffAt 𝕜 (minSmoothness 𝕜 2) F (t, x)) : deriv (fun (s : 𝕜) => (spatialFDeriv F x s) w) t = (fderiv 𝕜 (timeFDeriv F t) x) w

For a sufficiently smooth parametric map, the parameter derivative of its spatial Jacobian, applied to w, is the spatial derivative of its parameter-velocity field applied to w.

theorem deriv_deriv_comm {𝕜 : Type u_1} {F' : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {g : 𝕜 × 𝕜 → F'} {t x : 𝕜} (hg : ContDiffAt 𝕜 (minSmoothness 𝕜 2) g (t, x)) : deriv (fun (s : 𝕜) => deriv (fun (r : 𝕜) => g (s, r)) x) t = deriv (fun (r : 𝕜) => deriv (fun (s : 𝕜) => g (s, r)) t) x

Iterated partial derivatives of a map of two scalar variables commute. For a map g : 𝕜 × 𝕜 → F' which is smooth enough at (t, x) for its second derivative to be symmetric, differentiating the second partial derivative in the first variable gives the same value as differentiating the first partial derivative in the second variable.