Estimator.improveUntilAux_spec
theorem Estimator.improveUntilAux_spec :
∀ {α : Type u_2} [inst : Preorder α] {ε : Type u_1} (a : Thunk α) (p : α → Bool) [inst_1 : Estimator a ε]
[inst_2 : WellFoundedGT ↑(Set.range (EstimatorData.bound a))] (e : ε) (r : Bool),
match Estimator.improveUntilAux a p e r with
| Except.error a_1 => ¬p a.get = true
| Except.ok e' => p (EstimatorData.bound a e') = true
This theorem, `Estimator.improveUntilAux_spec`, states that for any types `α` (with a preorder structure) and `ε`, for any thunk `a` of type `α`, for any predicate `p` on type `α` that maps to a boolean, any estimator `inst_1` of `a` of type `ε`, any well-founded ordering `inst_2` on the range of the bound function of the estimator data of `a`, any value `e` of type `ε`, and any boolean `r`, the function `Estimator.improveUntilAux a p e r` behaves in the following way:
If `Estimator.improveUntilAux a p e r` returns an exception with some error `a_1`, then the predicate `p` applied to the get method of `a` is not true. On the other hand, if `Estimator.improveUntilAux a p e r` returns successfully with some value `e'`, then the predicate `p` applied to the bound of `a` at `e'` is true.
In other words, if the `improveUntilAux` function of the estimator is successful, it guarantees that the bound value of the estimator data for `a` at the returned value satisfies the predicate. If it fails, then the predicate does not hold for the thunk value of `a`.
More concisely: If `Estimator.improveUntilAux a p e r` successfully returns a value `e'` with predicate `p(a.get e')` holding true, then the predicate `p(a.get e)` would have held true for any input `e` that `Estimator.improveUntilAux` considered prior to returning `e'`.
|
Estimator.improveUntil_spec
theorem Estimator.improveUntil_spec :
∀ {α : Type u_2} [inst : Preorder α] {ε : Type u_1} (a : Thunk α) (p : α → Bool) [inst_1 : Estimator a ε]
[inst_2 : WellFoundedGT ↑(Set.range (EstimatorData.bound a))] (e : ε),
match Estimator.improveUntil a p e with
| Except.error a_1 => ¬p a.get = true
| Except.ok e' => p (EstimatorData.bound a e') = true
The theorem `Estimator.improveUntil_spec` states that for any types `α` and `ε`, where `α` is preordered, a thunk `a` of type `α`, a predicate `p` on `α`, and `ε` value `e`, such that `Estimator a ε` and `WellFoundedGT ↑(Set.range (EstimatorData.bound a))` instances exist. If the function `Estimator.improveUntil a p e` returns `some e'`, then the `EstimatorData.bound a e'` should satisfy the predicate `p`. However, if it does not return `some e'`, then the value `a` must not satisfy the predicate `p`.
More concisely: If `Estimator.improveUntil` on a preordered type `α` with thunk `a`, predicate `p`, and value `e` terminates with an improved value `e'`, then `EstimatorData.bound a e'` satisfies `p`. Otherwise, `a` does not satisfy `p`.
|
Estimator.improve_spec
theorem Estimator.improve_spec :
∀ {α : Type u_2} [inst : Preorder α] {a : Thunk α} {ε : Type u_1} [self : Estimator a ε] (e : ε),
match EstimatorData.improve a e with
| none => EstimatorData.bound a e = a.get
| some e' => EstimatorData.bound a e < EstimatorData.bound a e'
The theorem `Estimator.improve_spec` states that for any types `α` (with a `Preorder` structure) and `ε`, and for any objects `a` of type `Thunk α` and `e` of type `ε`, when the `improve` function of `EstimatorData` is called with inputs `a` and `e`, it returns either `none` or `some e'`. If it returns `none`, then the `bound` of `a` with respect to `e` is exactly the value obtained from `a`. If it returns `some e'`, then the `bound` of `a` with respect to `e` is strictly less than the `bound` of `a` with respect to `e'`.
In other words, calling `improve` gives either a strictly better bound (the case when `some e'` is returned and the bound with respect to `e'` is higher than the bound with respect to `e`), or a proof that the current bound is exact (the case when `none` is returned and the bound equals to the value obtained from `a`).
More concisely: For any type `α` with a `Preorder` structure, given `α` object `a`, `Thunk α` value `e`, and `EstimatorData`'s `improve` function output `none` or `some e'`, if `none` then the bound of `a` with respect to `e` is exact, otherwise the bound of `a` with respect to `e'` strictly improves the bound of `a` with respect to `e`.
|
Estimator.bound_le
theorem Estimator.bound_le :
∀ {α : Type u_2} [inst : Preorder α] {a : Thunk α} {ε : Type u_1} [self : Estimator a ε] (e : ε),
EstimatorData.bound a e ≤ a.get
The theorem `Estimator.bound_le` asserts that for all types `α` (where `α` has a preorder), for a thunk `a` of type `α`, and for all types `ε`, if `a` has an associated estimator `ε`, then for any element `e` of type `ε`, the calculated bound (`EstimatorData.bound a e`) is always less than or equal to the actual value of `a` (`a.get`). In simpler terms, this theorem guarantees that any estimated bounds produced by the `EstimatorData.bound` function will never exceed the true value they're estimating.
More concisely: For all types `α` with a preorder, and for any `α` value `a` with an estimator `ε` and an `ε` value `e`, the estimated bound `EstimatorData.bound a e` is less than or equal to the actual value `a.get`.
|