InitialLocalCorrection.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Local finite-accuracy criterion for an actual exact correction.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData.local_exact_correction line 29
Source documentation
A finite order metric-accuracy criterion, with all constants chosen before the smoothing scale. The resulting isometric map stays in the prescribed geometric neighborhood of the reference immersion.
```
theorem local_exact_correction (d : MetricGoodPhaseData g F)
    (hF : ContMDiff planeModel spaceModel ∞ F) :
    ∃ c : PreparedCorrection d.toCorrectionGeometry, ∃ e ε : ℝ, 0 < e ∧ 0 < ε ∧ ε ≤ 1/32 ∧
    ∀ t : ℝ, 0 < t → t < ε →
      d.A.TensorWeightedBound t 440 ((t^(10 : ℝ))^2*e) (inducedTensor F-g.inner) →
      ∃ G : M → Space, IsSmoothIsometricImmersion M g G ∧
        d.A.WeightedBound 1 2 (c.ρ/4) (G-F) := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.inducedTensor, OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.IsSmoothIsometricImmersion