# 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_3) :
Type (max u_1 u_3)

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.

• bound : εα

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

• improve : ε

Generate an improved lower bound.

Instances
class Estimator {α : Type u_1} [] (a : ) (ε : Type u_3) extends :
Type (max u_1 u_3)

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.
• bound : εα
• improve : ε
• bound_le : ∀ (e : ε), a.get

The calculated bounds are always lower bounds.

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

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

Instances
theorem Estimator.bound_le {α : Type u_1} [] {a : } {ε : Type u_3} [self : ] (e : ε) :
a.get

The calculated bounds are always lower bounds.

theorem Estimator.improve_spec {α : Type u_1} [] {a : } {ε : Type u_3} [self : ] (e : ε) :
match with | none => = a.get | some e' =>

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

@[reducible, inline]
abbrev Estimator.trivial {α : Type u} (a : α) :

A trivial estimator, containing the actual value.

Equations
• = { b : α // b = a }
Instances For
instance instBotTrivial {α : Type u_1} {a : α} :
Equations
• instBotTrivial = { bot := a, }
Equations
instance instWellFoundedGTTrivial {α : Type u_1} [] (a : α) :
Equations
• =
instance instEstimatorPureTrivial {α : Type u_1} [] {a : α} :
Equations
• instEstimatorPureTrivial =
@[irreducible]
def Estimator.improveUntilAux {α : Type u_1} {ε : Type u_2} [] (a : ) (p : αBool) [] [] (e : ε) (r : Bool) :
Except (Option ε) ε

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 (Option ε) ε

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

Equations
Instances For
@[irreducible]
theorem Estimator.improveUntilAux_spec {α : Type u_1} {ε : Type u_2} [] (a : ) (p : αBool) [] [] (e : ε) (r : Bool) :
match with | Except.error a_1 => ¬p a.get = true | => p (EstimatorData.bound a e') = 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_1} {ε : Type u_2} [] (a : ) (p : αBool) [] [] (e : ε) :
match with | Except.error a_1 => ¬p a.get = true | => p (EstimatorData.bound a e') = true

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

Estimators for sums.

@[simp]
theorem instEstimatorDataHAddThunkProd_bound {α : Type u_1} [Add α] {a : } {b : } (εa : Type u_3) (εb : Type u_4) [] [] (e : εa × εb) :
@[simp]
theorem instEstimatorDataHAddThunkProd_improve {α : Type u_1} [Add α] {a : } {b : } (εa : Type u_3) (εb : Type u_4) [] [] (e : εa × εb) :
EstimatorData.improve (a + b) e = match with | some e' => some (e', e.2) | none => match with | some e' => some (e.1, e') | none => none
instance instEstimatorDataHAddThunkProd {α : Type u_1} [Add α] {a : } {b : } (εa : Type u_3) (εb : Type u_4) [] [] :
EstimatorData (a + b) (εa × εb)
Equations
• One or more equations did not get rendered due to their size.
instance instEstimatorNatHAddThunkProd (a : ) (b : ) {εa : Type u_3} {εb : Type u_4} [Estimator a εa] [Estimator b εb] :
Estimator (a + b) (εa × εb)
Equations

Estimator for the first component of a pair.

structure Estimator.fst {α : Type u_1} {β : Type u_3} [] [] (p : Thunk (α × β)) (ε : Type u_4) [] :
Type u_4

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.

• inner : ε

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

Instances For
instance instWellFoundedGTElemRangeBound {α : Type u_1} {ε : Type u_2} [] [∀ (a : α), WellFoundedGT { x : α // x a }] {a : } [] :
Equations
• =
instance instEstimatorDataFstProdOfDecidableRelLtOfWellFoundedGTSubtypeProdLe {α : Type u_1} {β : Type u_3} [] [] [DecidableRel fun (x1 x2 : α) => x1 < x2] {a : } {b : } (ε : Type u_4) [Estimator (a.prod b) ε] [∀ (p : α × β), WellFoundedGT { q : α × β // q p }] :
EstimatorData a (Estimator.fst (a.prod b) ε)
Equations
• One or more equations did not get rendered due to their size.
def Estimator.fstInst {α : Type u_1} {ε : Type u_2} {β : Type u_3} [] [] [DecidableRel fun (x1 x2 : α) => x1 < x2] [∀ (p : α × β), WellFoundedGT { q : α × β // q p }] (a : ) (b : ) (i : Estimator (a.prod b) ε) :
Estimator a (Estimator.fst (a.prod b) ε)

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

Equations
Instances For