BanditRLProof.Algorithms.UCBConditionalRewardLawCenteredKernel

Direct selected-law conditional-MGF bridge for a centered reward kernel. Unlike the older raw-range source route, this theorem consumes the `CenteredRewardKernelLaw` MGF field directly. No pointwise or almost-everywhere reward-range hypothesis is needed.

theorem centeredReward_succ_hasCondSubgaussianMGF_of_reward_map_eq_selected_policy_centeredKernel_of_variance_le {Omega Context State Action : Type} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] (mu : Measure Omega) [IsFiniteMeasure mu] (rewardKernel : RewardKernel.MarkovRewardKernel (Context × Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> History.FiniteRewardHistory Rat n -> Context) (state : (n : Nat) -> History.FiniteRewardHistory Rat n -> State) (mean : Context -> Action -> Rat) (varianceProxy : Context -> Action -> NNReal) (defaultAction : Action) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega => reward omega t)) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (hmean : Measurable (fun pair : Context × Action => mean pair.1 pair.2)) (hkernel : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (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 (generatedActionFromRewardHistory policy state defaultAction reward) reward (generatedActionFromRewardHistory_measurable (policy := policy) (state := state) (defaultAction := defaultAction) (reward := reward) hreward hstate) hreward) i) omega) = RewardKernel.selectedMeasure rewardKernel (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i)))) (ae (mu.trim ((History.historyFiltrationSucc (generatedActionFromRewardHistory policy state defaultAction reward) reward (generatedActionFromRewardHistory_measurable (policy := policy) (state := state) (defaultAction := defaultAction) (reward := reward) hreward hstate) hreward).le i)))) (i : Nat) (c : NNReal) (hvariance : forall history : History.FiniteRewardHistory Rat i, varianceProxy (context i history) ((policy i).action (state i history)) <= c) : ProbabilityTheory.HasCondSubgaussianMGF ((History.historyFiltrationSucc (generatedActionFromRewardHistory policy state defaultAction reward) reward (generatedActionFromRewardHistory_measurable (policy := policy) (state := state) (defaultAction := defaultAction) (reward := reward) hreward hstate) hreward) i) ((History.historyFiltrationSucc (generatedActionFromRewardHistory policy state defaultAction reward) reward (generatedActionFromRewardHistory_measurable (policy := policy) (state := state) (defaultAction := defaultAction) (reward := reward) hreward hstate) hreward).le i) (fun omega : Omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real))) c mu

Predictable-variance two-sided tail for one arm, obtained directly from the centered-kernel conditional MGF. The selected arm is charged `sigma2` only at successor times when it is pulled.

theorem armMaskedCenteredRewardSuccProcess_sum_abs_tail_predictableVariance_ennreal_delta_of_reward_map_eq_selected_policy_centeredKernel {Omega Context State Action : Type} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] (mu : Measure Omega) [IsProbabilityMeasure mu] (rewardKernel : RewardKernel.MarkovRewardKernel (Context × Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> History.FiniteRewardHistory Rat n -> Context) (state : (n : Nat) -> History.FiniteRewardHistory Rat n -> State) (mean : Context -> Action -> Rat) (varianceProxy : Context -> Action -> NNReal) (defaultAction arm : Action) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega => reward omega t)) (sigma2 : NNReal) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (hmean : Measurable (fun pair : Context × Action => mean pair.1 pair.2)) (hkernel : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hvariance : forall i : Nat, forall history : History.FiniteRewardHistory Rat i, varianceProxy (context i history) ((policy i).action (state i history)) <= sigma2) (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 (generatedActionFromRewardHistory policy state defaultAction reward) reward (generatedActionFromRewardHistory_measurable (policy := policy) (state := state) (defaultAction := defaultAction) (reward := reward) hreward hstate) hreward) i) omega) = RewardKernel.selectedMeasure rewardKernel (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i)))) (ae (mu.trim ((History.historyFiltrationSucc (generatedActionFromRewardHistory policy state defaultAction reward) reward (generatedActionFromRewardHistory_measurable (policy := policy) (state := state) (defaultAction := defaultAction) (reward := reward) hreward hstate) hreward).le i)))) (n : Nat) (varianceBudget delta : Real) (hvarianceBudget : 0 < varianceBudget) (hdelta : 0 < delta) : let action := generatedActionFromRewardHistory policy state defaultAction reward let X : Nat -> Omega -> Real := fun i omega => (((reward omega (i + 1) - mean (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i))) : Rat) : Real)) let Y : Nat -> Omega -> Real := fun t omega => match t with | 0 => 0 | i + 1 => {omega : Omega | action omega (i + 1) = arm}.indicator (X i) omega let V : Nat -> Omega -> Real := fun t omega => match t with | 0 => 0 | i + 1 => {omega : Omega | action omega (i + 1) = arm}.indicator (fun _ => (((sigma2 : NNReal) : Real))) omega mu {omega | Concentration.subGaussianPredictableVarianceRadius varianceBudget delta <= |(Finset.range n).sum (fun t => Y t omega)| ∧ (Finset.range n).sum (fun t => V t omega) <= varianceBudget} <= ENNReal.ofReal delta

Exact positive pull-count confidence using the centered-kernel route.

theorem successorArmEmpiricalMean_abs_tail_exact_pullCount_ennreal_delta_of_reward_map_eq_selected_policy_centeredKernel {Omega Context State Action : Type} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] [DecidableEq Action] (mu : Measure Omega) [IsProbabilityMeasure mu] (rewardKernel : RewardKernel.MarkovRewardKernel (Context × Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> History.FiniteRewardHistory Rat n -> Context) (state : (n : Nat) -> History.FiniteRewardHistory Rat n -> State) (mean : Context -> Action -> Rat) (varianceProxy : Context -> Action -> NNReal) (defaultAction arm : Action) (armMean : Rat) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega => reward omega t)) (sigma2 : NNReal) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (hmean : Measurable (fun pair : Context × Action => mean pair.1 pair.2)) (hkernel : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hvariance : forall i : Nat, forall history : History.FiniteRewardHistory Rat i, varianceProxy (context i history) ((policy i).action (state i history)) <= sigma2) (harmMean : forall i : Nat, forall history : History.FiniteRewardHistory Rat i, mean (context i history) arm = armMean) (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 (generatedActionFromRewardHistory policy state defaultAction reward) reward (generatedActionFromRewardHistory_measurable (policy := policy) (state := state) (defaultAction := defaultAction) (reward := reward) hreward hstate) hreward) i) omega) = RewardKernel.selectedMeasure rewardKernel (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i)))) (ae (mu.trim ((History.historyFiltrationSucc (generatedActionFromRewardHistory policy state defaultAction reward) reward (generatedActionFromRewardHistory_measurable (policy := policy) (state := state) (defaultAction := defaultAction) (reward := reward) hreward hstate) hreward).le i)))) (n k : Nat) (hk : 0 < k) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) : let action := generatedActionFromRewardHistory policy state defaultAction reward let count : Omega -> Nat := fun omega => successorArmPullCount (action omega) arm n mu {omega | count omega = k ∧ successorArmEmpiricalMeanExactCountRadius sigma2 k delta <= |successorArmEmpiricalMean (action omega) (reward omega) arm n - (armMean : Real)|} <= ENNReal.ofReal delta

Positive random pull-count confidence via finite exact-count peeling.

theorem successorArmEmpiricalMean_abs_tail_random_pullCount_ennreal_delta_of_reward_map_eq_selected_policy_centeredKernel {Omega Context State Action : Type} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] [DecidableEq Action] (mu : Measure Omega) [IsProbabilityMeasure mu] (rewardKernel : RewardKernel.MarkovRewardKernel (Context × Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> History.FiniteRewardHistory Rat n -> Context) (state : (n : Nat) -> History.FiniteRewardHistory Rat n -> State) (mean : Context -> Action -> Rat) (varianceProxy : Context -> Action -> NNReal) (defaultAction arm : Action) (armMean : Rat) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega => reward omega t)) (sigma2 : NNReal) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (hmean : Measurable (fun pair : Context × Action => mean pair.1 pair.2)) (hkernel : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hvariance : forall i : Nat, forall history : History.FiniteRewardHistory Rat i, varianceProxy (context i history) ((policy i).action (state i history)) <= sigma2) (harmMean : forall i : Nat, forall history : History.FiniteRewardHistory Rat i, mean (context i history) arm = armMean) (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 (generatedActionFromRewardHistory policy state defaultAction reward) reward (generatedActionFromRewardHistory_measurable (policy := policy) (state := state) (defaultAction := defaultAction) (reward := reward) hreward hstate) hreward) i) omega) = RewardKernel.selectedMeasure rewardKernel (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i)))) (ae (mu.trim ((History.historyFiltrationSucc (generatedActionFromRewardHistory policy state defaultAction reward) reward (generatedActionFromRewardHistory_measurable (policy := policy) (state := state) (defaultAction := defaultAction) (reward := reward) hreward hstate) hreward).le i)))) (n : Nat) (hn : 0 < n) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) : let action := generatedActionFromRewardHistory policy state defaultAction reward let count : Omega -> Nat := fun omega => successorArmPullCount (action omega) arm n mu {omega | 0 < count omega ∧ successorArmEmpiricalMeanPeelingRadius sigma2 (count omega) n delta <= |successorArmEmpiricalMean (action omega) (reward omega) arm n - (armMean : Real)|} <= ENNReal.ofReal delta

Finite-arm, finite-time empirical-mean confidence from the centered-kernel selected-law route. This is fixed-horizon and union-bounded, not anytime.

theorem successorArmEmpiricalMean_simultaneous_finiteArmTime_abs_tail_ennreal_delta_of_reward_map_eq_selected_policy_centeredKernel {Omega Context State Action : Type} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] [DecidableEq Action] (mu : Measure Omega) [IsProbabilityMeasure mu] (rewardKernel : RewardKernel.MarkovRewardKernel (Context × Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> History.FiniteRewardHistory Rat n -> Context) (state : (n : Nat) -> History.FiniteRewardHistory Rat n -> State) (mean : Context -> Action -> Rat) (varianceProxy : Context -> Action -> NNReal) (defaultAction : Action) (arms : Finset Action) (harms : arms.Nonempty) (armMean : Action -> Rat) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega => reward omega t)) (sigma2 : NNReal) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (hmean : Measurable (fun pair : Context × Action => mean pair.1 pair.2)) (hkernel : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hvariance : forall i : Nat, forall history : History.FiniteRewardHistory Rat i, varianceProxy (context i history) ((policy i).action (state i history)) <= sigma2) (harmMean : forall i : Nat, forall history : History.FiniteRewardHistory Rat i, forall arm, arm ∈ arms -> 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 (generatedActionFromRewardHistory policy state defaultAction reward) reward (generatedActionFromRewardHistory_measurable (policy := policy) (state := state) (defaultAction := defaultAction) (reward := reward) hreward hstate) hreward) i) omega) = RewardKernel.selectedMeasure rewardKernel (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i)))) (ae (mu.trim ((History.historyFiltrationSucc (generatedActionFromRewardHistory policy state defaultAction reward) reward (generatedActionFromRewardHistory_measurable (policy := policy) (state := state) (defaultAction := defaultAction) (reward := reward) hreward hstate) hreward).le i)))) (T : Nat) (hT : 0 < T) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) : let action := generatedActionFromRewardHistory policy state defaultAction reward mu (successorArmEmpiricalMeanFiniteArmTimeBadEvent action reward arms armMean sigma2 T delta) <= ENNReal.ofReal delta

Practical selected-policy UCB large-gap event bound using the centered-kernel conditional-MGF route. No reward or mean range contract is exposed.

theorem measure_selectedPolicySuccessorLargeGapEvent_le_ennreal_delta_of_reward_map_eq_selected_policy_centeredKernel {Omega Context State Action : Type} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] [MeasurableSpace State] [MeasurableSpace Action] [MeasurableSingletonClass Action] [Countable Action] [DecidableEq Action] (mu : Measure Omega) [IsProbabilityMeasure mu] (rewardKernel : RewardKernel.MarkovRewardKernel (Context × Action) Rat) (policy : Nat -> Policy.MeasurablePolicy State Action) (context : (n : Nat) -> History.FiniteRewardHistory Rat n -> Context) (state : (n : Nat) -> History.FiniteRewardHistory Rat n -> State) (mean : Context -> Action -> Rat) (varianceProxy : Context -> Action -> NNReal) (defaultAction : Action) (arms : Finset Action) (harms : arms.Nonempty) (armMean : Action -> Rat) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega => reward omega t)) (sigma2 : NNReal) (hcontext : forall n : Nat, Measurable (context n)) (hstate : forall n : Nat, Measurable (state n)) (hmean : Measurable (fun pair : Context × Action => mean pair.1 pair.2)) (hkernel : RewardKernel.CenteredRewardKernelLaw rewardKernel mean varianceProxy) (hvariance : forall i : Nat, forall history : History.FiniteRewardHistory Rat i, varianceProxy (context i history) ((policy i).action (state i history)) <= sigma2) (harmMean : forall i : Nat, forall history : History.FiniteRewardHistory Rat i, forall arm, arm ∈ arms -> 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 (ConditionalExpectationReward.generatedActionFromRewardHistory policy state defaultAction reward) reward (ConditionalExpectationReward.generatedActionFromRewardHistory_measurable (policy := policy) (state := state) (defaultAction := defaultAction) (reward := reward) hreward hstate) hreward) i) omega) = RewardKernel.selectedMeasure rewardKernel (context i (History.finiteRewardHistoryOfTrace (reward omega) i)) ((policy i).action (state i (History.finiteRewardHistoryOfTrace (reward omega) i)))) (ae (mu.trim ((History.historyFiltrationSucc (ConditionalExpectationReward.generatedActionFromRewardHistory policy state defaultAction reward) reward (ConditionalExpectationReward.generatedActionFromRewardHistory_measurable (policy := policy) (state := state) (defaultAction := defaultAction) (reward := reward) hreward hstate) hreward).le i)))) (T : Nat) (hT : 0 < T) (hsigma2 : 0 < (((sigma2 : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) (source : SelectedPolicySuccessorInitializedScoreMaxSource (ConditionalExpectationReward.generatedActionFromRewardHistory policy state defaultAction reward) reward arms armMean sigma2 T delta) : mu (selectedPolicySuccessorLargeGapEvent source) <= ENNReal.ofReal delta

Exact selected-reward conditional-law contract for the generated UCB policy.

def SelectedPolicySuccessorRewardMapLaw {Omega Context : Type} {K : Nat} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [MeasurableSpace Context] (hK : 0 < K) (mu : Measure Omega) [IsFiniteMeasure mu] (rewardKernel : RewardKernel.MarkovRewardKernel (Context × Fin K) Rat) (context : (n : Nat) -> History.FiniteRewardHistory Rat n -> Context) (defaultAction : Fin K) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega => reward omega t)) (sigma2 : NNReal) (T : Nat) (delta : Real) : Prop

Generated-UCB large-gap event bound with no range assumptions.

theorem measure_selectedPolicySuccessorLargeGapEvent_generatedUCB_le_ennreal_delta_of_reward_map_eq_selected_policy_centeredKernel {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 => reward omega t)) (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) (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 : SelectedPolicySuccessorRewardMapLaw hK mu rewardKernel context defaultAction reward hreward sigma2 T delta) : mu (selectedPolicySuccessorLargeGapEvent (selectedPolicySuccessorGeneratedUCBInitializedScoreMaxSource hK reward armMean sigma2 T delta defaultAction best)) <= ENNReal.ofReal delta

Expected pull count at the explicit generated-UCB threshold, using only the centered-kernel law and the selected reward-map identity.

theorem lintegral_successorArmPullCount_selectedPolicySuccessorGeneratedUCBAction_le_explicitPullThreshold_add_horizon_mul_delta_of_reward_map_eq_selected_policy_centeredKernel {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 => reward omega t)) (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) (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 : SelectedPolicySuccessorRewardMapLaw hK mu rewardKernel context defaultAction reward hreward sigma2 T delta) (hgap : 0 < meanGap (fun arm => (armMean arm : Real)) best chosen) : ∫⁻ 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

Finite-arm ENNReal pseudo-regret assembly for the centered-kernel generated-UCB route. Positive-gap arms use their explicit pull threshold; zero gaps vanish.

theorem lintegral_ofReal_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction_le_explicitThresholdSum_of_reward_map_eq_selected_policy_centeredKernel {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 => reward omega t)) (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) (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 : SelectedPolicySuccessorRewardMapLaw model.hK mu rewardKernel context defaultAction reward hreward sigma2 T delta) : ∫⁻ omega, ENNReal.ofReal (((pseudoRegret model (selectedPolicySuccessorGeneratedUCBRegretAction model.hK sigma2 T delta defaultAction reward omega) T : Rat) : Real)) ∂mu <= (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)) : Nat) : ENNReal) + ENNReal.ofReal (((model.gap arm : Rat) : Real)) * ((T : ENNReal) * ENNReal.ofReal delta))

Textbook reciprocal-gap pseudo-regret sum for the centered-kernel route.

theorem lintegral_ofReal_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction_le_textbookGapSum_of_reward_map_eq_selected_policy_centeredKernel {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 => reward omega t)) (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) (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 : SelectedPolicySuccessorRewardMapLaw model.hK mu rewardKernel context defaultAction reward hreward sigma2 T delta) : ∫⁻ omega, ENNReal.ofReal (((pseudoRegret model (selectedPolicySuccessorGeneratedUCBRegretAction model.hK sigma2 T delta defaultAction reward omega) T : Rat) : Real)) ∂mu <= ((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))

Canonical reward-only generated-UCB textbook pseudo-regret theorem. The canonical `trajMeasure` supplies the selected conditional reward law, and `CenteredRewardKernelLaw` supplies the analytic MGF/integrability contract. Consequently no raw-reward or mean-range premise remains.

theorem lintegral_ofReal_pseudoRegret_selectedPolicySuccessorGeneratedUCBRegretAction_le_textbookGapSum_trajMeasure_centeredKernel {Context : Type} {K : Nat} [MeasurableSpace Context] (model : FiniteBanditModel K) (mu0 : Measure Rat) [IsProbabilityMeasure mu0] (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) (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) (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) : ∫⁻ trajectory : RewardTrace Rat, ENNReal.ofReal (((pseudoRegret model (selectedPolicySuccessorGeneratedUCBRegretAction model.hK sigma2 T delta defaultAction (fun y : RewardTrace Rat => y) trajectory) T : Rat) : Real)) ∂(selectedPolicySuccessorRewardTrajMeasure model.hK mu0 rewardKernel context hcontext sigma2 T delta defaultAction) <= ((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))