Refinement with separate degree and precision

A wider grid reduces rounding error; more series terms reduce truncation error. Increasing only the degree can therefore leave an enclosure straddling the same rounding boundary indefinitely.

After a failed check, the search tries twice the degree and one extra working bit. If the interval width then shrinks by at most a factor of four, the next attempt doubles the working precision instead. The degree stays fixed for that attempt. This is a work-selection heuristic: acceptance always uses the supplied checker, and the witness theorem below does not assume convergence.

@[specialize #[]]

def FloatLib.Numerics.RationalInterval.Internal.refine {α : Type} (enclose : ℕ → ℕ → RationalInterval) (check : RationalInterval → Option α) (degree precision : ℕ) (previousWidth : Option ℚ) : ℕ → Option α

Remember the previous failed width when choosing the next refinement step.

@[specialize #[]]

def FloatLib.Numerics.RationalInterval.refine {α : Type} (enclose : ℕ → ℕ → RationalInterval) (check : RationalInterval → Option α) (degree precision steps : ℕ) : Option α

Try at most steps enclosures, increasing degree or precision according to the observed width.

The first attempt uses the supplied degree and precision exactly. A successful check returns immediately; an exhausted budget returns none.

@[simp]

theorem FloatLib.Numerics.RationalInterval.refine_zero {α : Type} (enclose : ℕ → ℕ → RationalInterval) (check : RationalInterval → Option α) (degree precision : ℕ) : refine enclose check degree precision 0 = none

theorem FloatLib.Numerics.RationalInterval.exists_of_refine_eq_some {α : Type} {enclose : ℕ → ℕ → RationalInterval} {check : RationalInterval → Option α} {degree precision steps : ℕ} {result : α} (hresult : refine enclose check degree precision steps = some result) : ∃ (degree : ℕ) (precision : ℕ), check (enclose degree precision) = some result

Every returned value was accepted from an enclosure at an actual degree and precision.