Reference · Finite types, distributions and Markov chains

rainbow.math.finite.rational-argmax

Finite types, distributions and Markov chainssrc/rainbow/math/finite/rational_argmax.clj3 definitions, 15 theorems

Executable finite argmax with exact rational dominance certificates.

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

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

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

bool/false-not-true :
  (h₁ : data/false = data/true)
  → proposition/falsity

bool/true-not-false :
  (h₁ : data/true = data/false)
  → proposition/falsity

nat/decide-at-most-true-sound :
  (left right : ℕ)
  (same : nat/decide-at-most left right = data/true)
  → left ≤ right

nat/decide-at-most-false-reverse :
  (left right : ℕ)
  (same : nat/decide-at-most left right = data/false)
  → right ≤ left

nnrat/at-most-rewrite-left :
  (left equivalent-left right : ℚ≥0)
  (same : left = equivalent-left)
  (ordered : equivalent-left ≤ right)
  → left ≤ right

nnrat/decide-at-most-true-sound :
  (left right : ℚ≥0)
  (same : audit/decide-nnrat-at-most left right = data/true)
  → left ≤ right

nnrat/decide-at-most-false-reverse :
  (left right : ℚ≥0)
  (same : audit/decide-nnrat-at-most left right = data/false)
  → right ≤ left

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

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

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

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

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

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

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

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