CompactGeometryPolynomialIncrement.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Finite mean adjustment gives a small increment uniformly over nearby input maps.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.compact_geometry_polynomial_increment line 30

Source documentation

Compact good phase geometry yields the actual small increment; no mean data or linear solver is an input.

theorem compact_geometry_polynomial_increment
    {n : A.centers → ℕ}
    (Pol : ∀ i : A.centers, Fin 3 → Fin (n i) → Expression)
    (hPol : ∀ i k l, (Pol i k l).SmoothCoeffs univ)
    (F : M → Space) (hF : ContMDiff planeModel spaceModel ∞ F)
    (Q : A.centers → PhaseBasis) (w : A.centers → Fin 3 → ℝ)
    (hw : ∀ i j, w i j ≠ 0)
    (hImm : ∀ i x, x ∈ (modeSupport (A.chartWeightCompact i) : Set SmallModes.Base) →
      Function.Injective (fderiv ℝ (spaceCoordinates ∘ A.vectorPlaneRead i F) x))
    (hgood : ∀ i j x, x ∈ (modeSupport (A.chartWeightCompact i) : Set SmallModes.Base) →
      Good (RealModes.realSecondTensor (spaceCoordinates ∘ A.vectorPlaneRead i F) x) ((Q i).ξ j))
    (reference : ∀ x : M, CovariantTwoTensor x)
…

Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.spaceCoordinates, OAI.ClosedSurfaceR4.RealModes.realSecondTensor, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CovariantTwoTensor