BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeExploratoryBehaviorRegret

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

theorem exploratoryActionPMF_apply {mdp : MDP State Action} (table : DeterministicMarkovPolicyTable mdp) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (stage : Fin mdp.horizon) (state : State) (action : Action) : table.exploratoryActionPMF explorationRate hexplorationRate stage state action = (explorationRate : ENNReal) * (Fintype.card Action : ENNReal)⁻¹ + ((1 - explorationRate : NNReal) : ENNReal) * if action = table stage state then 1 else 0

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

theorem integral_exploratoryActionPMF {mdp : MDP State Action} (table : DeterministicMarkovPolicyTable mdp) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (stage : Fin mdp.horizon) (state : State) (f : Action -> Real) : (∫ action, f action ∂ (table.exploratoryActionPMF explorationRate hexplorationRate stage state).toMeasure) = (explorationRate : Real) * (∑ action, f action) / (Fintype.card Action : Real) + (1 - (explorationRate : Real)) * f (table stage state)

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

theorem selected_sub_integral_exploratoryActionPMF_le {mdp : MDP State Action} (table : DeterministicMarkovPolicyTable mdp) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (stage : Fin mdp.horizon) (state : State) (f : Action -> Real) (bound : Real) (hbound : forall action, |f action| <= bound) : f (table stage state) - (∫ action, f action ∂ (table.exploratoryActionPMF explorationRate hexplorationRate stage state).toMeasure) <= 2 * (explorationRate : Real) * bound

A bounded continuation gives a bounded one-step action value.

theorem bellmanQ_abs_le (mdp : MDP State Action) (rewardBound continuationBound : Real) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) {value : State -> Real} (hvalue : forall state, |value state| <= continuationBound) (state : State) (action : Action) : |mdp.bellmanQ value state action| <= rewardBound + continuationBound

A pointwise continuation difference bound transports through one transition kernel.

theorem transitionValue_sub_le_const (mdp : MDP State Action) {left right : State -> Real} {bound : Real} (hbound : forall state, left state - right state <= bound) (state : State) (action : Action) : mdp.transitionValue left state action - mdp.transitionValue right state action <= bound

Every bounded-reward policy value is bounded by remaining horizon times the reward bound.

theorem valueRemaining_abs_le {mdp : MDP State Action} (policy : MarkovPolicy mdp) (rewardBound : Real) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) : |policy.valueRemaining remaining hremaining state| <= (remaining : Real) * rewardBound

Bellman evaluation of a deterministic table selects exactly its table action.

theorem toMarkovPolicy_bellman {mdp : MDP State Action} (table : DeterministicMarkovPolicyTable mdp) (stage : Fin mdp.horizon) (value : State -> Real) (state : State) : table.toMarkovPolicy.bellman stage value state = mdp.bellmanQ value state (table stage state)

Bellman evaluation of the exploratory table is its explicit PMF mixture.

theorem exploratoryPolicy_bellman {mdp : MDP State Action} (table : DeterministicMarkovPolicyTable mdp) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (stage : Fin mdp.horizon) (value : State -> Real) (state : State) : (table.exploratoryPolicy explorationRate hexplorationRate).bellman stage value state = (explorationRate : Real) * (∑ action, mdp.bellmanQ value state action) / (Fintype.card Action : Real) + (1 - (explorationRate : Real)) * mdp.bellmanQ value state (table stage state)

Exploration around a deterministic table loses at most the explicit quadratic-horizon charge. The charge is linear in the exploration rate and reward bound.

theorem toMarkovPolicy_valueRemaining_sub_exploratoryPolicy_valueRemaining_le {mdp : MDP State Action} (table : DeterministicMarkovPolicyTable mdp) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (rewardBound : Real) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) : table.toMarkovPolicy.valueRemaining remaining hremaining state - (table.exploratoryPolicy explorationRate hexplorationRate).valueRemaining remaining hremaining state <= (explorationRate : Real) * rewardBound * (remaining : Real) * ((remaining + 1 : Nat) : Real)

Exploratory-behavior expected regret is bounded by table regret plus its exploration charge.

theorem exploratoryPolicy_expectedRegret_le_toMarkovPolicy_expectedRegret_add_charge {mdp : MDP State Action} (table : DeterministicMarkovPolicyTable mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (rewardBound : Real) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) : (table.exploratoryPolicy explorationRate hexplorationRate).expectedRegret initialState <= table.toMarkovPolicy.expectedRegret initialState + (explorationRate : Real) * rewardBound * (mdp.horizon : Real) * ((mdp.horizon + 1 : Nat) : Real)

The per-policy price of uniform exploration over a bounded-reward horizon.

noncomputable def exploratoryBehaviorRegretCharge (mdp : MDP State Action) (explorationRate : NNReal) (rewardBound : Real) : Real

Sum of expected regrets of exploratory behaviors centered on cumulative recommendations.

noncomputable def adaptiveCumulativeEmpiricalOptimisticExploratoryBehaviorExpectedRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (defaultState : State) (countRadius : TransitionCountRadius) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (rounds : Nat) : Real

Average expected regret of those exploratory behaviors.

noncomputable def adaptiveCumulativeEmpiricalOptimisticAverageExploratoryBehaviorExpectedRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (defaultState : State) (countRadius : TransitionCountRadius) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (rounds : Nat) : Real

Cumulative exploratory behavior regret is bounded by recommendation regret plus one charge per round.

theorem adaptiveCumulativeEmpiricalOptimisticExploratoryBehaviorExpectedRegret_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (defaultState : State) (countRadius : TransitionCountRadius) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (rewardBound : Real) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (rounds : Nat) : adaptiveCumulativeEmpiricalOptimisticExploratoryBehaviorExpectedRegret (initialState

For a nonempty window, averaging removes the repeated-round factor from the charge.

theorem adaptiveCumulativeEmpiricalOptimisticAverageExploratoryBehaviorExpectedRegret_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (defaultState : State) (countRadius : TransitionCountRadius) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (rewardBound : Real) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (rounds : Nat) (hrounds : 0 < rounds) : adaptiveCumulativeEmpiricalOptimisticAverageExploratoryBehaviorExpectedRegret (initialState

The finite-window behavior-regret certificate adds the explicit exploration charge.

noncomputable def vanishingDeltaScheduledAverageExploratoryBehaviorExpectedRegretBound (mdp : MDP State Action) (n : Nat) (visitFloor : Real) (explorationRate : NNReal) : Real

With a fixed exploration rate, the deterministic certificate tends to its exploration charge.

theorem vanishingDeltaScheduledAverageExploratoryBehaviorBound_tendsto_charge (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (visitFloor : Real) (hvisitFloor : 0 < visitFloor) (explorationRate : NNReal) : Filter.Tendsto (fun n => vanishingDeltaScheduledAverageExploratoryBehaviorExpectedRegretBound mdp n visitFloor explorationRate) Filter.atTop (nhds (exploratoryBehaviorRegretCharge mdp explorationRate 1))

The regret term indexed by `round` is the source's successor behavior at coordinate `round + 1`; the initial behavior at coordinate zero is intentionally excluded.

theorem exploratorySource_policyAt_succ_eq_cumulativeOptimisticExploratoryPolicy {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (countRadius : TransitionCountRadius) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (trajectory : EpisodeBatchTrajectory mdp episodes) (round : Nat) : (exploratorySource mdp initialState episodes initialTable defaultState countRadius explorationRate hexplorationRate).policyAt trajectory (round + 1) = ((cumulativeTransitionCountSummaryAt trajectory round) |>.countRadiusOptimisticPolicyTable mdp defaultState countRadius |>.exploratoryPolicy explorationRate hexplorationRate)

Trajectories whose average exploratory-behavior regret exceeds its charged certificate.

noncomputable def vanishingDeltaScheduledAverageExploratoryBehaviorRegretViolationSet (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (defaultState : State) (n : Nat) (visitFloor : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) : Set (EpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.vanishingDeltaScheduledEpisodes mdp n visitFloor))

Finite-window high-probability endpoint for successor exploratory behaviors at source coordinates `1` through `n + 1`; the initial-table behavior at coordinate zero is not charged here. The violation set is contained in the measurable count bad event; outside that event, optimism and the charged average behavior-regret certificate hold simultaneously.

theorem exploratorySource_trajectoryMeasure_cumulativeInverseSqrtPathSupport_optimism_and_vanishingDeltaScheduledAverageExploratoryBehaviorExpectedRegret (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (n : Nat) (visitFloor : Real) [StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.vanishingDeltaScheduledEpisodes mdp n visitFloor))] [StandardBorelSpace (EpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.vanishingDeltaScheduledEpisodes mdp n visitFloor))] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (support : ExploratoryPathSupport mdp initialState) (hfloor : ExploratoryPathUniformVisitFloor support explorationRate visitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hvisitFloor : 0 < visitFloor) : let episodes := AdaptiveEpisodeBatchSource.vanishingDeltaScheduledEpisodes mdp n visitFloor let delta := AdaptiveEpisodeBatchSource.vanishingAverageConfidenceDelta n let countRadius := AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtCountRadius mdp (n + 1) delta visitFloor let source := exploratorySource mdp initialState episodes initialTable defaultState countRadius explorationRate hexplorationRate let violationSet := vanishingDeltaScheduledAverageExploratoryBehaviorRegretViolationSet mdp initialState defaultState n visitFloor explorationRate hexplorationRate MeasurableSet (source.adaptiveCumulativeCountBadEvent (n + 1) delta) /\ source.trajectoryMeasure (source.adaptiveCumulativeCountBadEvent (n + 1) delta) <= ENNReal.ofReal delta /\ violationSet ⊆ source.adaptiveCumulativeCountBadEvent (n + 1) delta /\ source.trajectoryMeasure violationSet <= ENNReal.ofReal delta /\ forall trajectory, trajectory ∉ source.adaptiveCumulativeCountBadEvent (n + 1) delta -> (forall round : Fin (n + 1), forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= (adaptiveCumulativeEmpiricalOptimisticPlanAt trajectory defaultState countRadius round).upperValueRemaining mdp.horizon le_rfl state) /\ adaptiveCumulativeEmpiricalOptimisticAverageExploratoryBehaviorExpectedRegret (initialState