Lean module · UCB
BanditRLProof.Algorithms.UCBConditionalRewardPairTrajectory
# Canonical pair-trajectory UCB confidence consumer This module consumes the canonical action/reward trajectory simultaneous empirical-mean event in the random-width UCB score algebra. It proves a fixed finite-arm/time large-gap event bound, a positive-gap chosen-arm explicit-threshold tail/ENNReal expected pull-count bound, and the resulting finite-arm explicit-threshold and textbook positive-gap ENNReal pseudo-regret sums. It requires a `CenteredRewardKernelLaw`, but no caller selected-reward trajectory law or reward-range premise. It does not prove anytime confidence, an asymptotic normalization, or a Real/Bochner expectation endpoint.
Module map
Imports
BanditRLProof.Algorithms.UCBConditionalRewardLaw, BanditRLProof.Algorithms.UCBConditionalRewardLawPolicy, BanditRLProof.Algorithms.UCBConditionalRewardLawRegret, BanditRLProof.ConditionalRewardPartialTrajectoryMaskedLaw
Imported by
BanditRLProof, BanditRLProof.Algorithms.UCBConditionalRewardPairTrajectoryReal, BanditRLProof.Algorithms.UCBFixedPolicyTelescopingAnytimeRegret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.UCB.measure_actionRewardHistoryStepKernelFamily_selectedPolicySuccessorLargeGapEvent_le_ennreal_delta_trajMeasure
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem measure_actionRewardHistoryStepKernelFamily_selectedPolicySuccessorLargeGapEvent_le_ennreal_delta_trajMeasure {Context : Type u} {State : Type v} {Action : Type} [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [StandardBorelSpace Action] [MeasurableSingletonClass Action] [Countable 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)) (arms : Finset Action) (harms : arms.Nonempty) (armMean : Action -> Rat) (sigma2 : NNReal) (T : Nat) (hvariance : forall i : Nat, i < T - 1 -> 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) (hT : 0 < T) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) (source : SelectedPolicySuccessorInitializedScoreMaxSource (fun trajectory : Nat -> Prod Action Rat => fun t => (trajectory t).1) (fun trajectory : Nat -> Prod Action Rat => fun t => (trajectory t).2) arms armMean sigma2 T delta) : let pairContext : (i : Nat) -> ((j : Finset.Iic i) -> Prod Action Rat) -> Context
theorem
BanditRLProof.UCB.measure_selectedPolicySuccessorLargeGapEvent_generatedUCB_le_ennreal_delta_actionRewardTrajMeasure_centeredKernel
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem measure_selectedPolicySuccessorLargeGapEvent_generatedUCB_le_ennreal_delta_actionRewardTrajMeasure_centeredKernel {Context : Type u} {K : Nat} [MeasurableSpace Context] (hK : 0 < K) (mu0 : Measure (Prod (Fin K) Rat)) [IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context (Fin K)) Rat) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (mean : Context -> Fin K -> Rat) (varianceProxy : Context -> Fin K -> NNReal) (defaultAction best : Fin K) (armMean : Fin K -> Rat) (sigma2 : NNReal) (T : Nat) (delta : Real) (hcontext : forall n : Nat, Measurable (context n)) (hmean : Measurable (fun pair : Prod Context (Fin K) => mean pair.1 pair.2)) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hvariance : forall i : Nat, i < T - 1 -> forall history : ((j : Finset.Iic i) -> Rat), varianceProxy (context i history) ((selectedPolicySuccessorHistoryPolicy hK sigma2 T delta defaultAction i).action (selectedPolicySuccessorHistoryState hK sigma2 T delta defaultAction i history)) <= sigma2) (harmMean : forall i : Nat, forall history : ((j : Finset.Iic i) -> Rat), forall arm : Fin K, mean (context i history) arm = armMean arm) (hT : 0 < T) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (hdelta : 0 < delta) : let policy := selectedPolicySuccessorHistoryPolicy hK sigma2 T delta defaultAction let state := selectedPolicySuccessorHistoryState hK sigma2 T delta defaultAction let pairContext : (i : Nat) -> ((j : Finset.Iic i) -> Prod (Fin K) Rat) -> Context
theorem
BanditRLProof.UCB.measure_successorArmPullCount_selectedPolicySuccessorGeneratedUCBAction_gt_explicitPullThreshold_le_ennreal_delta_actionRewardTrajMeasure_centeredKernel
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem measure_successorArmPullCount_selectedPolicySuccessorGeneratedUCBAction_gt_explicitPullThreshold_le_ennreal_delta_actionRewardTrajMeasure_centeredKernel {Context : Type u} {K : Nat} [MeasurableSpace Context] (hK : 0 < K) (mu0 : Measure (Prod (Fin K) Rat)) [IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context (Fin K)) Rat) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (mean : Context -> Fin K -> Rat) (varianceProxy : Context -> Fin K -> NNReal) (defaultAction best chosen : Fin K) (armMean : Fin K -> Rat) (sigma2 : NNReal) (T : Nat) (delta : Real) (hcontext : forall n : Nat, Measurable (context n)) (hmean : Measurable (fun pair : Prod Context (Fin K) => mean pair.1 pair.2)) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hvariance : forall i : Nat, i < T - 1 -> forall history : ((j : Finset.Iic i) -> Rat), varianceProxy (context i history) ((selectedPolicySuccessorHistoryPolicy hK sigma2 T delta defaultAction i).action (selectedPolicySuccessorHistoryState hK sigma2 T delta defaultAction i history)) <= sigma2) (harmMean : forall i : Nat, forall history : ((j : Finset.Iic i) -> Rat), forall arm : Fin K, mean (context i history) arm = armMean arm) (hT : 0 < T) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (hdelta : 0 < delta) (hgap : 0 < meanGap (fun arm => (armMean arm : Real)) best chosen) : let policy := selectedPolicySuccessorHistoryPolicy hK sigma2 T delta defaultAction let state := selectedPolicySuccessorHistoryState hK sigma2 T delta defaultAction let pairContext : (i : Nat) -> ((j : Finset.Iic i) -> Prod (Fin K) Rat) -> Context
theorem
BanditRLProof.UCB.lintegral_successorArmPullCount_selectedPolicySuccessorGeneratedUCBAction_le_explicitPullThreshold_add_horizon_mul_delta_actionRewardTrajMeasure_centeredKernel
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem lintegral_successorArmPullCount_selectedPolicySuccessorGeneratedUCBAction_le_explicitPullThreshold_add_horizon_mul_delta_actionRewardTrajMeasure_centeredKernel {Context : Type u} {K : Nat} [MeasurableSpace Context] (hK : 0 < K) (mu0 : Measure (Prod (Fin K) Rat)) [IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context (Fin K)) Rat) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (mean : Context -> Fin K -> Rat) (varianceProxy : Context -> Fin K -> NNReal) (defaultAction best chosen : Fin K) (armMean : Fin K -> Rat) (sigma2 : NNReal) (T : Nat) (delta : Real) (hcontext : forall n : Nat, Measurable (context n)) (hmean : Measurable (fun pair : Prod Context (Fin K) => mean pair.1 pair.2)) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hvariance : forall i : Nat, i < T - 1 -> forall history : ((j : Finset.Iic i) -> Rat), varianceProxy (context i history) ((selectedPolicySuccessorHistoryPolicy hK sigma2 T delta defaultAction i).action (selectedPolicySuccessorHistoryState hK sigma2 T delta defaultAction i history)) <= sigma2) (harmMean : forall i : Nat, forall history : ((j : Finset.Iic i) -> Rat), forall arm : Fin K, mean (context i history) arm = armMean arm) (hT : 0 < T) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (hdelta : 0 < delta) (hgap : 0 < meanGap (fun arm => (armMean arm : Real)) best chosen) : let policy := selectedPolicySuccessorHistoryPolicy hK sigma2 T delta defaultAction let state := selectedPolicySuccessorHistoryState hK sigma2 T delta defaultAction let pairContext : (i : Nat) -> ((j : Finset.Iic i) -> Prod (Fin K) Rat) -> Context
theorem
BanditRLProof.UCB.lintegral_ofReal_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction_le_explicitThresholdSum_actionRewardTrajMeasure_centeredKernel
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem lintegral_ofReal_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction_le_explicitThresholdSum_actionRewardTrajMeasure_centeredKernel {Context : Type u} {K : Nat} [MeasurableSpace Context] (model : FiniteBanditModel K) (mu0 : Measure (Prod (Fin K) Rat)) [IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context (Fin K)) Rat) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (mean : Context -> Fin K -> Rat) (varianceProxy : Context -> Fin K -> NNReal) (defaultAction : Fin K) (sigma2 : NNReal) (T : Nat) (delta : Real) (hcontext : forall n : Nat, Measurable (context n)) (hmean : Measurable (fun pair : Prod Context (Fin K) => mean pair.1 pair.2)) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hvariance : forall i : Nat, i < T - 1 -> forall history : ((j : Finset.Iic i) -> Rat), varianceProxy (context i history) ((selectedPolicySuccessorHistoryPolicy model.hK sigma2 T delta defaultAction i).action (selectedPolicySuccessorHistoryState model.hK sigma2 T delta defaultAction i history)) <= sigma2) (harmMean : forall i : Nat, forall history : ((j : Finset.Iic i) -> Rat), forall arm : Fin K, mean (context i history) arm = model.mean arm) (hT : 0 < T) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (hdelta : 0 < delta) : let policy := selectedPolicySuccessorHistoryPolicy model.hK sigma2 T delta defaultAction let state := selectedPolicySuccessorHistoryState model.hK sigma2 T delta defaultAction let pairContext : (i : Nat) -> ((j : Finset.Iic i) -> Prod (Fin K) Rat) -> Context
theorem
BanditRLProof.UCB.lintegral_ofReal_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction_le_textbookGapSum_actionRewardTrajMeasure_centeredKernel
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem lintegral_ofReal_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction_le_textbookGapSum_actionRewardTrajMeasure_centeredKernel {Context : Type u} {K : Nat} [MeasurableSpace Context] (model : FiniteBanditModel K) (mu0 : Measure (Prod (Fin K) Rat)) [IsProbabilityMeasure mu0] (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context (Fin K)) Rat) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (mean : Context -> Fin K -> Rat) (varianceProxy : Context -> Fin K -> NNReal) (defaultAction : Fin K) (sigma2 : NNReal) (T : Nat) (delta : Real) (hcontext : forall n : Nat, Measurable (context n)) (hmean : Measurable (fun pair : Prod Context (Fin K) => mean pair.1 pair.2)) (law : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hvariance : forall i : Nat, i < T - 1 -> forall history : ((j : Finset.Iic i) -> Rat), varianceProxy (context i history) ((selectedPolicySuccessorHistoryPolicy model.hK sigma2 T delta defaultAction i).action (selectedPolicySuccessorHistoryState model.hK sigma2 T delta defaultAction i history)) <= sigma2) (harmMean : forall i : Nat, forall history : ((j : Finset.Iic i) -> Rat), forall arm : Fin K, mean (context i history) arm = model.mean arm) (hT : 0 < T) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (hdelta : 0 < delta) : let policy := selectedPolicySuccessorHistoryPolicy model.hK sigma2 T delta defaultAction let state := selectedPolicySuccessorHistoryState model.hK sigma2 T delta defaultAction let pairContext : (i : Nat) -> ((j : Finset.Iic i) -> Prod (Fin K) Rat) -> Context