BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalSource

A trajectory whose complete stochastic batch size may vary by coordinate.

abbrev HeterogeneousStochasticEpisodeBatchTrajectory (mdp : MDP State Action) (episodes : Nat -> Nat)

A finite dependent batch history through coordinate `n`.

abbrev HeterogeneousStochasticEpisodeBatchPrefix (mdp : MDP State Action) (episodes : Nat -> Nat) (n : Nat)

An adaptive source of stochastic episode batches with coordinate-dependent batch sizes.

structure HeterogeneousAdaptiveStochasticEpisodeBatchSource (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat -> Nat) where

The one-process dependent Ionescu-Tulcea trajectory law.

noncomputable def trajectoryMeasure {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) : Measure (HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes)

Coordinate zero has the configured initial stochastic batch law.

theorem trajectoryMeasure_map_eval_zero {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) : source.trajectoryMeasure.map (Function.eval 0) = source.rewardSource.iidStochasticTrajectoryFamilyMeasure source.initialPolicy initialState (episodes 0)

Every prefix/next marginal has the configured causal `compProd` law.

theorem trajectoryMeasure_prefix_compProd {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) : source.trajectoryMeasure.map (Preorder.frestrictLe n) ⊗ₘ source.batchKernel n = source.trajectoryMeasure.map (fun trajectory => (Preorder.frestrictLe n trajectory, trajectory (n + 1)))

The regular conditional law of coordinate `n + 1` is its source kernel.

theorem trajectoryMeasure_condDistrib_nextBatch {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) [StandardBorelSpace (StochasticEpisodeBatch mdp (episodes (n + 1)))] [Nonempty (StochasticEpisodeBatch mdp (episodes (n + 1)))] : condDistrib (fun trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes => trajectory (n + 1)) (Preorder.frestrictLe n) source.trajectoryMeasure =ᵐ[ source.trajectoryMeasure.map (Preorder.frestrictLe n)] source.batchKernel n

Finite marginals of the causal law form a projective family.

theorem trajectoryMeasure_map_prefix_projective {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) {m n : Nat} (hmn : m <= n) : (source.trajectoryMeasure.map (Preorder.frestrictLe n)).map (Preorder.frestrictLe₂ (π := fun k : Nat => StochasticEpisodeBatch mdp (episodes k)) hmn) = source.trajectoryMeasure.map (Preorder.frestrictLe m)

The latest batch in a dependent finite history.

def heterogeneousLatestBatch {mdp : MDP State Action} {episodes : Nat -> Nat} {n : Nat} (history : HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n) : StochasticEpisodeBatch mdp (episodes n)

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

theorem measurable_heterogeneousLatestBatch {mdp : MDP State Action} {episodes : Nat -> Nat} {n : Nat} : Measurable (heterogeneousLatestBatch : HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n -> StochasticEpisodeBatch mdp (episodes n))

The actual-sampled optimistic table selected from dependent history.

noncomputable def heterogeneousSuccessorTable {mdp : MDP State Action} {episodes : Nat -> Nat} (defaultState : State) (rewardBudget transitionBudget : Nat -> Real) (n : Nat) (history : HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n) : DeterministicMarkovPolicyTable mdp

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

theorem measurable_heterogeneousSuccessorTable {mdp : MDP State Action} {episodes : Nat -> Nat} (defaultState : State) (rewardBudget transitionBudget : Nat -> Real) (n : Nat) : Measurable (heterogeneousSuccessorTable (mdp := mdp) (episodes := episodes) defaultState rewardBudget transitionBudget n)

Actual-sampled exploratory source with coordinate-dependent batch sizes, budgets, and exploration rates.

noncomputable def heterogeneousExploratorySource (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 n, explorationRate n <= 1) : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes where

The genuinely causal round-varying self-consistent scheduled source.

noncomputable def selfConsistentScheduledCausalSource (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState (fun n => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n)

Exact conditional and projective laws of the self-consistent causal source.

theorem selfConsistentScheduledCausalSource_trajectoryMeasure_exactLaws_and_projective (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) : let episodes := fun n => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor source.trajectoryMeasure.map (Function.eval 0) = rewardSource.iidStochasticTrajectoryFamilyMeasure (initialTable.exploratoryPolicy (AdaptiveEpisodeBatchSource.decayingExplorationRate 0) (AdaptiveEpisodeBatchSource.decayingExplorationRate_le_one 0)) initialState (episodes 0) /\ (forall n history, source.batchKernel n history = rewardSource.iidStochasticTrajectoryFamilyMeasure ((heterogeneousSuccessorTable defaultState (fun k => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRewardBudget mdp varianceProxy baseVisitFloor k) (fun k => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledTransitionBudget mdp varianceProxy baseVisitFloor k) n history).exploratoryPolicy (AdaptiveEpisodeBatchSource.decayingExplorationRate (n + 1)) (AdaptiveEpisodeBatchSource.decayingExplorationRate_le_one (n + 1))) initialState (episodes (n + 1))) /\ (forall n, condDistrib (fun trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes => trajectory (n + 1)) (Preorder.frestrictLe n) source.trajectoryMeasure =ᵐ[ source.trajectoryMeasure.map (Preorder.frestrictLe n)] source.batchKernel n) /\ (forall n, source.trajectoryMeasure.map (Preorder.frestrictLe n) ⊗ₘ source.batchKernel n = source.trajectoryMeasure.map (fun trajectory => (Preorder.frestrictLe n trajectory, trajectory (n + 1)))) /\ (forall m n (hmn : m <= n), (source.trajectoryMeasure.map (Preorder.frestrictLe n)).map (Preorder.frestrictLe₂ (π := fun k : Nat => StochasticEpisodeBatch mdp (episodes k)) hmn) = source.trajectoryMeasure.map (Preorder.frestrictLe m))