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_2} (a : Thunk α) (ε : Type u_1) : Type (max u_1 u_2)

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 : ε → Option ε

  Generate an improved lower bound.

class Estimator {α : Type u_2} [Preorder α] (a : Thunk α) (ε : Type u_1) extends EstimatorData : Type (max u_1 u_2)

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 : ε → Option ε
• bound_le : ∀ (e : ε), EstimatorData.bound a e ≤ a.get

  The calculated bounds are always lower bounds.

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

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

theorem Estimator.bound_le {α : Type u_2} [Preorder α] {a : Thunk α} {ε : Type u_1} [self : Estimator a ε] (e : ε) : EstimatorData.bound a e ≤ a.get

The calculated bounds are always lower bounds.

theorem Estimator.improve_spec {α : Type u_2} [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'

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

@[reducible, inline]

abbrev Estimator.trivial {α : Type u_1} (a : α) : Type u_1

A trivial estimator, containing the actual value.

Equations

• Estimator.trivial a = { b : α // b = a }

instance instBotTrivial : {α : Type u_1} → {a : α} → Bot (Estimator.trivial a)

Equations

• instBotTrivial = { bot := ⟨a, ⋯⟩ }

instance instWellFoundedGTUnit : WellFoundedGT Unit

Equations

• instWellFoundedGTUnit = ⋯

instance instWellFoundedGTTrivial {α : Type u_1} [Preorder α] (a : α) : WellFoundedGT (Estimator.trivial a)

Equations

• ⋯ = ⋯

instance instEstimatorPureTrivial {α : Type u_1} [Preorder α] {a : α} : Estimator (Thunk.pure a) (Estimator.trivial a)

Equations

• instEstimatorPureTrivial = Estimator.mk ⋯ ⋯

def Estimator.improveUntilAux {α : Type u_1} [Preorder α] {ε : Type u_2} (a : Thunk α) (p : α → Bool) [Estimator a ε] [WellFoundedGT ↑(Set.range (EstimatorData.bound a))] (e : ε) (r : Bool) : Except (Option ε) ε

Implementation of Estimator.improveUntil.

Equations

• One or more equations did not get rendered due to their size.

def Estimator.improveUntil {α : Type u_1} [Preorder α] {ε : Type u_2} (a : Thunk α) (p : α → Bool) [Estimator a ε] [WellFoundedGT ↑(Set.range (EstimatorData.bound a))] (e : ε) : Except (Option ε) ε

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

Equations

• Estimator.improveUntil a p e = Estimator.improveUntilAux a p e false

theorem Estimator.improveUntilAux_spec {α : Type u_2} [Preorder α] {ε : Type u_1} (a : Thunk α) (p : α → Bool) [Estimator a ε] [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

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} [Preorder α] {ε : Type u_1} (a : Thunk α) (p : α → Bool) [Estimator a ε] [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

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_improve {α : Type u_3} [Add α] {a : Thunk α} {b : Thunk α} (εa : Type u_1) (εb : Type u_2) [EstimatorData a εa] [EstimatorData b εb] (e : εa × εb) : EstimatorData.improve (a + b) e = match EstimatorData.improve a e.1 with | some e' => some (e', e.2) | none => match EstimatorData.improve b e.2 with | some e' => some (e.1, e') | none => none

@[simp]

theorem instEstimatorDataHAddThunkProd_bound {α : Type u_3} [Add α] {a : Thunk α} {b : Thunk α} (εa : Type u_1) (εb : Type u_2) [EstimatorData a εa] [EstimatorData b εb] (e : εa × εb) : EstimatorData.bound (a + b) e = EstimatorData.bound a e.1 + EstimatorData.bound b e.2

instance instEstimatorDataHAddThunkProd {α : Type u_3} [Add α] {a : Thunk α} {b : Thunk α} (εa : Type u_1) (εb : Type u_2) [EstimatorData a εa] [EstimatorData b εb] : EstimatorData (a + b) (εa × εb)

Equations

• One or more equations did not get rendered due to their size.

instance instEstimatorNatHAddThunkProd (a : Thunk ℕ) (b : Thunk ℕ) {εa : Type u_1} {εb : Type u_2} [Estimator a εa] [Estimator b εb] : Estimator (a + b) (εa × εb)

Equations

• instEstimatorNatHAddThunkProd a b = Estimator.mk ⋯ ⋯

Estimator for the first component of a pair.

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

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.

instance instWellFoundedGTElemRangeBound {α : Type u_1} [PartialOrder α] [∀ (a : α), WellFoundedGT { x : α // x ≤ a }] {a : Thunk α} {ε : Type u_2} [Estimator a ε] : WellFoundedGT ↑(Set.range (EstimatorData.bound a))

Equations

• ⋯ = ⋯

instance instEstimatorDataFstProdOfDecidableRelLtOfWellFoundedGTSubtypeProdLe {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [DecidableRel fun (x x_1 : α) => x < x_1] {a : Thunk α} {b : Thunk β} (ε : Type u_1) [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_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [DecidableRel fun (x x_1 : α) => x < x_1] [∀ (p : α × β), WellFoundedGT { q : α × β // q ≤ p }] (a : Thunk α) (b : Thunk β) {ε : Type u_1} (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

• Estimator.fstInst a b i = Estimator.mk ⋯ ⋯