BanditRLProof.Algorithms.UCBConditionalRewardLaw

Successor empirical mean at the positive horizon `t + 1`.

noncomputable def selectedPolicySuccessorEmpiricalMeanAt {Omega : Type u} {Action : Type} [DecidableEq Action] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Rat) (omega : Omega) (t : Nat) (arm : Action) : Real

Realized-count confidence width used at one arm/time pair.

noncomputable def selectedPolicySuccessorRadiusAt {Omega : Type u} {Action : Type} [DecidableEq Action] (action : Omega -> ActionTrace Action) (sigma2 : NNReal) (arms : Finset Action) (T : Nat) (delta : Real) (omega : Omega) (t : Nat) (arm : Action) : Real

Practical UCB index with a sample-dependent realized-count width.

noncomputable def selectedPolicySuccessorIndexAt {Omega : Type u} {Action : Type} [DecidableEq Action] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Rat) (sigma2 : NNReal) (arms : Finset Action) (T : Nat) (delta : Real) (omega : Omega) (t : Nat) (arm : Action) : Real

Initialization and score-maximality contract for the finite set of charged UCB times. The time set may omit initialization rounds; every retained time must lie below `T`, and both the designated best arm and the selected arm must have positive realized successor pull counts.

structure SelectedPolicySuccessorInitializedScoreMaxSource {Omega : Type u} {Action : Type} [DecidableEq Action] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Rat) (arms : Finset Action) (armMean : Action -> Rat) (sigma2 : NNReal) (T : Nat) (delta : Real) where

Large-gap selected-time event charged by the practical confidence event.

noncomputable def selectedPolicySuccessorLargeGapEvent {Omega : Type u} {Action : Type} [DecidableEq Action] {action : Omega -> ActionTrace Action} {reward : Omega -> RewardTrace Rat} {arms : Finset Action} {armMean : Action -> Rat} {sigma2 : NNReal} {T : Nat} {delta : Real} (source : SelectedPolicySuccessorInitializedScoreMaxSource action reward arms armMean sigma2 T delta) : Set Omega

Outside the practical simultaneous confidence event, score maximality implies the standard UCB gap bound at every initialized charged time.

theorem SelectedPolicySuccessorInitializedScoreMaxSource.meanGap_le_two_radius_of_not_badEvent {Omega : Type u} {Action : Type} [DecidableEq Action] {action : Omega -> ActionTrace Action} {reward : Omega -> RewardTrace Rat} {arms : Finset Action} {armMean : Action -> Rat} {sigma2 : NNReal} {T : Nat} {delta : Real} (source : SelectedPolicySuccessorInitializedScoreMaxSource action reward arms armMean sigma2 T delta) (omega : Omega) (t : Nat) (ht : t ∈ source.times) (hgood : omega ∉ ConditionalExpectationReward.successorArmEmpiricalMeanFiniteArmTimeBadEvent action reward arms armMean sigma2 T delta) : meanGap (fun arm => (armMean arm : Real)) source.best (source.chosen omega t) <= 2 * selectedPolicySuccessorRadiusAt action sigma2 arms T delta omega t (source.chosen omega t)

Practical selected-policy UCB large-gap event bound on initialized times. The simultaneous empirical-mean theorem supplies the probability bound. The source contract turns any large-gap score-maximal selection outside that event into a contradiction via the deterministic UCB confidence algebra.

theorem measure_selectedPolicySuccessorLargeGapEvent_le_ennreal_delta_of_reward_map_eq_selected_policy_definitionalRawRangeMeasurableMeanRangeHistoryVarianceBounded {Omega : Type u} {Context : Type v} {State : Type w} {Action : Type} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] [DecidableEq Action] (mu : Measure Omega) [IsProbabilityMeasure mu] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (state : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> State) (mean : Context -> Action -> Rat) (varianceProxy : Context -> Action -> NNReal) (defaultAction : Action) (arms : Finset Action) (harms : arms.Nonempty) (armMean : Action -> Rat) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (rewardLo rewardHi meanLo meanHi : Nat -> Real) (sigma2 : NNReal) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (hmean : Measurable (fun pair : Prod Context Action => mean pair.1 pair.2)) (hkernel : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hraw : forall i : Nat, forall omega : Omega, Set.Icc (rewardLo i) (rewardHi i) (((reward omega (i + 1) : Rat) : Real))) (hmean_range : forall i : Nat, forall context : Context, forall action : Action, Set.Icc (meanLo i) (meanHi i) (((mean context action : Rat) : Real))) (hvariance : forall i : Nat, forall history : ((j : Finset.Iic i) -> Rat), varianceProxy (context i history) ((policy i).action (state i history)) <= sigma2) (harmMean : forall i : Nat, forall history : ((j : Finset.Iic i) -> Rat), forall arm, arm ∈ arms -> mean (context i history) arm = armMean arm) (h_reward_map_eq_policy : forall i : Nat, Filter.Eventually (fun omega : Omega => @Measure.map Omega Rat mOmega inferInstance (fun y : Omega => reward y (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc (ConditionalExpectationReward.generatedActionFromRewardHistory policy state defaultAction reward) reward (ConditionalExpectationReward.generatedActionFromRewardHistory_measurable (policy