Fourth-order geodesic midpoint algebra

This file checks the Dirichlet polynomial normalization and the cancellation between opposite Christoffel tensors. The coefficients use divided derivatives: u_j = (1/j!) ∂ε^j γ. No analytic expansion is assumed in these identities.

theorem PlanarMidpoint.obstruction_neg (c : Coeff) (J : E →L[ℝ] Coeff) (h : E) : obstruction (-c) (-J) h = obstruction c J h

The obstruction is even when the connection and its spatial derivative are simultaneously negated.

noncomputable def PlanarMidpoint.fourthDirichlet (B₀ B₂ : E) (t : ℝ) : E

The second and fourth even Dirichlet primitives of B₀ + B₂(t-1/2)².

Equations

• PlanarMidpoint.fourthDirichlet B₀ B₂ t = (((t - 1 / 2) ^ 2 - 1 / 4) / 2) • B₀ + (((t - 1 / 2) ^ 4 - 1 / 16) / 12) • B₂

@[simp]

theorem PlanarMidpoint.fourthDirichlet_zero (B₀ B₂ : E) : fourthDirichlet B₀ B₂ 0 = 0

@[simp]

theorem PlanarMidpoint.fourthDirichlet_one (B₀ B₂ : E) : fourthDirichlet B₀ B₂ 1 = 0

theorem PlanarMidpoint.fourthDirichlet_midpoint (B₀ B₂ : E) : fourthDirichlet B₀ B₂ (1 / 2) = -(1 / 8) • B₀ - (1 / 192) • B₂

theorem PlanarMidpoint.hasDerivAt_fourthDirichlet (B₀ B₂ : E) (t : ℝ) : HasDerivAt (fourthDirichlet B₀ B₂) ((t - 1 / 2) • B₀ + ((t - 1 / 2) ^ 3 / 3) • B₂) t

theorem PlanarMidpoint.hasDerivAt_fourthDirichlet_velocity (B₀ B₂ : E) (t : ℝ) : HasDerivAt (fun (s : ℝ) => (s - 1 / 2) • B₀ + ((s - 1 / 2) ^ 3 / 3) • B₂) (B₀ + (t - 1 / 2) ^ 2 • B₂) t

noncomputable def PlanarMidpoint.fourthMidpointCoefficient (c : Coeff) (J : E →L[ℝ] Coeff) (H : Coeff) (h : E) : E

The quartic midpoint coefficient after solving the Dirichlet jet equations. H denotes (D_h²K) in coefficient coordinates.

Equations

• One or more equations did not get rendered due to their size.

def PlanarMidpoint.cubicJetVector (c : Coeff) (J : E →L[ℝ] Coeff) (h : E) : E

The cubic jet vector n = 2K(h,K(h,h)) - (D_hK)(h,h).

Equations

• PlanarMidpoint.cubicJetVector c J h = 2 • PlanarMidpoint.K c h (PlanarMidpoint.K c h h) - PlanarMidpoint.K (J h) h h

noncomputable def PlanarMidpoint.fourthAccelerationZero (c : Coeff) (J : E →L[ℝ] Coeff) (h : E) : E

Constant term of the fourth jet's acceleration in centered time.

Equations

• PlanarMidpoint.fourthAccelerationZero c J h = (1 / 12) • PlanarMidpoint.K c h (PlanarMidpoint.cubicJetVector c J h) - (1 / 8) • PlanarMidpoint.K (J (PlanarMidpoint.K c h h)) h h

noncomputable def PlanarMidpoint.fourthAccelerationTwo (c : Coeff) (J : E →L[ℝ] Coeff) (H : Coeff) (h : E) : E

Quadratic term of the fourth jet's acceleration in centered time.

Equations

• One or more equations did not get rendered due to their size.

theorem PlanarMidpoint.fourthDirichlet_coefficient (c : Coeff) (J : E →L[ℝ] Coeff) (H : Coeff) (h : E) : fourthDirichlet (fourthAccelerationZero c J h) (fourthAccelerationTwo c J H h) (1 / 2) = fourthMidpointCoefficient c J H h

Solving the quartic Dirichlet equation gives the exact coefficient.

theorem PlanarMidpoint.fourthMidpointCoefficient_add_opposite (c : Coeff) (J : E →L[ℝ] Coeff) (H : Coeff) (h : E) : fourthMidpointCoefficient c J H h + fourthMidpointCoefficient (-c) (-J) (-H) h = (1 / 192) • obstruction c J h

Opposite connections cancel every quartic contribution except the first-order obstruction.

theorem PlanarMidpoint.fourth_defect_factor (c : Coeff) (J : E →L[ℝ] Coeff) (H : Coeff) (h : E) : 24 • (fourthMidpointCoefficient c J H h + fourthMidpointCoefficient (-c) (-J) (-H) h) = (1 / 8) • obstruction c J h

Multiplication by 4! converts the sum of divided quartic coefficients into the fourth derivative of the midpoint defect.