OAI/Geometry/SurfaceImmersion/Atlas/AtlasNormalProjection.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Project a global ambient field to the normal bundle using the fixed finite atlas. No orientation or global tangent frame is chosen.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.localizedNormalField line 23
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.localProjectedNormal line 26
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.localizedNormalField_smooth line 32
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.localizedNormalField_support line 40
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.localProjectedNormal_smooth line 56
  6. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.projectedNormalField line 75
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.projectedNormalField_smooth line 78
  8. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.localProjectedNormal_zero line 88
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.vectorPlaneRead_fderiv_at_weight line 98
  10. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.vectorPlaneRead_normal line 114
  11. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.localProjectedNormal_normal line 127
  12. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.projectedNormalField_normal line 163
  13. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.projectedNormalField_fixed line 196
  14. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.projectedPreferredNormal line 229

    Source documentation

    Normalize the actual global normal projection wherever it is nonzero.

    def projectedPreferredNormal {F n : M → Space}
    (hF : ContMDiff planeModel spaceModel ∞ F) (hn : ContMDiff planeModel spaceModel ∞ n)
    (hD : ∀ i x, x ∈ tsupport (A.planeWeight i) →
      gramDet (coordDeriv dx (spaceCoordinates ∘ A.vectorPlaneRead i F) x)
        (coordDeriv dy (spaceCoordinates ∘ A.vectorPlaneRead i F) x) ≠ 0)
    (hne : ∀ p, A.projectedNormalField F n p ≠ 0) : PreferredNormal F where
…

    Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.spaceCoordinates, OAI.ClosedSurfaceR4.PreferredNormal