OAI/Geometry/SurfaceImmersion/Correction/AtlasPrimitivePolynomial.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Embed the three mean-polynomial coefficients of one primitive in the actual global atlas operator, with zero contribution from every other chart.

  1. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.meanTensorPolynomial_global_extension line 15
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitiveAtlasPolynomial line 64

    Source documentation

    A single primitive's mean polynomial in the fixed atlas.

    def primitiveAtlasPolynomial {n : ℕ} (i : A.centers) (P : Fin 3 → Fin n → Expression)
    (j : A.centers) : Fin 3 → Fin n → Expression := by
…
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitiveAtlasPolynomial_smooth line 70
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlasPolynomialValue_primitive line 81