Example, pp. 961–962 — gains ; optimal for all with ; Cesàro biases
ProvedJewellMRP.InfiniteStep.machine_exampleThe paper's two-state machine maintenance-repair example. State 1 is "running", state 2 "broken down". Every alternative moves the machine to the other state with probability one, so under every stationary policy the embedded chain is
With the linear reward structure (8) (, ) the one-step expected reward of an alternative is : in state 1, alternative gives and alternative gives ; in state 2, alternative gives and alternative gives . Let be the reward vector of the policy , , and . Then
- is ergodic (irreducible, row-stochastic, of period ) and is a stationary probability vector;
- the gains of the four stationary policies are , , , ;
- is optimal for every : the return of satisfies the optimality recursion (I 16),
so it is the optimal -step return; 4. for every ,
- the limiting bias vector is ;
- the relative values , solve equations (5): with .
The example shows why the bias limit is a Cesàro limit: oscillates between two values forever, and only its average converges.
Formalization Note States 1 and 2 are the Lean indices 0 and 1, and the paper's is . The paper's "optimal for all values of " is stated as: the return satisfies (I 16) with the maximum over both alternatives in each state, which determines the optimal return uniquely from . The rewards are written as so that each number can be read off p. 961.
import Mathlib import Definitions.Def_JewellMRP_InfiniteStep_Model open Matrix Filter Topology
namespace JewellMRP.InfiniteStep
theorem machine_example :
let P : Matrix (Fin 2) (Fin 2) ℝ := !![0, 1; 1, 0]
let ρA₁ : ℝ := 0 + 100 * 4
let ρB₁ : ℝ := 0 + 84 * 5
let ρA₂ : ℝ := 0 + (-65) * 4
let ρB₂ : ℝ := -100 + (-200) * 1
let ρ : Fin 2 → ℝ := ![ρB₁, ρA₂]
let π : Fin 2 → ℝ := ![1 / 2, 1 / 2]
IsErgodic P ∧ IsStationary P π ∧
gain π ![ρA₁, ρA₂] = 70 ∧ gain π ![ρA₁, ρB₂] = 50 ∧ gain π ρ = 80 ∧
gain π ![ρB₁, ρB₂] = 60 ∧
(∀ n : ℕ,
stepReturn P ρ 0 (n + 1) 0 =
max (ρA₁ + ∑ j, P 0 j * stepReturn P ρ 0 n j)
(ρB₁ + ∑ j, P 0 j * stepReturn P ρ 0 n j) ∧
stepReturn P ρ 0 (n + 1) 1 =
max (ρA₂ + ∑ j, P 1 j * stepReturn P ρ 0 n j)
(ρB₂ + ∑ j, P 1 j * stepReturn P ρ 0 n j)) ∧
(∀ n : ℕ, stepReturn P ρ 0 n 0 = 80 * n + 170 + (-1) ^ (n + 1) * 170 ∧
stepReturn P ρ 0 n 1 = 80 * n - 170 - (-1) ^ (n + 1) * 170) ∧
(fundamentalMatrix P π - limitMatrix π) *ᵥ ρ + limitMatrix π *ᵥ 0 = ![170, -170] ∧
(∀ i, ![340, 0] i + gain π ρ = ρ i + ∑ j, P i j * ![(340 : ℝ), 0] j) := by sorry
end JewellMRP.InfiniteStep
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.