OAI/Geometry/SurfaceImmersion/Primitive/PhasePrimitiveGlobalTensor.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Identification of a supported analytic primitive with the square of its actual global surface phase differential.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.localized_primitive_tensor_at line 28
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phase_primitive_global_tensor line 49