OAI/Geometry/SurfaceImmersion/Primitive/PrimitiveCycleMetrics.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

A finite positive primitive family can be repeated in equally weighted cycles. Every partial cycle is an actual smooth positive metric, and every completed cycle advances by exactly the prescribed fraction of the tensor.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.cyclePrimitiveAmplitude line 33
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.cyclePrimitiveAmplitude_square line 36
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.cyclePrimitiveAmplitude_pos_iff line 44
  4. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitiveCycleTensor line 53
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitiveCycleTensor_empty line 58
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitiveCycleTensor_start line 62
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitiveCycleTensor_insert line 67
  8. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitiveCycleTensor_insert_apply line 75
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitiveCycleTensor_complete line 93
  10. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitiveCycleTensor_finish line 105
  11. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.positivePrimitiveSum_nonneg line 109
  12. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitiveCycleTensor_nonneg line 118
  13. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitiveCycleTensor_symmetric line 133
  14. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitiveCycleTensor_smooth line 151
  15. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitiveCycleMetric line 165