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

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonIIDSimultaneousCountConfidence

# Simultaneous iid count confidence for finite-horizon RL This module puts every finite visit and joint-transition count coordinate into one index type and applies an equal-share finite union bound to the compiled fixed-coordinate tails. The route remains fixed-policy iid. It does not form visit-conditioned ratios or claim adaptive, anytime, or cumulative regret.

Module map

Declarations
20
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonIIDCountConcentration, BanditRLProof.ProbabilityUnionBound

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonIIDEligibleVisitCountPositivity

Declarations

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

inductive BanditRLProof.FiniteHorizonRL.CountCoordinate Compiled

Finite index of all visit and joint-transition count coordinates of an MDP.

inductive CountCoordinate (mdp : MDP State Action) where
Source line 31 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.CountCoordinate.equivVisitSumTransition Compiled

Explicit finite-sum presentation of the two coordinate families.

def equivVisitSumTransition (mdp : MDP State Action) : CountCoordinate mdp ≃ (Fin mdp.horizon × State × Action) ⊕ (Fin mdp.horizon × State × Action × State) where
Source line 40 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.countCoordinateCard Compiled

Number of visit and joint-transition coordinates in the simultaneous family.

def countCoordinateCard (mdp : MDP State Action) : Nat
Source line 63 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.countCoordinateCard_eq Compiled

The simultaneous family contains `H*S*A` visits and `H*S*A*S` transitions.

theorem countCoordinateCard_eq (mdp : MDP State Action) : countCoordinateCard mdp = mdp.horizon * Fintype.card State * Fintype.card Action + mdp.horizon * Fintype.card State * Fintype.card Action * Fintype.card State
Source line 70 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.simultaneousCountDelta Compiled

Equal confidence share assigned to each count coordinate.

noncomputable def simultaneousCountDelta (mdp : MDP State Action) (delta : Real) : Real
Source line 80 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.simultaneousCountConfidenceRadius Compiled

Common count radius after allocating the global confidence budget equally.

noncomputable def simultaneousCountConfidenceRadius (mdp : MDP State Action) (episodes : Nat) (delta : Real) : Real
Source line 85 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.CountCoordinate.deviation Compiled

Real count deviation selected by a visit or joint-transition coordinate.

noncomputable def deviation {mdp : MDP State Action} (coordinate : CountCoordinate mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} (batch : EpisodeBatch mdp episodes) : Real
Source line 94 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.CountCoordinate.measurable_deviation Compiled

Every selected count deviation is measurable on the mapped batch space.

theorem measurable_deviation {mdp : MDP State Action} (coordinate : CountCoordinate mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} : Measurable (coordinate.deviation policy initialState : EpisodeBatch mdp episodes → Real)
Source line 111 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.CountCoordinate.badEvent Compiled

Two-sided bad event for one selected coordinate at a supplied delta.

noncomputable def badEvent {mdp : MDP State Action} (coordinate : CountCoordinate mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (coordinateDelta : Real) : Set (EpisodeBatch mdp episodes)
Source line 126 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.CountCoordinate.measurableSet_badEvent Compiled

Every selected fixed-coordinate bad event is measurable.

theorem measurableSet_badEvent {mdp : MDP State Action} (coordinate : CountCoordinate mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (coordinateDelta : Real) : MeasurableSet (coordinate.badEvent policy initialState episodes coordinateDelta)
Source line 138 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.measure_countCoordinate_badEvent_le Compiled

The compiled marginal tail dispatches over the finite coordinate type.

theorem measure_countCoordinate_badEvent_le {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (hepisodes : 0 < episodes) (coordinate : CountCoordinate mdp) (coordinateDelta : Real) (hdelta : 0 < coordinateDelta) (hdelta_le_one : coordinateDelta ≤ 1) : (policy.iidEpisodeBatchMeasure initialState episodes) (coordinate.badEvent policy initialState episodes coordinateDelta) ≤ ENNReal.ofReal coordinateDelta
Source line 153 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MarkovPolicy.simultaneousCountBadEvent Compiled

Union of every visit and joint-transition count bad event.

noncomputable def simultaneousCountBadEvent {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (delta : Real) : Set (EpisodeBatch mdp episodes)
Source line 176 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.measurableSet_simultaneousCountBadEvent Compiled

The simultaneous count bad event is measurable.

theorem measurableSet_simultaneousCountBadEvent {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (delta : Real) : MeasurableSet (policy.simultaneousCountBadEvent initialState episodes delta)
Source line 186 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.simultaneousCountDelta_pos Compiled

A nonempty coordinate family receives a positive equal delta share.

theorem simultaneousCountDelta_pos {mdp : MDP State Action} (hcoordinate : Nonempty (CountCoordinate mdp)) {delta : Real} (hdelta : 0 < delta) : 0 < simultaneousCountDelta mdp delta
Source line 200 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.simultaneousCountDelta_le_one Compiled

A global delta at most one gives every nonempty-family share at most one.

theorem simultaneousCountDelta_le_one {mdp : MDP State Action} (hcoordinate : Nonempty (CountCoordinate mdp)) {delta : Real} (hdelta : 0 < delta) (hdelta_le_one : delta ≤ 1) : simultaneousCountDelta mdp delta ≤ 1
Source line 212 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iidEpisodeBatch_simultaneousCountBadEvent_le Compiled

All finite visit and joint-transition count deviations share one global delta budget. When the coordinate family is empty (in particular at horizon zero), the bad union is empty and no positive-horizon premise is needed.

theorem iidEpisodeBatch_simultaneousCountBadEvent_le {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) : (policy.iidEpisodeBatchMeasure initialState episodes) (policy.simultaneousCountBadEvent initialState episodes delta) ≤ ENNReal.ofReal delta
Source line 228 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.countCoordinate_abs_deviation_lt_of_not_mem_simultaneousCountBadEvent Compiled

Outside the simultaneous union, every indexed deviation is below its radius.

theorem countCoordinate_abs_deviation_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) (coordinate : CountCoordinate mdp) : |coordinate.deviation policy initialState batch| < simultaneousCountConfidenceRadius mdp episodes delta
Source line 271 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.visitCount_abs_deviation_lt_of_not_mem_simultaneousCountBadEvent Compiled

Visit-count specialization of the simultaneous good-side bound.

theorem visitCount_abs_deviation_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) (stage : Fin mdp.horizon) (state : State) (action : Action) : |(batch.visitCount stage state action : Real) - (episodes : Real) * policy.stageVisitProbability initialState stage state action| < simultaneousCountConfidenceRadius mdp episodes delta
Source line 290 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.transitionCount_abs_deviation_lt_of_not_mem_simultaneousCountBadEvent Compiled

Joint-transition-count specialization of the simultaneous good-side bound.

theorem transitionCount_abs_deviation_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) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : |(batch.transitionCount stage state action nextState : Real) - (episodes : Real) * policy.stageTransitionJointProbability initialState stage state action nextState| < simultaneousCountConfidenceRadius mdp episodes delta
Source line 307 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.iidEpisodeBatch_simultaneous_count_confidence Compiled

Route endpoint: one global-delta bad union and all coordinatewise good-side bounds under the same mapped fixed-policy iid episode-batch law.

theorem iidEpisodeBatch_simultaneous_count_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) : (policy.iidEpisodeBatchMeasure initialState episodes) (policy.simultaneousCountBadEvent initialState episodes delta) ≤ ENNReal.ofReal delta ∧ ∀ batch ∉ policy.simultaneousCountBadEvent initialState episodes delta, ∀ coordinate : CountCoordinate mdp, |coordinate.deviation policy initialState batch| < simultaneousCountConfidenceRadius mdp episodes delta
Source line 328 Chapter context: Finite-horizon RL