BanditRLProof.RL.FiniteHorizonAdaptiveEmpiricalOptimisticConfidence

Compressing a batch preserves every visit count.

theorem transitionCountSummary_visitCount {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (stage : Fin mdp.horizon) (state : State) (action : Action) : batch.transitionCountSummary.visitCount stage state action = batch.visitCount stage state action

The summary-normalized PMF is exactly the raw batch empirical PMF.

theorem transitionCountSummary_empiricalTransitionPMF {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (defaultState : State) (stage : Fin mdp.horizon) (state : State) (action : Action) : batch.transitionCountSummary.empiricalTransitionPMF defaultState stage state action = batch.empiricalTransitionPMF defaultState stage state action

The summary kernel singleton mass is the named raw empirical mass.

theorem transitionCountSummary_empiricalTransitionKernel_real_singleton {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (defaultState : State) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : (batch.transitionCountSummary.empiricalTransitionKernel defaultState stage (state, action)).real {nextState} = batch.empiricalTransitionMass defaultState stage state action nextState

The known-reward empirical plan has the same explicit linear value envelope as the raw empirical model when the fixed transition bonus is nonnegative.

theorem optimisticPlan_upperValueRemaining_abs_le (mdp : MDP State Action) (summary : TransitionCountSummary mdp) (defaultState : State) (rewardBound transitionBonus : Real) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (htransitionBonus_nonneg : 0 <= transitionBonus) : forall (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State), |(summary.optimisticPlan mdp defaultState transitionBonus).upperValueRemaining remaining hremaining state| <= empiricalFiniteBatchValueEnvelope rewardBound transitionBonus remaining

Policy-local statistical calibration needed to make the fixed transition bonus cover all finite-state empirical transition-coordinate errors.

structure EmpiricalOptimisticCalibration {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (delta rewardBound transitionBonus : Real) : Prop where

One good generated batch and one calibration contract produce coordinate confidence for the exact known-reward empirical plan used by the source.

noncomputable def empiricalOptimisticPlanCoordinateConfidence_of_not_mem {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} {delta : Real} (batch : EpisodeBatch mdp episodes) (hbatch : batch ∉ policy.simultaneousCountBadEvent initialState episodes delta) (defaultState : State) (rewardBound transitionBonus : Real) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (htransitionBonus_nonneg : 0 <= transitionBonus) (calibration : policy.EmpiricalOptimisticCalibration initialState episodes delta rewardBound transitionBonus) : (batch.transitionCountSummary.optimisticPlan mdp defaultState transitionBonus).CoordinateConfidence where

Action law that explores uniformly with the supplied probability and otherwise uses the deterministic optimistic table action.

noncomputable def exploratoryActionPMF {mdp : MDP State Action} (table : DeterministicMarkovPolicyTable mdp) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (stage : Fin mdp.horizon) (state : State) : PMF Action

Every action receives at least its uniform-exploration mass.

theorem explorationRate_mul_inv_card_le_exploratoryActionPMF {mdp : MDP State Action} (table : DeterministicMarkovPolicyTable mdp) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (stage : Fin mdp.horizon) (state : State) (action : Action) : (explorationRate : ENNReal) * (Fintype.card Action : ENNReal)⁻¹ <= table.exploratoryActionPMF explorationRate hexplorationRate stage state action

Markov behavior policy obtained by uniformly exploring around one table.

noncomputable def exploratoryPolicy {mdp : MDP State Action} (table : DeterministicMarkovPolicyTable mdp) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) : MarkovPolicy mdp where

Iid generated episode-batch kernel indexed by exploratory table policies.

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

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

theorem exploratoryIIDEpisodeBatchKernel_apply {mdp : MDP State Action} (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (table : DeterministicMarkovPolicyTable mdp) : exploratoryIIDEpisodeBatchKernel initialState episodes explorationRate hexplorationRate table = (table.exploratoryPolicy explorationRate hexplorationRate).iidEpisodeBatchMeasure initialState episodes

The known-reward empirical plan selected from one batch coordinate.

noncomputable def adaptiveEmpiricalOptimisticPlanAt {mdp : MDP State Action} {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (defaultState : State) (transitionBonus : Real) (round : Nat) : mdp.EstimatedModelPlan

Sum of expected regrets of the optimistic policies recommended by each batch.

noncomputable def adaptiveEmpiricalOptimisticRecommendedExpectedRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (defaultState : State) (transitionBonus : Real) (rounds : Nat) : Real

Sum of the confidence-produced occupancy radius bounds after each batch.

noncomputable def adaptiveEmpiricalOptimisticOccupancyRadiusSum {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (defaultState : State) (transitionBonus : Real) (rounds : Nat) : Real

Concrete behavior source with uniform action exploration around every latest-batch optimistic table.

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

The exploratory successor behavior is centered on the latest optimistic table.

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

Measurability of finite-table-selected exploratory count events.

theorem measurableSet_selectedExploratorySimultaneousCountBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} {History : Type*} [MeasurableSpace History] (selector : History -> DeterministicMarkovPolicyTable mdp) (hselector : Measurable selector) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (delta : Real) : MeasurableSet {pair : History × EpisodeBatch mdp episodes | pair.2 ∈ ((selector pair.1).exploratoryPolicy explorationRate hexplorationRate).simultaneousCountBadEvent initialState episodes delta}

Every selected successor event of the exploratory source is measurable.

theorem exploratorySource_measurableSet_successorSimultaneousCountBadEvent {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) (n : Nat) : MeasurableSet (AdaptiveEpisodeBatchSource.successorSimultaneousCountBadEvent (exploratorySource mdp initialState episodes initialTable defaultState transitionBonus explorationRate hexplorationRate) rounds delta n)

The exploratory behavior source inherits the adaptive global count event.

theorem exploratorySource_trajectoryMeasure_adaptiveSimultaneousCountConfidence {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) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : let behaviorSource := exploratorySource mdp initialState episodes initialTable defaultState transitionBonus explorationRate hexplorationRate MeasurableSet (behaviorSource.adaptiveSimultaneousCountBadEvent rounds delta) ∧ behaviorSource.trajectoryMeasure (behaviorSource.adaptiveSimultaneousCountBadEvent rounds delta) <= ENNReal.ofReal delta ∧ forall trajectory, trajectory ∉ behaviorSource.adaptiveSimultaneousCountBadEvent rounds delta -> forall round : Fin rounds, forall coordinate : CountCoordinate mdp, |coordinate.deviation (behaviorSource.policyAt trajectory round) initialState (trajectory round)| < simultaneousCountConfidenceRadius mdp episodes (multiBatchLocalDelta rounds delta)

The plan from batch `n` is exactly the source policy used at `n + 1`.

theorem source_policyAt_succ_eq_adaptiveEmpiricalOptimisticPlanAt {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (transitionBonus : Real) (trajectory : EpisodeBatchTrajectory mdp episodes) (n : Nat) : let concreteSource := source mdp initialState episodes initialTable defaultState transitionBonus concreteSource.policyAt trajectory (n + 1) = (adaptiveEmpiricalOptimisticPlanAt (mdp

Outside the adaptive union, every batch avoids its selected local event.

theorem policyAt_batch_not_mem_simultaneousCountBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes rounds : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) {delta : Real} (trajectory : EpisodeBatchTrajectory mdp episodes) (htrajectory : trajectory ∉ source.adaptiveSimultaneousCountBadEvent rounds delta) (round : Fin rounds) : trajectory round ∉ (source.policyAt trajectory round).simultaneousCountBadEvent initialState episodes (multiBatchLocalDelta rounds delta)

Calibration contract selected by the data-generating policy at each round.

def SourceCalibration {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (delta rewardBound transitionBonus : Real) : Prop

Every observed batch plan has coordinate confidence outside the global event.

noncomputable def exploratorySource_coordinateConfidenceAt_of_not_mem {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes rounds : Nat} (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (rewardBound transitionBonus delta : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (htransitionBonus_nonneg : 0 <= transitionBonus) (calibration : let behaviorSource := exploratorySource mdp initialState episodes initialTable defaultState transitionBonus explorationRate hexplorationRate SourceCalibration behaviorSource rounds delta rewardBound transitionBonus) (trajectory : EpisodeBatchTrajectory mdp episodes) (htrajectory : trajectory ∉ (exploratorySource mdp initialState episodes initialTable defaultState transitionBonus explorationRate hexplorationRate).adaptiveSimultaneousCountBadEvent rounds delta) (round : Fin rounds) : (adaptiveEmpiricalOptimisticPlanAt (mdp

Outside the one adaptive event, every batch plan is optimistic and the finite sum of recommended optimistic-policy expected regrets is radius-controlled.

theorem exploratorySource_optimism_and_recommendedExpectedRegret_of_not_mem {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes rounds : Nat} (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (rewardBound transitionBonus delta : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (htransitionBonus_nonneg : 0 <= transitionBonus) (calibration : let behaviorSource := exploratorySource mdp initialState episodes initialTable defaultState transitionBonus explorationRate hexplorationRate SourceCalibration behaviorSource rounds delta rewardBound transitionBonus) (trajectory : EpisodeBatchTrajectory mdp episodes) (htrajectory : trajectory ∉ (exploratorySource mdp initialState episodes initialTable defaultState transitionBonus explorationRate hexplorationRate).adaptiveSimultaneousCountBadEvent rounds delta) : (forall round : Fin rounds, forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= (adaptiveEmpiricalOptimisticPlanAt (mdp

Route endpoint: calibrated all-coordinate confidence, global optimism, and a finite recommended-policy expected-regret sum under one global delta event.

theorem exploratorySource_trajectoryMeasure_allCoordinateConfidence_optimism_and_recommendedExpectedRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (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 behaviorSource := exploratorySource mdp initialState episodes initialTable defaultState transitionBonus explorationRate hexplorationRate SourceCalibration behaviorSource rounds delta rewardBound transitionBonus) : let behaviorSource := exploratorySource mdp initialState episodes initialTable defaultState transitionBonus explorationRate hexplorationRate let bad := behaviorSource.adaptiveSimultaneousCountBadEvent rounds delta MeasurableSet bad /\ behaviorSource.trajectoryMeasure bad <= ENNReal.ofReal delta /\ forall trajectory, trajectory ∉ bad -> (forall round : Fin rounds, forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= (adaptiveEmpiricalOptimisticPlanAt (mdp