BanditRLProof.RL.FiniteHorizonTrajectory

The finite sequence of sampled actions and their resulting next states.

abbrev StepTrace (Action : Type v) (State : Type u) (n : Nat)

Prepending one action-state step is measurable for the product Pi-space.

theorem measurable_cons (n : Nat) : Measurable (fun p : Prod (Prod Action State) (StepTrace Action State n) => @Fin.cons n (fun _ => Prod Action State) p.1 p.2)

Removing the first action-state step is measurable.

theorem measurable_tail (n : Nat) : Measurable (fun trace : StepTrace Action State (n + 1) => Fin.tail trace)

A measurable Real function on a finite type is integrable under every finite measure.

theorem integrable_of_fintype {Omega : Type*} [Fintype Omega] [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (f : Omega -> Real) (hf : Measurable f) : Integrable f mu

One chronological policy step, retaining both the action and next state.

noncomputable def actionStateKernel {mdp : MDP State Action} (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) : ProbabilityTheory.Kernel State (Prod Action State)

Kernel of the next `remaining` action-state steps. Its first chronological stage is `mdp.horizon - remaining`.

noncomputable def trajectoryKernelRemaining {mdp : MDP State Action} (policy : MarkovPolicy mdp) : (remaining : Nat) -> remaining <= mdp.horizon -> ProbabilityTheory.Kernel State (StepTrace Action State remaining) | 0, _ => ProbabilityTheory.Kernel.deterministic (fun _ => fun i => Fin.elim0 i) measurable_const | remaining + 1, hremaining => let stage : Fin mdp.horizon := ⟨mdp.horizon - (remaining + 1), by omega⟩ let tailKernel : ProbabilityTheory.Kernel (Prod State (Prod Action State)) (StepTrace Action State remaining)

Total reward of a finite trace, starting from the supplied current state.

def cumulativeRewardFrom (mdp : MDP State Action) : (remaining : Nat) -> State -> StepTrace Action State remaining -> Real | 0, _, _ => 0 | remaining + 1, state, trace => mdp.reward state (trace 0).1 + mdp.cumulativeRewardFrom remaining (trace 0).2 (Fin.tail trace) /-- The finite cumulative reward is measurable jointly in its initial state and trace. -/ theorem measurable_cumulativeRewardFrom (mdp : MDP State Action) (remaining : Nat) : Measurable (fun p : Prod State (StepTrace Action State remaining) => mdp.cumulativeRewardFrom remaining p.1 p.2)

The finite cumulative reward is measurable jointly in its initial state and trace.

theorem measurable_cumulativeRewardFrom (mdp : MDP State Action) (remaining : Nat) : Measurable (fun p : Prod State (StepTrace Action State remaining) => mdp.cumulativeRewardFrom remaining p.1 p.2)

Every statewise finite-trace cumulative reward is integrable under its trajectory law.

theorem integrable_cumulativeRewardFrom_trajectoryKernelRemaining {mdp : MDP State Action} (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) : Integrable (mdp.cumulativeRewardFrom remaining state) (policy.trajectoryKernelRemaining remaining hremaining state)

Statewise policy-evaluation identity: integrating the finite generated return over the remaining trajectory gives the backward policy value.

theorem integral_cumulativeRewardFrom_trajectoryKernelRemaining_eq_valueRemaining {mdp : MDP State Action} (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) : (∫ trace, mdp.cumulativeRewardFrom remaining state trace ∂policy.trajectoryKernelRemaining remaining hremaining state) = policy.valueRemaining remaining hremaining state

Joint law of the initial state and all finite action-state steps.

noncomputable def trajectoryMeasure {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) : Measure (Prod State (StepTrace Action State mdp.horizon))

Cumulative reward on the full finite policy trajectory.

def cumulativeReward (mdp : MDP State Action) (trajectory : Prod State (StepTrace Action State mdp.horizon)) : Real

The full finite-trajectory cumulative reward is measurable.

theorem measurable_cumulativeReward (mdp : MDP State Action) : Measurable mdp.cumulativeReward

The cumulative reward is automatically integrable under the finite trajectory law.

theorem integrable_cumulativeReward_trajectoryMeasure {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] : Integrable mdp.cumulativeReward (policy.trajectoryMeasure initialState)

Route endpoint: expected cumulative reward under the generated finite policy trajectory equals the initial-state expectation of the stage-zero policy value.

theorem integral_cumulativeReward_trajectoryMeasure_eq_integral_valueAt_zero {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] : (∫ trajectory, mdp.cumulativeReward trajectory ∂policy.trajectoryMeasure initialState) = ∫ state, policy.valueAt 0 (Nat.zero_le mdp.horizon) state ∂initialState