# Documentation

Mathlib.Order.Estimator

# Improvable lower bounds. #

The typeclass Estimator a ε, where a : Thunk α and ε : Type, states that e : ε carries the data of a lower bound for a.get, in the form bound_le : bound a e ≤ a.get, along with a mechanism for asking for a better bound improve e : Option ε, satisfying

match improve e with
| none => bound e = a.get
| some e' => bound e < bound e'


i.e. it returns none if the current bound is already optimal, and otherwise a strictly better bound.

(The value in α is hidden inside a Thunk to prevent evaluating it: the point of this typeclass is to work with cheap-to-compute lower bounds for expensive values.)

An appropriate well-foundedness condition would then ensure that repeated improvements reach the exact value.

class EstimatorData {α : Type u_1} (a : ) (ε : Type u_2) :
Type (max u_1 u_2)
• bound : εα

The value of the bound for a representation by a term of ε.

• improve : ε

Generate an improved lower bound.

Given [EstimatorData a ε]

• a term e : ε can be interpreted via bound a e : α as a lower bound for a, and
• we can ask for an improved lower bound via improve a e : Option ε.

The value a in α that we are estimating is hidden inside a Thunk to avoid evaluation.

Instances
class Estimator {α : Type u_1} [] (a : ) (ε : Type u_2) extends :
Type (max u_1 u_2)
• bound : εα
• improve : ε
• bound_le : ∀ (e : ε),

The calculated bounds are always lower bounds.

• improve_spec : ∀ (e : ε), match with | none => | some e' =>

Calling improve either gives a strictly better bound, or a proof that the current bound is exact.

Given [Estimator a ε]

• we have bound a e ≤ a.get, and
• improve a e returns none iff bound a e = a.get, and otherwise it returns a strictly better bound.
Instances
instance instEstimatorPureSubtypeEq {α : Type u_1} [] (a : α) :
Estimator () { x // x = a }

A trivial estimator.

def Estimator.improveUntilAux {α : Type u_1} {ε : Type u_2} [] (a : ) (p : αBool) [] [] (e : ε) (r : Bool) :
Except () ε

Implementation of Estimator.improveUntil.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Estimator.improveUntil {α : Type u_1} {ε : Type u_2} [] (a : ) (p : αBool) [] [] (e : ε) :
Except () ε

Improve an estimate until it satisfies a predicate, or else return the best available estimate, if any improvement was made.

Instances For
theorem Estimator.improveUntilAux_spec {α : Type u_2} [] {ε : Type u_1} (a : ) (p : αBool) [] [] (e : ε) (r : Bool) :
match with | => ¬p () = true | => p () = true

If Estimator.improveUntil a p e returns some e', then bound a e' satisfies p. Otherwise, that value a must not satisfy p.

theorem Estimator.improveUntil_spec {α : Type u_2} [] {ε : Type u_1} (a : ) (p : αBool) [] [] (e : ε) :
match with | => ¬p () = true | => p () = true

If Estimator.improveUntil a p e returns some e', then bound a e' satisfies p. Otherwise, that value a must not satisfy p.

instance instWellFoundedGTElemRangeBoundToEstimatorDataToPreorderLtToLTMemSetInstMembershipSet {α : Type u_1} [] [∀ (a : α), WellFoundedGT { x // x a }] {a : } {ε : Type u_2} [] :
structure Estimator.fst {α : Type u_1} {β : Type u_2} [] [] (p : Thunk (α × β)) (ε : Type u_3) [] :
Type u_3
• inner : ε

The wrapped bound for a value in α × β, which we will use as a bound for the first component.

An estimator for (a, b) can be turned into an estimator for a, simply by repeatedly running improve until the first factor "improves". The hypothesis that > is well-founded on { q // q ≤ (a, b) } ensures this terminates.

Instances For
instance instEstimatorDataFstToPreorderToPreorderProd {α : Type u_1} {β : Type u_2} [] [DecidableRel fun x x_1 => x < x_1] [] {a : } {b : } (ε : Type u_3) [Estimator () ε] [∀ (p : α × β), WellFoundedGT { q // q p }] :
def Estimator.fstInst {α : Type u_1} {β : Type u_2} [] [DecidableRel fun x x_1 => x < x_1] [] [∀ (p : α × β), WellFoundedGT { q // q p }] (a : ) (b : ) {ε : Type u_3} (i : Estimator () ε) :

Given an estimator for a pair, we can extract an estimator for the first factor.

Instances For