Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonIIDCountConcentration

# IID fixed-coordinate count concentration for finite-horizon RL This module applies the Mathlib-backed bounded-variable Hoeffding route to the fixed-policy iid episode-batch law. It proves two-sided confidence tails for one visit coordinate and one transition coordinate. Simultaneous finite coordinate events, random-denominator ratios, and adaptive episode policies remain downstream.

Module map

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

Imports

BanditRLProof.RL.FiniteHorizonIIDTrajectoryBatch, BanditRLProof.ConcentrationSubGaussian

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonIIDSimultaneousCountConfidence, BanditRLProof.RL.FiniteHorizonStageTransitionJointFactorization

Declarations

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

def BanditRLProof.FiniteHorizonRL.EpisodeStep.visitIndicator Compiled

Real indicator that one record visits a fixed state-action coordinate.

def visitIndicator (state : State) (action : Action) (step : EpisodeStep State Action) : Real

Source line 32 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.EpisodeStep.transitionIndicator Compiled

Real indicator that one record realizes a fixed transition coordinate.

def transitionIndicator (state : State) (action : Action) (nextState : State) (step : EpisodeStep State Action) : Real

Source line 37 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.EpisodeStep.measurable_visitIndicator Compiled

A fixed visit indicator is measurable on empirical records.

theorem measurable_visitIndicator (state : State) (action : Action) : Measurable (visitIndicator state action)

Source line 44 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.EpisodeStep.measurable_transitionIndicator Compiled

A fixed transition indicator is measurable on empirical records.

theorem measurable_transitionIndicator (state : State) (action : Action) (nextState : State) : Measurable (transitionIndicator state action nextState)

Source line 54 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.EpisodeStep.visitIndicator_mem_Icc Compiled

Every visit indicator lies in the Hoeffding interval `[0,1]`.

theorem visitIndicator_mem_Icc (state : State) (action : Action) (step : EpisodeStep State Action) : visitIndicator state action step ∈ Set.Icc (0 : Real) 1

Source line 68 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.EpisodeStep.transitionIndicator_mem_Icc Compiled

Every transition indicator lies in the Hoeffding interval `[0,1]`.

theorem transitionIndicator_mem_Icc (state : State) (action : Action) (nextState : State) (step : EpisodeStep State Action) : transitionIndicator state action nextState step ∈ Set.Icc (0 : Real) 1

Source line 78 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MarkovPolicy.stageVisitProbability Compiled

Genuine single-trajectory mean of a fixed stage/state/action visit indicator.

noncomputable def stageVisitProbability {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (stage : Fin mdp.horizon) (state : State) (action : Action) : Real

Source line 91 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MarkovPolicy.stageTransitionJointProbability Compiled

Genuine single-trajectory joint probability of a fixed `(state, action, nextState)` coordinate. This is not a conditional transition probability given the current state and action.

noncomputable def stageTransitionJointProbability {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : Real

Source line 104 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.stageVisitProbability_eq_measureReal Compiled

A stage visit mean is the real mass of its measurable trajectory event.

theorem stageVisitProbability_eq_measureReal {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (stage : Fin mdp.horizon) (state : State) (action : Action) : policy.stageVisitProbability initialState stage state action = (policy.trajectoryMeasure initialState).real {trajectory | (mdp.episodeStepOfTrajectory trajectory stage).state = state /\ (mdp.episodeStepOfTrajectory trajectory stage).action = action}

Source line 115 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.stageTransitionJointProbability_eq_measureReal Compiled

A stage joint-transition mean is the real mass of its measurable event.

theorem stageTransitionJointProbability_eq_measureReal {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : policy.stageTransitionJointProbability initialState stage state action nextState = (policy.trajectoryMeasure initialState).real {trajectory | (mdp.episodeStepOfTrajectory trajectory stage).state = state /\ (mdp.episodeStepOfTrajectory trajectory stage).action = action /\ (mdp.episodeStepOfTrajectory trajectory stage).nextState = nextState}

Source line 140 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.stageVisitProbability_mem_Icc Compiled

Every genuine stage visit probability lies in `[0,1]`.

theorem stageVisitProbability_mem_Icc {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (stage : Fin mdp.horizon) (state : State) (action : Action) : policy.stageVisitProbability initialState stage state action ∈ Set.Icc (0 : Real) 1

Source line 171 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.stageTransitionJointProbability_mem_Icc Compiled

Every genuine stage joint-transition probability lies in `[0,1]`.

theorem stageTransitionJointProbability_mem_Icc {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : policy.stageTransitionJointProbability initialState stage state action nextState ∈ Set.Icc (0 : Real) 1

Source line 181 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.stageTransitionJointProbability_le_stageVisitProbability Compiled

A fixed joint-transition probability is bounded by its visit probability.

theorem stageTransitionJointProbability_le_stageVisitProbability {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : policy.stageTransitionJointProbability initialState stage state action nextState ≤ policy.stageVisitProbability initialState stage state action

Source line 194 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.integral_visitIndicator_iidEpisodeBatchMeasure_eval Compiled

Every mapped episode coordinate has the common genuine visit-indicator mean.

theorem integral_visitIndicator_iidEpisodeBatchMeasure_eval {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} (episode : Fin episodes) (stage : Fin mdp.horizon) (state : State) (action : Action) : integral (policy.iidEpisodeBatchMeasure initialState episodes) (fun batch => EpisodeStep.visitIndicator state action (batch episode stage)) = policy.stageVisitProbability initialState stage state action

Source line 209 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.integral_transitionIndicator_iidEpisodeBatchMeasure_eval Compiled

Every mapped episode coordinate has the common genuine transition-indicator mean.

theorem integral_transitionIndicator_iidEpisodeBatchMeasure_eval {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} (episode : Fin episodes) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : integral (policy.iidEpisodeBatchMeasure initialState episodes) (fun batch => EpisodeStep.transitionIndicator state action nextState (batch episode stage)) = policy.stageTransitionJointProbability initialState stage state action nextState

Source line 245 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MarkovPolicy.centeredVisitIndicator Compiled

Centered visit indicator for one episode coordinate of a mapped batch.

noncomputable def centeredVisitIndicator {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} (stage : Fin mdp.horizon) (state : State) (action : Action) (episode : Fin episodes) (batch : EpisodeBatch mdp episodes) : Real

Source line 281 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MarkovPolicy.centeredTransitionIndicator Compiled

Centered transition indicator for one episode coordinate of a mapped batch.

noncomputable def centeredTransitionIndicator {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) (episode : Fin episodes) (batch : EpisodeBatch mdp episodes) : Real

Source line 290 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.sum_visitIndicator_eq_cast_visitCount Compiled

The named visit count is the Real sum of mapped record indicators.

theorem sum_visitIndicator_eq_cast_visitCount {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (stage : Fin mdp.horizon) (state : State) (action : Action) : (∑ episode : Fin episodes, EpisodeStep.visitIndicator state action (batch episode stage)) = (batch.visitCount stage state action : Real)

Source line 302 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.sum_transitionIndicator_eq_cast_transitionCount Compiled

The named transition count is the Real sum of mapped record indicators.

theorem sum_transitionIndicator_eq_cast_transitionCount {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : (∑ episode : Fin episodes, EpisodeStep.transitionIndicator state action nextState (batch episode stage)) = (batch.transitionCount stage state action nextState : Real)

Source line 314 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.sum_centeredVisitIndicator_eq_cast_visitCount_sub Compiled

Centered visit-indicator sums are exactly count minus episode-count times mean.

theorem sum_centeredVisitIndicator_eq_cast_visitCount_sub {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} (batch : EpisodeBatch mdp episodes) (stage : Fin mdp.horizon) (state : State) (action : Action) : (∑ episode : Fin episodes, policy.centeredVisitIndicator initialState stage state action episode batch) = (batch.visitCount stage state action : Real) - (episodes : Real) * policy.stageVisitProbability initialState stage state action

Source line 327 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.sum_centeredTransitionIndicator_eq_cast_transitionCount_sub Compiled

Centered transition-indicator sums are count minus episode-count times mean.

theorem sum_centeredTransitionIndicator_eq_cast_transitionCount_sub {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} (batch : EpisodeBatch mdp episodes) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : (∑ episode : Fin episodes, policy.centeredTransitionIndicator initialState stage state action nextState episode batch) = (batch.transitionCount stage state action nextState : Real) - (episodes : Real) * policy.stageTransitionJointProbability initialState stage state action nextState

Source line 350 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.measurable_cast_visitCount Compiled

A fixed visit count, coerced to `Real`, is measurable on episode batches.

theorem measurable_cast_visitCount {mdp : MDP State Action} {episodes : Nat} (stage : Fin mdp.horizon) (state : State) (action : Action) : Measurable fun batch : EpisodeBatch mdp episodes => (batch.visitCount stage state action : Real)

Source line 376 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.measurable_cast_transitionCount Compiled

A fixed transition count, coerced to `Real`, is measurable on episode batches.

theorem measurable_cast_transitionCount {mdp : MDP State Action} {episodes : Nat} (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : Measurable fun batch : EpisodeBatch mdp episodes => (batch.transitionCount stage state action nextState : Real)

Source line 391 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.measurable_visitCountDeviation Compiled

The fixed visit-count deviation from its genuine mean is measurable.

theorem measurable_visitCountDeviation {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} (stage : Fin mdp.horizon) (state : State) (action : Action) : Measurable fun batch : EpisodeBatch mdp episodes => (batch.visitCount stage state action : Real) - (episodes : Real) * policy.stageVisitProbability initialState stage state action

Source line 408 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.measurable_transitionCountDeviation Compiled

The fixed joint-transition-count deviation from its genuine mean is measurable.

theorem measurable_transitionCountDeviation {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : Measurable fun batch : EpisodeBatch mdp episodes => (batch.transitionCount stage state action nextState : Real) - (episodes : Real) * policy.stageTransitionJointProbability initialState stage state action nextState

Source line 421 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MarkovPolicy.iidBernoulliVarianceProxy Compiled

Total Hoeffding variance proxy for a finite iid family of `[0,1]` indicators.

noncomputable def iidBernoulliVarianceProxy (episodes : Nat) : NNReal

Source line 433 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iidBernoulliVarianceProxy_eq Compiled

The iid Bernoulli Hoeffding proxy is exactly one quarter per episode.

theorem iidBernoulliVarianceProxy_eq (episodes : Nat) : iidBernoulliVarianceProxy episodes = (episodes : NNReal) / 4

Source line 437 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iidBernoulliVarianceProxy_pos Compiled

A positive episode count gives a positive total Bernoulli variance proxy.

theorem iidBernoulliVarianceProxy_pos {episodes : Nat} (hepisodes : 0 < episodes) : 0 < ((iidBernoulliVarianceProxy episodes : NNReal) : Real)

Source line 443 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.centeredVisitIndicator_hasSubgaussianMGF Compiled

One centered visit coordinate has the `[0,1]` Hoeffding MGF proxy.

theorem centeredVisitIndicator_hasSubgaussianMGF {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} (stage : Fin mdp.horizon) (state : State) (action : Action) (episode : Fin episodes) : ProbabilityTheory.HasSubgaussianMGF (policy.centeredVisitIndicator initialState stage state action episode) (Concentration.intervalVarianceProxy 0 1) (policy.iidEpisodeBatchMeasure initialState episodes)

Source line 457 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.centeredTransitionIndicator_hasSubgaussianMGF Compiled

One centered transition coordinate has the `[0,1]` Hoeffding MGF proxy.

theorem centeredTransitionIndicator_hasSubgaussianMGF {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) (episode : Fin episodes) : ProbabilityTheory.HasSubgaussianMGF (policy.centeredTransitionIndicator initialState stage state action nextState episode) (Concentration.intervalVarianceProxy 0 1) (policy.iidEpisodeBatchMeasure initialState episodes)

Source line 488 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iIndepFun_centeredVisitIndicator Compiled

Centered visit coordinates remain independent under the mapped batch law.

theorem iIndepFun_centeredVisitIndicator {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (stage : Fin mdp.horizon) (state : State) (action : Action) : ProbabilityTheory.iIndepFun (policy.centeredVisitIndicator initialState stage state action) (policy.iidEpisodeBatchMeasure initialState episodes)

Source line 522 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iIndepFun_centeredTransitionIndicator Compiled

Centered transition coordinates remain independent under the mapped batch law.

theorem iIndepFun_centeredTransitionIndicator {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 (policy.centeredTransitionIndicator initialState stage state action nextState) (policy.iidEpisodeBatchMeasure initialState episodes)

Source line 538 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.measurableSet_visitCountBadEvent Compiled

The fixed visit-count two-sided bad event is measurable.

theorem measurableSet_visitCountBadEvent {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (stage : Fin mdp.horizon) (state : State) (action : Action) (delta : Real) : MeasurableSet {batch : EpisodeBatch mdp episodes | Concentration.subGaussianSumConfidenceRadius (iidBernoulliVarianceProxy episodes) delta ≤ |(batch.visitCount stage state action : Real) - (episodes : Real) * policy.stageVisitProbability initialState stage state action|}

Source line 555 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.measurableSet_transitionCountBadEvent Compiled

The fixed joint-transition-count two-sided bad event is measurable.

theorem measurableSet_transitionCountBadEvent {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) (delta : Real) : MeasurableSet {batch : EpisodeBatch mdp episodes | Concentration.subGaussianSumConfidenceRadius (iidBernoulliVarianceProxy episodes) delta ≤ |(batch.transitionCount stage state action nextState : Real) - (episodes : Real) * policy.stageTransitionJointProbability initialState stage state action nextState|}

Source line 572 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iidEpisodeBatch_visitCount_abs_tail_le Compiled

Two-sided delta confidence tail for one fixed visit-count coordinate under the mapped fixed-policy iid episode-batch law.

theorem iidEpisodeBatch_visitCount_abs_tail_le {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (hepisodes : 0 < episodes) (stage : Fin mdp.horizon) (state : State) (action : Action) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : (policy.iidEpisodeBatchMeasure initialState episodes) {batch | Concentration.subGaussianSumConfidenceRadius (iidBernoulliVarianceProxy episodes) delta <= |(batch.visitCount stage state action : Real) - (episodes : Real) * policy.stageVisitProbability initialState stage state action|} <= ENNReal.ofReal delta

Source line 594 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iidEpisodeBatch_transitionCount_abs_tail_le Compiled

Two-sided delta confidence tail for one fixed transition-count coordinate under the mapped fixed-policy iid episode-batch law.

theorem iidEpisodeBatch_transitionCount_abs_tail_le {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (hepisodes : 0 < episodes) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : (policy.iidEpisodeBatchMeasure initialState episodes) {batch | Concentration.subGaussianSumConfidenceRadius (iidBernoulliVarianceProxy episodes) delta <= |(batch.transitionCount stage state action nextState : Real) - (episodes : Real) * policy.stageTransitionJointProbability initialState stage state action nextState|} <= ENNReal.ofReal delta

Source line 629 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iidEpisodeBatch_visit_and_transition_count_abs_tail_le Compiled

Route endpoint: both named fixed-coordinate count tails are available under the same mapped iid episode-batch law. This conjunction does not union the two bad events or spend a shared failure budget.

theorem iidEpisodeBatch_visit_and_transition_count_abs_tail_le {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (hepisodes : 0 < episodes) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : (policy.iidEpisodeBatchMeasure initialState episodes) {batch | Concentration.subGaussianSumConfidenceRadius (iidBernoulliVarianceProxy episodes) delta <= |(batch.visitCount stage state action : Real) - (episodes : Real) * policy.stageVisitProbability initialState stage state action|} <= ENNReal.ofReal delta /\ (policy.iidEpisodeBatchMeasure initialState episodes) {batch | Concentration.subGaussianSumConfidenceRadius (iidBernoulliVarianceProxy episodes) delta <= |(batch.transitionCount stage state action nextState : Real) - (episodes : Real) * policy.stageTransitionJointProbability initialState stage state action nextState|} <= ENNReal.ofReal delta

Source line 667 Chapter context: Finite-horizon RL