OAI/Geometry/SurfaceImmersion/Primitive/VelocityNormalEstimates.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Normal-component bounds independent of the chosen angular derivative.

  1. lemma OAI.ClosedSurfaceR4.VelocityFrame.unit_coordinate_abs_le line 12
  2. lemma OAI.ClosedSurfaceR4.VelocityFrame.abs_dot_unit_le line 20
  3. theorem OAI.ClosedSurfaceR4.VelocityFrame.first_normal_bound line 33
  4. theorem OAI.ClosedSurfaceR4.VelocityFrame.second_normal_error_bound line 38
  5. theorem OAI.ClosedSurfaceR4.VelocityFrame.turn_dominates line 44

    Source documentation

    A fixed threshold is exceeded by a sufficiently large derivative at a turn.

    theorem turn_dominates {r R B M T C d E : ℝ}
    (hr : 0 < r) (hR : r ≤ R) (hT : 0 ≤ T) (hC : 0 ≤ C)
    (hB : M + (T + C + 1) / r < B) (hd : B - M ≤ d) (hE : |E| ≤ C) :
    T + 1 < R * d + E := by
…