Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-optimal-contraction

Finite types, distributions and Markov chainssrc/rainbow/math/finite/bellman_optimal_contraction.clj0 definitions, 4 theorems

Finite-argmax nonexpansiveness for the NNRAT Bellman optimality layer. The existing finite sup metric is a Nat/numerator construction, whereas value/nnrat-optimality-step lives directly in NonnegativeRational. This module therefore states the metric-free epsilon form of max nonexpansiveness: (forall a in actions, f a <= g a + epsilon) -> max f <= max g + epsilon. The two-sided theorem says that pointwise additive epsilon-closeness is preserved by finite argmax. Its optimality-step specialization transports through value/nnrat-optimality-step-unfold, keeping the reducible argmax implementation opaque to the proof. Native and axiom-free on D63.

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

decision/finite-nnrat-argmax-additively-nonexpansive.{v} :
  (A : Type v) (actions : Finset A) (fallback : A)
  (fallback-member : fallback ∈ actions)
  (left right : A → ℚ≥0) (epsilon : ℚ≥0)
  (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-nnrat-argmax A actions fallback right
  where argmax₁ := decision/finite-nnrat-argmax A actions fallback left

value/nnrat-optimality-step-additive-upper-bound.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (fallback-admissible : ∀ (current : S), fallback current ∈ actions)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (left-value right-value : S → ℚ≥0) (epsilon : ℚ≥0)
  (state : S)
  (pointwise : ∀ (action : A), ∀ (member : action ∈ actions), backup left-value state action ≤ backup right-value state action + epsilon)
  → step left-value state ≤ step right-value state + epsilon
  where step := value/nnrat-optimality-step S A actions fallback backup

value/nnrat-optimality-step-additively-nonexpansive.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (fallback-admissible : ∀ (current : S), fallback current ∈ actions)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (left-value right-value : S → ℚ≥0) (epsilon : ℚ≥0)
  (state : S)
  (left-pointwise : ∀ (action : A), ∀ (member : action ∈ actions), backup left-value state action ≤ backup right-value state action + epsilon)
  (right-pointwise : ∀ (action : A), ∀ (member : action ∈ actions), backup right-value state action ≤ backup left-value state action + epsilon)
  → proposition/conjunction (step₁ ≤ step + epsilon) (step ≤ step₁ + epsilon)
  where step := value/nnrat-optimality-step S A actions fallback backup right-value state
  where step₁ := value/nnrat-optimality-step S A actions fallback backup left-value state