OAI/Geometry/SurfaceImmersion/Primitive/PrimitiveMetric.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The supported primitive tensor is positive semidefinite, so the target of a primitive addition is an actual smooth Riemannian metric.

  1. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.amplitude_eq_zero_of_velocity_eq_normal line 15
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitiveTensor line 40
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitiveTensor_smooth line 44
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitiveTensor_symmetric line 58
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitiveTensor_nonneg line 69
  6. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitiveMetric line 85
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitive_amplitude_zero_off_weight line 101