AdaptiveOrderControl.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Scalar progress of an adaptive derivative order. No uniform control of all the higher input norms is required.

lemma OAI.ClosedSurfaceR4.ExactCorrection.eventually_lt_of_eventual_vanishing_recurrence line 13
lemma OAI.ClosedSurfaceR4.ExactCorrection.order_tendsto_of_no_constant_tail line 37

theorem OAI.ClosedSurfaceR4.ExactCorrection.adaptive_order_tendsto line 55

Source documentation

Holding one order forever is impossible: every fixed higher input norm contracts toward the baseline, so the rule must eventually advance.

theorem adaptive_order_tendsto
    {k : ℕ → ℕ} {x : ℕ → ℕ → ℝ} {t : ℕ → ℝ}
    {A B : ℝ} {N : ℕ → ℕ → ℝ} {ε : ℕ → ℝ} {r : ℕ → ℕ}
    (hA : 0 ≤ A) (hAB : A < B) (_hB : 0 < B)
    (hN : ∀ j m, 0 ≤ N j m) (hε : ∀ j, 0 < ε j)
    (ht : ∀ n, 0 < t n) (ht0 : Tendsto t atTop (𝓝 0))
    (hx : ∀ m n, 0 ≤ x m n)
    (hstep : ∀ m n, x m (n+1) ≤ A+N (k n) m*(t n)^(1/5 : ℝ)*(1+x m n))
    (hmono : Monotone k)
    (hadvance : ∀ n, t n < ε (k n+1) →
      A+N (k n) (r (k n+1))*(t n)^(1/5 : ℝ)*(1+x (r (k n+1)) n) ≤ B →
      k (n+1) = k n+1) : Tendsto k atTop atTop := by
…