BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardEmpiricalOptimisticProjection

Map both coordinates of a measure composition product when the base measure and every kernel fiber have the prescribed mapped laws.

theorem measure_compProd_map_prodMap_of_map_eq {Alpha Alpha' Beta Beta' : Type*} [MeasurableSpace Alpha] [MeasurableSpace Alpha'] [MeasurableSpace Beta] [MeasurableSpace Beta'] (mu : Measure Alpha) [IsProbabilityMeasure mu] (kappa : ProbabilityTheory.Kernel Alpha Beta) [ProbabilityTheory.IsMarkovKernel kappa] (mu' : Measure Alpha') [IsProbabilityMeasure mu'] (kappa' : ProbabilityTheory.Kernel Alpha' Beta') [ProbabilityTheory.IsMarkovKernel kappa'] (f : Alpha -> Alpha') (hf : Measurable f) (g : Beta -> Beta') (hg : Measurable g) (hmu : mu.map f = mu') (hkappa : forall alpha, (kappa alpha).map g = kappa' (f alpha)) : (mu ⊗ₘ kappa).map (Prod.map f g) = mu' ⊗ₘ kappa'

Project one stochastic batch to the existing known-mean empirical batch.

def knownRewardEpisodeBatch (episodes : Nat) (batch : StochasticEpisodeBatch mdp episodes) : EpisodeBatch mdp episodes

The stochastic-batch known-reward projection is measurable.

theorem measurable_knownRewardEpisodeBatch (episodes : Nat) : Measurable (knownRewardEpisodeBatch (mdp

Project every coordinate of a finite stochastic batch prefix.

def knownRewardEpisodeBatchPrefix (episodes n : Nat) (history : StochasticEpisodeBatchPrefix mdp episodes n) : EpisodeBatchPrefix mdp episodes n

The coordinatewise known-reward prefix projection is measurable.

theorem measurable_knownRewardEpisodeBatchPrefix (episodes n : Nat) : Measurable (knownRewardEpisodeBatchPrefix (mdp

Project every coordinate of an infinite stochastic batch trajectory.

def knownRewardEpisodeBatchTrajectory (episodes : Nat) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) : EpisodeBatchTrajectory mdp episodes

The coordinatewise complete known-reward trajectory projection is measurable.

theorem measurable_knownRewardEpisodeBatchTrajectory (episodes : Nat) : Measurable (knownRewardEpisodeBatchTrajectory (mdp

Projection commutes with restricting a complete trajectory to a prefix.

theorem knownRewardEpisodeBatchPrefix_frestrictLe (episodes n : Nat) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) : knownRewardEpisodeBatchPrefix episodes n (Preorder.frestrictLe n trajectory) = Preorder.frestrictLe n (knownRewardEpisodeBatchTrajectory episodes trajectory)

Stochastic iid episode-batch law indexed by an exploratory policy table.

noncomputable def exploratoryIIDStochasticEpisodeBatchKernel {mdp : MDP State Action} (rewardSource : mdp.MeanCompatibleRewardKernel) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) : ProbabilityTheory.Kernel (DeterministicMarkovPolicyTable mdp) (StochasticEpisodeBatch mdp episodes)

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

theorem exploratoryIIDStochasticEpisodeBatchKernel_apply {mdp : MDP State Action} (rewardSource : mdp.MeanCompatibleRewardKernel) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (table : DeterministicMarkovPolicyTable mdp) : exploratoryIIDStochasticEpisodeBatchKernel rewardSource initialState episodes explorationRate hexplorationRate table = rewardSource.iidStochasticTrajectoryFamilyMeasure (table.exploratoryPolicy explorationRate hexplorationRate) initialState episodes

A finite table selector and its batch statistic form a measurable dynamic sampled-return deviation. This discharges the regularity field required by `AdaptiveStochasticEpisodeBatchSource` without constraining sampled rewards.

theorem measurable_selectedExploratorySampledReturnDeviation {mdp : MDP State Action} {episodes : Nat} {History : Type*} [MeasurableSpace History] (selector : History -> DeterministicMarkovPolicyTable mdp) (hselector : Measurable selector) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) : Measurable fun pair : History × StochasticEpisodeBatch mdp episodes => mdp.sampledCumulativeReturnDeviationSum ((selector pair.1).exploratoryPolicy explorationRate hexplorationRate) episodes pair.2

Concrete stochastic-reward lift of the deterministic exploratory empirical optimistic source. Every policy update factors through known-reward history.

noncomputable def exploratorySource (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (transitionBonus : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes where

The stochastic and deterministic initial policies agree definitionally.

theorem exploratorySource_initialPolicy {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (transitionBonus : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) : (exploratorySource mdp initialState episodes rewardSource initialTable defaultState transitionBonus explorationRate hexplorationRate).initialPolicy = (AdaptiveEmpiricalOptimisticSource.exploratorySource mdp initialState episodes initialTable defaultState transitionBonus explorationRate hexplorationRate).initialPolicy

The stochastic successor policy is selected from the projected prefix.

theorem exploratorySource_successorPolicy {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (transitionBonus : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (n : Nat) (history : StochasticEpisodeBatchPrefix mdp episodes n) : (exploratorySource mdp initialState episodes rewardSource initialTable defaultState transitionBonus explorationRate hexplorationRate).successorPolicy n history = (AdaptiveEmpiricalOptimisticSource.exploratorySource mdp initialState episodes initialTable defaultState transitionBonus explorationRate hexplorationRate).successorPolicy n (MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatchPrefix (mdp

The initial stochastic batch maps to the deterministic exploratory batch.

theorem exploratorySource_initialBatch_map_knownRewardEpisodeBatch {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (transitionBonus : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) : (rewardSource.iidStochasticTrajectoryFamilyMeasure (exploratorySource mdp initialState episodes rewardSource initialTable defaultState transitionBonus explorationRate hexplorationRate).initialPolicy initialState episodes).map (MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatch (mdp

Every selected stochastic successor batch maps to its deterministic fiber.

theorem exploratorySource_batchKernel_map_knownRewardEpisodeBatch {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (transitionBonus : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (n : Nat) (history : StochasticEpisodeBatchPrefix mdp episodes n) : ((exploratorySource mdp initialState episodes rewardSource initialTable defaultState transitionBonus explorationRate hexplorationRate).batchKernel n history).map (MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatch (mdp

After projecting both coordinates, every stochastic prefix/next-batch joint law is the projected-prefix measure composed with the deterministic source kernel.

theorem exploratorySource_trajectoryMeasure_map_projectedPrefix_next_eq_compProd {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (transitionBonus : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (n : Nat) : let stochasticSource := exploratorySource mdp initialState episodes rewardSource initialTable defaultState transitionBonus explorationRate hexplorationRate let deterministicSource := AdaptiveEmpiricalOptimisticSource.exploratorySource mdp initialState episodes initialTable defaultState transitionBonus explorationRate hexplorationRate stochasticSource.trajectoryMeasure.map (fun trajectory => (MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatchPrefix (mdp

Conditioned on the projected stochastic prefix, the projected next batch has the deterministic exploratory empirical-optimistic source kernel.

theorem exploratorySource_trajectoryMeasure_condDistrib_projectedNext {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (EpisodeBatch mdp episodes)] [Nonempty (EpisodeBatch mdp episodes)] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (transitionBonus : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (n : Nat) : let stochasticSource := exploratorySource mdp initialState episodes rewardSource initialTable defaultState transitionBonus explorationRate hexplorationRate let deterministicSource := AdaptiveEmpiricalOptimisticSource.exploratorySource mdp initialState episodes initialTable defaultState transitionBonus explorationRate hexplorationRate ProbabilityTheory.condDistrib (fun trajectory : StochasticEpisodeBatchTrajectory mdp episodes => MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatch (mdp

The complete known-reward projection of the concrete stochastic adaptive source is exactly the existing deterministic exploratory source trajectory law.

theorem exploratorySource_trajectoryMeasure_map_knownRewardEpisodeBatchTrajectory {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (EpisodeBatch mdp episodes)] [Nonempty (EpisodeBatch mdp episodes)] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (transitionBonus : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) : let stochasticSource := exploratorySource mdp initialState episodes rewardSource initialTable defaultState transitionBonus explorationRate hexplorationRate let deterministicSource := AdaptiveEmpiricalOptimisticSource.exploratorySource mdp initialState episodes initialTable defaultState transitionBonus explorationRate hexplorationRate stochasticSource.trajectoryMeasure.map (MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatchTrajectory (mdp

The stochastic count bad event is the inverse image of the deterministic adaptive count event under complete known-reward projection.

def projectedAdaptiveSimultaneousCountBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (transitionBonus : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (rounds : Nat) (delta : Real) : Set (StochasticEpisodeBatchTrajectory mdp episodes)

Route endpoint: the concrete stochastic source inherits the deterministic known-mean all-coordinate confidence event, projected optimism, and projected recommended-policy expected-regret bound.

theorem exploratorySource_trajectoryMeasure_projectedAllCoordinateConfidence_optimism_and_recommendedExpectedRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (EpisodeBatch mdp episodes)] [Nonempty (EpisodeBatch mdp episodes)] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (rewardBound transitionBonus : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (htransitionBonus_nonneg : 0 <= transitionBonus) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (calibration : let deterministicSource := AdaptiveEmpiricalOptimisticSource.exploratorySource mdp initialState episodes initialTable defaultState transitionBonus explorationRate hexplorationRate AdaptiveEmpiricalOptimisticSource.SourceCalibration deterministicSource rounds delta rewardBound transitionBonus) : let stochasticSource := exploratorySource mdp initialState episodes rewardSource initialTable defaultState transitionBonus explorationRate hexplorationRate let projection := MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatchTrajectory (mdp