AtlasPolynomialNearbyCancellation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Atlas cancellation uniform over a neighborhood of a fixed immersion. The reference geometry, per-chart shifted profiles and finite phase family determine all constants before the varying map, target or scale is chosen.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlas_polynomial_nearby_cancellation_all_profiles line 44

Source documentation

Fixed good-phase geometry gives uniform global cancellation for nearby maps with the specified shifted derivative profiles at the actual slow scale.

theorem atlas_polynomial_nearby_cancellation_all_profiles
    {ι : A.centers → Type*} [∀ i, Fintype (ι i)]
    {n : A.centers → ℕ} {nq : ℕ}
    (P : ∀ i : A.centers, Fin 3 → Fin (n i) → Expression)
    (Q : A.centers → Fin 3 → Fin nq → Expression)
    (hQ : ∀ i k l, (Q i k l).SmoothCoeffs univ)
    (hrepr : A.PolynomialLinearRepresentation P Q)
    (F : M → Space) (hF : ContMDiff planeModel spaceModel ∞ F)
    (φ : (i : A.centers) → ι i → JetPolynomial.Base → ℝ)
    (hφ : ∀ i j, ContDiff ℝ ∞ (φ i j))
    (K : (i : A.centers) → ι i → TopologicalSpace.Compacts JetPolynomial.Base)
    (hK : ∀ i j, (modeSupport (K i j) : Set SmallModes.Base) ⊆
…

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