OAI/Geometry/SurfaceImmersion/Atlas/AtlasQuadraticTargets.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual supported quadratic targets for the global phase expansion.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.globalQuadraticPhase line 30
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.globalQuadraticPhase_smooth line 35
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.globalQuadraticTarget line 42
  4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.globalQuadraticTarget_expansion line 58
  5. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.global_quadratic_cancellation line 80