OAI/Geometry/SurfaceImmersion/Correction/OrderwiseCorrectionLimit.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Smooth correction limits with a separate summable bound at each derivative order.

  1. theorem OAI.ClosedSurfaceR4.ExactCorrection.smooth_limitMap_orderwise line 15
  2. theorem OAI.ClosedSurfaceR4.ExactCorrection.hasFDerivAt_limitMap_orderwise line 26
  3. theorem OAI.ClosedSurfaceR4.ExactCorrection.tendsto_fderiv_partialMap_orderwise line 54
  4. lemma OAI.ClosedSurfaceR4.ExactCorrection.local_coordinate_representative_derivative line 82

    Source documentation

    A representative in any smooth local coordinate map determines the actual manifold derivative, with the fixed coordinate derivative as the right factor.

    lemma local_coordinate_representative_derivative
    {c : M β†’ E} {G : M β†’ Space} {K : E β†’ Space} (p : M)
    (hc : ContMDiffAt planeModel π“˜(ℝ,E) ∞ c p) (hK : ContDiff ℝ ∞ K)
    (heq : G =αΆ [𝓝 p] K ∘ c) :
    ContMDiffAt planeModel spaceModel ∞ G p ∧
      mfderiv planeModel spaceModel G p =
        (fderiv ℝ K (c p)).comp (mfderiv planeModel π“˜(ℝ,E) c p) := by
…

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

  5. theorem OAI.ClosedSurfaceR4.ExactCorrection.local_coordinate_correction_limit line 103

    Source documentation

    Local coordinate representatives with order-dependent summable tails give smoothness of the series and convergence of the true manifold derivatives.

    theorem local_coordinate_correction_limit
    {F : M β†’ Space} {U : β„• β†’ M β†’ Space} {c : M β†’ E}
    {K : E β†’ Space} {A : β„• β†’ E β†’ Space} {ρ : β„• β†’ β„• β†’ ℝ} (p : M)
    (hc : ContMDiffAt planeModel π“˜(ℝ,E) ∞ c p)
    (hK : ContDiff ℝ ∞ K) (hA : βˆ€ n, ContDiff ℝ ∞ (A n))
    (hρ : βˆ€ m, Summable (ρ m))
    (hbound : βˆ€ m : β„•, βˆ€αΆ  n in atTop,
      βˆ€ x, β€–iteratedFDeriv ℝ m (A n) xβ€– ≀ ρ m n)
    (heq : βˆ€αΆ  x in 𝓝 p, F x = K (c x) ∧ βˆ€ n, U n x = A n (c x)) :
    ContMDiffAt planeModel spaceModel ∞ (manifoldLimitMap F U) p ∧
      Tendsto (fun N => mfderiv planeModel spaceModel (manifoldPartialMap F U N) p) atTop
        (𝓝 (mfderiv planeModel spaceModel (manifoldLimitMap F U) p)) := by
…

    Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.ExactCorrection.manifoldLimitMap, OAI.ClosedSurfaceR4.ExactCorrection.manifoldPartialMap