CorrectionErrorEnvelope.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The six normalized errors satisfy the common all-order recurrence bound.

theorem OAI.ClosedSurfaceR4.ExactCorrection.normalized_error_envelope line 12

Source documentation

A common envelope for the six powers in the exact-correction error table. The coefficients of both high-derivative terms remain linear.

theorem normalized_error_envelope {t k B C P Q R : ℝ}
    (ht : 0 < t) (ht1 : t ≤ 1) (hk : 10 ≤ k)
    (hB : 0 ≤ B) (hC : 0 ≤ C) (hP : 0 ≤ P) (hQ : 0 ≤ Q) (hR : 0 ≤ R) :
    P * (B * t ^ ((18 * k + 8) / 5) + C * t ^ ((38 * k + 28) / 5)) +
      Q * (t ^ ((13 * k + 8) / 5) + t ^ ((3 * k - 18) / 5)) +
      R * (B * t ^ ((13 * k + 8) / 5) + C * t ^ ((33 * k + 28) / 5)) ≤
      (P + 2 * Q + R) * (1 + B + C) * t ^ (1 / 5 : ℝ) := by
…