BanditRLProof.RL.FiniteHorizonIIDSimultaneousCountConfidence

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

inductive CountCoordinate (mdp : MDP State Action) where

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

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

def countCoordinateCard (mdp : MDP State Action) : Nat

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

Equal confidence share assigned to each count coordinate.

noncomputable def simultaneousCountDelta (mdp : MDP State Action) (delta : Real) : Real

Common count radius after allocating the global confidence budget equally.

noncomputable def simultaneousCountConfidenceRadius (mdp : MDP State Action) (episodes : Nat) (delta : Real) : Real

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

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)

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)

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)

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

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)

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)

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

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

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

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

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

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

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