OAI/Geometry/SurfaceImmersion/Correction/SmoothingAtlas.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite chart data with inner and outer cutoffs for smoothing on a closed surface. All chart and cutoff data are chosen independently of the input.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.chart line 18
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.chart_source line 22
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.chart_smooth line 27
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.chart_symm_smooth line 32
  5. structure OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas line 41

    Source documentation

    The outer cutoff is one on the support of the partition weight and has its own closed support inside the same chart.

    structure SmoothingAtlas (M : Type*) [TopologicalSpace M] [ChartedSpace Plane M]
    [IsManifold planeModel ∞ M] where
…

    Mentions: OAI.ClosedSurfaceR4.Plane, OAI.ClosedSurfaceR4.planeModel

  6. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.exists_smoothingAtlas line 56

    Source documentation

    A compact smooth surface admits fixed finite smoothing chart data.

    theorem exists_smoothingAtlas : Nonempty (SmoothingAtlas M) := by
…

    Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas