AtlasPrimitiveUpdate.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Propagation of the actual slow-map norms and normalized polynomial error through one primitive increment.

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.weighted_increment_unscaled line 20

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.polynomial_increment_propagation line 31

Source documentation

The output bounds concern the map that is actually added, and the normalized defect of its actual polynomial metric.

theorem polynomial_increment_propagation {n : A.centers → ℕ}
    {Pol : ∀ i : A.centers, Fin 3 → Fin (n i) → Expression}
    (hPol : ∀ i k l, (Pol i k l).SmoothCoeffs univ)
    {γ : ∀ x : M, CovariantTwoTensor x}
    (hγ : ContMDiff planeModel (planeModel.prod 𝓘(ℝ,TensorFiber)) ∞
      (fun x => TotalSpace.mk' TensorFiber x (γ x)))
    {F G X : M → Space} (hF : ContMDiff planeModel spaceModel ∞ F)
    (hG : ContMDiff planeModel spaceModel ∞ G) (hX : ContMDiff planeModel spaceModel ∞ X)
    {s τ δ δ' ε c : ℝ} (hs : 0 < s) (hτ : 0 < τ) (hτs : τ ≤ s) (hτ1 : τ ≤ 1)
    (hδ : 0 < δ) (hδ' : 0 < δ')
    (P B E : ℕ → ℝ) (hP : ∀ m, 0 ≤ P m) (hB : ∀ m, 0 ≤ B m)
    (hclose : A.WeightedBound 1 2 c (G-F))
…

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