Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonIIDGeneratedEmpiricalRewardExactness

# Generated empirical reward exactness for finite-horizon iid batches The finite-horizon MDP surface has a deterministic reward function. Consequently, records extracted from genuine trajectories have exact empirical rewards at every visited coordinate; no reward concentration or additional failure budget is needed. This module records that structural fact and combines it with the existing eligible empirical-transition confidence event.

Module map

Source: BanditRLProof/RL/FiniteHorizonIIDGeneratedEmpiricalRewardExactness.lean
Teaching chapter: 9. Finite-horizon reinforcement learning
Declarations: 11
Placeholders: 0

Imports

BanditRLProof.RL.FiniteHorizonIIDTrajectoryBatch, BanditRLProof.RL.FiniteHorizonIIDEligibleEmpiricalTransitionConfidence

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonIIDAllCoordinateFiniteBatchConfidence

Declarations

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

def BanditRLProof.FiniteHorizonRL.EpisodeBatch.RewardConsistent Compiled

Every recorded reward agrees with the MDP reward at its recorded state and action.

def RewardConsistent {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) : Prop

Source line 29 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.EpisodeBatch.measurableSet_rewardConsistent Compiled

Reward consistency is a measurable property of finite episode batches.

theorem measurableSet_rewardConsistent {mdp : MDP State Action} {episodes : Nat} : MeasurableSet {batch : EpisodeBatch mdp episodes | batch.RewardConsistent}

Source line 36 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.EpisodeBatch.rewardSum_eq_visitCount_mul_reward_of_rewardConsistent Compiled

In a reward-consistent batch, the reward sum is visit count times the true reward.

theorem rewardSum_eq_visitCount_mul_reward_of_rewardConsistent [DecidableEq State] [DecidableEq Action] {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (hbatch : batch.RewardConsistent) (stage : Fin mdp.horizon) (state : State) (action : Action) : batch.rewardSum stage state action = (batch.visitCount stage state action : Real) * mdp.reward state action

Source line 57 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.EpisodeBatch.empiricalReward_eq_reward_of_rewardConsistent Compiled

Positive visits cancel the denominator, so empirical reward is exact.

theorem empiricalReward_eq_reward_of_rewardConsistent [DecidableEq State] [DecidableEq Action] {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (hbatch : batch.RewardConsistent) (stage : Fin mdp.horizon) (state : State) (action : Action) (hcount : batch.visitCount stage state action ≠ 0) : batch.empiricalReward stage state action = mdp.reward state action

Source line 77 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.episodeBatchOfTrajectories_rewardConsistent Compiled

Every finite episode batch extracted from genuine trajectories is reward-consistent.

theorem episodeBatchOfTrajectories_rewardConsistent (mdp : MDP State Action) (episodes : Nat) (trajectories : Fin episodes -> State × StepTrace Action State mdp.horizon) : (mdp.episodeBatchOfTrajectories episodes trajectories).RewardConsistent

Source line 95 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.episodeBatchOfTrajectories_rewardSum_eq_visitCount_mul_reward Compiled

Generated reward sums are exactly visit counts times deterministic MDP rewards.

theorem episodeBatchOfTrajectories_rewardSum_eq_visitCount_mul_reward [DecidableEq State] [DecidableEq Action] (mdp : MDP State Action) (episodes : Nat) (trajectories : Fin episodes -> State × StepTrace Action State mdp.horizon) (stage : Fin mdp.horizon) (state : State) (action : Action) : (mdp.episodeBatchOfTrajectories episodes trajectories).rewardSum stage state action = ((mdp.episodeBatchOfTrajectories episodes trajectories).visitCount stage state action : Real) * mdp.reward state action

Source line 104 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.episodeBatchOfTrajectories_empiricalReward_eq_reward Compiled

A generated empirical reward is exact whenever its visit count is nonzero.

theorem episodeBatchOfTrajectories_empiricalReward_eq_reward [DecidableEq State] [DecidableEq Action] (mdp : MDP State Action) (episodes : Nat) (trajectories : Fin episodes -> State × StepTrace Action State mdp.horizon) (stage : Fin mdp.horizon) (state : State) (action : Action) (hcount : (mdp.episodeBatchOfTrajectories episodes trajectories).visitCount stage state action ≠ 0) : (mdp.episodeBatchOfTrajectories episodes trajectories).empiricalReward stage state action = mdp.reward state action

Source line 119 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iidEpisodeBatchMeasure_rewardConsistent_ae Compiled

The mapped iid episode-batch law is supported a.e. on reward-consistent records.

theorem iidEpisodeBatchMeasure_rewardConsistent_ae {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) : ∀ᵐ batch ∂policy.iidEpisodeBatchMeasure initialState episodes, batch.RewardConsistent

Source line 143 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.empiricalReward_eq_and_transition_lt_of_not_mem_simultaneousCountBadEvent Compiled

On the simultaneous good event, reward consistency gives exact empirical reward and the existing eligible margin gives every next-state transition bound.

theorem empiricalReward_eq_and_transition_lt_of_not_mem_simultaneousCountBadEvent {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} {delta : Real} (batch : EpisodeBatch mdp episodes) (hbatch : batch ∉ policy.simultaneousCountBadEvent initialState episodes delta) (hreward : batch.RewardConsistent) (defaultState : State) (coordinate : VisitCoordinate mdp) (hmargin : simultaneousCountConfidenceRadius mdp episodes delta < coordinate.expectedCount policy initialState episodes) : batch.empiricalReward coordinate.stage coordinate.state coordinate.action = mdp.reward coordinate.state coordinate.action ∧ ∀ nextState, |batch.empiricalTransitionMass defaultState coordinate.stage coordinate.state coordinate.action nextState - (mdp.transition (coordinate.state, coordinate.action)).real {nextState}| < 2 * simultaneousCountConfidenceRadius mdp episodes delta / (coordinate.count batch : Real)

Source line 160 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.episodeBatchOfTrajectories_empiricalReward_eq_and_transition_lt Compiled

Generated trajectory batches satisfy the reward side of the same good-event endpoint.

theorem episodeBatchOfTrajectories_empiricalReward_eq_and_transition_lt {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} {delta : Real} (trajectories : Fin episodes -> State × StepTrace Action State mdp.horizon) (hbatch : mdp.episodeBatchOfTrajectories episodes trajectories ∉ policy.simultaneousCountBadEvent initialState episodes delta) (defaultState : State) (coordinate : VisitCoordinate mdp) (hmargin : simultaneousCountConfidenceRadius mdp episodes delta < coordinate.expectedCount policy initialState episodes) : (mdp.episodeBatchOfTrajectories episodes trajectories).empiricalReward coordinate.stage coordinate.state coordinate.action = mdp.reward coordinate.state coordinate.action ∧ ∀ nextState, |(mdp.episodeBatchOfTrajectories episodes trajectories).empiricalTransitionMass defaultState coordinate.stage coordinate.state coordinate.action nextState - (mdp.transition (coordinate.state, coordinate.action)).real {nextState}| < 2 * simultaneousCountConfidenceRadius mdp episodes delta / (coordinate.count (mdp.episodeBatchOfTrajectories episodes trajectories) : Real)

Source line 191 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iidEpisodeBatch_eligible_empiricalReward_exact_and_transition_confidence Compiled

Route endpoint: the existing global-delta event simultaneously controls every eligible transition coordinate, while reward-consistent batches have zero reward error at those same positive-count coordinates.

theorem iidEpisodeBatch_eligible_empiricalReward_exact_and_transition_confidence {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta ≤ 1) (defaultState : State) (eligible : Finset (VisitCoordinate mdp)) (hmargin : ∀ coordinate ∈ eligible, simultaneousCountConfidenceRadius mdp episodes delta < coordinate.expectedCount policy initialState episodes) : MeasurableSet (policy.simultaneousCountBadEvent initialState episodes delta) ∧ (policy.iidEpisodeBatchMeasure initialState episodes) (policy.simultaneousCountBadEvent initialState episodes delta) ≤ ENNReal.ofReal delta ∧ ∀ᵐ batch ∂policy.iidEpisodeBatchMeasure initialState episodes, batch ∉ policy.simultaneousCountBadEvent initialState episodes delta -> ∀ coordinate ∈ eligible, batch.empiricalReward coordinate.stage coordinate.state coordinate.action = mdp.reward coordinate.state coordinate.action ∧ ∀ nextState, |batch.empiricalTransitionMass defaultState coordinate.stage coordinate.state coordinate.action nextState - (mdp.transition (coordinate.state, coordinate.action)).real {nextState}| < 2 * simultaneousCountConfidenceRadius mdp episodes delta / (coordinate.count batch : Real)

Source line 223 Chapter context: Finite-horizon RL