OAI/Geometry/SurfaceImmersion/Atlas/TensorPhaseDecomposition.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The finite phase-basis decomposition on global symmetric tensor sections. The atlas partition restores the tensor exactly, including chart overlaps.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorEncode_symmetric line 33
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.tensorDecode_symmetric line 45
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phaseCoefficient line 60
  4. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phaseTensor line 64
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.sum_phaseTensor line 68
  6. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.global_phase_tensor_decomposition line 86

    Source documentation

    The actual finite restored phase family sums to the original global tensor.

    theorem global_phase_tensor_decomposition (P : A.centers → PhaseBasis)
    {u : ∀ x : M, CovariantTwoTensor x} (hu : ∀ p v w, u p v w = u p w v) (p : M) :
    (∑ i : A.centers, ∑ j : Fin 3, A.bundleRestore A.tensorTriv i (A.phaseTensor P u i j) p) = u p := by
…

    Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CovariantTwoTensor