Reference · Finite types, distributions and Markov chains

rainbow.math.finite.signed-argmax-nonexpansive

Finite types, distributions and Markov chainssrc/rainbow/math/finite/signed_argmax_nonexpansive.clj0 definitions, 2 theorems

Additive nonexpansiveness of runtime-length finite signed-rational argmax. If every declared action satisfies f(a) <= g(a) + epsilon, the maximum selected by the executable signed argmax satisfies the same upper bound. Supplying both pointwise directions yields the usual two-sided additive epsilon certificate. Scores and epsilon are arbitrary exact signed rationals; carrier finiteness and fallback membership are explicit. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.signed-argmax

decision/finite-signed-argmax-additive-upper-bound.{u} :
  (A : Type u) (actions : Finset A) (fallback : A)
  (fallback-member : fallback ∈ actions)
  (left right : A → ℚ) (epsilon : ℚ)
  (pointwise : ∀ (candidate : A), ∀ (member : candidate ∈ actions), left candidate ≤ right candidate + epsilon)
  → left (argmax left) ≤ right (argmax right) + epsilon
  where argmax := decision/finite-signed-argmax A actions fallback

decision/finite-signed-argmax-additively-nonexpansive.{u} :
  (A : Type u) (actions : Finset A) (fallback : A)
  (fallback-member : fallback ∈ actions)
  (left right : A → ℚ) (epsilon : ℚ)
  (left-pointwise : ∀ (candidate : A), ∀ (member : candidate ∈ actions), left candidate ≤ right candidate + epsilon)
  (right-pointwise : ∀ (candidate : A), ∀ (member : candidate ∈ actions), right candidate ≤ left candidate + epsilon)
  → proposition/conjunction (left (argmax₁) ≤ right (argmax) + epsilon) (right (argmax) ≤ left (argmax₁) + epsilon)
  where argmax := decision/finite-signed-argmax A actions fallback right
  where argmax₁ := decision/finite-signed-argmax A actions fallback left