BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticConfidence

Policy whose iid stochastic law generated a batch coordinate.

def policyAt {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) : Nat -> MarkovPolicy mdp | 0 => source.initialPolicy | n + 1 => source.successorPolicy n (Preorder.frestrictLe n trajectory) /-- Pull an initial stochastic-batch event back to the adaptive trajectory. -/ def initialBadEvent {mdp : MDP State Action} {episodes : Nat} (bad : Set (StochasticEpisodeBatch mdp episodes)) : Set (StochasticEpisodeBatchTrajectory mdp episodes)

Pull an initial stochastic-batch event back to the adaptive trajectory.

def initialBadEvent {mdp : MDP State Action} {episodes : Nat} (bad : Set (StochasticEpisodeBatch mdp episodes)) : Set (StochasticEpisodeBatchTrajectory mdp episodes)

Pull a prefix-dependent successor stochastic-batch event back to the trajectory.

def successorBadEvent {mdp : MDP State Action} {episodes : Nat} (n : Nat) (bad : Set (StochasticEpisodeBatchPrefix mdp episodes n × StochasticEpisodeBatch mdp episodes)) : Set (StochasticEpisodeBatchTrajectory mdp episodes)

Round-indexed adapted stochastic-batch event.

def roundBadEvent {mdp : MDP State Action} {episodes : Nat} (initialBad : Set (StochasticEpisodeBatch mdp episodes)) (successorBad : (n : Nat) -> Set (StochasticEpisodeBatchPrefix mdp episodes n × StochasticEpisodeBatch mdp episodes)) : Nat -> Set (StochasticEpisodeBatchTrajectory mdp episodes) | 0 => initialBadEvent initialBad | n + 1 => successorBadEvent n (successorBad n) /-- Union of the first `rounds` adapted stochastic-batch events. -/ def finiteHorizonBadEvent {mdp : MDP State Action} {episodes : Nat} (rounds : Nat) (initialBad : Set (StochasticEpisodeBatch mdp episodes)) (successorBad : (n : Nat) -> Set (StochasticEpisodeBatchPrefix mdp episodes n × StochasticEpisodeBatch mdp episodes)) : Set (StochasticEpisodeBatchTrajectory mdp episodes)

Union of the first `rounds` adapted stochastic-batch events.

def finiteHorizonBadEvent {mdp : MDP State Action} {episodes : Nat} (rounds : Nat) (initialBad : Set (StochasticEpisodeBatch mdp episodes)) (successorBad : (n : Nat) -> Set (StochasticEpisodeBatchPrefix mdp episodes n × StochasticEpisodeBatch mdp episodes)) : Set (StochasticEpisodeBatchTrajectory mdp episodes)

Measurability of the finite adapted stochastic-batch union.

theorem measurableSet_finiteHorizonBadEvent {mdp : MDP State Action} {episodes rounds : Nat} {initialBad : Set (StochasticEpisodeBatch mdp episodes)} {successorBad : (n : Nat) -> Set (StochasticEpisodeBatchPrefix mdp episodes n × StochasticEpisodeBatch mdp episodes)} (hinitial : MeasurableSet initialBad) (hsuccessor : forall n, n + 1 < rounds -> MeasurableSet (successorBad n)) : MeasurableSet (finiteHorizonBadEvent rounds initialBad successorBad)

Exact mass of a pulled-back initial stochastic-batch event.

theorem trajectoryMeasure_initialBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) {bad : Set (StochasticEpisodeBatch mdp episodes)} (hbad : MeasurableSet bad) : source.trajectoryMeasure (initialBadEvent bad) = source.rewardSource.iidStochasticTrajectoryFamilyMeasure source.initialPolicy initialState episodes bad

A successor event inherits a uniform bound on every history fiber.

theorem trajectoryMeasure_successorBadEvent_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) {bad : Set (StochasticEpisodeBatchPrefix mdp episodes n × StochasticEpisodeBatch mdp episodes)} (hbad : MeasurableSet bad) (budget : ENNReal) (hfiber : forall history, source.batchKernel n history (Prod.mk history ⁻¹' bad) <= budget) : source.trajectoryMeasure (successorBadEvent n bad) <= budget

Initial selected count-and-reward empirical-model event.

noncomputable def initialAllCoordinateEmpiricalModelBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (varianceProxy : NNReal) (countDelta rewardDelta : Real) : Set (StochasticEpisodeBatch mdp episodes)

Prefix-selected successor count-and-reward empirical-model event.

noncomputable def successorAllCoordinateEmpiricalModelBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (varianceProxy : NNReal) (countDelta rewardDelta : Real) (n : Nat) : Set (StochasticEpisodeBatchPrefix mdp episodes n × StochasticEpisodeBatch mdp episodes)

Finite-round selected count-and-reward empirical-model event.

noncomputable def adaptiveAllCoordinateEmpiricalModelBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (varianceProxy : NNReal) (countDelta rewardDelta : Real) : Set (StochasticEpisodeBatchTrajectory mdp episodes)

A positive global share gives a positive finite-round local share.

theorem multiBatchLocalDelta_pos_of_pos {rounds : Nat} (hrounds : 0 < rounds) {delta : Real} (hdelta : 0 < delta) : 0 < multiBatchLocalDelta rounds delta

A global share at most one gives every finite-round local share at most one.

theorem multiBatchLocalDelta_le_one_of_le_one {rounds : Nat} (hrounds : 0 < rounds) {delta : Real} (hdelta_le_one : delta <= 1) : multiBatchLocalDelta rounds delta <= 1

The initial selected empirical-model event is measurable.

theorem measurableSet_initialAllCoordinateEmpiricalModelBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (varianceProxy : NNReal) (countDelta rewardDelta : Real) : MeasurableSet (source.initialAllCoordinateEmpiricalModelBadEvent rounds varianceProxy countDelta rewardDelta)

Measurability of every selected successor event closes the global event.

theorem measurableSet_adaptiveAllCoordinateEmpiricalModelBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (varianceProxy : NNReal) (countDelta rewardDelta : Real) (hsuccessor : forall n, n + 1 < rounds -> MeasurableSet (source.successorAllCoordinateEmpiricalModelBadEvent rounds varianceProxy countDelta rewardDelta n)) : MeasurableSet (source.adaptiveAllCoordinateEmpiricalModelBadEvent rounds varianceProxy countDelta rewardDelta)

The initial selected empirical-model event receives its two local shares.

theorem initialAllCoordinateEmpiricalModelBadEvent_le [StandardBorelSpace State] [StandardBorelSpace Action] {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (varianceProxy : NNReal) (law : source.rewardSource.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) : (source.rewardSource.iidStochasticTrajectoryFamilyMeasure source.initialPolicy initialState episodes) (source.initialAllCoordinateEmpiricalModelBadEvent rounds varianceProxy countDelta rewardDelta) <= ENNReal.ofReal (multiBatchLocalDelta rounds countDelta) + ENNReal.ofReal (multiBatchLocalDelta rounds rewardDelta)

Every selected successor fiber receives the same two local shares.

theorem successorAllCoordinateEmpiricalModelBadEvent_fiber_le [StandardBorelSpace State] [StandardBorelSpace Action] {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (varianceProxy : NNReal) (law : source.rewardSource.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) (n : Nat) (history : StochasticEpisodeBatchPrefix mdp episodes n) : source.batchKernel n history (Prod.mk history ⁻¹' source.successorAllCoordinateEmpiricalModelBadEvent rounds varianceProxy countDelta rewardDelta n) <= ENNReal.ofReal (multiBatchLocalDelta rounds countDelta) + ENNReal.ofReal (multiBatchLocalDelta rounds rewardDelta)

The two local shares are the local share of their sum.

theorem ofReal_multiBatchLocalDelta_add (rounds : Nat) {countDelta rewardDelta : Real} (hcountDelta : 0 <= countDelta) (hrewardDelta : 0 <= rewardDelta) : ENNReal.ofReal (multiBatchLocalDelta rounds countDelta) + ENNReal.ofReal (multiBatchLocalDelta rounds rewardDelta) = ENNReal.ofReal (multiBatchLocalDelta rounds (countDelta + rewardDelta))

Finite-round adaptive count-and-reward confidence under exact selected-policy iid fibers. The two global shares remain separate in the terminal bound.

theorem trajectoryMeasure_adaptiveAllCoordinateEmpiricalModelBadEvent_le [StandardBorelSpace State] [StandardBorelSpace Action] {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (varianceProxy : NNReal) (law : source.rewardSource.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) (hsuccessor : forall n, n + 1 < rounds -> MeasurableSet (source.successorAllCoordinateEmpiricalModelBadEvent rounds varianceProxy countDelta rewardDelta n)) : source.trajectoryMeasure (source.adaptiveAllCoordinateEmpiricalModelBadEvent rounds varianceProxy countDelta rewardDelta) <= ENNReal.ofReal countDelta + ENNReal.ofReal rewardDelta

Outside the adaptive event, each batch avoids its generating policy's event.

theorem policyAt_batch_not_mem_allCoordinateEmpiricalModelBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes rounds : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (varianceProxy : NNReal) (countDelta rewardDelta : Real) (htrajectory : trajectory ∉ source.adaptiveAllCoordinateEmpiricalModelBadEvent rounds varianceProxy countDelta rewardDelta) (round : Fin rounds) : trajectory round ∉ source.rewardSource.stochasticAllCoordinateEmpiricalModelBadEvent (source.policyAt trajectory round) initialState episodes varianceProxy (multiBatchLocalDelta rounds countDelta) (multiBatchLocalDelta rounds rewardDelta)

Selected exploratory count-and-reward events are measurable after pulling the stochastic batch back to its raw sampled `EpisodeBatch`.

theorem measurableSet_selectedExploratoryStochasticAllCoordinateEmpiricalModelBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} {History : Type*} [MeasurableSpace History] (rewardSource : mdp.MeanCompatibleRewardKernel) (selector : History -> DeterministicMarkovPolicyTable mdp) (hselector : Measurable selector) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (varianceProxy : NNReal) (countDelta rewardDelta : Real) : MeasurableSet {pair : History × StochasticEpisodeBatch mdp episodes | pair.2 ∈ rewardSource.stochasticAllCoordinateEmpiricalModelBadEvent ((selector pair.1).exploratoryPolicy explorationRate hexplorationRate) initialState episodes varianceProxy countDelta rewardDelta}

Every successor event of the concrete sampled optimistic source is measurable.

theorem exploratorySource_measurableSet_successorAllCoordinateEmpiricalModelBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (rewardBudget transitionBudget : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (rounds : Nat) (varianceProxy : NNReal) (countDelta rewardDelta : Real) (n : Nat) : let source := exploratorySource mdp initialState episodes rewardSource initialTable defaultState rewardBudget transitionBudget explorationRate hexplorationRate MeasurableSet (source.successorAllCoordinateEmpiricalModelBadEvent rounds varianceProxy countDelta rewardDelta n)

The concrete sampled optimistic source inherits the finite-round selected count-and-reward event without any caller-supplied measurability premise.

theorem exploratorySource_trajectoryMeasure_adaptiveAllCoordinateEmpiricalModelBadEvent_le [StandardBorelSpace State] [StandardBorelSpace Action] {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (rewardBudget transitionBudget : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (varianceProxy : NNReal) (law : rewardSource.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) : let source := exploratorySource mdp initialState episodes rewardSource initialTable defaultState rewardBudget transitionBudget explorationRate hexplorationRate let event := source.adaptiveAllCoordinateEmpiricalModelBadEvent rounds varianceProxy countDelta rewardDelta MeasurableSet event /\ source.trajectoryMeasure event <= ENNReal.ofReal countDelta + ENNReal.ofReal rewardDelta

Finite-round sampled-reward adaptive optimism with explicit exploratory path support calibration. Every model is built from the actual observed rewards; outside one measurable event, every round is optimistic and its recommended policy satisfies the compiled selected-radius expected-regret bound.

theorem exploratorySource_trajectoryMeasure_finiteRound_allCoordinateConfidence_optimism_and_recommendedExpectedRegret_of_pathSupport_explicitCalibration [StandardBorelSpace State] [StandardBorelSpace Action] {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (varianceProxy : NNReal) (law : rewardSource.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 (multiBatchLocalDelta rounds countDelta) < (episodes : Real) * visitFloor) (hcontraction : (Fintype.card State : Real) * uniformFloorTransitionCoordinateRadius mdp episodes (multiBatchLocalDelta rounds countDelta) visitFloor * (mdp.horizon : Real) <= 1 / 2) : let localCountDelta := multiBatchLocalDelta rounds countDelta let localRewardDelta := multiBatchLocalDelta rounds rewardDelta let rewardBudget := uniformFloorStochasticRewardCoordinateRadius mdp episodes varianceProxy localCountDelta localRewardDelta visitFloor let transitionBudget := uniformFloorStochasticTransitionBudget rewardBound rewardBudget let source := exploratorySource mdp initialState episodes rewardSource initialTable defaultState rewardBudget transitionBudget explorationRate hexplorationRate let event := source.adaptiveAllCoordinateEmpiricalModelBadEvent rounds varianceProxy countDelta rewardDelta MeasurableSet event /\ source.trajectoryMeasure event <= ENNReal.ofReal countDelta + ENNReal.ofReal rewardDelta /\ forall trajectory, trajectory ∉ event -> forall round : Fin rounds, let model := mdp.stochasticAllCoordinateEmpiricalFiniteBatchModel episodes (mdp.sampledEpisodeBatchOfStochasticTrajectories episodes (trajectory round)) 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