BanditRLProof.RL.FiniteHorizonStochasticRewardIIDSelfConsistentCalibration

Exact nonnegative fixed-point budget for `q * (base + budget) <= budget`.

noncomputable def selfConsistentTransitionBudget (q base : Real) : Real

The fixed-point budget is nonnegative when `0 <= q < 1` and `base >= 0`.

theorem selfConsistentTransitionBudget_nonneg {q base : Real} (hq_nonneg : 0 <= q) (hq : q < 1) (hbase : 0 <= base) : 0 <= selfConsistentTransitionBudget q base

The chosen budget solves the transition-envelope fixed point exactly.

theorem selfConsistentTransitionBudget_fixedPoint {q base : Real} (hq : q < 1) : q * (base + selfConsistentTransitionBudget q base) = selfConsistentTransitionBudget q base

The exact common-floor transition contraction factor.

noncomputable def uniformFloorStochasticTransitionContraction (mdp : MDP State Action) (episodes : Nat) (countDelta visitFloor : Real) : Real

The common-floor contraction factor is nonnegative under the count margin.

theorem uniformFloorStochasticTransitionContraction_nonneg {mdp : MDP State Action} {episodes : Nat} {countDelta visitFloor : Real} (hmargin : simultaneousCountConfidenceRadius mdp episodes countDelta < (episodes : Real) * visitFloor) : 0 <= uniformFloorStochasticTransitionContraction mdp episodes countDelta visitFloor

Shrinking transition budget obtained from the exact contraction factor.

noncomputable def uniformFloorStochasticSelfConsistentTransitionBudget (mdp : MDP State Action) (episodes : Nat) (countDelta visitFloor rewardBound rewardBudget : Real) : Real

The shrinking transition budget is nonnegative under `q < 1`.

theorem uniformFloorStochasticSelfConsistentTransitionBudget_nonneg {mdp : MDP State Action} {episodes : Nat} {countDelta visitFloor rewardBound rewardBudget : Real} (hmargin : simultaneousCountConfidenceRadius mdp episodes countDelta < (episodes : Real) * visitFloor) (hrewardBound_nonneg : 0 <= rewardBound) (hrewardBudget_nonneg : 0 <= rewardBudget) (hq : uniformFloorStochasticTransitionContraction mdp episodes countDelta visitFloor < 1) : 0 <= uniformFloorStochasticSelfConsistentTransitionBudget mdp episodes countDelta visitFloor rewardBound rewardBudget

The common-floor shrinking budget satisfies the exact envelope identity.

theorem uniformFloorStochasticSelfConsistentTransitionBudget_fixedPoint {mdp : MDP State Action} {episodes : Nat} {countDelta visitFloor rewardBound rewardBudget : Real} (hq : uniformFloorStochasticTransitionContraction mdp episodes countDelta visitFloor < 1) : uniformFloorStochasticTransitionContraction mdp episodes countDelta visitFloor * (rewardBound + 2 * rewardBudget + uniformFloorStochasticSelfConsistentTransitionBudget mdp episodes countDelta visitFloor rewardBound rewardBudget) = uniformFloorStochasticSelfConsistentTransitionBudget mdp episodes countDelta visitFloor rewardBound rewardBudget

The exact `q < 1` fixed point covers every transition-radius/value-envelope sum with a budget that shrinks as `q` tends to zero.

theorem stochasticTransitionCover_of_uniformExpectedCountFloor_selfConsistent {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) (hq : uniformFloorStochasticTransitionContraction mdp episodes countDelta visitFloor < 1) : let rewardBudget := uniformFloorStochasticRewardCoordinateRadius mdp episodes varianceProxy countDelta rewardDelta visitFloor let transitionBudget := uniformFloorStochasticSelfConsistentTransitionBudget mdp episodes countDelta visitFloor 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 all-coordinate confidence under the shrinking transition budget.

theorem iidStochasticTrajectoryFamilyMeasure_allCoordinate_optimism_and_expectedRegret_of_uniformExpectedCountFloor_selfConsistent [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) (hq : uniformFloorStochasticTransitionContraction mdp episodes countDelta visitFloor < 1) : let rewardBudget := uniformFloorStochasticRewardCoordinateRadius mdp episodes varianceProxy countDelta rewardDelta visitFloor let transitionBudget := uniformFloorStochasticSelfConsistentTransitionBudget mdp episodes countDelta visitFloor 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

Exploratory path support feeds the shrinking fixed-policy calibration.

theorem exploratoryPolicy_iidStochasticTrajectoryFamilyMeasure_allCoordinate_optimism_and_expectedRegret_of_pathSupport_selfConsistentCalibration [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) (hq : uniformFloorStochasticTransitionContraction mdp episodes countDelta visitFloor < 1) : let policy := table.exploratoryPolicy explorationRate hexplorationRate let rewardBudget := uniformFloorStochasticRewardCoordinateRadius mdp episodes varianceProxy countDelta rewardDelta visitFloor let transitionBudget := uniformFloorStochasticSelfConsistentTransitionBudget mdp episodes countDelta visitFloor 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