BanditRLProof.Algorithms.UCBConditionalRewardLawRegret

The UCB designated-best Real mean gap is the local model gap after casting.

theorem modelMeanGap_bestArm_eq_realGap {K : Nat} (model : FiniteBanditModel K) (arm : Fin K) : meanGap (fun a => ((model.mean a : Rat) : Real)) model.bestArm arm = ((model.gap arm : Rat) : Real)

Textbook-style real contribution of one positive-gap arm's count threshold.

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

The explicit integer pull threshold is at most its real max plus two.

theorem selectedPolicySuccessorPullThreshold_cast_le_realThreshold_add_two (K : Nat) (sigma2 : NNReal) (T : Nat) (delta gap : Real) (hgap : 0 < gap) : (selectedPolicySuccessorPullThreshold K sigma2 T delta gap : Real) <= selectedPolicySuccessorRealPullThreshold K sigma2 T delta gap + 2

Multiplying the explicit threshold by a positive gap removes one gap power.

theorem gap_mul_selectedPolicySuccessorPullThreshold_cast_le_textbookGapBudget (K : Nat) (sigma2 : NNReal) (T : Nat) (delta gap : Real) (hgap : 0 < gap) : gap * (selectedPolicySuccessorPullThreshold K sigma2 T delta gap : Real) <= selectedPolicySuccessorTextbookGapBudget K sigma2 T delta gap

ENNReal form of the one-arm textbook threshold contribution.

theorem ofReal_gap_mul_selectedPolicySuccessorPullThreshold_le_textbookGapBudget (K : Nat) (sigma2 : NNReal) (T : Nat) (delta gap : Real) (hgap : 0 < gap) : ENNReal.ofReal gap * (selectedPolicySuccessorPullThreshold K sigma2 T delta gap : ENNReal) <= ENNReal.ofReal (selectedPolicySuccessorTextbookGapBudget K sigma2 T delta gap)

Finite-arm threshold simplification. Only positive model gaps remain in the textbook sum, and the confidence-failure contribution is preserved exactly.

theorem sum_gap_mul_explicitThreshold_add_failure_le_textbookGapSum {K : Nat} (model : FiniteBanditModel K) (sigma2 : NNReal) (T : Nat) (delta : Real) : (Finset.univ : Finset (Fin K)).sum (fun arm => ENNReal.ofReal (((model.gap arm : Rat) : Real)) * (selectedPolicySuccessorPullThreshold K sigma2 T delta (((model.gap arm : Rat) : Real)) : ENNReal) + ENNReal.ofReal (((model.gap arm : Rat) : Real)) * ((T : ENNReal) * ENNReal.ofReal delta)) <= ((Finset.univ : Finset (Fin K)).filter (fun arm => 0 < (((model.gap arm : Rat) : Real)))).sum (fun arm => ENNReal.ofReal (selectedPolicySuccessorTextbookGapBudget K sigma2 T delta (((model.gap arm : Rat) : Real))) + ENNReal.ofReal (((model.gap arm : Rat) : Real)) * ((T : ENNReal) * ENNReal.ofReal delta))

Shift successor generated actions `1, ..., T` to regret times `0, ..., T-1`.

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

Every coordinate of the shifted generated UCB regret action is measurable.

theorem measurable_selectedPolicySuccessorGeneratedUCBRegretAction {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 => selectedPolicySuccessorGeneratedUCBRegretAction hK sigma2 T delta defaultAction reward omega t)

The shifted regret pull count is exactly the existing successor pull count.

theorem pullCount_selectedPolicySuccessorGeneratedUCBRegretAction_eq {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) : pullCount (selectedPolicySuccessorGeneratedUCBRegretAction hK sigma2 T delta defaultAction reward omega) arm T = ConditionalExpectationReward.successorArmPullCount (selectedPolicySuccessorGeneratedUCBAction hK sigma2 T delta defaultAction reward omega) arm (T + 1)

Generic finite-arm ENNReal pseudo-regret assembly. Only positive-gap arms need a pull-count bound; zero-gap arms disappear after multiplication.

theorem lintegral_ofReal_pseudoRegret_le_sum_gap_mul_bound_of_positiveGap_pullCount {Omega : Type} [MeasurableSpace Omega] {K : Nat} (mu : Measure Omega) (model : FiniteBanditModel K) (action : Omega -> ActionTrace (Fin K)) (haction : forall t : Nat, Measurable (fun omega : Omega => action omega t)) (n : Nat) (bound : Fin K -> ENNReal) (hcount : forall arm : Fin K, 0 < (((model.gap arm : Rat) : Real)) -> ∫⁻ omega, ((pullCount (action omega) arm n : Nat) : ENNReal) ∂mu <= bound arm) : ∫⁻ omega, ENNReal.ofReal (((pseudoRegret model (action omega) n : Rat) : Real)) ∂mu <= (Finset.univ : Finset (Fin K)).sum (fun arm => ENNReal.ofReal (((model.gap arm : Rat) : Real)) * bound arm)

End-to-end practical selected-reward-law pseudo-regret bound for the concrete generated UCB policy. Every positive-gap arm uses its own explicit threshold; zero-gap arms vanish from the finite weighted sum.

theorem lintegral_ofReal_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction_le_explicitThresholdSum_of_reward_map_eq_selected_policy {Omega Context : Type} {K : Nat} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] (mu : Measure Omega) [IsProbabilityMeasure mu] (model : FiniteBanditModel K) (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 : Fin K) (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 model.hK sigma2 T delta defaultAction i).action (selectedPolicySuccessorHistoryState model.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 = model.mean 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 model.hK sigma2 T delta defaultAction reward) reward (ConditionalExpectationReward.generatedActionFromRewardHistory_measurable (policy

End-to-end practical selected-reward-law pseudo-regret bound with the integer threshold eliminated in favor of a textbook reciprocal-gap finite sum.

theorem lintegral_ofReal_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction_le_textbookGapSum_of_reward_map_eq_selected_policy {Omega Context : Type} {K : Nat} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] (mu : Measure Omega) [IsProbabilityMeasure mu] (model : FiniteBanditModel K) (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 : Fin K) (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 model.hK sigma2 T delta defaultAction i).action (selectedPolicySuccessorHistoryState model.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 = model.mean 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 model.hK sigma2 T delta defaultAction reward) reward (ConditionalExpectationReward.generatedActionFromRewardHistory_measurable (policy