BanditRLProof.RL.FiniteHorizonExploratoryPathSupportReachability

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

theorem trajectoryStateAt_zero (mdp : MDP State Action) (trajectory : State × StepTrace Action State mdp.horizon) (hhorizon : 0 < mdp.horizon) : mdp.trajectoryStateAt trajectory ⟨0, hhorizon⟩ = trajectory.1

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

theorem episodeStepOfTrajectory_nextState_eq_trajectoryStateAt_succ (mdp : MDP State Action) (trajectory : State × StepTrace Action State mdp.horizon) (stage : Nat) (hstage : stage + 1 < mdp.horizon) : (mdp.episodeStepOfTrajectory trajectory ⟨stage, by omega⟩).nextState = mdp.trajectoryStateAt trajectory ⟨stage + 1, hstage⟩

The generated state mass at stage zero is the initial singleton mass.

theorem stageStateProbability_zero {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (hhorizon : 0 < mdp.horizon) (state : State) : policy.stageStateProbability initialState ⟨0, hhorizon⟩ state = initialState.real {state}

A selected transition event is contained in its successor state event.

theorem stageTransitionJointProbability_le_stageStateProbability_succ {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (stage : Nat) (hstage : stage + 1 < mdp.horizon) (state : State) (action : Action) (nextState : State) : policy.stageTransitionJointProbability initialState ⟨stage, by omega⟩ state action nextState <= policy.stageStateProbability initialState ⟨stage + 1, hstage⟩ nextState

One explicit predecessor path for each successor-stage state, together with nonnegative singleton-mass floors along those paths.

structure ExploratoryPathSupport (mdp : MDP State Action) (initialState : Measure State) where

Recursive state floor along the selected predecessor paths.

noncomputable def exploratoryPathStateLowerNat {mdp : MDP State Action} {initialState : Measure State} (support : ExploratoryPathSupport mdp initialState) (explorationRate : NNReal) : (stage : Nat) -> stage < mdp.horizon -> State -> Real | 0, _hstage, state => support.initialFloor state | stage + 1, hstage, state => exploratoryPathStateLowerNat support explorationRate stage (by omega) (support.predecessorState ⟨stage + 1, hstage⟩ state) * exploratoryActionProbabilityFloor Action explorationRate * support.transitionFloor ⟨stage + 1, hstage⟩ state /-- The selected-path lower envelope indexed by valid chronological stages. -/ noncomputable def exploratoryPathStateLower {mdp : MDP State Action} {initialState : Measure State} (support : ExploratoryPathSupport mdp initialState) (explorationRate : NNReal) (stage : Fin mdp.horizon) (state : State) : Real

The selected-path lower envelope indexed by valid chronological stages.

noncomputable def exploratoryPathStateLower {mdp : MDP State Action} {initialState : Measure State} (support : ExploratoryPathSupport mdp initialState) (explorationRate : NNReal) (stage : Fin mdp.horizon) (state : State) : Real

Every recursively constructed path-support floor is nonnegative.

theorem exploratoryPathStateLowerNat_nonneg {mdp : MDP State Action} {initialState : Measure State} (support : ExploratoryPathSupport mdp initialState) (explorationRate : NNReal) : forall (stage : Nat) (hstage : stage < mdp.horizon) (state : State), 0 <= exploratoryPathStateLowerNat support explorationRate stage hstage state

The Fin-indexed selected-path envelope is nonnegative.

theorem exploratoryPathStateLower_nonneg {mdp : MDP State Action} {initialState : Measure State} (support : ExploratoryPathSupport mdp initialState) (explorationRate : NNReal) (stage : Fin mdp.horizon) (state : State) : 0 <= exploratoryPathStateLower support explorationRate stage state

Every exploratory table policy dominates the same explicit path-support state envelope, independently of the table's deterministic center.

theorem exploratoryPathStateLower_le_stageStateProbability {mdp : MDP State Action} (table : DeterministicMarkovPolicyTable mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (support : ExploratoryPathSupport mdp initialState) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (stage : Fin mdp.horizon) (state : State) : exploratoryPathStateLower support explorationRate stage state <= (table.exploratoryPolicy explorationRate hexplorationRate).stageStateProbability initialState stage state

Every policy selected by the exploratory source shares the path-support floor.

theorem exploratorySource_sourceStateReachability_of_pathSupport {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (transitionBonus : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (rounds : Nat) (support : ExploratoryPathSupport mdp initialState) : let behaviorSource := exploratorySource mdp initialState episodes initialTable defaultState transitionBonus explorationRate hexplorationRate SourceStateReachability behaviorSource rounds (exploratoryPathStateLower support explorationRate)

Explicit path support constructs the exact adaptive source calibration.

theorem exploratorySource_sourceCalibration_of_pathSupport {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) (support : ExploratoryPathSupport mdp initialState) (hmargin : ExploratoryStateCountMargin mdp episodes (multiBatchLocalDelta rounds delta) explorationRate (exploratoryPathStateLower support explorationRate)) (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: explicit initial and transition path support replaces the abstract source state-reachability premise in the adaptive global theorem.

theorem exploratorySource_trajectoryMeasure_allCoordinateConfidence_optimism_and_recommendedExpectedRegret_of_pathSupport {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) (support : ExploratoryPathSupport mdp initialState) (hmargin : ExploratoryStateCountMargin mdp episodes (multiBatchLocalDelta rounds delta) explorationRate (exploratoryPathStateLower support explorationRate)) (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