AtlasPrimitiveError.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Exact decomposition of a global primitive's metric defect into the solved polynomial mean error and the finite periodic remainder.

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.periodicAtlasAnsatz_defect line 29

Source documentation

All terms refer to the same local ansatz and its actual global extension.

lemma periodicAtlasAnsatz_defect (i : A.centers) {F : M → Space}
    (hF : ContMDiff planeModel spaceModel ∞ F)
    {O : TopologicalSpace.Opens JetPolynomial.Base} (U : ℕ → Family O Space)
    {K : Set JetPolynomial.Base} (hK : IsClosed K) (hKO : K ⊆ O)
    (hKA : K ⊆ (A.chartWeightCompact i : Set JetPolynomial.Base))
    (hzero : ∀ j x, x ∉ K → (U j).val x = 0)
    (ℓ : JetPolynomial.Base →L[ℝ] ℝ) (L : ℕ) (z : ℝ)
    {n : ℕ} (P : Fin 3 → Fin n → Expression)
    (γ : ∀ x : M, CovariantTwoTensor x) (H : SmallModes.Base → PhaseMean.Tensor) :
    inducedTensor (A.periodicAtlasAnsatz i F U ℓ L z)-
        (γ+A.bundleRestore A.tensorTriv i (fun y => fiberFromThree (H (planeCoordinateIsometry y)))) =
      (A.atlasPolynomialMetric (A.primitiveAtlasPolynomial i P) z F-γ)+
…

Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CovariantTwoTensor, OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.PhaseMean.Tensor, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.inducedTensor, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.fiberFromThree