OAI/Geometry/SurfaceImmersion/Correction/TensorSmoothing.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Smoothing on the actual covariant two-tensor bundle of the surface.

  1. abbrev OAI.ClosedSurfaceR4.FiniteOrderSmoothing.TensorFiber line 13
  2. abbrev OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CovariantTwoTensor line 22
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorTriv line 34
  4. instance OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorTriv_mem line 39
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorTriv_domain line 43
  6. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorSmooth line 52
  7. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.TensorWeightedBound line 55
  8. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorSmooth_smooth line 61
  9. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensor_smoothing_bounds line 69
  10. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensor_smoothing_tail line 85