BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonStochasticRewardErasureLaw

# Finite-horizon stochastic reward erasure laws This module discards sampled Real rewards from generated stochastic-reward trajectories while retaining every action and next state. The resulting law is exactly the ordinary finite-horizon policy trajectory law. The equality is then lifted through the initial-state mixture, a finite iid episode family, and the existing known-reward `EpisodeBatch` conversion. The projected batch deliberately reinstates the deterministic mean reward `mdp.reward`. This is a law transport for transition-learning algorithms with known mean rewards, not a stochastic reward-estimation theorem.

Module map

Declarations
14
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonIIDTrajectoryBatch, BanditRLProof.RL.FiniteHorizonStochasticRewardIIDTotalReturnConcentration, BanditRLProof.RL.FiniteHorizonStochasticRewardBellmanInnovationConcentration

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardEmpiricalOptimisticProjection, BanditRLProof.RL.FiniteHorizonStochasticRewardIIDEmpiricalRewardConfidence

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

def BanditRLProof.FiniteHorizonRL.RewardStepTrace.eraseRewards Compiled

Discard sampled rewards while retaining every action and next state.

def eraseRewards (remaining : Nat) : RewardStepTrace Action State remaining -> StepTrace Action State remaining
Source line 34 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.RewardStepTrace.measurable_eraseRewards Compiled

Coordinatewise reward erasure is measurable on the finite Pi-space.

theorem measurable_eraseRewards (remaining : Nat) : Measurable (eraseRewards (Action
Source line 40 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.RewardStepTrace.eraseRewards_cons Compiled

Reward erasure commutes with prepending one generated coordinate.

theorem eraseRewards_cons (remaining : Nat) (head : Action × (Real × State)) (tail : RewardStepTrace Action State remaining) : eraseRewards (Action
Source line 51 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.ProbabilityTheory.compProd_map_prodMap_of_map_eq Compiled

Map both outputs of a composition-product kernel when the mapped head kernel and every mapped tail fiber agree with prescribed target kernels.

theorem compProd_map_prodMap_of_map_eq {Alpha Beta Beta' Gamma Gamma' : Type*} [MeasurableSpace Alpha] [MeasurableSpace Beta] [MeasurableSpace Beta'] [MeasurableSpace Gamma] [MeasurableSpace Gamma'] (kappa : ProbabilityTheory.Kernel Alpha Beta) [ProbabilityTheory.IsMarkovKernel kappa] (eta : ProbabilityTheory.Kernel (Alpha × Beta) Gamma) [ProbabilityTheory.IsMarkovKernel eta] (kappa' : ProbabilityTheory.Kernel Alpha Beta') [ProbabilityTheory.IsMarkovKernel kappa'] (eta' : ProbabilityTheory.Kernel (Alpha × Beta') Gamma') [ProbabilityTheory.IsMarkovKernel eta'] (f : Beta -> Beta') (hf : Measurable f) (g : Gamma -> Gamma') (hg : Measurable g) (hkappa : kappa.map f = kappa') (heta : forall alpha beta, (eta (alpha, beta)).map g = eta' (alpha, f beta)) : (kappa.compProd eta).map (Prod.map f g) = kappa'.compProd eta'
Source line 70 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryKernelRemaining_map_eraseRewards Compiled

Dropping all sampled rewards from a generated finite stochastic trajectory recovers the ordinary action/next-state trajectory kernel exactly.

theorem stochasticTrajectoryKernelRemaining_map_eraseRewards (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) : (source.stochasticTrajectoryKernelRemaining policy remaining hremaining).map (RewardStepTrace.eraseRewards (Action
Source line 130 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.eraseTrajectory Compiled

Erase sampled rewards from a full stochastic trajectory, retaining its initial state.

def eraseTrajectory (trajectory : State × RewardStepTrace Action State mdp.horizon) : State × StepTrace Action State mdp.horizon
Source line 235 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.measurable_eraseTrajectory Compiled

Full-trajectory reward erasure is measurable.

theorem measurable_eraseTrajectory : Measurable (eraseTrajectory (mdp
Source line 241 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.stochasticTrajectoryMeasure_map_eraseTrajectory Compiled

The full stochastic trajectory law maps exactly to the ordinary trajectory law.

theorem stochasticTrajectoryMeasure_map_eraseTrajectory (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] : (source.stochasticTrajectoryMeasure policy initialState).map (eraseTrajectory (mdp
Source line 247 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.eraseTrajectoryFamily Compiled

Erase sampled rewards coordinatewise from a finite iid trajectory family.

def eraseTrajectoryFamily (episodes : Nat) (trajectories : Fin episodes -> State × RewardStepTrace Action State mdp.horizon) : Fin episodes -> State × StepTrace Action State mdp.horizon
Source line 267 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.measurable_eraseTrajectoryFamily Compiled

Finite-family reward erasure is measurable.

theorem measurable_eraseTrajectoryFamily (episodes : Nat) : Measurable (eraseTrajectoryFamily (mdp
Source line 274 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.iidStochasticTrajectoryFamilyMeasure_map_eraseTrajectoryFamily Compiled

Finite iid stochastic trajectories map to the deterministic iid family law.

theorem iidStochasticTrajectoryFamilyMeasure_map_eraseTrajectoryFamily (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) : (source.iidStochasticTrajectoryFamilyMeasure policy initialState episodes).map (eraseTrajectoryFamily (mdp
Source line 282 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatchOfStochasticTrajectories Compiled

Convert a stochastic trajectory family to the existing empirical batch after erasing rewards. Batch rewards are the known means `mdp.reward`.

def knownRewardEpisodeBatchOfStochasticTrajectories (episodes : Nat) (trajectories : Fin episodes -> State × RewardStepTrace Action State mdp.horizon) : EpisodeBatch mdp episodes
Source line 312 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.measurable_knownRewardEpisodeBatchOfStochasticTrajectories Compiled

The known-reward stochastic-family batch projection is measurable.

theorem measurable_knownRewardEpisodeBatchOfStochasticTrajectories (episodes : Nat) : Measurable (knownRewardEpisodeBatchOfStochasticTrajectories (mdp
Source line 322 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.MeanCompatibleRewardKernel.iidStochasticTrajectoryFamilyMeasure_map_knownRewardEpisodeBatch_eq_iidEpisodeBatchMeasure Compiled

The known-reward batch extracted from iid stochastic trajectories has exactly the existing deterministic iid episode-batch law.

theorem iidStochasticTrajectoryFamilyMeasure_map_knownRewardEpisodeBatch_eq_iidEpisodeBatchMeasure (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) : (source.iidStochasticTrajectoryFamilyMeasure policy initialState episodes).map (knownRewardEpisodeBatchOfStochasticTrajectories (mdp
Source line 335 Chapter context: Finite-horizon RL