AdaptiveExactCorrection.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The adaptive construction produces a smooth isometric immersion from admissible finite initial data by choosing a correction sequence.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.sequence_limit_isometric line 30
Source documentation
Construction, growth of derivative order, and passage to the actual metric limit are combined here. Only finite initial input data remain.
```
theorem sequence_limit_isometric (c : PreparedCorrection d)
    (hF : ContMDiff planeModel spaceModel ∞ F) {t : ℝ} (ht : 0 < t) (htsmall : t ≤ 1/32)
    (seed : c.Stage t 0) : IsSmoothIsometricImmersion M g
      (manifoldLimitMap seed.map (c.increment hF ht htsmall seed)) := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.IsSmoothIsometricImmersion
theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.exists_isometric_of_stage line 52

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData.finite_input_exact_correction line 71

Source documentation

Finite quantitative initial conditions suffice for an exact smooth correction. The derivative order is exactly the initial order 440, and all later higher norms are dealt with by the constructed adaptive sequence.

theorem finite_input_exact_correction (d : MetricGoodPhaseData g F)
    (hF : ContMDiff planeModel spaceModel ∞ F) :
    ∃ a ρ B ε : ℝ, 0 < a ∧ 0 < ρ ∧ 0 < B ∧ 0 < ε ∧ ε ≤ 1/32 ∧
    ∀ (t : ℝ), 0 < t → t < ε → ∀ G : M → Space,
    ContMDiff planeModel spaceModel ∞ G →
    d.A.InputBound t 440 B G (normalizedTensorDefect g.inner (t^(10 : ℝ)) G) →
    d.A.WeightedBound 1 2 (ρ/8) (G-F) →
    (∀ x, ‖d.A.tensorEncode (normalizedTensorDefect g.inner (t^(10 : ℝ)) G) x-
      d.A.tensorEncode g.inner x‖ ≤ a/8) →
    ∃ G' : M → Space, IsSmoothIsometricImmersion M g G' := by
…

Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.normalizedTensorDefect, OAI.ClosedSurfaceR4.IsSmoothIsometricImmersion