ManifoldCorrectionLimit.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The correction-series limit on the surface

The bounds are imposed on smooth coordinate representatives on a fixed neighborhood of each point. They may depend on the chart, and are only eventual in the correction index for each derivative order.

def OAI.ClosedSurfaceR4.ExactCorrection.manifoldPartialMap line 24
def OAI.ClosedSurfaceR4.ExactCorrection.manifoldLimitMap line 27

lemma OAI.ClosedSurfaceR4.ExactCorrection.local_representative_derivative line 32

Source documentation

A smooth local representative gives both smoothness and the manifold derivative at the center of its chart.

lemma local_representative_derivative {F : M → Space} {K : Plane → Space} (p : M)
    (hK : ContDiff ℝ ∞ K)
    (heq : F =ᶠ[𝓝 p] K ∘ extChartAt planeModel p) :
    ContMDiffAt planeModel spaceModel ∞ F p ∧
      mfderiv planeModel spaceModel F p =
        fderiv ℝ K (extChartAt planeModel p p) := by
…

Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.Plane, OAI.ClosedSurfaceR4.planeModel

theorem OAI.ClosedSurfaceR4.ExactCorrection.manifold_correction_limit line 54

Source documentation

Chartwise summable correction bounds give a smooth limit and convergence of the actual manifold derivatives of its finite stages.

theorem manifold_correction_limit
    {F : M → Space} {U : ℕ → M → Space}
    (K : M → Plane → Space) (A : M → ℕ → Plane → Space)
    (ρ : M → ℕ → ℝ)
    (hK : ∀ p, ContDiff ℝ ∞ (K p))
    (hA : ∀ p n, ContDiff ℝ ∞ (A p n))
    (hρ : ∀ p, Summable (ρ p))
    (hbound : ∀ p m, ∀ᶠ n in atTop,
      ∀ x, ‖iteratedFDeriv ℝ m (A p n) x‖ ≤ ρ p n)
    (heq : ∀ p, ∀ᶠ x in 𝓝 p,
      F x = K p (extChartAt planeModel p x) ∧
      ∀ n, U n x = A p n (extChartAt planeModel p x)) :
…

Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.Plane, OAI.ClosedSurfaceR4.planeModel

theorem OAI.ClosedSurfaceR4.ExactCorrection.manifold_limit_isometric line 94

Source documentation

Once the constructed finite stages have vanishing metric defect, the chartwise correction estimates produce an isometric immersion of the surface. The existence of such corrections is a separate construction.

theorem manifold_limit_isometric
    {F : M → Space} {U : ℕ → M → Space}
    (K : M → Plane → Space) (A : M → ℕ → Plane → Space)
    (ρ : M → ℕ → ℝ)
    (hK : ∀ p, ContDiff ℝ ∞ (K p))
    (hA : ∀ p n, ContDiff ℝ ∞ (A p n))
    (hρ : ∀ p, Summable (ρ p))
    (hbound : ∀ p m, ∀ᶠ n in atTop,
      ∀ x, ‖iteratedFDeriv ℝ m (A p n) x‖ ≤ ρ p n)
    (heq : ∀ p, ∀ᶠ x in 𝓝 p,
      F x = K p (extChartAt planeModel p x) ∧
      ∀ n, U n x = A p n (extChartAt planeModel p x))
…

Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.Plane, OAI.ClosedSurfaceR4.planeModel