Exact fourth-order approximate-geodesic identities.

@[reducible, inline]

abbrev PlanarMidpoint.Hessian : Type

A bilinear second derivative of a planar cubic coefficient field.

Equations

• PlanarMidpoint.Hessian = (PlanarMidpoint.E →L[ℝ] PlanarMidpoint.E →L[ℝ] PlanarMidpoint.Coeff)

def PlanarMidpoint.forceTail (c c₁ c₂ c₃ : Coeff) (v₁ v₂ v₃ v₄ : E) (ε : ℝ) : E

The polynomial tail after removing the first three force coefficients.

Equations

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

theorem PlanarMidpoint.force_expansion (c c₁ c₂ c₃ : Coeff) (v₁ v₂ v₃ v₄ : E) (ε : ℝ) : K (c + ε • c₁ + ε ^ 2 • c₂ + ε ^ 3 • c₃) (ε • v₁ + ε ^ 2 • v₂ + ε ^ 3 • v₃ + ε ^ 4 • v₄) (ε • v₁ + ε ^ 2 • v₂ + ε ^ 3 • v₃ + ε ^ 4 • v₄) = ε ^ 2 • K c v₁ v₁ + ε ^ 3 • (2 • K c v₁ v₂ + K c₁ v₁ v₁) + ε ^ 4 • (2 • K c v₁ v₃ + K c v₂ v₂ + 2 • K c₁ v₁ v₂ + K c₂ v₁ v₁) + ε ^ 5 • forceTail c c₁ c₂ c₃ v₁ v₂ v₃ v₄ ε

Exact trilinear expansion, with no division by the small parameter.

noncomputable def PlanarMidpoint.coefficientTail (J : E →L[ℝ] Coeff) (H : Hessian) (d₁ d₂ d₃ d₄ : E) (ε : ℝ) : Coeff

The exact coefficient-field Taylor tail induced by a quartic displacement.

Equations

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

theorem PlanarMidpoint.coefficient_expansion (c : Coeff) (J : E →L[ℝ] Coeff) (H : Hessian) (d₁ d₂ d₃ d₄ : E) (ε : ℝ) : have δ := ε • d₁ + ε ^ 2 • d₂ + ε ^ 3 • d₃ + ε ^ 4 • d₄; c + J δ + (1 / 2) • (H δ) δ = c + ε • J d₁ + ε ^ 2 • (J d₂ + (1 / 2) • (H d₁) d₁) + ε ^ 3 • coefficientTail J H d₁ d₂ d₃ d₄ ε

Exact substitution into the quadratic spatial Taylor polynomial.

noncomputable def PlanarMidpoint.secondJet (c : Coeff) (h : E) (t : ℝ) : E

The quadratic Dirichlet jet.

Equations

• PlanarMidpoint.secondJet c h t = (1 / 8 - 1 / 2 * (t - 1 / 2) ^ 2) • PlanarMidpoint.K c h h

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

The cubic Dirichlet jet.

Equations

• PlanarMidpoint.thirdJet c J h t = ((t - 1 / 2) ^ 3 / 6 - (t - 1 / 2) / 24) • PlanarMidpoint.cubicJetVector c J h

noncomputable def PlanarMidpoint.secondJetVelocity (c : Coeff) (h : E) (t : ℝ) : E

The velocity of the quadratic Dirichlet jet.

Equations

• PlanarMidpoint.secondJetVelocity c h t = -(t - 1 / 2) • PlanarMidpoint.K c h h

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

The velocity of the cubic Dirichlet jet.

Equations

• PlanarMidpoint.thirdJetVelocity c J h t = ((t - 1 / 2) ^ 2 / 2 - 1 / 24) • PlanarMidpoint.cubicJetVector c J h

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

The quartic Dirichlet jet determined by its constant and quadratic acceleration.

Equations

• PlanarMidpoint.fourthJet c J H h = PlanarMidpoint.fourthDirichlet (PlanarMidpoint.fourthAccelerationZero c J h) (PlanarMidpoint.fourthAccelerationTwo c J ((H h) h) h)

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

The velocity of the quartic Dirichlet jet.

Equations

• PlanarMidpoint.fourthJetVelocity c J H h t = (t - 1 / 2) • PlanarMidpoint.fourthAccelerationZero c J h + ((t - 1 / 2) ^ 3 / 3) • PlanarMidpoint.fourthAccelerationTwo c J ((H h) h) h

noncomputable def PlanarMidpoint.approxDisplacement (c : Coeff) (J : E →L[ℝ] Coeff) (H : Hessian) (h : E) (ε t : ℝ) : E

Quartic endpoint-matched approximate geodesic, relative to its center.

Equations

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

noncomputable def PlanarMidpoint.approxVelocity (c : Coeff) (J : E →L[ℝ] Coeff) (H : Hessian) (h : E) (ε t : ℝ) : E

The velocity of the fourth-order endpoint-matched approximate geodesic.

Equations

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

noncomputable def PlanarMidpoint.approxAcceleration (c : Coeff) (J : E →L[ℝ] Coeff) (H : Hessian) (h : E) (ε t : ℝ) : E

The acceleration of the fourth-order approximate geodesic.

Equations

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

@[simp]

theorem PlanarMidpoint.secondJet_zero (c : Coeff) (h : E) : secondJet c h 0 = 0

@[simp]

theorem PlanarMidpoint.secondJet_one (c : Coeff) (h : E) : secondJet c h 1 = 0

@[simp]

theorem PlanarMidpoint.thirdJet_zero (c : Coeff) (J : E →L[ℝ] Coeff) (h : E) : thirdJet c J h 0 = 0

@[simp]

theorem PlanarMidpoint.thirdJet_one (c : Coeff) (J : E →L[ℝ] Coeff) (h : E) : thirdJet c J h 1 = 0

@[simp]

theorem PlanarMidpoint.approxDisplacement_zero (c : Coeff) (J : E →L[ℝ] Coeff) (H : Hessian) (h : E) (ε : ℝ) : approxDisplacement c J H h ε 0 = (-ε / 2) • h

@[simp]

theorem PlanarMidpoint.approxDisplacement_one (c : Coeff) (J : E →L[ℝ] Coeff) (H : Hessian) (h : E) (ε : ℝ) : approxDisplacement c J H h ε 1 = (ε / 2) • h

theorem PlanarMidpoint.hasDerivAt_secondJet (c : Coeff) (h : E) (t : ℝ) : HasDerivAt (secondJet c h) (secondJetVelocity c h t) t

theorem PlanarMidpoint.hasDerivAt_secondJetVelocity (c : Coeff) (h : E) (t : ℝ) : HasDerivAt (secondJetVelocity c h) (-K c h h) t

theorem PlanarMidpoint.hasDerivAt_thirdJet (c : Coeff) (J : E →L[ℝ] Coeff) (h : E) (t : ℝ) : HasDerivAt (thirdJet c J h) (thirdJetVelocity c J h t) t

theorem PlanarMidpoint.hasDerivAt_thirdJetVelocity (c : Coeff) (J : E →L[ℝ] Coeff) (h : E) (t : ℝ) : HasDerivAt (thirdJetVelocity c J h) ((t - 1 / 2) • cubicJetVector c J h) t

theorem PlanarMidpoint.hasDerivAt_approxDisplacement (c : Coeff) (J : E →L[ℝ] Coeff) (H : Hessian) (h : E) (ε t : ℝ) : HasDerivAt (approxDisplacement c J H h ε) (approxVelocity c J H h ε t) t

theorem PlanarMidpoint.hasDerivAt_approxVelocity (c : Coeff) (J : E →L[ℝ] Coeff) (H : Hessian) (h : E) (ε t : ℝ) : HasDerivAt (approxVelocity c J H h ε) (approxAcceleration c J H h ε t) t

noncomputable def PlanarMidpoint.approxResidualTail (c : Coeff) (J : E →L[ℝ] Coeff) (H : Hessian) (h : E) (ε t : ℝ) : E

The exact fifth-order residual tail for the quadratic spatial model.

Equations

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

theorem PlanarMidpoint.approx_residual_exact (c : Coeff) (J : E →L[ℝ] Coeff) (H : Hessian) (h : E) (ε t : ℝ) : have δ := approxDisplacement c J H h ε t; approxAcceleration c J H h ε t + K (c + J δ + (1 / 2) • (H δ) δ) (approxVelocity c J H h ε t) (approxVelocity c J H h ε t) = ε ^ 5 • approxResidualTail c J H h ε t

The approximate geodesic solves the quadratic spatial model through order four. The remainder is a polynomial expression, including at ε=0.

noncomputable def PlanarMidpoint.approxDisplacementScaled (c : Coeff) (J : E →L[ℝ] Coeff) (H : Hessian) (h : E) (ε t : ℝ) : E

Removing the explicit small parameter from the approximate displacement.

Equations

• PlanarMidpoint.approxDisplacementScaled c J H h ε t = (t - 1 / 2) • h + ε • PlanarMidpoint.secondJet c h t + ε ^ 2 • PlanarMidpoint.thirdJet c J h t + ε ^ 3 • PlanarMidpoint.fourthJet c J H h t

noncomputable def PlanarMidpoint.approxVelocityScaled (c : Coeff) (J : E →L[ℝ] Coeff) (H : Hessian) (h : E) (ε t : ℝ) : E

Removing the explicit small parameter from the approximate velocity.

Equations

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

theorem PlanarMidpoint.approxDisplacement_factor (c : Coeff) (J : E →L[ℝ] Coeff) (H : Hessian) (h : E) (ε t : ℝ) : approxDisplacement c J H h ε t = ε • approxDisplacementScaled c J H h ε t

theorem PlanarMidpoint.approxVelocity_factor (c : Coeff) (J : E →L[ℝ] Coeff) (H : Hessian) (h : E) (ε t : ℝ) : approxVelocity c J H h ε t = ε • approxVelocityScaled c J H h ε t

theorem PlanarMidpoint.continuous_approxDisplacementScaled (c : Coeff) (J : E →L[ℝ] Coeff) (H : Hessian) (h : E) : Continuous fun (p : ℝ × ℝ) => approxDisplacementScaled c J H h p.1 p.2

theorem PlanarMidpoint.continuous_approxVelocityScaled (c : Coeff) (J : E →L[ℝ] Coeff) (H : Hessian) (h : E) : Continuous fun (p : ℝ × ℝ) => approxVelocityScaled c J H h p.1 p.2

theorem PlanarMidpoint.continuous_K_family {X : Type u_1} [TopologicalSpace X] {c : X → Coeff} {u v : X → E} (hc : Continuous c) (hu : Continuous u) (hv : Continuous v) : Continuous fun (x : X) => K (c x) (u x) (v x)

theorem PlanarMidpoint.continuous_approxResidualTail (c : Coeff) (J : E →L[ℝ] Coeff) (H : Hessian) (h : E) : Continuous fun (p : ℝ × ℝ) => approxResidualTail c J H h p.1 p.2

theorem PlanarMidpoint.approx_uniform_bounds (c : Coeff) (J : E →L[ℝ] Coeff) (H : Hessian) (h : E) : ∃ (B : ℝ), 1 ≤ B ∧ ∃ (R : ℝ), 0 ≤ R ∧ ∀ (ε t : ℝ), |ε| ≤ 1 → t ∈ Set.Icc 0 1 → ‖approxDisplacement c J H h ε t‖ ≤ B * |ε| ∧ ‖approxVelocity c J H h ε t‖ ≤ B * |ε| ∧ ‖approxResidualTail c J H h ε t‖ ≤ R

Uniform estimates on the compact parameter rectangle. The displacement and velocity bounds include their explicit first-order small parameter.

theorem PlanarMidpoint.approxDisplacement_midpoint (c : Coeff) (J : E →L[ℝ] Coeff) (H : Hessian) (h : E) (ε : ℝ) : approxDisplacement c J H h ε (1 / 2) = (ε ^ 2 / 8) • K c h h + ε ^ 4 • fourthMidpointCoefficient c J ((H h) h) h

Midpoint value of the approximate geodesic.

theorem PlanarMidpoint.approxDisplacement_add_opposite_midpoint (c : Coeff) (J : E →L[ℝ] Coeff) (H : Hessian) (h : E) (ε : ℝ) : approxDisplacement c J H h ε (1 / 2) + approxDisplacement (-c) (-J) (-H) h ε (1 / 2) = (ε ^ 4 / 192) • obstruction c J h

The opposite approximate midpoints retain exactly the quartic obstruction.