OAI/Geometry/SurfaceImmersion/Primitive/InteriorVelocityPath.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The interior oscillatory path covers the whole velocity circle.

  1. def OAI.ClosedSurfaceR4.LoopDensity.interiorPath line 12
  2. lemma OAI.ClosedSurfaceR4.LoopDensity.interiorPath_continuous line 16
  3. theorem OAI.ClosedSurfaceR4.LoopDensity.interiorPath_covers line 26

    Source documentation

    All circle directions occur away from the endpoints and turning points.

    theorem interiorPath_covers {A h : ℝ} (hA : Real.pi + |h| < A)
    {e : Plane} (he : e 0 ^ 2 + e 1 ^ 2 = 1) :
    ∃ t ∈ Ioo (0 : ℝ) 1, interiorPath A h t = e := by
…

    Mentions: OAI.ClosedSurfaceR4.LoopDensity.Plane, OAI.ClosedSurfaceR4.LoopDensity.interiorPath