OAI/Geometry/SurfaceImmersion/Correction/TensorMeanCoordinates.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Encode global tensor sections by their finite atlas coordinates. This retains the compact-surface partition identity while permitting the finite mean iteration to run on a normed vector-valued function space.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorEncode line 34
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorDecode line 37
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorDecode_encode line 40
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorEncode_add line 45
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorEncode_smul line 50
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorDecode_add line 55
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorDecode_smul line 63
  8. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorEncode_sub line 71
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorDecode_sub line 81
  10. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorProject line 89
  11. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorProject_encode line 92
  12. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorProject_idempotent line 97
  13. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorEncode_smooth line 103
  14. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorDecode_smooth line 111
  15. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorEncode_bound line 118
  16. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorBound_of_encode line 127
  17. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorDecode_bound line 133