Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-signed-policy-approximate-fixed-point

Finite types, distributions and Markov chainssrc/rainbow/math/finite/bellman_signed_policy_approximate_fixed_point.clj0 definitions, 6 theorems

Constructive approximate fixed points for finite signed policy evaluation. The signed fixed-policy Bellman operator is an affine map on an explicit vector. For nonnegative rows whose sums are bounded by gamma <= 1/2, and an initial residual at most one, its kth iterate is an independently checkable approximate fixed point with residual at most 1/(k+1). The existential theorem exposes that computed iterate as proof data. This removes the exact-fixed-point premise from finite-tolerance policy evaluation. It does not construct an exact rational fixed point: the latter remains a separate algebraic existence obligation. Native, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-approximate-fixed-pointmath.finite.bellman-signed-policymath.finite.bellman-signed-value-iteration-general-converges

bellman/signed-policy-eventually-approximate-fixed-point :
  (rows : List (List ℚ)) (reward initial : List ℚ) (gamma : ℚ≥0)
  (gamma-at-most-half : gamma ≤ nnrat/half)
  (step-shape : vector/same-shape initial (step₁))
  (reward-shape : vector/same-shape reward (matrix/vector-multiply rows initial))
  (positive-rows : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) rows row), vector/at-most (vector/zero-like row) row)
  (bounded-sums : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) rows row), vector/sum row ≤ signed/from-nnrat gamma)
  (initial-residual-at-most-one : vector/sup-distance initial (step₁) ≤ 1)
  (index steps : ℕ)
  (large-enough : index ≤ steps)
  → vector/sup-distance (bellman/signed-policy-iterate rows reward steps initial) (step) ≤ signed/from-nnrat (nnrat/harmonic index)
  where step := bellman/signed-policy-step rows reward (bellman/signed-policy-iterate rows reward steps initial)
  where step₁ := bellman/signed-policy-step rows reward initial

bellman/signed-policy-approximate-fixed-point-at-horizon :
  (rows : List (List ℚ)) (reward initial : List ℚ) (gamma : ℚ≥0)
  (gamma-at-most-half : gamma ≤ nnrat/half)
  (step-shape : vector/same-shape initial (step₁))
  (reward-shape : vector/same-shape reward (matrix/vector-multiply rows initial))
  (positive-rows : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) rows row), vector/at-most (vector/zero-like row) row)
  (bounded-sums : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) rows row), vector/sum row ≤ signed/from-nnrat gamma)
  (initial-residual-at-most-one : vector/sup-distance initial (step₁) ≤ 1)
  (index : ℕ)
  → vector/sup-distance (bellman/signed-policy-iterate rows reward index initial) (step) ≤ signed/from-nnrat (nnrat/harmonic index)
  where step := bellman/signed-policy-step rows reward (bellman/signed-policy-iterate rows reward index initial)
  where step₁ := bellman/signed-policy-step rows reward initial

bellman/signed-policy-approximate-fixed-point-exists :
  (rows : List (List ℚ)) (reward initial : List ℚ) (gamma : ℚ≥0)
  (gamma-at-most-half : gamma ≤ nnrat/half)
  (step-shape : vector/same-shape initial (step))
  (reward-shape : vector/same-shape reward (matrix/vector-multiply rows initial))
  (positive-rows : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) rows row), vector/at-most (vector/zero-like row) row)
  (bounded-sums : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) rows row), vector/sum row ≤ signed/from-nnrat gamma)
  (initial-residual-at-most-one : vector/sup-distance initial (step) ≤ 1)
  (index : ℕ)
  → proposition/existence (List ℚ) (fun candidate => vector/sup-distance candidate (bellman/signed-policy-step rows reward candidate) ≤ signed/from-nnrat (nnrat/harmonic index))
  where step := bellman/signed-policy-step rows reward initial

bellman/signed-policy-successive-residual-rate-null-general :
  (ap gp : ℕ) (rows : List (List ℚ)) (reward initial : List ℚ)
  (step-shape : vector/same-shape initial (step))
  (reward-shape : vector/same-shape reward (matrix/vector-multiply rows initial))
  (positive-rows : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) rows row), vector/at-most (vector/zero-like row) row)
  (bounded-sums : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) rows row), vector/sum row ≤ signed/from-nnrat (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))))
  (initial-bound : vector/sup-distance initial (step) ≤ signed/from-nnrat (nnrat/general-harmonic ap gp 0))
  → analysis/signed-rate-null (fun steps => vector/sup-distance (iterate steps initial) (iterate (data/succ steps) initial)) (fun index => nat/multiply (data/succ ap) index)
  where iterate := bellman/signed-policy-iterate rows reward
  where step := bellman/signed-policy-step rows reward initial

bellman/signed-policy-approximate-fixed-point-general-rate :
  (ap gp : ℕ) (rows : List (List ℚ)) (reward initial : List ℚ)
  (step-shape : vector/same-shape initial (step₁))
  (reward-shape : vector/same-shape reward (matrix/vector-multiply rows initial))
  (positive-rows : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) rows row), vector/at-most (vector/zero-like row) row)
  (bounded-sums : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) rows row), vector/sum row ≤ signed/from-nnrat (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))))
  (initial-bound : vector/sup-distance initial (step₁) ≤ signed/from-nnrat (nnrat/general-harmonic ap gp 0))
  (index : ℕ)
  → vector/sup-distance (bellman/signed-policy-iterate rows reward (nat/multiply (data/succ ap) index) initial) (step) ≤ signed/from-nnrat (nnrat/harmonic index)
  where step := bellman/signed-policy-step rows reward (bellman/signed-policy-iterate rows reward (nat/multiply (data/succ ap) index) initial)
  where step₁ := bellman/signed-policy-step rows reward initial

bellman/signed-policy-approximate-fixed-point-exists-general-rate :
  (ap gp : ℕ) (rows : List (List ℚ)) (reward initial : List ℚ)
  (step-shape : vector/same-shape initial (step))
  (reward-shape : vector/same-shape reward (matrix/vector-multiply rows initial))
  (positive-rows : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) rows row), vector/at-most (vector/zero-like row) row)
  (bounded-sums : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) rows row), vector/sum row ≤ signed/from-nnrat (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))))
  (initial-bound : vector/sup-distance initial (step) ≤ signed/from-nnrat (nnrat/general-harmonic ap gp 0))
  (index : ℕ)
  → proposition/existence (List ℚ) (fun candidate => vector/sup-distance candidate (bellman/signed-policy-step rows reward candidate) ≤ signed/from-nnrat (nnrat/harmonic index))
  where step := bellman/signed-policy-step rows reward initial