Reference · Finite types, distributions and Markov chains

rainbow.math.finite.rational-argmin

Finite types, distributions and Markov chainssrc/rainbow/math/finite/rational_argmin.clj3 definitions, 8 theorems

Executable finite argmin with exact rational minimality certificates.

Depends onmath.finite.rational-argmax

decision/nnrat-select-min.{u} :
  (A : Type u) (score : A → ℚ≥0) (x₁ x₂ : A)
  → A

list/nnrat-argmin-from.{u} :
  (A : Type u) (score : A → ℚ≥0) (x₁ : A) (x₂ : List A)
  → A

decision/finite-nnrat-argmin.{u} :
  (A : Type u) (actions : Finset A) (initial : A) (score : A → ℚ≥0)
  → A

decision/nnrat-select-min-is-left-or-right.{u} :
  (A : Type u) (score : A → ℚ≥0) (left right : A)
  → proposition/disjunction (min = left) (min = right)
  where min := decision/nnrat-select-min A score left right

decision/nnrat-select-min-bounds-left.{u} :
  (A : Type u) (score : A → ℚ≥0) (left right : A)
  → score (decision/nnrat-select-min A score left right) ≤ score left

decision/nnrat-select-min-bounds-right.{u} :
  (A : Type u) (score : A → ℚ≥0) (left right : A)
  → score (decision/nnrat-select-min A score left right) ≤ score right

list/nnrat-argmin-from-bounded-by-initial.{u} :
  (A : Type u) (score : A → ℚ≥0) (initial : A) (source : List A)
  → (fun source₁ => score (list/nnrat-argmin-from A score initial source₁) ≤ score initial) source

list/nnrat-argmin-from-bounded-by-member.{u} :
  (A : Type u) (score : A → ℚ≥0) (initial : A) (source : List A) (value : A)
  (member : list/membership A source value)
  → score (list/nnrat-argmin-from A score initial source) ≤ score value

list/nnrat-argmin-from-is-initial-or-member.{u} :
  (A : Type u) (score : A → ℚ≥0) (initial : A) (source : List A)
  → proposition/disjunction (list/nnrat-argmin-from A score initial source = initial) (membership)
  where membership := list/membership A source (list/nnrat-argmin-from A score initial source)

decision/finite-nnrat-argmin-is-member.{u} :
  (A : Type u) (actions : Finset A) (initial : A) (score : A → ℚ≥0)
  (initial-member : initial ∈ actions)
  → decision/finite-nnrat-argmin A actions initial score ∈ actions

decision/finite-nnrat-argmin-dominates.{u} :
  (A : Type u) (actions : Finset A) (initial : A) (score : A → ℚ≥0) (candidate : A)
  (candidate-member : candidate ∈ actions)
  → score (decision/finite-nnrat-argmin A actions initial score) ≤ score candidate