OAI/Geometry/SurfaceImmersion/Atlas/SupportedTensorChart.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Coordinate transport of the symmetric complex tensors used as targets in the perturbed phase equations.

  1. lemma OAI.ClosedSurfaceR4.JetPolynomial.tensorChartPush_zero line 18
  2. def OAI.ClosedSurfaceR4.JetPolynomial.tensorChartPush line 24
  3. lemma OAI.ClosedSurfaceR4.JetPolynomial.tensorChartPush_apply line 34
  4. def OAI.ClosedSurfaceR4.JetPolynomial.tensorChartPushLM line 37
  5. lemma OAI.ClosedSurfaceR4.JetPolynomial.tensorChartPull_zero line 51
  6. def OAI.ClosedSurfaceR4.JetPolynomial.tensorChartPull line 56
  7. lemma OAI.ClosedSurfaceR4.JetPolynomial.tensorChartPull_apply line 65
  8. lemma OAI.ClosedSurfaceR4.JetPolynomial.tensorChartPull_push line 69
  9. lemma OAI.ClosedSurfaceR4.JetPolynomial.tensorChartPush_pull line 86
  10. def OAI.ClosedSurfaceR4.JetPolynomial.tensorChartEquiv line 103