OAI/Geometry/SurfaceImmersion/Atlas/TensorChartRead.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Smooth chart readings of tensors agree with unweighted components on the phase support and are bounded by the fixed atlas seminorms.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorChartRead line 30
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorChartRead_on_weight line 33
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorEncode_read line 41
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorChartRead_smooth line 54
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorChartRead_bound line 61