BanditRLProof.RL.FiniteHorizonExploratoryReachabilityCalibration

Real probability floor contributed by uniform exploration.

noncomputable def exploratoryActionProbabilityFloor (Action : Type v) [Fintype Action] (explorationRate : NNReal) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem exploratoryActionProbabilityFloor_nonneg (explorationRate : NNReal) : 0 <= exploratoryActionProbabilityFloor Action explorationRate

Every generated stage-state probability is nonnegative.

theorem stageStateProbability_nonneg {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (stage : Fin mdp.horizon) (state : State) : 0 <= policy.stageStateProbability initialState stage state

The transition-coordinate cover field retained by empirical calibration.

def TransitionBonusCover {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (delta rewardBound transitionBonus : Real) : Prop

The ENNReal exploratory PMF floor as a Real inequality.

theorem exploratoryActionProbabilityFloor_le_exploratoryActionPMF_toReal {mdp : MDP State Action} (table : DeterministicMarkovPolicyTable mdp) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (stage : Fin mdp.horizon) (state : State) (action : Action) : exploratoryActionProbabilityFloor Action explorationRate <= (table.exploratoryActionPMF explorationRate hexplorationRate stage state action).toReal

The exploratory Markov kernel inherits the Real singleton floor.

theorem exploratoryActionProbabilityFloor_le_actionKernel_real {mdp : MDP State Action} (table : DeterministicMarkovPolicyTable mdp) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (stage : Fin mdp.horizon) (state : State) (action : Action) : exploratoryActionProbabilityFloor Action explorationRate <= ((table.exploratoryPolicy explorationRate hexplorationRate).actionKernel stage state {action}).toReal

State reachability times the exploratory action floor lower-bounds visits.

theorem stateLower_mul_exploratoryActionProbabilityFloor_le_stageVisitProbability {mdp : MDP State Action} (table : DeterministicMarkovPolicyTable mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (stateLower : Fin mdp.horizon -> State -> Real) (hstateLower : forall stage state, stateLower stage state <= (table.exploratoryPolicy explorationRate hexplorationRate).stageStateProbability initialState stage state) (stage : Fin mdp.horizon) (state : State) (action : Action) : stateLower stage state * exploratoryActionProbabilityFloor Action explorationRate <= (table.exploratoryPolicy explorationRate hexplorationRate).stageVisitProbability initialState stage state action

The state/action floor also lower-bounds the genuine expected visit count.

theorem stateLower_expectedCount_le {mdp : MDP State Action} (table : DeterministicMarkovPolicyTable mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (stateLower : Fin mdp.horizon -> State -> Real) (hstateLower : forall stage state, stateLower stage state <= (table.exploratoryPolicy explorationRate hexplorationRate).stageStateProbability initialState stage state) (coordinate : VisitCoordinate mdp) : (episodes : Real) * (stateLower coordinate.stage coordinate.state * exploratoryActionProbabilityFloor Action explorationRate) <= coordinate.expectedCount (table.exploratoryPolicy explorationRate hexplorationRate) initialState episodes

Strict count margin implied by a state lower envelope and exploration.

def ExploratoryStateCountMargin (mdp : MDP State Action) (episodes : Nat) (delta : Real) (explorationRate : NNReal) (stateLower : Fin mdp.horizon -> State -> Real) : Prop

Reachability plus the unchanged cover constructs policy-local calibration.

def empiricalOptimisticCalibration_exploratoryPolicy_of_stateReachability {mdp : MDP State Action} (table : DeterministicMarkovPolicyTable mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (delta rewardBound transitionBonus : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (stateLower : Fin mdp.horizon -> State -> Real) (hstateLower : forall stage state, stateLower stage state <= (table.exploratoryPolicy explorationRate hexplorationRate).stageStateProbability initialState stage state) (hmargin : ExploratoryStateCountMargin mdp episodes delta explorationRate stateLower) (hcover : (table.exploratoryPolicy explorationRate hexplorationRate).TransitionBonusCover initialState episodes delta rewardBound transitionBonus) : (table.exploratoryPolicy explorationRate hexplorationRate).EmpiricalOptimisticCalibration initialState episodes delta rewardBound transitionBonus where

State-only reachability envelope for every batch-generating source policy.

def SourceStateReachability {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (stateLower : Fin mdp.horizon -> State -> Real) : Prop

Transition-bonus cover for every batch-generating source policy.

def SourceTransitionBonusCover {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (delta rewardBound transitionBonus : Real) : Prop

State reachability and exploration discharge every expected-count margin in the exact adaptive calibration contract; the transition-bonus cover is preserved.

theorem exploratorySource_sourceCalibration_of_stateReachability {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (rewardBound transitionBonus delta : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (rounds : Nat) (stateLower : Fin mdp.horizon -> State -> Real) (hmargin : ExploratoryStateCountMargin mdp episodes (multiBatchLocalDelta rounds delta) explorationRate stateLower) (hreachability : let behaviorSource := exploratorySource mdp initialState episodes initialTable defaultState transitionBonus explorationRate hexplorationRate SourceStateReachability behaviorSource rounds stateLower) (hcover : let behaviorSource := exploratorySource mdp initialState episodes initialTable defaultState transitionBonus explorationRate hexplorationRate SourceTransitionBonusCover behaviorSource rounds (multiBatchLocalDelta rounds delta) rewardBound transitionBonus) : let behaviorSource := exploratorySource mdp initialState episodes initialTable defaultState transitionBonus explorationRate hexplorationRate SourceCalibration behaviorSource rounds delta rewardBound transitionBonus

Route endpoint: state reachability plus uniform exploration discharges the calibration premise of the adaptive confidence, optimism, and recommended expected-regret theorem.

theorem exploratorySource_trajectoryMeasure_allCoordinateConfidence_optimism_and_recommendedExpectedRegret_of_stateReachability {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (rewardBound transitionBonus : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (htransitionBonus_nonneg : 0 <= transitionBonus) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (stateLower : Fin mdp.horizon -> State -> Real) (hmargin : ExploratoryStateCountMargin mdp episodes (multiBatchLocalDelta rounds delta) explorationRate stateLower) (hreachability : let behaviorSource := exploratorySource mdp initialState episodes initialTable defaultState transitionBonus explorationRate hexplorationRate SourceStateReachability behaviorSource rounds stateLower) (hcover : let behaviorSource := exploratorySource mdp initialState episodes initialTable defaultState transitionBonus explorationRate hexplorationRate SourceTransitionBonusCover behaviorSource rounds (multiBatchLocalDelta rounds delta) rewardBound transitionBonus) : let behaviorSource := exploratorySource mdp initialState episodes initialTable defaultState transitionBonus explorationRate hexplorationRate let bad := behaviorSource.adaptiveSimultaneousCountBadEvent rounds delta MeasurableSet bad /\ behaviorSource.trajectoryMeasure bad <= ENNReal.ofReal delta /\ forall trajectory, trajectory ∉ bad -> (forall round : Fin rounds, forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= (adaptiveEmpiricalOptimisticPlanAt (mdp