ExactCorrectionConvergence.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Convergence after the derivative orders have been scheduled

This combines the particular scales and increasing derivative budgets of the exact-correction iteration with the smooth-series limit argument. Constructing the increments with these bounds remains a separate step.

theorem OAI.ClosedSurfaceR4.ExactCorrection.eventual_increment_bound line 27

Source documentation

Increasing finite derivative budgets suffice: every fixed derivative order eventually has a summable bound.

theorem eventual_increment_bound {U : ℕ → E → V} {t ρ : ℝ} {k : ℕ → ℕ}
    (hk : Tendsto k atTop atTop)
    (hU : ∀ n m, m ≤ k n / 2 → ∀ x,
      ‖iteratedFDeriv ℝ m (U n) x‖ ≤ ρ * correctionScale t n) (m : ℕ) :
    ∀ᶠ n in atTop, ∀ x,
      ‖iteratedFDeriv ℝ m (U n) x‖ ≤ ρ * correctionScale t n := by
…

Mentions: OAI.ClosedSurfaceR4.ExactCorrection.correctionScale

theorem OAI.ClosedSurfaceR4.ExactCorrection.exact_limit_of_increment_bounds line 39

Source documentation

Quantitative conclusion of the last part of exact-correction.tex: the superlinear scale decay, increasing derivative orders, and bounded normalized defect imply a smooth exact isometric limit.

theorem exact_limit_of_increment_bounds
    {F : E → V} {U : ℕ → E → V} {t ρ C : ℝ} {k : ℕ → ℕ}
    (ht : 0 ≤ t) (htsmall : t ≤ 1 / 32) (hC : 0 ≤ C)
    (hF : ContDiff ℝ ∞ F) (hU : ∀ n, ContDiff ℝ ∞ (U n))
    (hk : Tendsto k atTop atTop) (hkpos : ∀ n, 1 ≤ k n)
    (hinc : ∀ n m, m ≤ k n / 2 → ∀ x,
      ‖iteratedFDeriv ℝ m (U n) x‖ ≤ ρ * correctionScale t n)
    (g : E → E → E → ℝ)
    (herror : ∀ n x v w,
      |inner ℝ (fderiv ℝ (partialMap F U n) x v)
        (fderiv ℝ (partialMap F U n) x w) - g x v w| ≤
          C * correctionScale t n ^ (2 * k n) * ‖v‖ * ‖w‖) :
…

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