BanditRLProof.Algorithms.UCBConditionalRewardPairTrajectorySampledAsymptotics

Confidence schedule used by the fixed-model asymptotic UCB family.

noncomputable def selectedPolicySuccessorAsymptoticDelta (T : Nat) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem selectedPolicySuccessorAsymptoticDelta_pos (T : Nat) : 0 < selectedPolicySuccessorAsymptoticDelta T

No declaration docstring is present; use the chapter context and exact statement below.

theorem horizon_mul_selectedPolicySuccessorAsymptoticDelta_le_one (T : Nat) : (T : Real) * selectedPolicySuccessorAsymptoticDelta T <= 1

Under the asymptotic schedule, the full-horizon peeling argument is a polynomial.

theorem selectedPolicySuccessorFiniteArmTimeLogBudget_asymptoticDelta_eq (K T : Nat) (hK : 0 < K) (hT : 0 < T) : selectedPolicySuccessorFiniteArmTimeLogBudget K T T (selectedPolicySuccessorAsymptoticDelta T) = max (Real.log (2 * (K : Real) * (T : Real) * (T : Real) * (((T + 1 : Nat) : Real)))) 0

Eventually, the scheduled finite-arm/time peeling budget is at most `4 log(T+1)`.

theorem selectedPolicySuccessorFiniteArmTimeLogBudget_asymptoticDelta_le (K T : Nat) (hK : 0 < K) (hT : 0 < T) (hlarge : 2 * K <= T + 1) : selectedPolicySuccessorFiniteArmTimeLogBudget K T T (selectedPolicySuccessorAsymptoticDelta T) <= 4 * Real.log (((T + 1 : Nat) : Real))

Fixed coefficient that absorbs one positive-gap arm's scheduled textbook budget.

noncomputable def selectedPolicySuccessorAsymptoticGapCoefficient (sigma2 : NNReal) (gap : Real) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem selectedPolicySuccessorTextbookGapBudget_add_failure_asymptoticDelta_le (K : Nat) (sigma2 : NNReal) (T : Nat) (gap : Real) (hK : 0 < K) (hT : 0 < T) (hlarge : 2 * K <= T + 1) (hgap : 0 < gap) : selectedPolicySuccessorTextbookGapBudget K sigma2 T (selectedPolicySuccessorAsymptoticDelta T) gap + gap * ((T : Real) * selectedPolicySuccessorAsymptoticDelta T) <= selectedPolicySuccessorAsymptoticGapCoefficient sigma2 gap * (1 + Real.log (((T + 1 : Nat) : Real)))

Fixed finite-arm coefficient for the asymptotic textbook UCB envelope.

noncomputable def selectedPolicySuccessorAsymptoticModelCoefficient {K : Nat} (model : FiniteBanditModel K) (sigma2 : NNReal) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem selectedPolicySuccessorTextbookGapSum_asymptoticDelta_le {K : Nat} (model : FiniteBanditModel K) (sigma2 : NNReal) (T : Nat) (hT : 0 < T) (hlarge : 2 * K <= T + 1) : ((Finset.univ : Finset (Fin K)).filter (fun arm => 0 < (((model.gap arm : Rat) : Real)))).sum (fun arm => selectedPolicySuccessorTextbookGapBudget K sigma2 T (selectedPolicySuccessorAsymptoticDelta T) (((model.gap arm : Rat) : Real)) + (((model.gap arm : Rat) : Real)) * ((T : Real) * selectedPolicySuccessorAsymptoticDelta T)) <= selectedPolicySuccessorAsymptoticModelCoefficient model sigma2 * (1 + Real.log (((T + 1 : Nat) : Real)))

Exact sampled-successor expected pseudo-regret for the canonical pair process at confidence budget `1 / (T + 1)`.

noncomputable def selectedPolicySuccessorActionRewardTrajMeasureExpectedPseudoRegret {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) (defaultAction : Fin K) (sigma2 : NNReal) (hcontext : forall n : Nat, Measurable (context n)) (T : Nat) : Real

Pointwise fixed-horizon envelope used by the asymptotic route.

theorem selectedPolicySuccessorActionRewardTrajMeasureExpectedPseudoRegret_nonneg_and_le {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) (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, forall history : ((j : Finset.Iic i) -> Rat), forall arm : Fin K, varianceProxy (context i history) arm <= sigma2) (harmMean : forall i : Nat, forall history : ((j : Finset.Iic i) -> Rat), forall arm : Fin K, mean (context i history) arm = model.mean arm) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (T : Nat) (hT : 0 < T) (hlarge : 2 * K <= T + 1) : 0 <= selectedPolicySuccessorActionRewardTrajMeasureExpectedPseudoRegret model mu0 rewardKernel context defaultAction sigma2 hcontext T /\ selectedPolicySuccessorActionRewardTrajMeasureExpectedPseudoRegret model mu0 rewardKernel context defaultAction sigma2 hcontext T <= selectedPolicySuccessorAsymptoticModelCoefficient model sigma2 * (1 + Real.log (((T + 1 : Nat) : Real)))

No declaration docstring is present; use the chapter context and exact statement below.

theorem selectedPolicySuccessorAsymptoticModelCoefficient_nonneg {K : Nat} (model : FiniteBanditModel K) (sigma2 : NNReal) : 0 <= selectedPolicySuccessorAsymptoticModelCoefficient model sigma2

No declaration docstring is present; use the chapter context and exact statement below.

theorem one_add_log_natCast_succ_isBigO_log_natCast_succ : (fun T : Nat => 1 + Real.log (((T + 1 : Nat) : Real))) =O[atTop] (fun T : Nat => Real.log (((T + 1 : Nat) : Real)))

For fixed model and reward-law data, the exact canonical sampled-successor expected pseudo-regret is logarithmic for the horizon-indexed confidence schedule `1 / (T + 1)`.

theorem selectedPolicySuccessorActionRewardTrajMeasureExpectedPseudoRegret_isBigO_log {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) (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, forall history : ((j : Finset.Iic i) -> Rat), forall arm : Fin K, varianceProxy (context i history) arm <= sigma2) (harmMean : forall i : Nat, forall history : ((j : Finset.Iic i) -> Rat), forall arm : Fin K, mean (context i history) arm = model.mean arm) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) : (selectedPolicySuccessorActionRewardTrajMeasureExpectedPseudoRegret model mu0 rewardKernel context defaultAction sigma2 hcontext) =O[atTop] (fun T : Nat => Real.log (((T + 1 : Nat) : Real)))

No declaration docstring is present; use the chapter context and exact statement below.

theorem log_natCast_succ_isLittleO_natCast_succ : (fun T : Nat => Real.log (((T + 1 : Nat) : Real))) =o[atTop] (fun T : Nat => (((T + 1 : Nat) : Real)))

No declaration docstring is present; use the chapter context and exact statement below.

theorem selectedPolicySuccessorActionRewardTrajMeasureExpectedPseudoRegret_isLittleO_natCast_succ {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) (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, forall history : ((j : Finset.Iic i) -> Rat), forall arm : Fin K, varianceProxy (context i history) arm <= sigma2) (harmMean : forall i : Nat, forall history : ((j : Finset.Iic i) -> Rat), forall arm : Fin K, mean (context i history) arm = model.mean arm) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) : (selectedPolicySuccessorActionRewardTrajMeasureExpectedPseudoRegret model mu0 rewardKernel context defaultAction sigma2 hcontext) =o[atTop] (fun T : Nat => (((T + 1 : Nat) : Real)))

Expected sampled-successor pseudo-regret normalized by `T + 1`.

noncomputable def selectedPolicySuccessorActionRewardTrajMeasureExpectedAveragePseudoRegret {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) (defaultAction : Fin K) (sigma2 : NNReal) (hcontext : forall n : Nat, Measurable (context n)) (T : Nat) : Real

For the fixed-model horizon-indexed canonical UCB family, expected sampled-successor pseudo-regret normalized by `T + 1` tends to zero.

theorem selectedPolicySuccessorActionRewardTrajMeasureExpectedAveragePseudoRegret_tendsto_zero {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) (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, forall history : ((j : Finset.Iic i) -> Rat), forall arm : Fin K, varianceProxy (context i history) arm <= sigma2) (harmMean : forall i : Nat, forall history : ((j : Finset.Iic i) -> Rat), forall arm : Fin K, mean (context i history) arm = model.mean arm) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) : Tendsto (selectedPolicySuccessorActionRewardTrajMeasureExpectedAveragePseudoRegret model mu0 rewardKernel context defaultAction sigma2 hcontext) atTop (nhds 0)