OAI/Geometry/SurfaceImmersion/Atlas/UniformNearbyAtlasSmallIncrement.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite mean adjustment gives a small increment uniformly over nearby input maps.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.linearAtlasPhase line 28

    Source documentation

    The fixed geometric phase expressed as a smooth function on the surface.

    def linearAtlasPhase (Q : A.centers → PhaseBasis) (w : A.centers → Fin 3 → ℝ)
    (a : A.centers × Fin 3) : M → ℝ :=
…
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.uniform_nearby_atlas_small_increment line 33