BanditRLProof.RL.FiniteHorizonStochasticRewardIIDExplicitCalibration

Uniform reward-mean radius obtained from one common expected-count floor.

noncomputable def uniformFloorStochasticRewardCoordinateRadius (mdp : MDP State Action) (episodes : Nat) (varianceProxy : NNReal) (countDelta rewardDelta visitFloor : Real) : Real

The uniform reward radius is nonnegative under the strict count margin.

theorem uniformFloorStochasticRewardCoordinateRadius_nonneg {mdp : MDP State Action} {episodes : Nat} {varianceProxy : NNReal} {countDelta rewardDelta visitFloor : Real} (hmargin : simultaneousCountConfidenceRadius mdp episodes countDelta < (episodes : Real) * visitFloor) : 0 <= uniformFloorStochasticRewardCoordinateRadius mdp episodes varianceProxy countDelta rewardDelta visitFloor

The explicit transition budget paired with the uniform reward budget.

def uniformFloorStochasticTransitionBudget (rewardBound rewardBudget : Real) : Real

A common expected-count floor dominates every coordinate reward radius.

theorem expectedCountRewardCoordinateRadius_le_uniformFloor (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (varianceProxy : NNReal) (countDelta rewardDelta visitFloor : Real) (hmargin : simultaneousCountConfidenceRadius mdp episodes countDelta < (episodes : Real) * visitFloor) (hcountFloor : forall coordinate : VisitCoordinate mdp, (episodes : Real) * visitFloor <= coordinate.expectedCount policy initialState episodes) (coordinate : VisitCoordinate mdp) : source.expectedCountRewardCoordinateRadius policy initialState episodes varianceProxy countDelta rewardDelta coordinate <= uniformFloorStochasticRewardCoordinateRadius mdp episodes varianceProxy countDelta rewardDelta visitFloor

The common count floor and half-contraction condition cover every stochastic transition-radius/value-envelope sum with the explicit transition budget.

theorem stochasticTransitionCover_of_uniformExpectedCountFloor {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (varianceProxy : NNReal) (countDelta rewardDelta visitFloor rewardBound : Real) (hmargin : simultaneousCountConfidenceRadius mdp episodes countDelta < (episodes : Real) * visitFloor) (hcountFloor : forall coordinate : VisitCoordinate mdp, (episodes : Real) * visitFloor <= coordinate.expectedCount policy initialState episodes) (hrewardBound_nonneg : 0 <= rewardBound) (hcontraction : (Fintype.card State : Real) * uniformFloorTransitionCoordinateRadius mdp episodes countDelta visitFloor * (mdp.horizon : Real) <= 1 / 2) : let rewardBudget := uniformFloorStochasticRewardCoordinateRadius mdp episodes varianceProxy countDelta rewardDelta visitFloor let transitionBudget := uniformFloorStochasticTransitionBudget rewardBound rewardBudget forall (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) (action : Action), (∑ nextState, policy.expectedCountTransitionCoordinateRadius initialState episodes countDelta (mdp.decisionStageRemaining remaining hremaining) state action nextState * stochasticEmpiricalFiniteBatchValueEnvelope rewardBound rewardBudget transitionBudget remaining) <= transitionBudget

Fixed-policy route endpoint with every coordinate margin and cover produced by one common expected-count floor and one scalar half-contraction condition.

theorem iidStochasticTrajectoryFamilyMeasure_allCoordinate_optimism_and_expectedRegret_of_uniformExpectedCountFloor [StandardBorelSpace State] [StandardBorelSpace Action] {mdp : MDP State Action} (source : mdp.MeanCompatibleRewardKernel) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (hepisodes : 0 < episodes) (varianceProxy : NNReal) (law : source.UniformSubgaussianRewardLaw varianceProxy) (htotal : 0 < ((((episodes : NNReal) * varianceProxy : NNReal) : Real))) (countDelta : Real) (hcountDelta : 0 < countDelta) (hcountDelta_le_one : countDelta <= 1) (rewardDelta : Real) (hrewardDelta : 0 < rewardDelta) (hrewardDelta_le_one : rewardDelta <= 1) (defaultState : State) (rewardBound visitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (hmargin : simultaneousCountConfidenceRadius mdp episodes countDelta < (episodes : Real) * visitFloor) (hcountFloor : forall coordinate : VisitCoordinate mdp, (episodes : Real) * visitFloor <= coordinate.expectedCount policy initialState episodes) (hcontraction : (Fintype.card State : Real) * uniformFloorTransitionCoordinateRadius mdp episodes countDelta visitFloor * (mdp.horizon : Real) <= 1 / 2) : let rewardBudget := uniformFloorStochasticRewardCoordinateRadius mdp episodes varianceProxy countDelta rewardDelta visitFloor let transitionBudget := uniformFloorStochasticTransitionBudget rewardBound rewardBudget let event := source.stochasticAllCoordinateEmpiricalModelBadEvent policy initialState episodes varianceProxy countDelta rewardDelta MeasurableSet event /\ (source.iidStochasticTrajectoryFamilyMeasure policy initialState episodes) event <= ENNReal.ofReal countDelta + ENNReal.ofReal rewardDelta /\ forall trajectories, trajectories ∉ event -> let model := mdp.stochasticAllCoordinateEmpiricalFiniteBatchModel episodes (mdp.sampledEpisodeBatchOfStochasticTrajectories episodes trajectories) defaultState rewardBudget transitionBudget (forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= model.plan.upperValueRemaining mdp.horizon le_rfl state) /\ model.plan.optimisticPolicy.expectedRegret initialState <= model.plan.optimisticPolicy.occupancySumRemaining (fun remaining hremaining state => 2 * model.plan.selectedRadiusRemaining remaining hremaining state) mdp.horizon le_rfl initialState

Practical endpoint: exploratory path support constructs the common count floor, then the explicit stochastic calibration yields confidence and recommended expected regret for the exploratory policy's sampled-reward empirical model.

theorem exploratoryPolicy_iidStochasticTrajectoryFamilyMeasure_allCoordinate_optimism_and_expectedRegret_of_pathSupport_explicitCalibration [StandardBorelSpace State] [StandardBorelSpace Action] {mdp : MDP State Action} (table : DeterministicMarkovPolicyTable mdp) (source : mdp.MeanCompatibleRewardKernel) (initialState : Measure State) [IsProbabilityMeasure initialState] (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (episodes : Nat) (hepisodes : 0 < episodes) (varianceProxy : NNReal) (law : source.UniformSubgaussianRewardLaw varianceProxy) (htotal : 0 < ((((episodes : NNReal) * varianceProxy : NNReal) : Real))) (countDelta : Real) (hcountDelta : 0 < countDelta) (hcountDelta_le_one : countDelta <= 1) (rewardDelta : Real) (hrewardDelta : 0 < rewardDelta) (hrewardDelta_le_one : rewardDelta <= 1) (defaultState : State) (rewardBound : Real) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (support : ExploratoryPathSupport mdp initialState) (visitFloor : Real) (hfloor : ExploratoryPathUniformVisitFloor support explorationRate visitFloor) (hmargin : simultaneousCountConfidenceRadius mdp episodes countDelta < (episodes : Real) * visitFloor) (hcontraction : (Fintype.card State : Real) * uniformFloorTransitionCoordinateRadius mdp episodes countDelta visitFloor * (mdp.horizon : Real) <= 1 / 2) : let policy := table.exploratoryPolicy explorationRate hexplorationRate let rewardBudget := uniformFloorStochasticRewardCoordinateRadius mdp episodes varianceProxy countDelta rewardDelta visitFloor let transitionBudget := uniformFloorStochasticTransitionBudget rewardBound rewardBudget let event := source.stochasticAllCoordinateEmpiricalModelBadEvent policy initialState episodes varianceProxy countDelta rewardDelta MeasurableSet event /\ (source.iidStochasticTrajectoryFamilyMeasure policy initialState episodes) event <= ENNReal.ofReal countDelta + ENNReal.ofReal rewardDelta /\ forall trajectories, trajectories ∉ event -> let model := mdp.stochasticAllCoordinateEmpiricalFiniteBatchModel episodes (mdp.sampledEpisodeBatchOfStochasticTrajectories episodes trajectories) defaultState rewardBudget transitionBudget (forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= model.plan.upperValueRemaining mdp.horizon le_rfl state) /\ model.plan.optimisticPolicy.expectedRegret initialState <= model.plan.optimisticPolicy.occupancySumRemaining (fun remaining hremaining state => 2 * model.plan.selectedRadiusRemaining remaining hremaining state) mdp.horizon le_rfl initialState