OAI/Geometry/SurfaceImmersion/Primitive/VelocityNormalBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClosedSurfaceR4.VelocityFrame.leadingNormal line 14
2. def OAI.ClosedSurfaceR4.VelocityFrame.normalSize line 17
3. lemma OAI.ClosedSurfaceR4.VelocityFrame.leadingTangent_smoothOn line 23
4. lemma OAI.ClosedSurfaceR4.VelocityFrame.leadingNormal_smoothOn line 34
5. lemma OAI.ClosedSurfaceR4.VelocityFrame.normalSize_positive line 48
6. theorem OAI.ClosedSurfaceR4.VelocityFrame.compact_normalSize_bounds line 54

   Source documentation

   Both the normal length and its reciprocal are uniformly controlled on compact data.

   theorem compact_normalSize_bounds (hU : IsOpen U)
       (hX : ContDiffOn ℝ ∞ X U) (hY : ContDiffOn ℝ ∞ Y U)
       (hC : ContDiffOn ℝ ∞ C U) (hV : ContDiffOn ℝ ∞ V U)
       (hD : ∀ x ∈ U, gramDet (Y x) (C x) ≠ 0)
       (hYV : ∀ x ∈ U, Y x ⬝ᵥ V x = 0) (hCV : ∀ x ∈ U, C x ⬝ᵥ V x = 0)
       (hV0 : ∀ x ∈ U, V x ≠ 0) {K : Set E} (hK : IsCompact K) (hKU : K ⊆ U) :
       ∃ c D : ℝ, 0 < c ∧ 0 < D ∧ ∀ x ∈ K,
         c ≤ normalSize (X x) (Y x) (C x) (V x) ∧
         normalSize (X x) (Y x) (C x) (V x) ≤ D ∧
         1 / normalSize (X x) (Y x) (C x) (V x) ≤ 1 / c := by
   …

   Mentions: OAI.ClosedSurfaceR4.VelocityFrame.normalSize