OAI/Geometry/SurfaceImmersion/Atlas/SpatialPhaseBasis.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Actual point-dependent phase bases. Outside the region of invertible phase triples a fixed basis supplies harmless global values.

  1. def OAI.ClosedSurfaceR4.PhaseGeometry.admissiblePhaseCovectors line 14
  2. lemma OAI.ClosedSurfaceR4.PhaseGeometry.admissiblePhaseCovectors_eventually line 17
  3. def OAI.ClosedSurfaceR4.PhaseGeometry.resolvedPhaseBasis line 28
  4. lemma OAI.ClosedSurfaceR4.PhaseGeometry.resolvedPhaseBasis_covectors line 34
  5. lemma OAI.ClosedSurfaceR4.PhaseGeometry.resolvedPhaseBasis_coefficients line 38
  6. lemma OAI.ClosedSurfaceR4.PhaseGeometry.resolvedPhaseBasis_coefficient_smoothAt line 43
  7. def OAI.ClosedSurfaceR4.PhaseGeometry.convexSpatialBasis line 55
  8. lemma OAI.ClosedSurfaceR4.PhaseGeometry.convexSpatialBasis_coefficient_smoothAt line 58