Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonIIDEligibleEmpiricalTransitionConfidence
# Eligible empirical transition confidence for finite-horizon iid batches This module combines the compiled simultaneous visit/joint-count event, eligible positive denominators, and generated population-law factorization. For every eligible state-action-stage coordinate, the empirical singleton transition mass is within `2 * countRadius / visitCount` of the true transition kernel singleton mass. The bundled endpoint reuses the existing global-delta event; it does not spend another failure budget or add reward confidence.
Module map
Imports
BanditRLProof.RL.FiniteHorizonEmpiricalModel, BanditRLProof.RL.FiniteHorizonIIDEligibleVisitCountPositivity, BanditRLProof.RL.FiniteHorizonStageTransitionJointFactorization
Imported by
BanditRLProof, BanditRLProof.RL.FiniteHorizonIIDGeneratedEmpiricalRewardExactness
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.FiniteHorizonRL.MarkovPolicy.empiricalTransitionMass_abs_sub_transition_lt_of_not_mem_simultaneousCountBadEvent
Compiled
A single eligible coordinate inherits a strict empirical transition-mass bound from the simultaneous visit and joint-transition count deviations.
theorem empiricalTransitionMass_abs_sub_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) (defaultState : State) (coordinate : VisitCoordinate mdp) (hmargin : simultaneousCountConfidenceRadius mdp episodes delta < coordinate.expectedCount policy initialState episodes) (nextState : State) : |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)
theorem
BanditRLProof.FiniteHorizonRL.MarkovPolicy.iidEpisodeBatch_eligible_empiricalTransitionMass_confidence
Compiled
Route endpoint: the existing measurable simultaneous-count event has global delta mass, and outside it all eligible empirical transition singleton masses obey the positive-random-denominator confidence bound simultaneously.
theorem iidEpisodeBatch_eligible_empiricalTransitionMass_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.simultaneousCountBadEvent initialState episodes delta, ∀ coordinate ∈ eligible, ∀ 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)