BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalModelConfidence

Policy whose exact iid law generated coordinate `t`.

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

Pull an initial heterogeneous-batch event back to the causal trajectory.

def initialBadEvent {mdp : MDP State Action} {episodes : Nat -> Nat} (bad : Set (StochasticEpisodeBatch mdp (episodes 0))) : Set (HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes)

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

def successorBadEvent {mdp : MDP State Action} {episodes : Nat -> Nat} (n : Nat) (bad : Set (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n × StochasticEpisodeBatch mdp (episodes (n + 1)))) : Set (HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes)

Coordinate-indexed adapted heterogeneous-batch event.

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

Union of the first `rounds` heterogeneous adapted events.

def finiteHorizonBadEvent {mdp : MDP State Action} {episodes : Nat -> Nat} (rounds : Nat) (initialBad : Set (StochasticEpisodeBatch mdp (episodes 0))) (successorBad : (n : Nat) -> Set (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n × StochasticEpisodeBatch mdp (episodes (n + 1)))) : Set (HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes)

Measurability of the finite heterogeneous adapted union.

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

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

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

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

theorem trajectoryMeasure_successorBadEvent_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) {bad : Set (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n × StochasticEpisodeBatch mdp (episodes (n + 1)))} (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 empirical-model event with coordinate-specific shares.

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

Prefix-selected successor empirical-model event with local shares.

noncomputable def successorAllCoordinateEmpiricalModelBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (varianceProxy : NNReal) (countDelta rewardDelta : Nat -> Real) (n : Nat) : Set (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n × StochasticEpisodeBatch mdp (episodes (n + 1)))

First-`rounds` selected count-and-reward empirical-model event.

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

Exact finite sum of coordinate-specific count and reward failure shares.

noncomputable def cumulativeModelFailureBudget (rounds : Nat) (countDelta rewardDelta : Nat -> Real) : ENNReal

The initial coordinate event is measurable.

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

Selected successor measurability closes the finite heterogeneous event.

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

The initial selected iid fiber receives its coordinate shares.

theorem initialAllCoordinateEmpiricalModelBadEvent_le [StandardBorelSpace State] [StandardBorelSpace Action] {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (hepisodes : 0 < episodes 0) (varianceProxy : NNReal) (law : source.rewardSource.UniformSubgaussianRewardLaw varianceProxy) (htotal : 0 < ((((episodes 0 : NNReal) * varianceProxy : NNReal) : Real))) (countDelta rewardDelta : Nat -> Real) (hcountDelta : 0 < countDelta 0) (hcountDelta_le_one : countDelta 0 <= 1) (hrewardDelta : 0 < rewardDelta 0) (hrewardDelta_le_one : rewardDelta 0 <= 1) : (source.rewardSource.iidStochasticTrajectoryFamilyMeasure source.initialPolicy initialState (episodes 0)) (source.initialAllCoordinateEmpiricalModelBadEvent varianceProxy countDelta rewardDelta) <= ENNReal.ofReal (countDelta 0) + ENNReal.ofReal (rewardDelta 0)

Every selected successor iid fiber receives its coordinate shares.

theorem successorAllCoordinateEmpiricalModelBadEvent_fiber_le [StandardBorelSpace State] [StandardBorelSpace Action] {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (varianceProxy : NNReal) (law : source.rewardSource.UniformSubgaussianRewardLaw varianceProxy) (countDelta rewardDelta : Nat -> Real) (n : Nat) (hepisodes : 0 < episodes (n + 1)) (htotal : 0 < ((((episodes (n + 1) : NNReal) * varianceProxy : NNReal) : Real))) (hcountDelta : 0 < countDelta (n + 1)) (hcountDelta_le_one : countDelta (n + 1) <= 1) (hrewardDelta : 0 < rewardDelta (n + 1)) (hrewardDelta_le_one : rewardDelta (n + 1) <= 1) (history : HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n) : source.batchKernel n history (Prod.mk history ⁻¹' source.successorAllCoordinateEmpiricalModelBadEvent varianceProxy countDelta rewardDelta n) <= ENNReal.ofReal (countDelta (n + 1)) + ENNReal.ofReal (rewardDelta (n + 1))

Every selected successor iid fiber receives its coordinate shares. -/ theorem successorAllCoordinateEmpiricalModelBadEvent_fiber_le [StandardBorelSpace State] [StandardBorelSpace Action] {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (varianceProxy : NNReal) (law : source.rewardSource.UniformSubgaussianRewardLaw varianceProxy) (countDelta rewardDelta : Nat -> Real) (n : Nat) (hepisodes : 0 < episodes (n + 1)) (htotal : 0 < ((((episodes (n + 1) : NNReal) * varianceProxy : NNReal) : Real))) (hcountDelta : 0 < countDelta (n + 1)) (hcountDelta_le_one : countDelta (n + 1) <= 1) (hrewardDelta : 0 < rewardDelta (n + 1)) (hrewardDelta_le_one : rewardDelta (n + 1) <= 1) (history : HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n) : source.batchKernel n history (Prod.mk history ⁻¹' source.successorAllCoordinateEmpiricalModelBadEvent varianceProxy countDelta rewardDelta n) <= ENNReal.ofReal (countDelta (n + 1)) + ENNReal.ofReal (rewardDelta (n + 1)) := by rw [source.batchKernel_eq_iidStochasticTrajectoryFamilyMeasure] change (source.rewardSource.iidStochasticTrajectoryFamilyMeasure (source.successorPolicy n history) initialState (episodes (n + 1))) (source.rewardSource.stochasticAllCoordinateEmpiricalModelBadEvent (source.successorPolicy n history) initialState (episodes (n + 1)) varianceProxy (countDelta (n + 1)) (rewardDelta (n + 1))) <= _ exact source.rewardSource.iidStochasticTrajectoryFamilyMeasure_stochasticAllCoordinateEmpiricalModelBadEvent_le (source.successorPolicy n history) initialState (episodes (n + 1)) hepisodes varianceProxy law htotal (countDelta (n + 1)) hcountDelta hcountDelta_le_one (rewardDelta (n + 1)) hrewardDelta hrewardDelta_le_one /- Finite-prefix heterogeneous count-and-reward confidence. No independence between coordinates is used; every successor is integrated through its exact selected iid history fiber.

theorem trajectoryMeasure_adaptiveAllCoordinateEmpiricalModelBadEvent_le [StandardBorelSpace State] [StandardBorelSpace Action] {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (hepisodes : forall t, 0 < episodes t) (varianceProxy : NNReal) (law : source.rewardSource.UniformSubgaussianRewardLaw varianceProxy) (htotal : forall t, 0 < ((((episodes t : NNReal) * varianceProxy : NNReal) : Real))) (countDelta rewardDelta : Nat -> Real) (hcountDelta : forall t, t < rounds -> 0 < countDelta t) (hcountDelta_le_one : forall t, t < rounds -> countDelta t <= 1) (hrewardDelta : forall t, t < rounds -> 0 < rewardDelta t) (hrewardDelta_le_one : forall t, t < rounds -> rewardDelta t <= 1) (hsuccessor : forall n, n + 1 < rounds -> MeasurableSet (source.successorAllCoordinateEmpiricalModelBadEvent varianceProxy countDelta rewardDelta n)) : source.trajectoryMeasure (source.adaptiveAllCoordinateEmpiricalModelBadEvent rounds varianceProxy countDelta rewardDelta) <= cumulativeModelFailureBudget rounds countDelta rewardDelta

Outside the finite event, every batch avoids its generating-policy event.

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

Concrete heterogeneous successor events are measurable.

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

Concrete heterogeneous source event and its finite failure-budget bound.

theorem heterogeneousExploratorySource_trajectoryMeasure_adaptiveAllCoordinateEmpiricalModelBadEvent_le [StandardBorelSpace State] [StandardBorelSpace Action] {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (rewardBudget transitionBudget : Nat -> Real) (explorationRate : Nat -> NNReal) (hexplorationRate : forall t, explorationRate t <= 1) (rounds : Nat) (hepisodes : forall t, 0 < episodes t) (varianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (htotal : forall t, 0 < ((((episodes t : NNReal) * varianceProxy : NNReal) : Real))) (countDelta rewardDelta : Nat -> Real) (hcountDelta : forall t, t < rounds -> 0 < countDelta t) (hcountDelta_le_one : forall t, t < rounds -> countDelta t <= 1) (hrewardDelta : forall t, t < rounds -> 0 < rewardDelta t) (hrewardDelta_le_one : forall t, t < rounds -> rewardDelta t <= 1) : let source := heterogeneousExploratorySource mdp initialState episodes rewardSource initialTable defaultState rewardBudget transitionBudget explorationRate hexplorationRate let event := source.adaptiveAllCoordinateEmpiricalModelBadEvent rounds varianceProxy countDelta rewardDelta MeasurableSet event ∧ source.trajectoryMeasure event <= HeterogeneousAdaptiveStochasticEpisodeBatchSource.cumulativeModelFailureBudget rounds countDelta rewardDelta

Model-confidence failure budget of the first causal schedule coordinates.

noncomputable def selfConsistentScheduledCausalModelFailureBudget (mdp : MDP State Action) (rounds : Nat) : ENNReal

Named actual-sampled model event on the self-consistent causal source.

noncomputable def selfConsistentScheduledCausalModelBadEvent (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : Set (HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t))

Named actual-sampled model event on the self-consistent causal source. -/ noncomputable def selfConsistentScheduledCausalModelBadEvent (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : Set (HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t)) := let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor source.adaptiveAllCoordinateEmpiricalModelBadEvent rounds varianceProxy (AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledLocalDelta mdp) (AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledLocalDelta mdp) /- The genuine causal schedule receives coordinatewise sampled-model confidence. Every model is computed from the actual batch at that coordinate, with the same reward and transition budgets used by the next causal selector.

theorem selfConsistentScheduledCausalSource_trajectoryMeasure_allCoordinateConfidence_optimism_and_recommendedExpectedRegret (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (baseVisitFloor : Real) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (rounds : Nat) : let episodes := fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t let rewardBudget := fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRewardBudget mdp varianceProxy baseVisitFloor t let transitionBudget := fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledTransitionBudget mdp varianceProxy baseVisitFloor t let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let event := selfConsistentScheduledCausalModelBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds MeasurableSet event ∧ source.trajectoryMeasure event <= selfConsistentScheduledCausalModelFailureBudget mdp rounds ∧ forall trajectory, trajectory ∉ event -> forall round : Fin rounds, let t := (round : Nat) let model := mdp.stochasticAllCoordinateEmpiricalFiniteBatchModel (episodes t) (mdp.sampledEpisodeBatchOfStochasticTrajectories (episodes t) (trajectory t)) defaultState (rewardBudget t) (transitionBudget t) (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