Lean module · Probability layer
BanditRLProof.ConditionalRewardPartialTrajectoryTelescopingAllTime
# Generated finite-arm empirical-mean telescoping all-time confidence This module instantiates the canonical action/reward trajectory's fixed-arm, fixed-successor-horizon random-pull-count empirical-mean tail at the telescoping confidence share `delta / ((n+1)(n+2))` per time, divided equally across arms. The resulting countable event has outer measure at most `delta` on one generated trajectory measure. The polynomial reciprocal schedule is suitable infrastructure for a later horizon-free UCB score. This result is not itself a UCB policy, pull-count or regret theorem, maximal inequality, optional-stopping theorem, or self-normalized bound.
Module map
Imports
BanditRLProof.ConditionalRewardPartialTrajectoryMaskedLaw, BanditRLProof.ConcentrationFintypeTelescopingAllTime
Imported by
BanditRLProof, BanditRLProof.Algorithms.UCBFixedPolicyTelescopingAnytimeRegret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.ConditionalExpectationReward.successorArmEmpiricalMeanFintypeTelescopingAllTimeBadEvent
Compiled
The union, over every positive successor horizon and finite arm, of the canonical positive-random-count empirical-mean failures at equal per-arm telescoping confidence shares.
noncomputable def successorArmEmpiricalMeanFintypeTelescopingAllTimeBadEvent {Omega : Type u} {Action : Type x} [Fintype Action] [DecidableEq Action] (action : Omega -> ActionTrace Action) (reward : Omega -> RewardTrace Rat) (armMean : Action -> Rat) (sigma2 : NNReal) (delta : Real) : Set Omega
theorem
BanditRLProof.ConditionalExpectationReward.actionRewardHistoryStepKernelFamily_successorArmEmpiricalMean_simultaneous_fintype_telescopingAllTime_abs_tail_ennreal_delta_trajMeasure
Compiled
On one canonical generated action/reward trajectory, every positive successor horizon and every arm satisfies the random-count empirical-mean radius outside one telescoping-schedule event of outer measure at most `ENNReal.ofReal delta`.
theorem actionRewardHistoryStepKernelFamily_successorArmEmpiricalMean_simultaneous_fintype_telescopingAllTime_abs_tail_ennreal_delta_trajMeasure {Context : Type v} {State : Type w} {Action : Type x} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [StandardBorelSpace Action] [MeasurableSingletonClass Action] [Fintype Action] [Nonempty Action] [DecidableEq Action] (mu0 : Measure (Prod Action Rat)) [IsProbabilityMeasure mu0] (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) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (mean : Context -> Action -> Rat) (varianceProxy : Context -> Action -> NNReal) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hmean : Measurable (fun pair : Prod Context Action => mean pair.1 pair.2)) (armMean : Action -> Rat) (sigma2 : NNReal) (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 : Action, mean (context i history) arm = armMean arm) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) : let pairContext : (i : Nat) -> ((j : Finset.Iic i) -> Prod Action Rat) -> Context