ExactCorrectionRecurrence.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Scalar estimates for the smooth correction iteration

The scalar recurrence used in exact-correction.tex, subsection "Initialization and passage through the derivative orders", is treated here. These are estimates for that iteration, not an isometric immersion existence theorem.

theorem OAI.ClosedSurfaceR4.ExactCorrection.affine_tail_bound line 20

Source documentation

A tail of a subsolution is dominated by the corresponding affine recurrence.

theorem affine_tail_bound {x : ℕ → ℝ} {a b : ℝ} (ha : 0 ≤ a) (N : ℕ)
    (hstep : ∀ n, N ≤ n → x (n + 1) ≤ a * x n + b) (j : ℕ) :
    x (N + j) ≤ arithGeom a b (x N) j := by
…

theorem OAI.ClosedSurfaceR4.ExactCorrection.eventually_lt_of_affine_tail line 33

Source documentation

An affine subsolution with contraction coefficient eventually lies below any strict upper bound for the fixed point.

theorem eventually_lt_of_affine_tail {x : ℕ → ℝ} {a b L : ℝ}
    (ha : 0 ≤ a) (ha1 : a < 1) (hL : b / (1 - a) < L) (N : ℕ)
    (hstep : ∀ n, N ≤ n → x (n + 1) ≤ a * x n + b) :
    ∀ᶠ n in atTop, x n < L := by
…

theorem OAI.ClosedSurfaceR4.ExactCorrection.eventually_lt_of_vanishing_recurrence line 48

Source documentation

The all-order recurrence from the manuscript eventually enters every strict upper neighborhood of its baseline. No initial bound on x is required.

theorem eventually_lt_of_vanishing_recurrence {x c : ℕ → ℝ} {A L : ℝ}
    (hx : ∀ n, 0 ≤ x n) (hA : 0 ≤ A)
    (hc : Tendsto c atTop (𝓝 0))
    (hstep : ∀ n, x (n + 1) ≤ A + c n * (1 + x n)) (hAL : A < L) :
    ∀ᶠ n in atTop, x n < L := by
…

theorem OAI.ClosedSurfaceR4.ExactCorrection.eventually_below_budget line 80
Source documentation
In particular, each fixed derivative order reaches the next block's budget after finitely many steps, as asserted in the exact-correction proof.
```
theorem eventually_below_budget {x c : ℕ → ℝ} {B : ℝ}
    (hB : 0 < B) (hx : ∀ n, 0 ≤ x n) (hc : Tendsto c atTop (𝓝 0))
    (hstep : ∀ n, x (n + 1) ≤ B / 4 + c n * (1 + x n)) :
    ∀ᶠ n in atTop, x n < B :=
…
```

theorem OAI.ClosedSurfaceR4.ExactCorrection.error_exponents_pos line 88

Source documentation

All six exponents in the exact-correction error table are positive at and after the initial block k = 10.

theorem error_exponents_pos {k : ℝ} (hk : 10 ≤ k) :
    0 < (13 * k + 8) / 5 ∧
    0 < (3 * k - 18) / 5 ∧
    0 < (18 * k + 8) / 5 ∧
    0 < (38 * k + 28) / 5 ∧
    0 < (13 * k + 8) / 5 ∧
    0 < (33 * k + 28) / 5 := by
…