Mixed mass and phase derivatives

The first homological equation differentiates phase derivatives with respect to the mass parameter. This file packages the needed Schwarz theorem for a jointly C² scalar function.

noncomputable def LeanPool.PoincareThreeBody.parameterCoefficient {B : Type u_1} [NormedAddCommGroup B] [NormedSpace ℝ B] (G : ℝ × B → ℝ) (b : B) : ℝ

The derivative in the distinguished real parameter direction at parameter zero.

Equations

• LeanPool.PoincareThreeBody.parameterCoefficient G b = (fderiv ℝ G (0, b)) (1, 0)

theorem LeanPool.PoincareThreeBody.differentiableAt_parameterCoefficient {B : Type u_1} [NormedAddCommGroup B] [NormedSpace ℝ B] {G : ℝ × B → ℝ} {b : B} (hG : ContDiffAt ℝ 2 G (0, b)) : DifferentiableAt ℝ (parameterCoefficient G) b

A jointly C² function has a differentiable first parameter coefficient in the remaining variables.

theorem LeanPool.PoincareThreeBody.contDiffAt_parameterCoefficient {B : Type u_1} [NormedAddCommGroup B] [NormedSpace ℝ B] {G : ℝ × B → ℝ} {b : B} (hG : ContDiffAt ℝ 2 G (0, b)) : ContDiffAt ℝ 1 (parameterCoefficient G) b

A jointly C² function has a continuously differentiable first parameter coefficient.

theorem LeanPool.PoincareThreeBody.fderiv_curry_right_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} [NormedAddCommGroup A] [NormedSpace ℝ A] [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup C] [NormedSpace ℝ C] {G : A × B → C} {a : A} {b v : B} (hG : DifferentiableAt ℝ G (a, b)) : (fderiv ℝ (fun (y : B) => G (a, y)) b) v = (fderiv ℝ G (a, b)) (0, v)

The phase derivative of a slice of a jointly differentiable function is its joint derivative in the pure phase direction.

theorem LeanPool.PoincareThreeBody.deriv_curry_left {B : Type u_1} [NormedAddCommGroup B] [NormedSpace ℝ B] {G : ℝ × B → ℝ} {b : B} (hG : DifferentiableAt ℝ G (0, b)) : deriv (fun (mass : ℝ) => G (mass, b)) 0 = parameterCoefficient G b

The mass derivative of a scalar slice is the joint derivative in the pure parameter direction.

theorem LeanPool.PoincareThreeBody.hasDerivAt_directionalFDeriv_along_line {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {G : E → ℝ} {x v w : E} (hG : ContDiffAt ℝ 2 G x) : HasDerivAt (fun (t : ℝ) => (iteratedFDeriv ℝ 1 G (x + t • w)) fun (x : Fin 1) => v) ((iteratedFDeriv ℝ 2 G x) ![w, v]) 0

Along an affine line, the derivative of a first directional derivative is the corresponding second directional derivative.

theorem LeanPool.PoincareThreeBody.iteratedFDeriv_two_swap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {G : E → ℝ} {x v w : E} (hG : ContDiffAt ℝ 2 G x) : (iteratedFDeriv ℝ 2 G x) ![v, w] = (iteratedFDeriv ℝ 2 G x) ![w, v]

The second derivative of a real C² function is symmetric.

theorem LeanPool.PoincareThreeBody.hasDerivAt_directionalFDeriv_along_line_swap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {G : E → ℝ} {x v w : E} (hG : ContDiffAt ℝ 2 G x) : HasDerivAt (fun (t : ℝ) => (iteratedFDeriv ℝ 1 G (x + t • w)) fun (x : Fin 1) => v) ((iteratedFDeriv ℝ 2 G x) ![v, w]) 0

The directional derivative along a line can equivalently be written with the two directions swapped. This is the form used to commute mass and phase differentiation.

theorem LeanPool.PoincareThreeBody.fderiv_parameterCoefficient {B : Type u_1} [NormedAddCommGroup B] [NormedSpace ℝ B] {G : ℝ × B → ℝ} {b v : B} (hG : ContDiffAt ℝ 2 G (0, b)) : (fderiv ℝ (parameterCoefficient G) b) v = (iteratedFDeriv ℝ 2 G (0, b)) ![(0, v), (1, 0)]

The phase derivative of the parameter coefficient is the mixed second derivative with phase first and parameter second.

theorem LeanPool.PoincareThreeBody.hasDerivAt_fderiv_curry_right {B : Type u_1} [NormedAddCommGroup B] [NormedSpace ℝ B] {G : ℝ × B → ℝ} {b v : B} (hG : ContDiffAt ℝ 2 G (0, b)) : HasDerivAt (fun (mass : ℝ) => (fderiv ℝ (fun (y : B) => G (mass, y)) b) v) ((fderiv ℝ (parameterCoefficient G) b) v) 0

Joint C² regularity commutes the parameter derivative with every phase derivative.