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_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.

Instances
    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.
    Instances
      @[inline, reducible]
      abbrev Estimator.trivial {α : Type u_1} (a : α) :
      Type u_1

      A trivial estimator, containing the actual value.

      Equations
      Instances For
        instance instBotTrivial :
        {α : Type u_1} → {a : α} → Bot (Estimator.trivial a)
        Equations
        • instBotTrivial = { bot := { val := a, property := } }
        Equations
        • =
        instance instEstimatorPureTrivial {α : Type u_1} [Preorder α] {a : α} :
        Equations
        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.
        Instances For
          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
          Instances For
            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 (Thunk.get a) = 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 (Thunk.get a) = 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 instEstimatorDataHAddThunkInstHAddInstAddThunkProd_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 instEstimatorDataHAddThunkInstHAddInstAddThunkProd_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) :
            instance instEstimatorDataHAddThunkInstHAddInstAddThunkProd {α : 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.

            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.

            Instances For
              Equations
              • =
              instance instEstimatorDataFstProd {α : Type u_2} {β : Type u_3} [PartialOrder α] [PartialOrder β] [DecidableRel fun (x x_1 : α) => x < x_1] {a : Thunk α} {b : Thunk β} (ε : Type u_1) [Estimator (Thunk.prod a b) ε] [∀ (p : α × β), WellFoundedGT { q : α × β // q p }] :
              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 (Thunk.prod a b) ε) :

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

              Equations
              Instances For