BanditRLProof.Algorithms.UCBConditionalRewardLawPolicy

A finite pair history packaged with its dependent horizon.

structure SelectedPolicySuccessorFiniteHistoryState (K : Nat) where

Complete a finite pair history with a fixed pair outside its prefix.

def completeFinitePairHistory {Action Reward : Type} (t : Nat) (history : History.FinitePairHistory Action Reward t) (defaultAction : Action) (defaultReward : Reward) : Nat -> Action × Reward

Action projection of a completed finite pair history.

def completeFinitePairHistoryAction {Action Reward : Type} (t : Nat) (history : History.FinitePairHistory Action Reward t) (defaultAction : Action) (defaultReward : Reward) : ActionTrace Action

Reward projection of a completed finite pair history.

def completeFinitePairHistoryReward {Action Reward : Type} (t : Nat) (history : History.FinitePairHistory Action Reward t) (defaultAction : Action) (defaultReward : Reward) : RewardTrace Reward

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

theorem completeFinitePairHistory_finitePairHistoryOfTrace_apply_of_le {Action Reward : Type} (action : ActionTrace Action) (reward : RewardTrace Reward) (t s : Nat) (defaultAction : Action) (defaultReward : Reward) (hs : s <= t) : completeFinitePairHistory t (History.finitePairHistoryOfTrace action reward t) defaultAction defaultReward s = (action s, reward s)

Practical random-width UCB score reconstructed from one finite history.

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

Round-robin initialization followed by finite-history score maximization.

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

The post-initialization history selector maximizes every candidate score.

theorem selectedPolicySuccessorHistoryIndex_le_nextArm_of_K_le {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (T : Nat) (delta : Real) (defaultAction : Fin K) (t : Nat) (history : History.FinitePairHistory (Fin K) Rat t) (ht : K <= t) (arm : Fin K) : selectedPolicySuccessorHistoryIndex sigma2 T delta defaultAction t history arm <= selectedPolicySuccessorHistoryIndex sigma2 T delta defaultAction t history (selectedPolicySuccessorHistoryNextArm hK sigma2 T delta defaultAction t history)

Reconstruct the inclusive action/reward pair history from a finite reward history. The recursion uses only the preceding reconstructed pair prefix when selecting the next action.

noncomputable def selectedPolicySuccessorPairHistory {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (T : Nat) (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 := selectedPolicySuccessorPairHistory hK sigma2 T delta defaultAction n previousRewardHistory let nextAction := selectedPolicySuccessorHistoryNextArm hK sigma2 T delta defaultAction n previousHistory History.extendPairHistorySucc previousHistory (nextAction, rewardHistory ⟨n + 1, Finset.mem_Iic.mpr le_rfl⟩) /-- Package the reconstructed history as the fixed policy state type. -/ noncomputable def selectedPolicySuccessorHistoryState {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (T : Nat) (delta : Real) (defaultAction : Fin K) (n : Nat) (rewardHistory : History.FiniteRewardHistory Rat n) : SelectedPolicySuccessorFiniteHistoryState K

Package the reconstructed history as the fixed policy state type.

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

Every finite reward-history state reconstruction is measurable.

theorem measurable_selectedPolicySuccessorHistoryState {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (T : Nat) (delta : Real) (defaultAction : Fin K) (n : Nat) : Measurable (selectedPolicySuccessorHistoryState hK sigma2 T delta defaultAction n)

Measurable policy reading the packaged finite pair history.

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

Generated action trace for the concrete finite-history UCB policy.

noncomputable def selectedPolicySuccessorGeneratedUCBAction {Omega : Type} {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (T : Nat) (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 selectedPolicySuccessorGeneratedUCBAction_succ {Omega : Type} {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (T : Nat) (delta : Real) (defaultAction : Fin K) (reward : Omega -> RewardTrace Rat) (omega : Omega) (t : Nat) : selectedPolicySuccessorGeneratedUCBAction hK sigma2 T delta defaultAction reward omega (t + 1) = selectedPolicySuccessorHistoryNextArm hK sigma2 T delta defaultAction t (selectedPolicySuccessorPairHistory hK sigma2 T delta defaultAction t (History.finiteRewardHistoryOfTrace (reward omega) t))

The reconstructed pair state is exactly the generated trace prefix.

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

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

private theorem sumRewards_eq_of_forall_lt {Action : Type} [DecidableEq Action] (action action' : ActionTrace Action) (reward reward' : RewardTrace Real) (arm : Action) : forall n : Nat, (forall s, s < n -> action s = action' s) -> (forall s, s < n -> reward s = reward' s) -> sumRewards action reward arm n = sumRewards action' reward' arm n

Completed actual prefixes preserve every successor pull count.

theorem successorArmPullCount_completeFinitePairHistory {K : Nat} (action : ActionTrace (Fin K)) (reward : RewardTrace Rat) (defaultAction : Fin K) (t : Nat) (arm : Fin K) : ConditionalExpectationReward.successorArmPullCount (completeFinitePairHistoryAction t (History.finitePairHistoryOfTrace action reward t) defaultAction (0 : Rat)) arm (t + 1) = ConditionalExpectationReward.successorArmPullCount action arm (t + 1)

Completed actual prefixes preserve every successor selected reward sum.

theorem successorArmRewardSum_completeFinitePairHistory {K : Nat} (action : ActionTrace (Fin K)) (reward : RewardTrace Rat) (defaultAction : Fin K) (t : Nat) (arm : Fin K) : ConditionalExpectationReward.successorArmRewardSum (completeFinitePairHistoryAction t (History.finitePairHistoryOfTrace action reward t) defaultAction (0 : Rat)) (completeFinitePairHistoryReward t (History.finitePairHistoryOfTrace action reward t) defaultAction (0 : Rat)) arm (t + 1) = ConditionalExpectationReward.successorArmRewardSum action reward arm (t + 1)

The finite-history score is exactly the score on the generated trace.

theorem selectedPolicySuccessorHistoryIndex_finitePairHistoryOfTrace {Omega : Type} {K : Nat} (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Rat) (sigma2 : NNReal) (T : Nat) (delta : Real) (defaultAction : Fin K) (omega : Omega) (t : Nat) (arm : Fin K) : selectedPolicySuccessorHistoryIndex sigma2 T delta defaultAction t (History.finitePairHistoryOfTrace (action omega) (reward omega) t) arm = selectedPolicySuccessorIndexAt action reward sigma2 (Finset.univ : Finset (Fin K)) T delta omega t arm

During initialization, successor action `t + 1` follows round robin.

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

Every arm appears once among successor actions `1, ..., K`.

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

After the successor initialization cycle, every arm count is positive.

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

Concrete initialized score-max source for the practical selected-policy UCB route. Charged times are exactly the post-initialization times below `T`.

noncomputable def selectedPolicySuccessorGeneratedUCBInitializedScoreMaxSource {Omega : Type} {K : Nat} (hK : 0 < K) (reward : Omega -> RewardTrace Rat) (armMean : Fin K -> Rat) (sigma2 : NNReal) (T : Nat) (delta : Real) (defaultAction best : Fin K) : SelectedPolicySuccessorInitializedScoreMaxSource (selectedPolicySuccessorGeneratedUCBAction hK sigma2 T delta defaultAction reward) reward Finset.univ armMean sigma2 T delta where

If the final pull count exceeds `B`, some selected time has prior pull count at least `B`.

theorem exists_selected_with_threshold_le_prior_pullCount {Action : Type} [DecidableEq Action] (action : ActionTrace Action) (arm : Action) (T B : Nat) (hcount : B < pullCount action arm T) : exists t, t < T ∧ action t = arm ∧ B <= pullCount action arm t

Log budget hidden inside one finite-arm/time peeling radius.

noncomputable def selectedPolicySuccessorFiniteArmTimeLogBudget (K T n : Nat) (delta : Real) : Real

The local log budget is maximized at the full positive horizon.

theorem selectedPolicySuccessorFiniteArmTimeLogBudget_le_horizon (K T n : Nat) (delta : Real) (hK : 0 < K) (hT : 0 < T) (hnT : n <= T) (hdelta : 0 < delta) : selectedPolicySuccessorFiniteArmTimeLogBudget K T n delta <= selectedPolicySuccessorFiniteArmTimeLogBudget K T T delta

Real count threshold that simultaneously dominates the quadratic and linear parts of the practical random-width radius inversion.

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

One more than the ceiling supplies the strict margin needed by the radius.

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

The explicit integer threshold is positive and satisfies both full-horizon strict radius-inversion inequalities.

theorem selectedPolicySuccessorPullThreshold_contracts (K : Nat) (sigma2 : NNReal) (T : Nat) (delta gap : Real) (hgap : 0 < gap) : 0 < selectedPolicySuccessorPullThreshold K sigma2 T delta gap /\ 32 * (((sigma2 : NNReal) : Real)) * selectedPolicySuccessorFiniteArmTimeLogBudget K T T delta < gap ^ 2 * (selectedPolicySuccessorPullThreshold K sigma2 T delta gap : Real) /\ 4 * selectedPolicySuccessorFiniteArmTimeLogBudget K T T delta < gap * (selectedPolicySuccessorPullThreshold K sigma2 T delta gap : Real)

Expanded algebraic form of the practical finite-arm/time radius.

theorem successorArmEmpiricalMeanFiniteArmTimePeelingRadius_eq {K : Nat} (sigma2 : NNReal) (k n T : Nat) (delta : Real) : ConditionalExpectationReward.successorArmEmpiricalMeanFiniteArmTimePeelingRadius sigma2 k n (Finset.univ : Finset (Fin K)) T delta = (2 * Real.sqrt ((1 / 2 : Real) * (((sigma2 : NNReal) : Real) * (k : Real)) * selectedPolicySuccessorFiniteArmTimeLogBudget K T n delta) + selectedPolicySuccessorFiniteArmTimeLogBudget K T n delta) / (k : Real)

Sufficient square-root and linear inequalities for inverting one realized-count peeling radius below half a positive arm gap.

theorem two_mul_successorArmEmpiricalMeanFiniteArmTimePeelingRadius_lt_gap {K : Nat} (sigma2 : NNReal) (k n T : Nat) (delta gap : Real) (hk : 0 < k) (hgap : 0 < gap) (hquadratic : 32 * (((sigma2 : NNReal) : Real)) * selectedPolicySuccessorFiniteArmTimeLogBudget K T n delta < gap ^ 2 * (k : Real)) (hlinear : 4 * selectedPolicySuccessorFiniteArmTimeLogBudget K T n delta < gap * (k : Real)) : 2 * ConditionalExpectationReward.successorArmEmpiricalMeanFiniteArmTimePeelingRadius sigma2 k n (Finset.univ : Finset (Fin K)) T delta < gap

Uniform count-threshold inversion. It is enough to check the quadratic and linear log-budget inequalities at the threshold `B`; larger realized counts only improve the radius.

theorem successorArmEmpiricalMeanFiniteArmTimePeelingRadius_lt_gap_of_threshold {K : Nat} (sigma2 : NNReal) (T : Nat) (delta gap : Real) (B : Nat) (hB : 0 < B) (hgap : 0 < gap) (hquadratic : forall n : Nat, n <= T -> 32 * (((sigma2 : NNReal) : Real)) * selectedPolicySuccessorFiniteArmTimeLogBudget K T n delta < gap ^ 2 * (B : Real)) (hlinear : forall n : Nat, n <= T -> 4 * selectedPolicySuccessorFiniteArmTimeLogBudget K T n delta < gap * (B : Real)) : forall k n : Nat, B <= k -> n <= T -> 2 * ConditionalExpectationReward.successorArmEmpiricalMeanFiniteArmTimePeelingRadius sigma2 k n (Finset.univ : Finset (Fin K)) T delta < gap

Full-horizon sufficient condition for uniform radius inversion. The finite arm/time/count peeling log cost is summarized by the single deterministic budget at `n = T`.

theorem successorArmEmpiricalMeanFiniteArmTimePeelingRadius_lt_gap_of_global_threshold {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (T : Nat) (hT : 0 < T) (delta : Real) (hdelta : 0 < delta) (gap : Real) (hgap : 0 < gap) (B : Nat) (hB : 0 < B) (hquadratic : 32 * (((sigma2 : NNReal) : Real)) * selectedPolicySuccessorFiniteArmTimeLogBudget K T T delta < gap ^ 2 * (B : Real)) (hlinear : 4 * selectedPolicySuccessorFiniteArmTimeLogBudget K T T delta < gap * (B : Real)) : forall k n : Nat, B <= k -> n <= T -> 2 * ConditionalExpectationReward.successorArmEmpiricalMeanFiniteArmTimePeelingRadius sigma2 k n (Finset.univ : Finset (Fin K)) T delta < gap

Uniform radius inversion at the explicit one-more-than-ceiling pull threshold.

theorem successorArmEmpiricalMeanFiniteArmTimePeelingRadius_lt_gap_of_explicitPullThreshold {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (T : Nat) (hT : 0 < T) (delta : Real) (hdelta : 0 < delta) (gap : Real) (hgap : 0 < gap) : forall k n : Nat, selectedPolicySuccessorPullThreshold K sigma2 T delta gap <= k -> n <= T -> 2 * ConditionalExpectationReward.successorArmEmpiricalMeanFiniteArmTimePeelingRadius sigma2 k n (Finset.univ : Finset (Fin K)) T delta < gap

A selected time with a positive prior count cannot lie inside the one-pass round-robin initialization prefix.

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

Generated-policy high-probability pull-count consumer. The deterministic `hradius` contract is the exact remaining radius-inversion obligation: every count at least `B`, at every horizon at most `T`, must make twice the realized confidence radius strictly smaller than the chosen arm gap. Under that contract, exceeding `B` pulls forces the global large-gap event.

theorem measure_successorArmPullCount_selectedPolicySuccessorGeneratedUCBAction_gt_threshold_le_of_largeGap {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) (mu : Measure Omega) (reward : Omega -> RewardTrace Rat) (armMean : Fin K -> Rat) (sigma2 : NNReal) (T : Nat) (delta : Real) (defaultAction best chosen : Fin K) (B : Nat) (hB : 0 < B) (hradius : forall k n : Nat, B <= k -> n <= T -> 2 * ConditionalExpectationReward.successorArmEmpiricalMeanFiniteArmTimePeelingRadius sigma2 k n (Finset.univ : Finset (Fin K)) T delta < meanGap (fun arm => (armMean arm : Real)) best chosen) (hlargeGap : mu (selectedPolicySuccessorLargeGapEvent (selectedPolicySuccessorGeneratedUCBInitializedScoreMaxSource hK reward armMean sigma2 T delta defaultAction best)) <= ENNReal.ofReal delta) : mu {omega | B < ConditionalExpectationReward.successorArmPullCount (selectedPolicySuccessorGeneratedUCBAction hK sigma2 T delta defaultAction reward omega) chosen (T + 1)} <= ENNReal.ofReal delta

Generated-policy high-probability pull-count bound with the radius inversion discharged by the two full-horizon numeric threshold inequalities.

theorem measure_successorArmPullCount_selectedPolicySuccessorGeneratedUCBAction_gt_threshold_le_of_global_threshold {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) (mu : Measure Omega) (reward : Omega -> RewardTrace Rat) (armMean : Fin K -> Rat) (sigma2 : NNReal) (T : Nat) (hT : 0 < T) (delta : Real) (hdelta : 0 < delta) (defaultAction best chosen : Fin K) (B : Nat) (hB : 0 < B) (hgap : 0 < meanGap (fun arm => (armMean arm : Real)) best chosen) (hquadratic : 32 * (((sigma2 : NNReal) : Real)) * selectedPolicySuccessorFiniteArmTimeLogBudget K T T delta < meanGap (fun arm => (armMean arm : Real)) best chosen ^ 2 * (B : Real)) (hlinear : 4 * selectedPolicySuccessorFiniteArmTimeLogBudget K T T delta < meanGap (fun arm => (armMean arm : Real)) best chosen * (B : Real)) (hlargeGap : mu (selectedPolicySuccessorLargeGapEvent (selectedPolicySuccessorGeneratedUCBInitializedScoreMaxSource hK reward armMean sigma2 T delta defaultAction best)) <= ENNReal.ofReal delta) : mu {omega | B < ConditionalExpectationReward.successorArmPullCount (selectedPolicySuccessorGeneratedUCBAction hK sigma2 T delta defaultAction reward omega) chosen (T + 1)} <= ENNReal.ofReal delta

Generated-policy pull-count tail at the explicit one-more-than-ceiling threshold; no caller-supplied radius or numeric threshold inequalities remain.

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

Practical selected-reward-law producer for the concrete generated UCB source's global random-width large-gap event.

theorem measure_selectedPolicySuccessorLargeGapEvent_generatedUCB_le_ennreal_delta_of_reward_map_eq_selected_policy {Omega Context : Type} {K : Nat} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] (hK : 0 < K) (mu : Measure Omega) [IsProbabilityMeasure mu] (rewardKernel : RewardKernel.MarkovRewardKernel (Context × Fin K) Rat) (context : (n : Nat) -> History.FiniteRewardHistory Rat n -> Context) (mean : Context -> Fin K -> Rat) (varianceProxy : Context -> Fin K -> NNReal) (defaultAction best : Fin K) (armMean : Fin K -> Rat) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (rewardLo rewardHi meanLo meanHi : Nat -> Real) (sigma2 : NNReal) (hcontext : forall n : Nat, Measurable (context n)) (hmean : Measurable (fun pair : Context × Fin K => mean pair.1 pair.2)) (hkernel : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hraw : forall i : Nat, forall omega : Omega, Set.Icc (rewardLo i) (rewardHi i) (((reward omega (i + 1) : Rat) : Real))) (hmean_range : forall i : Nat, forall c : Context, forall arm : Fin K, Set.Icc (meanLo i) (meanHi i) (((mean c arm : Rat) : Real))) (T : Nat) (hT : 0 < T) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) (hvariance : forall i : Nat, forall history : History.FiniteRewardHistory Rat i, 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 : History.FiniteRewardHistory Rat i, forall arm : Fin K, mean (context i history) arm = armMean arm) (h_reward_map_eq_policy : forall i : Nat, Filter.Eventually (fun omega : Omega => @Measure.map Omega Rat mOmega inferInstance (fun y : Omega => reward y (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc (selectedPolicySuccessorGeneratedUCBAction hK sigma2 T delta defaultAction reward) reward (ConditionalExpectationReward.generatedActionFromRewardHistory_measurable (policy

Practical conditional-reward-law endpoint for the concrete generated UCB policy. The only algorithmic numeric remainder is the explicit deterministic radius-inversion contract `hradius`.

theorem measure_successorArmPullCount_selectedPolicySuccessorGeneratedUCBAction_gt_threshold_le_ennreal_delta_of_reward_map_eq_selected_policy {Omega Context : Type} {K : Nat} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] (hK : 0 < K) (mu : Measure Omega) [IsProbabilityMeasure mu] (rewardKernel : RewardKernel.MarkovRewardKernel (Context × Fin K) Rat) (context : (n : Nat) -> History.FiniteRewardHistory Rat n -> Context) (mean : Context -> Fin K -> Rat) (varianceProxy : Context -> Fin K -> NNReal) (defaultAction best chosen : Fin K) (armMean : Fin K -> Rat) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (rewardLo rewardHi meanLo meanHi : Nat -> Real) (sigma2 : NNReal) (hcontext : forall n : Nat, Measurable (context n)) (hmean : Measurable (fun pair : Context × Fin K => mean pair.1 pair.2)) (hkernel : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hraw : forall i : Nat, forall omega : Omega, Set.Icc (rewardLo i) (rewardHi i) (((reward omega (i + 1) : Rat) : Real))) (hmean_range : forall i : Nat, forall c : Context, forall arm : Fin K, Set.Icc (meanLo i) (meanHi i) (((mean c arm : Rat) : Real))) (T : Nat) (hT : 0 < T) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) (hvariance : forall i : Nat, forall history : History.FiniteRewardHistory Rat i, 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 : History.FiniteRewardHistory Rat i, forall arm : Fin K, mean (context i history) arm = armMean arm) (h_reward_map_eq_policy : forall i : Nat, Filter.Eventually (fun omega : Omega => @Measure.map Omega Rat mOmega inferInstance (fun y : Omega => reward y (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc (selectedPolicySuccessorGeneratedUCBAction hK sigma2 T delta defaultAction reward) reward (ConditionalExpectationReward.generatedActionFromRewardHistory_measurable (policy

Timewise measurability of the concrete generated UCB action trace.

theorem measurable_selectedPolicySuccessorGeneratedUCBAction {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (T : Nat) (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 => selectedPolicySuccessorGeneratedUCBAction hK sigma2 T delta defaultAction reward omega t)

Integrate a bounded Nat-valued random variable from one upper-tail probability bound. This is the exact `B + horizon * delta` layer used by the generated UCB pull-count theorem below.

theorem lintegral_natCast_le_threshold_add_bound_mul_of_measure_gt {Omega : Type} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (count : Omega -> Nat) (hcount : Measurable count) (threshold bound : Nat) (hbound : forall omega, count omega <= bound) (epsilon : ENNReal) (htail : mu {omega | threshold < count omega} <= epsilon) : ∫⁻ omega, (count omega : ENNReal) ∂mu <= (threshold : ENNReal) + (bound : ENNReal) * epsilon

ENNReal expected pull-count bound for the concrete generated UCB process from the global large-gap probability theorem and the deterministic radius inversion contract.

theorem lintegral_successorArmPullCount_selectedPolicySuccessorGeneratedUCBAction_le_threshold_add_horizon_mul_delta_of_largeGap {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) (T : Nat) (delta : Real) (defaultAction best chosen : Fin K) (B : Nat) (hB : 0 < B) (hradius : forall k n : Nat, B <= k -> n <= T -> 2 * ConditionalExpectationReward.successorArmEmpiricalMeanFiniteArmTimePeelingRadius sigma2 k n (Finset.univ : Finset (Fin K)) T delta < meanGap (fun arm => (armMean arm : Real)) best chosen) (hlargeGap : mu (selectedPolicySuccessorLargeGapEvent (selectedPolicySuccessorGeneratedUCBInitializedScoreMaxSource hK reward armMean sigma2 T delta defaultAction best)) <= ENNReal.ofReal delta) : ∫⁻ omega, (ConditionalExpectationReward.successorArmPullCount (selectedPolicySuccessorGeneratedUCBAction hK sigma2 T delta defaultAction reward omega) chosen (T + 1) : ENNReal) ∂mu <= (B : ENNReal) + (T : ENNReal) * ENNReal.ofReal delta

ENNReal expected pull-count bound whose algorithmic remainder is stated only through the two full-horizon numeric threshold inequalities.

theorem lintegral_successorArmPullCount_selectedPolicySuccessorGeneratedUCBAction_le_threshold_add_horizon_mul_delta_of_global_threshold {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) (T : Nat) (hT : 0 < T) (delta : Real) (hdelta : 0 < delta) (defaultAction best chosen : Fin K) (B : Nat) (hB : 0 < B) (hgap : 0 < meanGap (fun arm => (armMean arm : Real)) best chosen) (hquadratic : 32 * (((sigma2 : NNReal) : Real)) * selectedPolicySuccessorFiniteArmTimeLogBudget K T T delta < meanGap (fun arm => (armMean arm : Real)) best chosen ^ 2 * (B : Real)) (hlinear : 4 * selectedPolicySuccessorFiniteArmTimeLogBudget K T T delta < meanGap (fun arm => (armMean arm : Real)) best chosen * (B : Real)) (hlargeGap : mu (selectedPolicySuccessorLargeGapEvent (selectedPolicySuccessorGeneratedUCBInitializedScoreMaxSource hK reward armMean sigma2 T delta defaultAction best)) <= ENNReal.ofReal delta) : ∫⁻ omega, (ConditionalExpectationReward.successorArmPullCount (selectedPolicySuccessorGeneratedUCBAction hK sigma2 T delta defaultAction reward omega) chosen (T + 1) : ENNReal) ∂mu <= (B : ENNReal) + (T : ENNReal) * ENNReal.ofReal delta

ENNReal expected pull-count bound at the explicit one-more-than-ceiling threshold; the numeric radius inversion is fully discharged internally.

theorem lintegral_successorArmPullCount_selectedPolicySuccessorGeneratedUCBAction_le_explicitPullThreshold_add_horizon_mul_delta_of_largeGap {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) (T : Nat) (hT : 0 < T) (delta : Real) (hdelta : 0 < delta) (defaultAction best chosen : Fin K) (hgap : 0 < meanGap (fun arm => (armMean arm : Real)) best chosen) (hlargeGap : mu (selectedPolicySuccessorLargeGapEvent (selectedPolicySuccessorGeneratedUCBInitializedScoreMaxSource hK reward armMean sigma2 T delta defaultAction best)) <= ENNReal.ofReal delta) : ∫⁻ omega, (ConditionalExpectationReward.successorArmPullCount (selectedPolicySuccessorGeneratedUCBAction hK sigma2 T delta defaultAction reward omega) chosen (T + 1) : ENNReal) ∂mu <= (selectedPolicySuccessorPullThreshold K sigma2 T delta (meanGap (fun arm => (armMean arm : Real)) best chosen) : ENNReal) + (T : ENNReal) * ENNReal.ofReal delta

End-to-end practical selected-reward-law expected pull-count theorem for the concrete generated UCB policy at its explicit integer threshold.

theorem lintegral_successorArmPullCount_selectedPolicySuccessorGeneratedUCBAction_le_explicitPullThreshold_add_horizon_mul_delta_of_reward_map_eq_selected_policy {Omega Context : Type} {K : Nat} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] (hK : 0 < K) (mu : Measure Omega) [IsProbabilityMeasure mu] (rewardKernel : RewardKernel.MarkovRewardKernel (Context × Fin K) Rat) (context : (n : Nat) -> History.FiniteRewardHistory Rat n -> Context) (mean : Context -> Fin K -> Rat) (varianceProxy : Context -> Fin K -> NNReal) (defaultAction best chosen : Fin K) (armMean : Fin K -> Rat) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (rewardLo rewardHi meanLo meanHi : Nat -> Real) (sigma2 : NNReal) (hcontext : forall n : Nat, Measurable (context n)) (hmean : Measurable (fun pair : Context × Fin K => mean pair.1 pair.2)) (hkernel : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hraw : forall i : Nat, forall omega : Omega, Set.Icc (rewardLo i) (rewardHi i) (((reward omega (i + 1) : Rat) : Real))) (hmean_range : forall i : Nat, forall c : Context, forall arm : Fin K, Set.Icc (meanLo i) (meanHi i) (((mean c arm : Rat) : Real))) (T : Nat) (hT : 0 < T) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) (hvariance : forall i : Nat, forall history : History.FiniteRewardHistory Rat i, 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 : History.FiniteRewardHistory Rat i, forall arm : Fin K, mean (context i history) arm = armMean arm) (h_reward_map_eq_policy : forall i : Nat, Filter.Eventually (fun omega : Omega => @Measure.map Omega Rat mOmega inferInstance (fun y : Omega => reward y (i + 1)) (@ProbabilityTheory.condExpKernel Omega mOmega _ mu _ ((History.historyFiltrationSucc (selectedPolicySuccessorGeneratedUCBAction hK sigma2 T delta defaultAction reward) reward (ConditionalExpectationReward.generatedActionFromRewardHistory_measurable (policy