OAI/Geometry/SurfaceImmersion/Primitive/VelocitySpatialDerivative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact spatial differentiation of the actual circular velocity, separating all dependence on the angular derivative from the bounded remainder.

  1. def OAI.ClosedSurfaceR4.VelocityFrame.spatialError line 15
  2. theorem OAI.ClosedSurfaceR4.VelocityFrame.circular_velocity_derivative line 20
  3. lemma OAI.ClosedSurfaceR4.VelocityFrame.norm_direction_le line 39
  4. theorem OAI.ClosedSurfaceR4.VelocityFrame.spatialError_bound line 48

    Source documentation

    The bound does not contain a derivative of α.

    theorem spatialError_bound (Q : E → Vec) (R : E → ℝ) (e₁ e₂ : E → Vec)
    (α : E → ℝ) (x v : E) :
    ‖spatialError Q R e₁ e₂ α x v‖ ≤
      ‖fderiv ℝ Q x v‖ + |fderiv ℝ R x v| * (‖e₁ x‖ + ‖e₂ x‖) +
        |R x| * (‖fderiv ℝ e₁ x v‖ + ‖fderiv ℝ e₂ x v‖) := by
…

    Mentions: OAI.ClosedSurfaceR4.VelocityFrame.spatialError