BanditRLProof.Algorithms.UCBFixedPolicyTelescopingAnytimeRegret

Realized-count radius with the time-`t` telescoping share divided over the finite arm set.

noncomputable def selectedPolicySuccessorTelescopingRadiusAt {Omega : Type} {K : Nat} (action : Omega -> ActionTrace (Fin K)) (sigma2 : NNReal) (delta : Real) (omega : Omega) (t : Nat) (arm : Fin K) : Real

The scheduled radius is nonnegative, including its explicit zero-count convention inherited from division in `Real`.

theorem selectedPolicySuccessorTelescopingRadiusAt_nonneg {Omega : Type} {K : Nat} (action : Omega -> ActionTrace (Fin K)) (sigma2 : NNReal) (delta : Real) (omega : Omega) (t : Nat) (arm : Fin K) : 0 <= selectedPolicySuccessorTelescopingRadiusAt action sigma2 delta omega t arm

The horizon-free scheduled UCB index on an action/reward trace.

noncomputable def selectedPolicySuccessorTelescopingIndexAt {Omega : Type} {K : Nat} (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Rat) (sigma2 : NNReal) (delta : Real) (omega : Omega) (t : Nat) (arm : Fin K) : Real

Scheduled score reconstructed from one finite generated pair history.

noncomputable def selectedPolicySuccessorTelescopingHistoryIndex {K : Nat} (sigma2 : NNReal) (delta : Real) (defaultAction : Fin K) (t : Nat) (history : History.FinitePairHistory (Fin K) Rat t) (arm : Fin K) : Real

Every fixed-arm scheduled history score is measurable.

theorem measurable_selectedPolicySuccessorTelescopingHistoryIndex {K : Nat} (sigma2 : NNReal) (delta : Real) (defaultAction : Fin K) (t : Nat) (arm : Fin K) : Measurable (fun history : History.FinitePairHistory (Fin K) Rat t => selectedPolicySuccessorTelescopingHistoryIndex sigma2 delta defaultAction t history arm)

Round-robin initialization followed by the scheduled score argmax.

noncomputable def selectedPolicySuccessorTelescopingHistoryNextArm {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta : Real) (defaultAction : Fin K) (t : Nat) (history : History.FinitePairHistory (Fin K) Rat t) : Fin K

After initialization, the scheduled selector maximizes every arm score.

theorem selectedPolicySuccessorTelescopingHistoryIndex_le_nextArm_of_K_le {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta : Real) (defaultAction : Fin K) (t : Nat) (history : History.FinitePairHistory (Fin K) Rat t) (ht : K <= t) (arm : Fin K) : selectedPolicySuccessorTelescopingHistoryIndex sigma2 delta defaultAction t history arm <= selectedPolicySuccessorTelescopingHistoryIndex sigma2 delta defaultAction t history (selectedPolicySuccessorTelescopingHistoryNextArm hK sigma2 delta defaultAction t history)

Pair-history reconstruction for the single scheduled policy.

noncomputable def selectedPolicySuccessorTelescopingPairHistory {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta : Real) (defaultAction : Fin K) : (n : Nat) -> History.FiniteRewardHistory Rat n -> History.FinitePairHistory (Fin K) Rat n | 0, rewardHistory => fun i => (defaultAction, rewardHistory i) | n + 1, rewardHistory => let previousRewardHistory : History.FiniteRewardHistory Rat n := fun i => rewardHistory ⟨i.1, Finset.mem_Iic.mpr ((Finset.mem_Iic.mp i.2).trans (Nat.le_succ n))⟩ let previousHistory := selectedPolicySuccessorTelescopingPairHistory hK sigma2 delta defaultAction n previousRewardHistory let nextAction := selectedPolicySuccessorTelescopingHistoryNextArm hK sigma2 delta defaultAction n previousHistory History.extendPairHistorySucc previousHistory (nextAction, rewardHistory ⟨n + 1, Finset.mem_Iic.mpr le_rfl⟩) /-- Fixed state package reconstructed by the scheduled policy. -/ noncomputable def selectedPolicySuccessorTelescopingHistoryState {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta : Real) (defaultAction : Fin K) (n : Nat) (rewardHistory : History.FiniteRewardHistory Rat n) : SelectedPolicySuccessorFiniteHistoryState K

Fixed state package reconstructed by the scheduled policy.

noncomputable def selectedPolicySuccessorTelescopingHistoryState {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta : Real) (defaultAction : Fin K) (n : Nat) (rewardHistory : History.FiniteRewardHistory Rat n) : SelectedPolicySuccessorFiniteHistoryState K

Scheduled state reconstruction is measurable at every history index.

theorem measurable_selectedPolicySuccessorTelescopingHistoryState {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta : Real) (defaultAction : Fin K) (n : Nat) : Measurable (selectedPolicySuccessorTelescopingHistoryState hK sigma2 delta defaultAction n)

One measurable UCB policy. Its declaration has no terminal horizon.

noncomputable def selectedPolicySuccessorTelescopingHistoryPolicy {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta : Real) (defaultAction : Fin K) (_t : Nat) : Policy.MeasurablePolicy (SelectedPolicySuccessorFiniteHistoryState K) (Fin K) where

Generated action trace for the single scheduled UCB policy.

noncomputable def selectedPolicySuccessorTelescopingGeneratedUCBAction {Omega : Type} {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta : Real) (defaultAction : Fin K) (reward : Omega -> RewardTrace Rat) : Omega -> ActionTrace (Fin K)

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

theorem selectedPolicySuccessorTelescopingGeneratedUCBAction_succ {Omega : Type} {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta : Real) (defaultAction : Fin K) (reward : Omega -> RewardTrace Rat) (omega : Omega) (t : Nat) : selectedPolicySuccessorTelescopingGeneratedUCBAction hK sigma2 delta defaultAction reward omega (t + 1) = selectedPolicySuccessorTelescopingHistoryNextArm hK sigma2 delta defaultAction t (selectedPolicySuccessorTelescopingPairHistory hK sigma2 delta defaultAction t (History.finiteRewardHistoryOfTrace (reward omega) t))

The reconstructed scheduled pair state is the generated trace prefix.

theorem selectedPolicySuccessorTelescopingPairHistory_eq_finitePairHistoryOfTrace {Omega : Type} {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta : Real) (defaultAction : Fin K) (reward : Omega -> RewardTrace Rat) (omega : Omega) (n : Nat) : selectedPolicySuccessorTelescopingPairHistory hK sigma2 delta defaultAction n (History.finiteRewardHistoryOfTrace (reward omega) n) = History.finitePairHistoryOfTrace (selectedPolicySuccessorTelescopingGeneratedUCBAction hK sigma2 delta defaultAction reward omega) (reward omega) n

Finite-history score, empirical count, and empirical mean are exactly the score, count, and mean on the generated scheduled trajectory.

theorem selectedPolicySuccessorTelescopingHistoryIndex_finitePairHistoryOfTrace {Omega : Type} {K : Nat} (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Rat) (sigma2 : NNReal) (delta : Real) (defaultAction : Fin K) (omega : Omega) (t : Nat) (arm : Fin K) : selectedPolicySuccessorTelescopingHistoryIndex sigma2 delta defaultAction t (History.finitePairHistoryOfTrace (action omega) (reward omega) t) arm = selectedPolicySuccessorTelescopingIndexAt action reward sigma2 delta omega t arm

At every post-initialization generated round, the chosen scheduled score dominates every candidate arm score on the same generated trace.

theorem selectedPolicySuccessorTelescopingIndexAt_le_generatedAction_of_K_le {Omega : Type} {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta : Real) (defaultAction : Fin K) (reward : Omega -> RewardTrace Rat) (omega : Omega) (t : Nat) (ht : K <= t) (arm : Fin K) : let action := selectedPolicySuccessorTelescopingGeneratedUCBAction hK sigma2 delta defaultAction reward selectedPolicySuccessorTelescopingIndexAt action reward sigma2 delta omega t arm <= selectedPolicySuccessorTelescopingIndexAt action reward sigma2 delta omega t (action omega (t + 1))

Scheduled successor initialization remains the one-pass round robin.

theorem selectedPolicySuccessorTelescopingGeneratedUCBAction_succ_eq_initializationArm_of_lt {Omega : Type} {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta : Real) (defaultAction : Fin K) (reward : Omega -> RewardTrace Rat) (omega : Omega) (t : Nat) (ht : t < K) : selectedPolicySuccessorTelescopingGeneratedUCBAction hK sigma2 delta defaultAction reward omega (t + 1) = initializationArm hK t

Every arm is pulled exactly once in the scheduled initialization cycle.

theorem successorArmPullCount_selectedPolicySuccessorTelescopingGeneratedUCBAction_K_add_one_eq_one {Omega : Type} {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta : Real) (defaultAction : Fin K) (reward : Omega -> RewardTrace Rat) (omega : Omega) (arm : Fin K) : ConditionalExpectationReward.successorArmPullCount (selectedPolicySuccessorTelescopingGeneratedUCBAction hK sigma2 delta defaultAction reward omega) arm (K + 1) = 1

After initialization every scheduled successor arm count is positive.

theorem successorArmPullCount_selectedPolicySuccessorTelescopingGeneratedUCBAction_pos_of_K_le {Omega : Type} {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta : Real) (defaultAction : Fin K) (reward : Omega -> RewardTrace Rat) (omega : Omega) (arm : Fin K) (t : Nat) (ht : K <= t) : 0 < ConditionalExpectationReward.successorArmPullCount (selectedPolicySuccessorTelescopingGeneratedUCBAction hK sigma2 delta defaultAction reward omega) arm (t + 1)

A selected scheduled round with positive prior count is post-initialization.

theorem K_le_of_selectedPolicySuccessorTelescopingGeneratedUCBAction_selected_and_count_pos {Omega : Type} {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta : Real) (defaultAction : Fin K) (reward : Omega -> RewardTrace Rat) (omega : Omega) (arm : Fin K) (t : Nat) (hselected : selectedPolicySuccessorTelescopingGeneratedUCBAction hK sigma2 delta defaultAction reward omega (t + 1) = arm) (hcount : 0 < ConditionalExpectationReward.successorArmPullCount (selectedPolicySuccessorTelescopingGeneratedUCBAction hK sigma2 delta defaultAction reward omega) arm (t + 1)) : K <= t

Timewise measurability of the fixed-policy generated action.

theorem measurable_selectedPolicySuccessorTelescopingGeneratedUCBAction {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta : Real) (defaultAction : Fin K) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (t : Nat) : Measurable (fun omega => selectedPolicySuccessorTelescopingGeneratedUCBAction hK sigma2 delta defaultAction reward omega t)

The logarithmic budget inside the scheduled radius at history index `n`.

noncomputable def selectedPolicySuccessorTelescopingLogBudget (K n : Nat) (delta : Real) : Real

Explicit polynomial reciprocal form of the scheduled log budget.

theorem selectedPolicySuccessorTelescopingLogBudget_eq (K n : Nat) (delta : Real) (hK : 0 < K) (hdelta : 0 < delta) : selectedPolicySuccessorTelescopingLogBudget K n delta = max (Real.log (2 * (K : Real) * ((n + 1 : Nat) : Real) ^ 2 * ((n + 2 : Nat) : Real) / delta)) 0

The scheduled log budget is nondecreasing in the history index.

theorem selectedPolicySuccessorTelescopingLogBudget_mono (K n T : Nat) (delta : Real) (hK : 0 < K) (hdelta : 0 < delta) (hnT : n <= T) : selectedPolicySuccessorTelescopingLogBudget K n delta <= selectedPolicySuccessorTelescopingLogBudget K T delta

Expanded algebraic form of one scheduled random-count radius.

theorem successorArmEmpiricalMeanTelescopingPeelingRadius_eq {K : Nat} (sigma2 : NNReal) (k n : Nat) (delta : Real) : ConditionalExpectationReward.successorArmEmpiricalMeanPeelingRadius sigma2 k (n + 1) (Concentration.telescopingConfidenceShare delta n / (K : Real)) = (2 * Real.sqrt ((1 / 2 : Real) * (((sigma2 : NNReal) : Real) * (k : Real)) * selectedPolicySuccessorTelescopingLogBudget K n delta) + selectedPolicySuccessorTelescopingLogBudget K n delta) / (k : Real)

Real terminal envelope for inverting every scheduled radius up to index `T`.

noncomputable def selectedPolicySuccessorTelescopingRealPullThreshold (K : Nat) (sigma2 : NNReal) (T : Nat) (delta gap : Real) : Real

One more than the ceiling supplies the strict count-inversion margin.

noncomputable def selectedPolicySuccessorTelescopingPullThreshold (K : Nat) (sigma2 : NNReal) (T : Nat) (delta gap : Real) : Nat

The terminal scheduled threshold satisfies the quadratic and linear radius-inversion contracts.

theorem selectedPolicySuccessorTelescopingPullThreshold_contracts (K : Nat) (sigma2 : NNReal) (T : Nat) (delta gap : Real) (hgap : 0 < gap) : 0 < selectedPolicySuccessorTelescopingPullThreshold K sigma2 T delta gap /\ 32 * (((sigma2 : NNReal) : Real)) * selectedPolicySuccessorTelescopingLogBudget K T delta < gap ^ 2 * (selectedPolicySuccessorTelescopingPullThreshold K sigma2 T delta gap : Real) /\ 4 * selectedPolicySuccessorTelescopingLogBudget K T delta < gap * (selectedPolicySuccessorTelescopingPullThreshold K sigma2 T delta gap : Real)

Every count beyond the terminal envelope makes the scheduled radius at every earlier history index strictly smaller than half the positive gap.

theorem two_mul_successorArmEmpiricalMeanTelescopingPeelingRadius_lt_gap_of_threshold {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta gap : Real) (hdelta : 0 < delta) (hgap : 0 < gap) (k n T : Nat) (hk : selectedPolicySuccessorTelescopingPullThreshold K sigma2 T delta gap <= k) (hnT : n <= T) : 2 * ConditionalExpectationReward.successorArmEmpiricalMeanPeelingRadius sigma2 k (n + 1) (Concentration.telescopingConfidenceShare delta n / (K : Real)) < gap

Outside the one telescoping bad event, scheduled score maximality implies the standard UCB gap bound at every initialized generated round.

theorem selectedPolicySuccessorTelescoping_meanGap_le_two_radius_of_not_badEvent {Omega : Type} {K : Nat} (hK : 0 < K) (reward : Omega -> RewardTrace Rat) (armMean : Fin K -> Rat) (sigma2 : NNReal) (delta : Real) (defaultAction best : Fin K) (omega : Omega) (t : Nat) (ht : K <= t) (hgood : omega ∉ ConditionalExpectationReward.successorArmEmpiricalMeanFintypeTelescopingAllTimeBadEvent (selectedPolicySuccessorTelescopingGeneratedUCBAction hK sigma2 delta defaultAction reward) reward armMean sigma2 delta) : let action := selectedPolicySuccessorTelescopingGeneratedUCBAction hK sigma2 delta defaultAction reward meanGap (fun arm => (armMean arm : Real)) best (action omega (t + 1)) <= 2 * selectedPolicySuccessorTelescopingRadiusAt action sigma2 delta omega t (action omega (t + 1))

The single all-time good event controls one positive-gap arm at every finite horizon; the horizon appears only in the deterministic bound.

theorem selectedPolicySuccessorTelescoping_pullCount_le_of_not_badEvent {Omega : Type} {K : Nat} (hK : 0 < K) (reward : Omega -> RewardTrace Rat) (armMean : Fin K -> Rat) (sigma2 : NNReal) (delta : Real) (hdelta : 0 < delta) (defaultAction best chosen : Fin K) (omega : Omega) (T : Nat) (hgap : 0 < meanGap (fun arm => (armMean arm : Real)) best chosen) (hgood : omega ∉ ConditionalExpectationReward.successorArmEmpiricalMeanFintypeTelescopingAllTimeBadEvent (selectedPolicySuccessorTelescopingGeneratedUCBAction hK sigma2 delta defaultAction reward) reward armMean sigma2 delta) : ConditionalExpectationReward.successorArmPullCount (selectedPolicySuccessorTelescopingGeneratedUCBAction hK sigma2 delta defaultAction reward omega) chosen (T + 1) <= selectedPolicySuccessorTelescopingPullThreshold K sigma2 T delta (meanGap (fun arm => (armMean arm : Real)) best chosen)

The accepted telescoping all-time confidence producer instantiated on the single scheduled policy. The sampled pair action and the reward-reconstructed policy action are transported on their explicit almost-everywhere alignment set, so the conclusion is about the action actually consumed by the UCB score and regret definitions.

theorem actionRewardHistoryStepKernelFamily_selectedPolicySuccessorTelescoping_allTimeConfidence {Context : Type} {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 : Fin K) (armMean : Fin K -> Rat) (sigma2 : NNReal) (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, forall history : ((j : Finset.Iic i) -> Rat), varianceProxy (context i history) ((selectedPolicySuccessorTelescopingHistoryPolicy hK sigma2 delta defaultAction i).action (selectedPolicySuccessorTelescopingHistoryState hK sigma2 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) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (hdelta : 0 < delta) : let policy := selectedPolicySuccessorTelescopingHistoryPolicy hK sigma2 delta defaultAction let state := selectedPolicySuccessorTelescopingHistoryState hK sigma2 delta defaultAction let pairContext : (i : Nat) -> ((j : Finset.Iic i) -> Prod (Fin K) Rat) -> Context

One global all-time confidence event yields the terminal pull-count tail for any requested finite horizon.

theorem measure_selectedPolicySuccessorTelescoping_pullCount_gt_threshold_le_of_allTimeConfidence {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) (mu : Measure Omega) (reward : Omega -> RewardTrace Rat) (armMean : Fin K -> Rat) (sigma2 : NNReal) (delta : Real) (hdelta : 0 < delta) (defaultAction best chosen : Fin K) (T : Nat) (hgap : 0 < meanGap (fun arm => (armMean arm : Real)) best chosen) (hconfidence : mu (ConditionalExpectationReward.successorArmEmpiricalMeanFintypeTelescopingAllTimeBadEvent (selectedPolicySuccessorTelescopingGeneratedUCBAction hK sigma2 delta defaultAction reward) reward armMean sigma2 delta) <= ENNReal.ofReal delta) : mu {omega | selectedPolicySuccessorTelescopingPullThreshold K sigma2 T delta (meanGap (fun arm => (armMean arm : Real)) best chosen) < ConditionalExpectationReward.successorArmPullCount (selectedPolicySuccessorTelescopingGeneratedUCBAction hK sigma2 delta defaultAction reward omega) chosen (T + 1)} <= ENNReal.ofReal delta

Expected scheduled pull count at any finite horizon. The explicit `T * delta` term is retained; no unconditional expectation claim is made from the good event alone.

theorem lintegral_selectedPolicySuccessorTelescoping_pullCount_le_of_allTimeConfidence {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) (mu : Measure Omega) [IsProbabilityMeasure mu] (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (armMean : Fin K -> Rat) (sigma2 : NNReal) (delta : Real) (hdelta : 0 < delta) (defaultAction best chosen : Fin K) (T : Nat) (hgap : 0 < meanGap (fun arm => (armMean arm : Real)) best chosen) (hconfidence : mu (ConditionalExpectationReward.successorArmEmpiricalMeanFintypeTelescopingAllTimeBadEvent (selectedPolicySuccessorTelescopingGeneratedUCBAction hK sigma2 delta defaultAction reward) reward armMean sigma2 delta) <= ENNReal.ofReal delta) : ∫⁻ omega, (ConditionalExpectationReward.successorArmPullCount (selectedPolicySuccessorTelescopingGeneratedUCBAction hK sigma2 delta defaultAction reward omega) chosen (T + 1) : ENNReal) ∂mu <= (selectedPolicySuccessorTelescopingPullThreshold K sigma2 T delta (meanGap (fun arm => (armMean arm : Real)) best chosen) : ENNReal) + (T : ENNReal) * ENNReal.ofReal delta

Standard regret-time shift of the single scheduled generated policy.

noncomputable def selectedPolicySuccessorTelescopingGeneratedUCBRegretAction {Omega : Type} {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta : Real) (defaultAction : Fin K) (reward : Omega -> RewardTrace Rat) : Omega -> ActionTrace (Fin K)

Timewise measurability of the shifted fixed-policy regret action.

theorem measurable_selectedPolicySuccessorTelescopingGeneratedUCBRegretAction {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta : Real) (defaultAction : Fin K) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (t : Nat) : Measurable (fun omega => selectedPolicySuccessorTelescopingGeneratedUCBRegretAction hK sigma2 delta defaultAction reward omega t)

Shifted fixed-policy pull counts are the existing successor counts.

theorem pullCount_selectedPolicySuccessorTelescopingGeneratedUCBRegretAction_eq {Omega : Type} {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta : Real) (defaultAction : Fin K) (reward : Omega -> RewardTrace Rat) (omega : Omega) (arm : Fin K) (T : Nat) : pullCount (selectedPolicySuccessorTelescopingGeneratedUCBRegretAction hK sigma2 delta defaultAction reward omega) arm T = ConditionalExpectationReward.successorArmPullCount (selectedPolicySuccessorTelescopingGeneratedUCBAction hK sigma2 delta defaultAction reward omega) arm (T + 1)

Finite-time expected pseudo-regret for the single scheduled policy from its one all-time confidence event.

theorem lintegral_ofReal_pseudoRegret_selectedPolicySuccessorTelescoping_le_of_allTimeConfidence {Omega : Type} [MeasurableSpace Omega] {K : Nat} (mu : Measure Omega) [IsProbabilityMeasure mu] (model : FiniteBanditModel K) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (sigma2 : NNReal) (delta : Real) (hdelta : 0 < delta) (defaultAction : Fin K) (T : Nat) (hconfidence : mu (ConditionalExpectationReward.successorArmEmpiricalMeanFintypeTelescopingAllTimeBadEvent (selectedPolicySuccessorTelescopingGeneratedUCBAction model.hK sigma2 delta defaultAction reward) reward model.mean sigma2 delta) <= ENNReal.ofReal delta) : ∫⁻ omega, ENNReal.ofReal (((pseudoRegret model (selectedPolicySuccessorTelescopingGeneratedUCBRegretAction model.hK sigma2 delta defaultAction reward omega) T : Rat) : Real)) ∂mu <= (Finset.univ : Finset (Fin K)).sum (fun arm => ENNReal.ofReal (((model.gap arm : Rat) : Real)) * ((selectedPolicySuccessorTelescopingPullThreshold K sigma2 T delta (((model.gap arm : Rat) : Real)) : Nat) : ENNReal) + ENNReal.ofReal (((model.gap arm : Rat) : Real)) * ((T : ENNReal) * ENNReal.ofReal delta))

A single good sample controls every finite horizon and every positive-gap arm simultaneously.

theorem selectedPolicySuccessorTelescoping_allHorizonPullCount_of_not_badEvent {Omega : Type} {K : Nat} (hK : 0 < K) (reward : Omega -> RewardTrace Rat) (armMean : Fin K -> Rat) (sigma2 : NNReal) (delta : Real) (hdelta : 0 < delta) (defaultAction best : Fin K) (omega : Omega) (hgood : omega ∉ ConditionalExpectationReward.successorArmEmpiricalMeanFintypeTelescopingAllTimeBadEvent (selectedPolicySuccessorTelescopingGeneratedUCBAction hK sigma2 delta defaultAction reward) reward armMean sigma2 delta) : forall T : Nat, forall chosen : Fin K, 0 < meanGap (fun arm => (armMean arm : Real)) best chosen -> ConditionalExpectationReward.successorArmPullCount (selectedPolicySuccessorTelescopingGeneratedUCBAction hK sigma2 delta defaultAction reward omega) chosen (T + 1) <= selectedPolicySuccessorTelescopingPullThreshold K sigma2 T delta (meanGap (fun arm => (armMean arm : Real)) best chosen)

The canonical action/reward trajectory measure of the single scheduled policy. This declaration itself contains no terminal horizon.

noncomputable def selectedPolicySuccessorTelescopingActionRewardTrajMeasure {Context : Type} {K : Nat} [MeasurableSpace Context] (hK : 0 < K) (mu0 : Measure (Prod (Fin K) Rat)) (rewardKernel : RewardKernel.MarkovRewardKernel (Prod Context (Fin K)) Rat) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (sigma2 : NNReal) (delta : Real) (defaultAction : Fin K) : Measure (Nat -> Prod (Fin K) Rat)

Short canonical surface for the same-policy all-time confidence theorem.

theorem measure_selectedPolicySuccessorTelescoping_allTimeBadEvent_le_trajMeasure {Context : Type} {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 : Fin K) (armMean : Fin K -> Rat) (sigma2 : NNReal) (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, forall history : ((j : Finset.Iic i) -> Rat), varianceProxy (context i history) ((selectedPolicySuccessorTelescopingHistoryPolicy hK sigma2 delta defaultAction i).action (selectedPolicySuccessorTelescopingHistoryState hK sigma2 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) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (hdelta : 0 < delta) : let mu := selectedPolicySuccessorTelescopingActionRewardTrajMeasure hK mu0 rewardKernel context hcontext sigma2 delta defaultAction let reward : (Nat -> Prod (Fin K) Rat) -> RewardTrace Rat := fun trajectory t => (trajectory t).2 let action := selectedPolicySuccessorTelescopingGeneratedUCBAction hK sigma2 delta defaultAction reward mu (ConditionalExpectationReward.successorArmEmpiricalMeanFintypeTelescopingAllTimeBadEvent action reward armMean sigma2 delta) <= ENNReal.ofReal delta

Canonical finite-horizon pull-count tail for the single scheduled policy and the same trajectory measure used by the all-time confidence theorem.

theorem measure_selectedPolicySuccessorTelescoping_pullCount_gt_threshold_le_trajMeasure {Context : Type} {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) (delta : Real) (T : Nat) (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), varianceProxy (context i history) ((selectedPolicySuccessorTelescopingHistoryPolicy hK sigma2 delta defaultAction i).action (selectedPolicySuccessorTelescopingHistoryState hK sigma2 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) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (hdelta : 0 < delta) (hgap : 0 < meanGap (fun arm => (armMean arm : Real)) best chosen) : let mu := selectedPolicySuccessorTelescopingActionRewardTrajMeasure hK mu0 rewardKernel context hcontext sigma2 delta defaultAction let reward : (Nat -> Prod (Fin K) Rat) -> RewardTrace Rat := fun trajectory t => (trajectory t).2 let action := selectedPolicySuccessorTelescopingGeneratedUCBAction hK sigma2 delta defaultAction reward mu {trajectory | selectedPolicySuccessorTelescopingPullThreshold K sigma2 T delta (meanGap (fun arm => (armMean arm : Real)) best chosen) < ConditionalExpectationReward.successorArmPullCount (action trajectory) chosen (T + 1)} <= ENNReal.ofReal delta

Canonical finite-time expected pseudo-regret of the single scheduled policy. The same all-time event supplies every horizon, and the failure term is explicitly retained as `T * delta`.

theorem lintegral_ofReal_pseudoRegret_selectedPolicySuccessorTelescoping_le_trajMeasure {Context : Type} {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) (delta : Real) (T : Nat) (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), varianceProxy (context i history) ((selectedPolicySuccessorTelescopingHistoryPolicy model.hK sigma2 delta defaultAction i).action (selectedPolicySuccessorTelescopingHistoryState model.hK sigma2 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) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (hdelta : 0 < delta) : let mu := selectedPolicySuccessorTelescopingActionRewardTrajMeasure model.hK mu0 rewardKernel context hcontext sigma2 delta defaultAction let reward : (Nat -> Prod (Fin K) Rat) -> RewardTrace Rat := fun trajectory t => (trajectory t).2 let action := selectedPolicySuccessorTelescopingGeneratedUCBRegretAction model.hK sigma2 delta defaultAction reward ∫⁻ trajectory, ENNReal.ofReal (((pseudoRegret model (action trajectory) T : Rat) : Real)) ∂mu <= (Finset.univ : Finset (Fin K)).sum (fun arm => ENNReal.ofReal (((model.gap arm : Rat) : Real)) * ((selectedPolicySuccessorTelescopingPullThreshold K sigma2 T delta (((model.gap arm : Rat) : Real)) : Nat) : ENNReal) + ENNReal.ofReal (((model.gap arm : Rat) : Real)) * ((T : ENNReal) * ENNReal.ofReal delta))