PolynomialInitialCorrection.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Initial exact correction from the finite power bounds in the manuscript.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.exact_correction_from_polynomial_initial_data line 30

Source documentation

The first correction block for a power-controlled input family. The geometric threshold and radii remain explicit; all finite jet and metric smallness conditions are discharged here by the prescribed powers of z.

theorem exact_correction_from_polynomial_initial_data
    {μ N C D e : ℝ} (hμ : 1 < μ) (hN : 20*μ < N)
    (hC : 0 ≤ C) (hD : 0 ≤ D) (he : 0 < e) :
    ∃ η : ℝ, 0 < η ∧ η ≤ 1/32 ∧ ∀ z : ℝ, 0 < z → z < η →
    ∀ (F : M → Space) (_hF : ContMDiff planeModel spaceModel ∞ F)
      (d : CorrectionGeometry g F) (c : PreparedCorrection d),
      z^μ < c.ε 0 → 1/z^4 ≤ c.budget → z^4 ≤ c.ρ → 8*e ≤ c.a →
      d.A.ShiftedBound 2 440 z (C/z^2) F →
      d.A.TensorWeightedBound 1 440 D g.inner →
      d.A.TensorWeightedBound 1 440 (C*z^N) (inducedTensor F-g.inner) →
      ∃ G : M → Space, IsSmoothIsometricImmersion M g G ∧
        d.A.WeightedBound 1 2 (z^4/8+2*c.ρ*z^μ) (G-F) := by
…

Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.CorrectionGeometry, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.inducedTensor, OAI.ClosedSurfaceR4.IsSmoothIsometricImmersion