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

    Generate an improved lower bound.

Instances
    class Estimator {α : Type u_1} [Preorder α] (a : Thunk α) (ε : Type u_3) extends EstimatorData :
    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.
    Instances
      theorem Estimator.bound_le {α : Type u_1} :
      ∀ {inst : Preorder α} {a : Thunk α} {ε : Type u_3} [self : Estimator a ε] (e : ε), EstimatorData.bound a e a.get

      The calculated bounds are always lower bounds.

      theorem Estimator.improve_spec {α : Type u_1} :
      ∀ {inst : Preorder α} {a : Thunk α} {ε : Type u_3} [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} (a : α) :

      A trivial estimator, containing the actual value.

      Equations
      Instances For
        instance instBotTrivial {α : Type u_1} {a : α} :
        Equations
        • instBotTrivial = { bot := a, }
        Equations
        • =
        instance instEstimatorPureTrivial {α : Type u_1} [Preorder α] {a : α} :
        Equations
        @[irreducible]
        def Estimator.improveUntilAux {α : Type u_1} {ε : Type u_2} [Preorder α] (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} {ε : Type u_2} [Preorder α] (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
            @[irreducible]
            theorem Estimator.improveUntilAux_spec {α : Type u_1} {ε : Type u_2} [Preorder α] (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_1} {ε : Type u_2} [Preorder α] (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_bound {α : Type u_1} [Add α] {a : Thunk α} {b : Thunk α} (εa : Type u_3) (εb : Type u_4) [EstimatorData a εa] [EstimatorData b εb] (e : εa × εb) :
            @[simp]
            theorem instEstimatorDataHAddThunkProd_improve {α : Type u_1} [Add α] {a : Thunk α} {b : Thunk α} (εa : Type u_3) (εb : Type u_4) [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
            instance instEstimatorDataHAddThunkProd {α : Type u_1} [Add α] {a : Thunk α} {b : Thunk α} (εa : Type u_3) (εb : Type u_4) [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_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} [PartialOrder α] [PartialOrder β] (p : Thunk (α × β)) (ε : Type u_4) [Estimator p ε] :
            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} [PartialOrder α] [∀ (a : α), WellFoundedGT { x : α // x a }] {a : Thunk α} [Estimator a ε] :
              Equations
              • =
              instance instEstimatorDataFstProdOfDecidableRelLtOfWellFoundedGTSubtypeProdLe {α : Type u_1} {β : Type u_3} [PartialOrder α] [PartialOrder β] [DecidableRel fun (x1 x2 : α) => x1 < x2] {a : Thunk α} {b : Thunk β} (ε : 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} [PartialOrder α] [PartialOrder β] [DecidableRel fun (x1 x2 : α) => x1 < x2] [∀ (p : α × β), WellFoundedGT { q : α × β // q p }] (a : Thunk α) (b : Thunk β) (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