improveUntilAux — Mathlib

English

Given an estimator a on α, a predicate p, and a bound, improveUntilAux refines an estimate e until p(bound(a,e)) holds, possibly returning an error or a new estimate.

Русский

Дано оцениватель a на α, предикат p и ограничение bound; improveUntilAux уточняет оценку e до тех пор, пока p(bound(a,e)) выполняется, либо возвращает ошибку, либо новую оценку.

LaTeX

$$$\text{improveUntilAux}(a,p,e,r) = \begin{cases} \text{Ok}(e) & p(\text{bound}(a,e)) \\ \\ \text{Error}(\text{None} \text{ or } \text{Some } e) & \text{при отсутствии продолжения} \\ \text{improveUntilAux}(a,p,e',\text{true}) & \text{если } \text{improve}(a,e) = \text{Some } e' \end{cases}$$$

Lean4

/-- Implementation of `Estimator.improveUntil`. -/
def improveUntilAux (a : Thunk α) (p : α → Bool) [Estimator a ε] [WellFoundedGT (range (bound a : ε → α))] (e : ε)
    (r : Bool) : Except (Option ε) ε :=
  if p (bound a e) then return e
  else
    match improve a e, improve_spec e with
    | none, _ => .error <| if r then none else e
    | some e', _ => improveUntilAux a p e' true
termination_by (⟨_, mem_range_self e⟩ : range (bound a))

Похожие утверждения