OAI/Geometry/SurfaceImmersion/Correction/SmoothPrimitiveFamily.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Actual finite smooth primitive families and their partial-cycle metrics. Different cycles may use different supports and phases.

  1. structure OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothPrimitiveFamily line 26
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothPrimitiveFamily.term line 39
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothPrimitiveFamily.term_apply line 43
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothPrimitiveFamily.term_symmetric line 53
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothPrimitiveFamily.term_nonneg line 59
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothPrimitiveFamily.term_smooth line 65
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothPrimitiveFamily.tensor_nonneg line 72
  8. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothPrimitiveFamily.tensor_symmetric line 79
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothPrimitiveFamily.tensor_smooth line 85
  10. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothPrimitiveFamily.cycleTensor line 93

    Source documentation

    The completed-cycle contribution plus any subset of the current cycle.

    def cycleTensor (N c : ℕ) (s : Finset ι) (p : M) : CovariantTwoTensor p :=
…

    Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CovariantTwoTensor

  11. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothPrimitiveFamily.cycleTensor_empty line 97
  12. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothPrimitiveFamily.cycleTensor_complete line 102
  13. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothPrimitiveFamily.cycleTensor_insert line 110
  14. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothPrimitiveFamily.cycleTensor_nonneg line 116
  15. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothPrimitiveFamily.cycleTensor_symmetric line 126
  16. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothPrimitiveFamily.cycleTensor_smooth line 135
  17. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothPrimitiveFamily.cycleMetric line 141
  18. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothPrimitiveFamily.cycleMetric_lower line 153
  19. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.correctedSmoothPrimitiveFamily line 164