CrossAtlasPolynomialRepresentation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Constructed coordinate representatives of the same global polynomial tensor. These are derived from the actual read/restore maps.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.cross_atlas_polynomial_representation line 33

Source documentation

Every correction chart reads the globally restored polynomial as a single finite polynomial in that chart's actual localized map.

theorem cross_atlas_polynomial_representation {n : B.centers → ℕ}
    (P : ∀ j : B.centers, Fin 3 → Fin (n j) → Expression)
    (hP : ∀ j k r, (P j k r).SmoothCoeffs univ) (i : A.centers) :
    ∃ Q : Fin 3 → Fin (polynomialFamilyDegree n) → Expression,
      (∀ k r, (Q k r).SmoothCoeffs univ) ∧
      ∀ (F : M → Space), ContMDiff planeModel spaceModel ∞ F →
        ∀ (x : Base), A.chartWeight i x ≠ 0 → ∀ ε : ℝ,
          coordinatePolynomialValue Q ε (A.jetChartMap i F) 0 (JetPolynomial.planeCoordinateIsometry x) =
            A.tensorChartRead i (B.atlasPolynomialValue P ε F) x := by
…

Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.JetPolynomial.planeCoordinateIsometry