AtlasPolynomialFreeSplit.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The global finite phase expansion has the prescribed quadratic mean.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlas_free_full_polynomial_split line 36

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.polynomial_modes_free_forced_increment line 78

Source documentation

Exact error decomposition before estimating the mixed and cubic terms.

theorem polynomial_modes_free_forced_increment {n : A.centers → ℕ} {m : ℕ}
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    (P : ∀ j : A.centers, Fin 3 → Fin (n j) → Expression)
    (Q : A.centers → Fin 3 → Fin m → Expression)
    (hQ : ∀ i k l, (Q i k l).SmoothCoeffs univ)
    (hrep : A.PolynomialQuadraticRepresentation P Q)
    (F V : M → Space) (hF : ContMDiff planeModel spaceModel ∞ F)
    (hV : ContMDiff planeModel spaceModel ∞ V) (ε τ : ℝ)
    (φ : ι → M → ℝ) (Z : ι → M → Fin 4 → ℂ)
    (hφ : ∀ j, ContMDiff planeModel 𝓘(ℝ) ∞ (φ j))
    (hZ : ∀ j, ContMDiff planeModel 𝓘(ℝ,Fin 4 → ℂ) ∞ (Z j))
    (T : ∀ p : M, CovariantTwoTensor p) :
…

Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CovariantTwoTensor