VelocitySpatialBounds.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Compact bounds for the actual circular velocity derivative, uniform in both the angle and its arbitrarily large derivatives.

theorem OAI.ClosedSurfaceR4.VelocityFrame.compact_spatialError_bound line 16
theorem OAI.ClosedSurfaceR4.VelocityFrame.compact_spatialError_bound_on line 41

theorem OAI.ClosedSurfaceR4.VelocityFrame.circular_first_normal_bound line 67

Source documentation

The true differentiated velocity has the first normal bound, with no angular derivative.

theorem circular_first_normal_bound {Q : E → Vec} {R : E → ℝ}
    {e₁ e₂ : E → Vec} {α : E → ℝ} {x v : E} {n : Vec}
    (hQ : DifferentiableAt ℝ Q x) (hR : DifferentiableAt ℝ R x)
    (h₁ : DifferentiableAt ℝ e₁ x) (h₂ : DifferentiableAt ℝ e₂ x)
    (hα : DifferentiableAt ℝ α x) (hn : n ⬝ᵥ n = 1)
    (horth : angularDirection (e₁ x) (e₂ x) (α x) ⬝ᵥ n = 0) :
    |fderiv ℝ (fun y => Q y + R y • direction (e₁ y) (e₂ y) (α y)) x v ⬝ᵥ n| ≤
      4 * ‖spatialError Q R e₁ e₂ α x v‖ := by
…

Mentions: OAI.ClosedSurfaceR4.VelocityFrame.angularDirection, OAI.ClosedSurfaceR4.VelocityFrame.direction, OAI.ClosedSurfaceR4.VelocityFrame.spatialError

theorem OAI.ClosedSurfaceR4.VelocityFrame.circular_second_normal_bound line 79

Source documentation

The other normal coefficient is R times the angular derivative plus the same bounded error.

theorem circular_second_normal_bound {Q : E → Vec} {R : E → ℝ}
    {e₁ e₂ : E → Vec} {α : E → ℝ} {x v : E}
    (hQ : DifferentiableAt ℝ Q x) (hR : DifferentiableAt ℝ R x)
    (h₁ : DifferentiableAt ℝ e₁ x) (h₂ : DifferentiableAt ℝ e₂ x)
    (hα : DifferentiableAt ℝ α x)
    (hunit : angularDirection (e₁ x) (e₂ x) (α x) ⬝ᵥ
      angularDirection (e₁ x) (e₂ x) (α x) = 1) :
    |fderiv ℝ (fun y => Q y + R y • direction (e₁ y) (e₂ y) (α y)) x v ⬝ᵥ
      angularDirection (e₁ x) (e₂ x) (α x) - R x * fderiv ℝ α x v| ≤
      4 * ‖spatialError Q R e₁ e₂ α x v‖ := by
…

Mentions: OAI.ClosedSurfaceR4.VelocityFrame.angularDirection, OAI.ClosedSurfaceR4.VelocityFrame.direction, OAI.ClosedSurfaceR4.VelocityFrame.spatialError