BanditRLProof.RL.FiniteHorizonOptimality

A finite action maximizing the one-step Bellman action value.

noncomputable def optimalAction (mdp : MDP State Action) (value : State -> Real) (state : State) : Action

The selected finite action dominates every Bellman action value.

theorem bellmanQ_le_optimalAction (mdp : MDP State Action) (value : State -> Real) (state : State) (action : Action) : mdp.bellmanQ value state action <= mdp.bellmanQ value state (mdp.optimalAction value state)

The finite-state maximizing selector is measurable.

theorem measurable_optimalAction (mdp : MDP State Action) (value : State -> Real) : Measurable (mdp.optimalAction value)

Pointwise finite-action Bellman maximum.

noncomputable def optimalBellman (mdp : MDP State Action) (value : State -> Real) (state : State) : Real

Every action value is bounded by the finite-action Bellman maximum.

theorem bellmanQ_le_optimalBellman (mdp : MDP State Action) (value : State -> Real) (state : State) (action : Action) : mdp.bellmanQ value state action <= mdp.optimalBellman value state

The optimal Bellman value is measurable on the finite discrete state space.

theorem measurable_optimalBellman (mdp : MDP State Action) (value : State -> Real) : Measurable (mdp.optimalBellman value)

Transition expectation is monotone in the continuation value.

theorem transitionValue_mono (mdp : MDP State Action) {left right : State -> Real} (hle : forall state, left state <= right state) (state : State) (action : Action) : mdp.transitionValue left state action <= mdp.transitionValue right state action

Bellman action values are monotone in their continuation value.

theorem bellmanQ_mono (mdp : MDP State Action) {left right : State -> Real} (hle : forall state, left state <= right state) (state : State) (action : Action) : mdp.bellmanQ left state action <= mdp.bellmanQ right state action

Backward optimal value indexed by the number of decisions remaining.

noncomputable def optimalValueRemaining (mdp : MDP State Action) : (remaining : Nat) -> remaining <= mdp.horizon -> State -> Real | 0, _ => fun _ => 0 | remaining + 1, hremaining => mdp.optimalBellman (mdp.optimalValueRemaining remaining (by omega)) /-- Every backward optimal-value surface is measurable. -/ theorem measurable_optimalValueRemaining (mdp : MDP State Action) (remaining : Nat) (hremaining : remaining <= mdp.horizon) : Measurable (mdp.optimalValueRemaining remaining hremaining)

Every backward optimal-value surface is measurable.

theorem measurable_optimalValueRemaining (mdp : MDP State Action) (remaining : Nat) (hremaining : remaining <= mdp.horizon) : Measurable (mdp.optimalValueRemaining remaining hremaining)

Optimal value at chronological stage `stage <= horizon`.

noncomputable def optimalValueAt (mdp : MDP State Action) (stage : Nat) (_hstage : stage <= mdp.horizon) : State -> Real

Every chronological optimal-value surface is measurable.

theorem measurable_optimalValueAt (mdp : MDP State Action) (stage : Nat) (hstage : stage <= mdp.horizon) : Measurable (mdp.optimalValueAt stage hstage)

Transport the dependent optimal-value recursion across equal remaining horizons.

theorem optimalValueRemaining_eq_of_eq (mdp : MDP State Action) {left right : Nat} (hleft : left <= mdp.horizon) (hright : right <= mdp.horizon) (h : left = right) : mdp.optimalValueRemaining left hleft = mdp.optimalValueRemaining right hright

The optimal value is zero at the terminal stage.

theorem optimalValueAt_horizon (mdp : MDP State Action) : mdp.optimalValueAt mdp.horizon le_rfl = fun _ => 0

Finite-action Bellman recursion for the chronological optimal value.

theorem optimalValueAt_bellman (mdp : MDP State Action) (stage : Nat) (hstage : stage < mdp.horizon) : mdp.optimalValueAt stage (Nat.le_of_lt hstage) = mdp.optimalBellman (mdp.optimalValueAt (stage + 1) (by omega))

Policy Bellman expectation is monotone in the continuation value.

theorem bellman_mono {mdp : MDP State Action} (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) {left right : State -> Real} (hle : forall state, left state <= right state) (state : State) : policy.bellman stage left state <= policy.bellman stage right state

Every policy Bellman expectation is bounded by the finite-action maximum.

theorem bellman_le_optimalBellman {mdp : MDP State Action} (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) (value : State -> Real) (state : State) : policy.bellman stage value state <= mdp.optimalBellman value state

Every Markov policy value is pointwise bounded by the optimal value.

theorem valueAt_le_optimalValueAt {mdp : MDP State Action} (policy : MarkovPolicy mdp) (stage : Nat) (hstage : stage <= mdp.horizon) (state : State) : policy.valueAt stage hstage state <= mdp.optimalValueAt stage hstage state

Greedy deterministic Markov policy for the backward optimal value.

noncomputable def optimalPolicy (mdp : MDP State Action) : MarkovPolicy mdp where

One greedy-policy Bellman step is exactly the finite-action maximum.

theorem optimalPolicy_bellman_eq_optimalBellman (mdp : MDP State Action) (stage : Fin mdp.horizon) (state : State) : mdp.optimalPolicy.bellman stage (mdp.optimalValueAt (stage + 1) (Nat.succ_le_of_lt stage.isLt)) state = mdp.optimalBellman (mdp.optimalValueAt (stage + 1) (Nat.succ_le_of_lt stage.isLt)) state

The measurable greedy deterministic policy attains the optimal value at every stage.

theorem optimalPolicy_valueAt_eq_optimalValueAt (mdp : MDP State Action) (stage : Nat) (hstage : stage <= mdp.horizon) : mdp.optimalPolicy.valueAt stage hstage = mdp.optimalValueAt stage hstage

Route endpoint: the backward Bellman value dominates every Markov policy and is attained by the measurable greedy deterministic policy.

theorem optimalValueAt_dominates_and_is_attained (mdp : MDP State Action) : (forall (policy : MarkovPolicy mdp) (stage : Nat) (hstage : stage <= mdp.horizon) (state : State), policy.valueAt stage hstage state <= mdp.optimalValueAt stage hstage state) /\ (exists policy : MarkovPolicy mdp, forall (stage : Nat) (hstage : stage <= mdp.horizon), policy.valueAt stage hstage = mdp.optimalValueAt stage hstage)