OAI/Geometry/SurfaceImmersion/Whitney/CollarVelocityFamily.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Smooth parameter families of the actual collar velocity.

  1. lemma OAI.ClosedSurfaceR4.CollarVelocity.vectorLoop_family_smoothOn line 17
  2. lemma OAI.ClosedSurfaceR4.CollarVelocity.vectorLoop_family_smooth line 40
  3. lemma OAI.ClosedSurfaceR4.CollarVelocity.vectorLoop_eq_of_amplitude_zero line 49
  4. theorem OAI.ClosedSurfaceR4.CollarVelocity.collar_flatness line 56

    Source documentation

    Every spatial derivative vanishes on the boundary of a zero-amplitude region.

    theorem collar_flatness
    (hR : ContDiff ℝ ∞ R) (hv : ContDiff ℝ ∞ v) (ha : ContDiff ℝ ∞ a)
    (h₁ : ContDiff ℝ ∞ e₁) (h₂ : ContDiff ℝ ∞ e₂)
    (hRp : ∀ p, 0 < R p) (hvp : ∀ p, 0 < v p)
    (hq : ∀ p, R p ^ 2 = v p ^ 2 + a p ^ 2)
    {O : Set A} (hO : IsOpen O) (hz : ∀ p ∈ O, a p = 0) (t : ℝ) (n : ℕ) :
    Set.EqOn (iteratedFDeriv ℝ n (fun p =>
      vectorLoop (e₁ p) (e₂ p) (R p) (v p) (a p) (t : Period) - v p • e₁ p))
      (fun _ => 0) (closure O) := by
…

    Mentions: OAI.ClosedSurfaceR4.CollarVelocity.vectorLoop