Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonIIDTrajectoryBatch

# IID generated-trajectory batches for finite-horizon RL This module maps a finite product of genuine policy trajectory laws into the finite-batch empirical-model surface. It exposes both the episode/stage marginal law and independence across episode coordinates. The policy is fixed across episodes; adaptive cross-episode policy updates and concentration of visit-conditioned empirical ratios remain downstream.

Module map

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

Imports

BanditRLProof.RL.FiniteHorizonEmpiricalModel

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonIIDCountConcentration, BanditRLProof.RL.FiniteHorizonIIDGeneratedEmpiricalRewardExactness, BanditRLProof.RL.FiniteHorizonStochasticRewardErasureLaw

Declarations

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

def BanditRLProof.FiniteHorizonRL.MDP.trajectoryStateAt Compiled

Current state immediately before a recorded trajectory action.

def trajectoryStateAt (mdp : MDP State Action) (trajectory : State × StepTrace Action State mdp.horizon) (stage : Fin mdp.horizon) : State

Source line 33 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MDP.episodeStepOfTrajectory Compiled

A full generated trajectory viewed as one empirical record at a stage.

def episodeStepOfTrajectory (mdp : MDP State Action) (trajectory : State × StepTrace Action State mdp.horizon) (stage : Fin mdp.horizon) : EpisodeStep State Action where

Source line 42 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MDP.episodeBatchOfTrajectories Compiled

A finite family of full trajectories mapped to empirical episode records.

def episodeBatchOfTrajectories (mdp : MDP State Action) (episodes : Nat) (trajectories : Fin episodes -> State × StepTrace Action State mdp.horizon) : EpisodeBatch mdp episodes

Source line 52 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MDP.trajectoryVisitContribution Compiled

One trajectory's contribution to a stage/state/action visit count.

def trajectoryVisitContribution (mdp : MDP State Action) (stage : Fin mdp.horizon) (state : State) (action : Action) (trajectory : State × StepTrace Action State mdp.horizon) : Nat

Source line 59 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MDP.trajectoryRewardContribution Compiled

One trajectory's contribution to a stage/state/action reward sum.

def trajectoryRewardContribution (mdp : MDP State Action) (stage : Fin mdp.horizon) (state : State) (action : Action) (trajectory : State × StepTrace Action State mdp.horizon) : Real

Source line 66 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MDP.trajectoryTransitionContribution Compiled

One trajectory's contribution to a stage/state/action/next-state count.

def trajectoryTransitionContribution (mdp : MDP State Action) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) (trajectory : State × StepTrace Action State mdp.horizon) : Nat

Source line 73 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.measurable_episodeStepOfTrajectory Compiled

The stage record extracted from a finite trajectory is measurable.

theorem measurable_episodeStepOfTrajectory (mdp : MDP State Action) (stage : Fin mdp.horizon) : Measurable (fun trajectory => mdp.episodeStepOfTrajectory trajectory stage)

Source line 84 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.measurable_episodeBatchOfTrajectories Compiled

Mapping a finite trajectory family to its empirical batch is measurable.

theorem measurable_episodeBatchOfTrajectories (mdp : MDP State Action) (episodes : Nat) : Measurable (mdp.episodeBatchOfTrajectories episodes)

Source line 92 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.episodeBatchOfTrajectories_apply Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem episodeBatchOfTrajectories_apply (mdp : MDP State Action) (episodes : Nat) (trajectories : Fin episodes -> State × StepTrace Action State mdp.horizon) (episode : Fin episodes) (stage : Fin mdp.horizon) : mdp.episodeBatchOfTrajectories episodes trajectories episode stage = mdp.episodeStepOfTrajectory (trajectories episode) stage

Source line 101 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.episodeBatchOfTrajectories_visitCount Compiled

Extracted batch visits are exactly the sum of trajectory contributions.

theorem episodeBatchOfTrajectories_visitCount (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).visitCount stage state action = ∑ episode, mdp.trajectoryVisitContribution stage state action (trajectories episode)

Source line 113 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.episodeBatchOfTrajectories_rewardSum Compiled

Extracted batch rewards are exactly the sum of trajectory contributions.

theorem episodeBatchOfTrajectories_rewardSum (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 = ∑ episode, mdp.trajectoryRewardContribution stage state action (trajectories episode)

Source line 128 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.episodeBatchOfTrajectories_transitionCount Compiled

Extracted transition counts are exactly trajectory-indicator sums.

theorem episodeBatchOfTrajectories_transitionCount (mdp : MDP State Action) (episodes : Nat) (trajectories : Fin episodes -> State × StepTrace Action State mdp.horizon) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : (mdp.episodeBatchOfTrajectories episodes trajectories).transitionCount stage state action nextState = ∑ episode, mdp.trajectoryTransitionContribution stage state action nextState (trajectories episode)

Source line 143 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.measurable_trajectoryVisitContribution Compiled

A fixed visit contribution is measurable on the generated trajectory.

theorem measurable_trajectoryVisitContribution (mdp : MDP State Action) (stage : Fin mdp.horizon) (state : State) (action : Action) : Measurable (mdp.trajectoryVisitContribution stage state action)

Source line 158 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.measurable_trajectoryRewardContribution Compiled

A fixed reward contribution is measurable on the generated trajectory.

theorem measurable_trajectoryRewardContribution (mdp : MDP State Action) (stage : Fin mdp.horizon) (state : State) (action : Action) : Measurable (mdp.trajectoryRewardContribution stage state action)

Source line 165 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.measurable_trajectoryTransitionContribution Compiled

A fixed transition contribution is measurable on the generated trajectory.

theorem measurable_trajectoryTransitionContribution (mdp : MDP State Action) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : Measurable (mdp.trajectoryTransitionContribution stage state action nextState)

Source line 172 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MarkovPolicy.iidTrajectoryFamilyMeasure Compiled

Finite iid product of the generated single-episode trajectory law.

noncomputable def iidTrajectoryFamilyMeasure {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) : Measure (Fin episodes -> State × StepTrace Action State mdp.horizon)

Source line 184 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MarkovPolicy.iidEpisodeBatchMeasure Compiled

Pushforward law of the empirical batch extracted from iid trajectories.

noncomputable def iidEpisodeBatchMeasure {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) : Measure (EpisodeBatch mdp episodes)

Source line 201 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iidTrajectoryFamilyMeasure_map_eval Compiled

Every product coordinate has the generated single-episode trajectory law.

theorem iidTrajectoryFamilyMeasure_map_eval {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} (episode : Fin episodes) : (policy.iidTrajectoryFamilyMeasure initialState episodes).map (Function.eval episode) = policy.trajectoryMeasure initialState

Source line 221 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iidEpisodeBatchMeasure_map_eval Compiled

Each episode/stage coordinate of the mapped batch has the corresponding pushforward of the genuine generated single-trajectory law.

theorem iidEpisodeBatchMeasure_map_eval {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} (episode : Fin episodes) (stage : Fin mdp.horizon) : (policy.iidEpisodeBatchMeasure initialState episodes).map (fun batch => batch episode stage) = (policy.trajectoryMeasure initialState).map (fun trajectory => mdp.episodeStepOfTrajectory trajectory stage)

Source line 239 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iIndepFun_episodeStepOfTrajectory Compiled

Stage records from distinct product coordinates are independent.

theorem iIndepFun_episodeStepOfTrajectory {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (stage : Fin mdp.horizon) : ProbabilityTheory.iIndepFun (fun episode trajectories => mdp.episodeStepOfTrajectory (trajectories episode) stage) (policy.iidTrajectoryFamilyMeasure initialState episodes)

Source line 273 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iIndepFun_iidEpisodeBatch_eval Compiled

Fixed-stage record coordinates are independent under the mapped batch law.

theorem iIndepFun_iidEpisodeBatch_eval {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (stage : Fin mdp.horizon) : ProbabilityTheory.iIndepFun (fun episode (batch : EpisodeBatch mdp episodes) => batch episode stage) (policy.iidEpisodeBatchMeasure initialState episodes)

Source line 288 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iIndepFun_iidEpisodeBatch_statistic Compiled

Measurable fixed-stage batch-record statistics are independent by episode.

theorem iIndepFun_iidEpisodeBatch_statistic {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (stage : Fin mdp.horizon) {Target : Type w} [MeasurableSpace Target] (statistic : EpisodeStep State Action -> Target) (hstatistic : Measurable statistic) : ProbabilityTheory.iIndepFun (fun episode (batch : EpisodeBatch mdp episodes) => statistic (batch episode stage)) (policy.iidEpisodeBatchMeasure initialState episodes)

Source line 342 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iIndepFun_episodeStatistic Compiled

Any measurable statistic of a fixed-stage record remains independent by episode.

theorem iIndepFun_episodeStatistic {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (stage : Fin mdp.horizon) {Target : Type w} [MeasurableSpace Target] (statistic : EpisodeStep State Action -> Target) (hstatistic : Measurable statistic) : ProbabilityTheory.iIndepFun (fun episode trajectories => statistic (mdp.episodeStepOfTrajectory (trajectories episode) stage)) (policy.iidTrajectoryFamilyMeasure initialState episodes)

Source line 360 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iIndepFun_trajectoryVisitContribution Compiled

Visit-count summands are independent across iid episode trajectories.

theorem iIndepFun_trajectoryVisitContribution {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (stage : Fin mdp.horizon) (state : State) (action : Action) : ProbabilityTheory.iIndepFun (fun episode trajectories => mdp.trajectoryVisitContribution stage state action (trajectories episode)) (policy.iidTrajectoryFamilyMeasure initialState episodes)

Source line 377 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iIndepFun_trajectoryRewardContribution Compiled

Reward-sum summands are independent across iid episode trajectories.

theorem iIndepFun_trajectoryRewardContribution {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (stage : Fin mdp.horizon) (state : State) (action : Action) : ProbabilityTheory.iIndepFun (fun episode trajectories => mdp.trajectoryRewardContribution stage state action (trajectories episode)) (policy.iidTrajectoryFamilyMeasure initialState episodes)

Source line 393 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iIndepFun_trajectoryTransitionContribution Compiled

Transition-count summands are independent across iid episode trajectories.

theorem iIndepFun_trajectoryTransitionContribution {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : ProbabilityTheory.iIndepFun (fun episode trajectories => mdp.trajectoryTransitionContribution stage state action nextState (trajectories episode)) (policy.iidTrajectoryFamilyMeasure initialState episodes)

Source line 409 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iidEpisodeBatch_stepLaw_and_independence Compiled

Route endpoint: generated batch coordinates have the correct marginal law and are independent across episodes at every fixed stage.

theorem iidEpisodeBatch_stepLaw_and_independence {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (stage : Fin mdp.horizon) : (forall episode : Fin episodes, (policy.iidEpisodeBatchMeasure initialState episodes).map (fun batch => batch episode stage) = (policy.trajectoryMeasure initialState).map (fun trajectory => mdp.episodeStepOfTrajectory trajectory stage)) /\ ProbabilityTheory.iIndepFun (fun episode (batch : EpisodeBatch mdp episodes) => batch episode stage) (policy.iidEpisodeBatchMeasure initialState episodes)

Source line 430 Chapter context: Finite-horizon RL