BanditRLProof.RL.FiniteHorizonStochasticRewardTrajectory

A finite trace of sampled action, reward, and resulting next state.

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

Prepending a sampled action-reward-state coordinate is measurable.

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

Removing the first sampled coordinate is measurable.

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

An a.e. strongly measurable Real function on a finite type is integrable.

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

One policy action followed by its sampled reward and next state.

noncomputable def actionRewardStateKernel (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) : ProbabilityTheory.Kernel State (Prod Action (Prod Real State))

Kernel of the next `remaining` sampled action-reward-state coordinates. The first chronological stage is `mdp.horizon - remaining`.

noncomputable def stochasticTrajectoryKernelRemaining (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) : (remaining : Nat) -> remaining <= mdp.horizon -> ProbabilityTheory.Kernel State (RewardStepTrace 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 (Prod Real State))) (RewardStepTrace Action State remaining)

Sum of the actual sampled rewards in a reward-bearing finite trace.

def sampledCumulativeRewardFrom : (remaining : Nat) -> RewardStepTrace Action State remaining -> Real | 0, _ => 0 | remaining + 1, trace => (trace 0).2.1 + sampledCumulativeRewardFrom remaining (Fin.tail trace) omit [Fintype State] [Fintype Action] in /-- The sampled finite cumulative reward is measurable. -/ theorem measurable_sampledCumulativeRewardFrom (remaining : Nat) : Measurable (sampledCumulativeRewardFrom (Action := Action) (State := State) remaining)

The sampled finite cumulative reward is measurable.

theorem measurable_sampledCumulativeRewardFrom (remaining : Nat) : Measurable (sampledCumulativeRewardFrom (Action := Action) (State := State) remaining)

The sampled cumulative reward is `L1` under every statewise stochastic trajectory law. No boundedness or second-moment hypothesis is used.

theorem integrable_sampledCumulativeRewardFrom_stochasticTrajectoryKernelRemaining (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) : Integrable (MDP.sampledCumulativeRewardFrom (Action := Action) (State := State) remaining) (source.stochasticTrajectoryKernelRemaining policy remaining hremaining state)

Statewise stochastic trajectory identity: expected sampled cumulative reward equals the independently defined stochastic backward policy value.

theorem integral_sampledCumulativeRewardFrom_stochasticTrajectoryKernelRemaining_eq_stochasticValueRemaining (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) : integral (source.stochasticTrajectoryKernelRemaining policy remaining hremaining state) (MDP.sampledCumulativeRewardFrom (Action := Action) (State := State) remaining) = source.stochasticValueRemaining policy remaining hremaining state

Full reward-bearing trajectory law, including the initial state.

noncomputable def stochasticTrajectoryMeasure (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) : Measure (Prod State (RewardStepTrace Action State mdp.horizon))

Sampled cumulative reward on the full stochastic trajectory.

def sampledCumulativeReward (trajectory : Prod State (RewardStepTrace Action State mdp.horizon)) : Real

The full sampled cumulative reward is measurable.

theorem measurable_sampledCumulativeReward : Measurable (sampledCumulativeReward (mdp := mdp))

The full sampled cumulative reward is integrable under its generated law.

theorem integrable_sampledCumulativeReward_stochasticTrajectoryMeasure (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] : Integrable (sampledCumulativeReward (mdp := mdp)) (source.stochasticTrajectoryMeasure policy initialState)

Route endpoint: expected sampled cumulative reward equals the stochastic and existing mean policy values at chronological stage zero.

theorem integral_sampledCumulativeReward_stochasticTrajectoryMeasure_eq_integral_valueAt_zero (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] : integral (source.stochasticTrajectoryMeasure policy initialState) (sampledCumulativeReward (mdp := mdp)) = integral initialState (source.stochasticValueAt policy 0 (Nat.zero_le mdp.horizon)) ∧ integral (source.stochasticTrajectoryMeasure policy initialState) (sampledCumulativeReward (mdp := mdp)) = integral initialState (policy.valueAt 0 (Nat.zero_le mdp.horizon))