Lean module · Probability layer
BanditRLProof.ConditionalRewardPartialTrajectoryGeometricAllTime
# Generated finite-arm empirical-mean geometric all-time confidence This module instantiates the canonical action/reward trajectory's fixed-arm, fixed-successor-horizon random-pull-count empirical-mean tail at one geometric confidence share per time and arm. The compiled finite-index geometric all-time adapter then controls the union over every positive successor horizon and every arm in a nonempty finite action type. The result is a model-specific confidence producer for the canonical generated trajectory. It is not a UCB policy, pull-count regret argument, maximal inequality, optional-stopping theorem, self-normalized bound, or general Freedman inequality.
Module map
Imports
BanditRLProof.ConditionalRewardPartialTrajectoryMaskedLaw, BanditRLProof.ConcentrationFintypeGeometricAllTime
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.ConditionalExpectationReward.successorArmEmpiricalMeanFintypeGeometricAllTimeBadEvent
Compiled
The union, over every positive successor horizon and every finite arm, of the canonical positive-random-count empirical-mean failures at equal per-arm geometric confidence shares.
noncomputable def successorArmEmpiricalMeanFintypeGeometricAllTimeBadEvent {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_geometricAllTime_abs_tail_ennreal_delta_trajMeasure
Compiled
On one canonical generated action/reward trajectory, all positive successor horizons and all arms in a nonempty finite action type satisfy the random-count empirical-mean confidence radius outside one event of outer measure at most `ENNReal.ofReal delta`.
theorem actionRewardHistoryStepKernelFamily_successorArmEmpiricalMean_simultaneous_fintype_geometricAllTime_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