OAI/Geometry/SurfaceImmersion/Correction/SurfaceMeanTensor.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The primitive's three mean metric coefficients are exactly the tensor operator used by the finite parametrix, in its product coordinates.

  1. def OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.meanTensorPolynomial line 16
  2. def OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.meanTensorOperator line 19
  3. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.meanTensorPolynomial_smooth line 25
  4. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.meanTensorPolynomial_order line 29
  5. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.realMetric_coordinate line 33
  6. theorem OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.coordinateMetricMap_eq_meanTensorOperator line 77

    Source documentation

    No identification of metric operators is assumed: the coordinate conversion and all three polynomial coefficients are proved equal.

    theorem coordinateMetricMap_eq_meanTensorOperator
    {G : JetPolynomial.Base → JetPolynomial.Space} (hG : ContDiff ℝ ∞ G)
    (n : ℕ) (z : ℝ) :
    Perturbation.coordinateMetricMap (l.meanTensorPolynomial n) z G =
      l.meanTensorOperator n z G := by
…

    Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space