ExactCorrectionLimit.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Passing the correction sequence to a smooth isometric limit

A correction sequence with eventually summable bounds at every derivative order converges smoothly in coordinate space. Convergence of its pullback metrics then gives an isometric immersion whenever the limiting metric is positive definite.

def OAI.ClosedSurfaceR4.ExactCorrection.partialMap line 27
Source documentation
Finite-stage maps, with the initial map kept separate from the corrections.
```
def partialMap (F : E → V) (U : ℕ → E → V) (N : ℕ) (x : E) : V :=
…
```
def OAI.ClosedSurfaceR4.ExactCorrection.limitMap line 31
Source documentation
The limit map defined by the convergent correction series.
```
def limitMap (F : E → V) (U : ℕ → E → V) (x : E) : V :=
…
```

theorem OAI.ClosedSurfaceR4.ExactCorrection.smooth_limitMap line 36

Source documentation

Each derivative order only needs a summable bound after a finite waiting period. This is why the initial, uncontrolled high derivatives cause no problem.

theorem smooth_limitMap {F : E → V} {U : ℕ → E → V} {ρ : ℕ → ℝ}
    (hF : ContDiff ℝ ∞ F) (hU : ∀ n, ContDiff ℝ ∞ (U n)) (hρ : Summable ρ)
    (hbound : ∀ m : ℕ, ∀ᶠ n in atTop,
      ∀ x, ‖iteratedFDeriv ℝ m (U n) x‖ ≤ ρ n) :
    ContDiff ℝ ∞ (limitMap F U) := by
…

Mentions: OAI.ClosedSurfaceR4.ExactCorrection.limitMap

theorem OAI.ClosedSurfaceR4.ExactCorrection.hasFDerivAt_limitMap line 48

Source documentation

Derivatives of the sum are the sums of the derivatives even though their uniform bound is only eventually available.

theorem hasFDerivAt_limitMap {F : E → V} {U : ℕ → E → V} {ρ : ℕ → ℝ}
    (hF : ContDiff ℝ ∞ F) (hU : ∀ n, ContDiff ℝ ∞ (U n)) (hρ : Summable ρ)
    (hbound : ∀ m : ℕ, ∀ᶠ n in atTop,
      ∀ x, ‖iteratedFDeriv ℝ m (U n) x‖ ≤ ρ n) (x : E) :
    HasFDerivAt (limitMap F U)
      (fderiv ℝ F x + ∑' n, fderiv ℝ (U n) x) x := by
…

Mentions: OAI.ClosedSurfaceR4.ExactCorrection.limitMap

theorem OAI.ClosedSurfaceR4.ExactCorrection.tendsto_fderiv_partialMap line 75

Source documentation

The finite-stage differential converges in operator norm.

theorem tendsto_fderiv_partialMap {F : E → V} {U : ℕ → E → V} {ρ : ℕ → ℝ}
    (hF : ContDiff ℝ ∞ F) (hU : ∀ n, ContDiff ℝ ∞ (U n)) (hρ : Summable ρ)
    (hbound : ∀ m : ℕ, ∀ᶠ n in atTop,
      ∀ x, ‖iteratedFDeriv ℝ m (U n) x‖ ≤ ρ n) (x : E) :
    Tendsto (fun N => fderiv ℝ (partialMap F U N) x) atTop
      (𝓝 (fderiv ℝ (limitMap F U) x)) := by
…

Mentions: OAI.ClosedSurfaceR4.ExactCorrection.partialMap, OAI.ClosedSurfaceR4.ExactCorrection.limitMap

theorem OAI.ClosedSurfaceR4.ExactCorrection.limitMap_metric line 97

Source documentation

The pullback metric is continuous under the differential convergence just proved, so a vanishing metric defect gives the exact desired metric.

theorem limitMap_metric {F : E → V} {U : ℕ → E → V} {ρ : ℕ → ℝ}
    (hF : ContDiff ℝ ∞ F) (hU : ∀ n, ContDiff ℝ ∞ (U n)) (hρ : Summable ρ)
    (hbound : ∀ m : ℕ, ∀ᶠ n in atTop,
      ∀ x, ‖iteratedFDeriv ℝ m (U n) x‖ ≤ ρ n)
    (g : E → E → E → ℝ)
    (hmetric : ∀ x v w, Tendsto
      (fun N => inner ℝ (fderiv ℝ (partialMap F U N) x v)
        (fderiv ℝ (partialMap F U N) x w)) atTop (𝓝 (g x v w))) :
    ∀ x v w, inner ℝ (fderiv ℝ (limitMap F U) x v)
      (fderiv ℝ (limitMap F U) x w) = g x v w := by
…

Mentions: OAI.ClosedSurfaceR4.ExactCorrection.partialMap, OAI.ClosedSurfaceR4.ExactCorrection.limitMap

theorem OAI.ClosedSurfaceR4.ExactCorrection.limitMap_metric_of_error_bound line 116

Source documentation

Quantitative metric defects tending to zero imply the metric convergence needed above. The bound is the bilinear operator-norm form of the residual estimate produced by the correction iteration.

theorem limitMap_metric_of_error_bound
    {F : E → V} {U : ℕ → E → V} {ρ ε : ℕ → ℝ}
    (hF : ContDiff ℝ ∞ F) (hU : ∀ n, ContDiff ℝ ∞ (U n)) (hρ : Summable ρ)
    (hbound : ∀ m : ℕ, ∀ᶠ n in atTop,
      ∀ x, ‖iteratedFDeriv ℝ m (U n) x‖ ≤ ρ n)
    (g : E → E → E → ℝ) (hε : Tendsto ε atTop (𝓝 0))
    (herror : ∀ n x v w,
      |inner ℝ (fderiv ℝ (partialMap F U n) x v)
        (fderiv ℝ (partialMap F U n) x w) - g x v w| ≤ ε n * ‖v‖ * ‖w‖) :
    ∀ x v w, inner ℝ (fderiv ℝ (limitMap F U) x v)
      (fderiv ℝ (limitMap F U) x w) = g x v w := by
…

Mentions: OAI.ClosedSurfaceR4.ExactCorrection.partialMap, OAI.ClosedSurfaceR4.ExactCorrection.limitMap

theorem OAI.ClosedSurfaceR4.ExactCorrection.limitMap_immersion line 137

Source documentation

Positive definiteness supplies injectivity; no separate rank estimate is needed after the metric has passed to the limit.

theorem limitMap_immersion {F : E → V} {U : ℕ → E → V} {ρ : ℕ → ℝ}
    (hF : ContDiff ℝ ∞ F) (hU : ∀ n, ContDiff ℝ ∞ (U n)) (hρ : Summable ρ)
    (hbound : ∀ m : ℕ, ∀ᶠ n in atTop,
      ∀ x, ‖iteratedFDeriv ℝ m (U n) x‖ ≤ ρ n)
    (g : E → E → E → ℝ)
    (hmetric : ∀ x v w, Tendsto
      (fun N => inner ℝ (fderiv ℝ (partialMap F U N) x v)
        (fderiv ℝ (partialMap F U N) x w)) atTop (𝓝 (g x v w)))
    (hpos : ∀ x v, v ≠ 0 → 0 < g x v v) :
    ContDiff ℝ ∞ (limitMap F U) ∧
      ∀ x, Function.Injective (fderiv ℝ (limitMap F U) x) := by
…

Mentions: OAI.ClosedSurfaceR4.ExactCorrection.partialMap, OAI.ClosedSurfaceR4.ExactCorrection.limitMap