OAI/Geometry/SurfaceImmersion/Correction/TensorSmoothingSymmetry.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Tensor coordinate maps commute with transposition.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.tensorTranspose line 27

    Source documentation

    Transpose a covariant tensor by interchanging its two arguments.

    def tensorTranspose {p : M} (u : CovariantTwoTensor p) : CovariantTwoTensor p :=
…

    Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CovariantTwoTensor

  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.tensorTranspose_apply line 31
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorComponent_flip line 37
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorLocalize_flip line 54
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorRestore_flip line 67
  6. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorSmooth_flip line 101

    Source documentation

    The actual tensor smoother preserves transposition, so it acts on symmetric tensors without any extra projection.

    theorem tensorSmooth_flip (r : ℕ) {s : ℝ} (hs : 0 < s)
    {u : ∀ p : M, CovariantTwoTensor p}
    (hu : ContMDiff planeModel (planeModel.prod 𝓘(ℝ, TensorFiber)) ∞
      (fun p => TotalSpace.mk' TensorFiber p (u p))) :
    A.tensorSmooth r s (fun p => tensorTranspose (u p)) =
      fun p => tensorTranspose (A.tensorSmooth r s u p) := by
…

    Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CovariantTwoTensor, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.TensorFiber, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.tensorTranspose

  7. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorSmooth_symmetric line 125