OAI/Geometry/SurfaceImmersion/Correction/TensorMeanIteration.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Finite mean substitution on actual global tensor sections, represented by redundant atlas coordinates. Every iterate stays in the representation range, so no leading-identity premise on arbitrary plane fields is needed.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorEncodeLM line 34
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorDecodeLM line 39
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorProjectLM line 44
  4. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorMeanOperator line 47
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorMeanOperator_project line 52
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorMean_trial_project line 58
  7. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorMeanTrial line 71
  8. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorEncode_meanTrial line 76
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorMeanTrial_zero line 82
  10. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorMeanTrial_succ line 86
  11. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorEncode_meanResidual line 95