BanditRLProof.RL.FiniteHorizonIIDMultiBatchCumulativeConfidenceRegret

Equal confidence share assigned to every product-batch coordinate.

noncomputable def multiBatchLocalDelta (rounds : Nat) (delta : Real) : Real

Finite product of one fixed-policy iid episode-batch law.

noncomputable def iidEpisodeBatchFamilyMeasure {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (rounds episodes : Nat) : Measure (Fin rounds -> EpisodeBatch mdp episodes)

Every product coordinate has the compiled single-batch marginal law.

theorem iidEpisodeBatchFamilyMeasure_map_eval {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (rounds episodes : Nat) (round : Fin rounds) : (policy.iidEpisodeBatchFamilyMeasure initialState rounds episodes).map (Function.eval round) = policy.iidEpisodeBatchMeasure initialState episodes

Pullback of one local simultaneous-count event to a product coordinate.

def multiBatchRoundBadEvent {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (rounds episodes : Nat) (delta : Real) (round : Fin rounds) : Set (Fin rounds -> EpisodeBatch mdp episodes)

Union of the local simultaneous-count events over all product batches.

def multiBatchSimultaneousCountBadEvent {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (rounds episodes : Nat) (delta : Real) : Set (Fin rounds -> EpisodeBatch mdp episodes)

The pulled-back finite union is measurable.

theorem measurableSet_multiBatchSimultaneousCountBadEvent {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (rounds episodes : Nat) (delta : Real) : MeasurableSet (policy.multiBatchSimultaneousCountBadEvent initialState rounds episodes delta)

Each pulled-back local event has its equal-share probability bound.

theorem iidEpisodeBatchFamilyMeasure_roundBadEvent_le {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (rounds : Nat) (hrounds : 0 < rounds) (episodes : Nat) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (round : Fin rounds) : (policy.iidEpisodeBatchFamilyMeasure initialState rounds episodes) (policy.multiBatchRoundBadEvent initialState rounds episodes delta round) <= ENNReal.ofReal (multiBatchLocalDelta rounds delta)

Equal-share union over product coordinates retains the global delta.

theorem iidEpisodeBatchFamilyMeasure_multiBatchSimultaneousCountBadEvent_le {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (rounds : Nat) (hrounds : 0 < rounds) (episodes : Nat) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : (policy.iidEpisodeBatchFamilyMeasure initialState rounds episodes) (policy.multiBatchSimultaneousCountBadEvent initialState rounds episodes delta) <= ENNReal.ofReal delta

Every product batch is reward-consistent almost everywhere.

theorem iidEpisodeBatchFamilyMeasure_rewardConsistent_ae {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (rounds episodes : Nat) : ∀ᵐ batches ∂policy.iidEpisodeBatchFamilyMeasure initialState rounds episodes, ∀ round, (batches round).RewardConsistent

Batch-specific canonical empirical model at one product coordinate.

noncomputable def multiBatchEmpiricalModelAt {mdp : MDP State Action} (_policy : MarkovPolicy mdp) {rounds episodes : Nat} (batches : Fin rounds -> EpisodeBatch mdp episodes) (defaultState : State) (transitionBudget : Real) (round : Fin rounds) : MDP.FiniteBatchModel mdp episodes

Sum of batch-specific optimistic-policy expected regrets.

noncomputable def multiBatchCumulativeExpectedRegret {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) {rounds episodes : Nat} (batches : Fin rounds -> EpisodeBatch mdp episodes) (defaultState : State) (transitionBudget : Real) : Real

Sum of the batch-specific selected-radius occupancy bounds.

noncomputable def multiBatchCumulativeSelectedRadiusOccupancy {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) {rounds episodes : Nat} (batches : Fin rounds -> EpisodeBatch mdp episodes) (defaultState : State) (transitionBudget : Real) : Real

Pathwise confidence-family producer outside the finite pulled-back bad-event union, assuming the generated reward-consistency support at every coordinate.

noncomputable def allCoordinateConfidenceFamily_of_not_mem {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {rounds episodes : Nat} {delta : Real} (batches : Fin rounds -> EpisodeBatch mdp episodes) (hbatches : batches ∉ policy.multiBatchSimultaneousCountBadEvent initialState rounds episodes delta) (hreward : ∀ round, (batches round).RewardConsistent) (defaultState : State) (rewardBound transitionBudget : Real) (hrewardBound : ∀ state action, |mdp.reward state action| <= rewardBound) (htransitionBudget_nonneg : 0 <= transitionBudget) (hmargin : ∀ coordinate : VisitCoordinate mdp, simultaneousCountConfidenceRadius mdp episodes (multiBatchLocalDelta rounds delta) < coordinate.expectedCount policy initialState episodes) (hcover : ∀ (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) (action : Action), (∑ nextState, policy.expectedCountTransitionCoordinateRadius initialState episodes (multiBatchLocalDelta rounds delta) (mdp.decisionStageRemaining remaining hremaining) state action nextState * empiricalFiniteBatchValueEnvelope rewardBound transitionBudget remaining) <= transitionBudget) : ∀ round, (policy.multiBatchEmpiricalModelAt batches defaultState transitionBudget round).Confidence

Finite sums preserve all roundwise optimism and expected-regret bounds.

theorem confidenceFamily_optimism_and_cumulativeExpectedRegret {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {rounds episodes : Nat} (batches : Fin rounds -> EpisodeBatch mdp episodes) (defaultState : State) (transitionBudget : Real) (confidence : ∀ round, (policy.multiBatchEmpiricalModelAt batches defaultState transitionBudget round).Confidence) : (∀ round state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= (policy.multiBatchEmpiricalModelAt batches defaultState transitionBudget round).plan.upperValueRemaining mdp.horizon le_rfl state) ∧ policy.multiBatchCumulativeExpectedRegret initialState batches defaultState transitionBudget <= policy.multiBatchCumulativeSelectedRadiusOccupancy initialState batches defaultState transitionBudget

Mapped finite-product confidence endpoint: one global-delta event and an a.e. family of confidence witnesses, with no measurable witness selection claim.

theorem iidEpisodeBatchFamily_allCoordinate_finiteBatchModel_confidence {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (rounds : Nat) (hrounds : 0 < rounds) (episodes : Nat) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (defaultState : State) (rewardBound transitionBudget : Real) (hrewardBound : ∀ state action, |mdp.reward state action| <= rewardBound) (htransitionBudget_nonneg : 0 <= transitionBudget) (hmargin : ∀ coordinate : VisitCoordinate mdp, simultaneousCountConfidenceRadius mdp episodes (multiBatchLocalDelta rounds delta) < coordinate.expectedCount policy initialState episodes) (hcover : ∀ (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) (action : Action), (∑ nextState, policy.expectedCountTransitionCoordinateRadius initialState episodes (multiBatchLocalDelta rounds delta) (mdp.decisionStageRemaining remaining hremaining) state action nextState * empiricalFiniteBatchValueEnvelope rewardBound transitionBudget remaining) <= transitionBudget) : MeasurableSet (policy.multiBatchSimultaneousCountBadEvent initialState rounds episodes delta) ∧ (policy.iidEpisodeBatchFamilyMeasure initialState rounds episodes) (policy.multiBatchSimultaneousCountBadEvent initialState rounds episodes delta) <= ENNReal.ofReal delta ∧ ∀ᵐ batches ∂policy.iidEpisodeBatchFamilyMeasure initialState rounds episodes, batches ∉ policy.multiBatchSimultaneousCountBadEvent initialState rounds episodes delta -> Nonempty (∀ round, (policy.multiBatchEmpiricalModelAt batches defaultState transitionBudget round).Confidence)

Route endpoint: the same finite-product event simultaneously yields optimism for every batch model and the cumulative finite sum of expected-regret bounds.

theorem iidEpisodeBatchFamily_allCoordinate_optimism_and_cumulativeExpectedRegret {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (rounds : Nat) (hrounds : 0 < rounds) (episodes : Nat) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (defaultState : State) (rewardBound transitionBudget : Real) (hrewardBound : ∀ state action, |mdp.reward state action| <= rewardBound) (htransitionBudget_nonneg : 0 <= transitionBudget) (hmargin : ∀ coordinate : VisitCoordinate mdp, simultaneousCountConfidenceRadius mdp episodes (multiBatchLocalDelta rounds delta) < coordinate.expectedCount policy initialState episodes) (hcover : ∀ (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) (action : Action), (∑ nextState, policy.expectedCountTransitionCoordinateRadius initialState episodes (multiBatchLocalDelta rounds delta) (mdp.decisionStageRemaining remaining hremaining) state action nextState * empiricalFiniteBatchValueEnvelope rewardBound transitionBudget remaining) <= transitionBudget) : MeasurableSet (policy.multiBatchSimultaneousCountBadEvent initialState rounds episodes delta) ∧ (policy.iidEpisodeBatchFamilyMeasure initialState rounds episodes) (policy.multiBatchSimultaneousCountBadEvent initialState rounds episodes delta) <= ENNReal.ofReal delta ∧ ∀ᵐ batches ∂policy.iidEpisodeBatchFamilyMeasure initialState rounds episodes, batches ∉ policy.multiBatchSimultaneousCountBadEvent initialState rounds episodes delta -> (∀ round state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= (policy.multiBatchEmpiricalModelAt batches defaultState transitionBudget round).plan.upperValueRemaining mdp.horizon le_rfl state) ∧ policy.multiBatchCumulativeExpectedRegret initialState batches defaultState transitionBudget <= policy.multiBatchCumulativeSelectedRadiusOccupancy initialState batches defaultState transitionBudget