Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonIIDEligibleVisitCountPositivity
# Eligible positive visit counts for finite-horizon iid batches This module turns the compiled simultaneous visit-count deviation into a positive-denominator guarantee on an arbitrary finite set of eligible visit coordinates. Eligibility carries the necessary strict expected-count margin; unreachable coordinates are not assigned a false positivity conclusion.
Module map
Imports
BanditRLProof.RL.FiniteHorizonIIDSimultaneousCountConfidence
Imported by
BanditRLProof, BanditRLProof.RL.FiniteHorizonIIDEligibleEmpiricalTransitionConfidence
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
structure
BanditRLProof.FiniteHorizonRL.VisitCoordinate
Compiled
One stage/state/action coordinate whose empirical visit count may be used as a denominator.
structure VisitCoordinate (mdp : MDP State Action) where
def
BanditRLProof.FiniteHorizonRL.VisitCoordinate.count
Compiled
Realized visit count selected by a visit coordinate.
def count {mdp : MDP State Action} (coordinate : VisitCoordinate mdp) {episodes : Nat} (batch : EpisodeBatch mdp episodes) : Nat
def
BanditRLProof.FiniteHorizonRL.VisitCoordinate.expectedCount
Compiled
Genuine expected visit count under the fixed-policy single-episode law.
noncomputable def expectedCount {mdp : MDP State Action} (coordinate : VisitCoordinate mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) : Real
def
BanditRLProof.FiniteHorizonRL.VisitCoordinate.zeroCountEvent
Compiled
Event that the selected visit coordinate has zero realized count.
def zeroCountEvent {mdp : MDP State Action} (coordinate : VisitCoordinate mdp) (episodes : Nat) : Set (EpisodeBatch mdp episodes)
theorem
BanditRLProof.FiniteHorizonRL.VisitCoordinate.measurableSet_zeroCountEvent
Compiled
A selected zero visit-count event is measurable.
theorem measurableSet_zeroCountEvent {mdp : MDP State Action} (coordinate : VisitCoordinate mdp) (episodes : Nat) : MeasurableSet (coordinate.zeroCountEvent episodes)
def
BanditRLProof.FiniteHorizonRL.eligibleZeroVisitCountEvent
Compiled
Union of zero-count events over a finite caller-selected coordinate set.
def eligibleZeroVisitCountEvent {mdp : MDP State Action} (episodes : Nat) (eligible : Finset (VisitCoordinate mdp)) : Set (EpisodeBatch mdp episodes)
theorem
BanditRLProof.FiniteHorizonRL.measurableSet_eligibleZeroVisitCountEvent
Compiled
The finite eligible zero-count union is measurable.
theorem measurableSet_eligibleZeroVisitCountEvent {mdp : MDP State Action} (episodes : Nat) (eligible : Finset (VisitCoordinate mdp)) : MeasurableSet (eligibleZeroVisitCountEvent episodes eligible)
theorem
BanditRLProof.FiniteHorizonRL.visitCoordinate_count_pos_of_not_mem_eligibleZeroVisitCountEvent
Compiled
Outside the eligible zero-count union, every selected Nat count is positive.
theorem visitCoordinate_count_pos_of_not_mem_eligibleZeroVisitCountEvent {mdp : MDP State Action} {episodes : Nat} (eligible : Finset (VisitCoordinate mdp)) (batch : EpisodeBatch mdp episodes) (hbatch : batch ∉ eligibleZeroVisitCountEvent episodes eligible) (coordinate : VisitCoordinate mdp) (hcoordinate : coordinate ∈ eligible) : 0 < coordinate.count batch
theorem
BanditRLProof.FiniteHorizonRL.MarkovPolicy.visitCoordinate_count_pos_of_not_mem_simultaneousCountBadEvent
Compiled
A strict expected-count margin turns the simultaneous deviation bound into a positive realized visit count.
theorem visitCoordinate_count_pos_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 : VisitCoordinate mdp) (hmargin : simultaneousCountConfidenceRadius mdp episodes delta < coordinate.expectedCount policy initialState episodes) : 0 < coordinate.count batch
theorem
BanditRLProof.FiniteHorizonRL.MarkovPolicy.eligibleZeroVisitCountEvent_subset_simultaneousCountBadEvent
Compiled
Under the eligible margins, every eligible zero-count outcome lies in the already-budgeted simultaneous bad event.
theorem eligibleZeroVisitCountEvent_subset_simultaneousCountBadEvent {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} {delta : Real} (eligible : Finset (VisitCoordinate mdp)) (hmargin : ∀ coordinate ∈ eligible, simultaneousCountConfidenceRadius mdp episodes delta < coordinate.expectedCount policy initialState episodes) : eligibleZeroVisitCountEvent episodes eligible ⊆ policy.simultaneousCountBadEvent initialState episodes delta
theorem
BanditRLProof.FiniteHorizonRL.MarkovPolicy.iidEpisodeBatch_eligibleZeroVisitCountEvent_le
Compiled
The eligible zero-count union inherits the simultaneous global-delta tail.
theorem iidEpisodeBatch_eligibleZeroVisitCountEvent_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) (eligible : Finset (VisitCoordinate mdp)) (hmargin : ∀ coordinate ∈ eligible, simultaneousCountConfidenceRadius mdp episodes delta < coordinate.expectedCount policy initialState episodes) : (policy.iidEpisodeBatchMeasure initialState episodes) (eligibleZeroVisitCountEvent episodes eligible) ≤ ENNReal.ofReal delta
theorem
BanditRLProof.FiniteHorizonRL.MarkovPolicy.iidEpisodeBatch_eligible_visit_count_positivity
Compiled
Route endpoint: eligible zero counts have global-delta probability, and every eligible denominator is positive outside that exact zero-count event. The named subset theorem separately embeds this event in the compiled simultaneous bad event.
theorem iidEpisodeBatch_eligible_visit_count_positivity {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) (eligible : Finset (VisitCoordinate mdp)) (hmargin : ∀ coordinate ∈ eligible, simultaneousCountConfidenceRadius mdp episodes delta < coordinate.expectedCount policy initialState episodes) : MeasurableSet (eligibleZeroVisitCountEvent episodes eligible) ∧ (policy.iidEpisodeBatchMeasure initialState episodes) (eligibleZeroVisitCountEvent episodes eligible) ≤ ENNReal.ofReal delta ∧ ∀ batch ∉ eligibleZeroVisitCountEvent episodes eligible, ∀ coordinate ∈ eligible, 0 < coordinate.count batch