BanditRLProof.Algorithms.KLUCBGeneratedRegret

KL exploration budget on a realized generated prefix. The margin is a known regularity contract, while the empirical count and radius are computed from the actual action/reward trace.

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

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

theorem generatedBudgetAt_nonneg {Omega : Type} {K : Nat} (action : Omega -> ActionTrace (Fin K)) (sigma2 : NNReal) (delta margin : Real) (hmargin0 : 0 < margin) (hmargin1 : margin < 1) (omega : Omega) (t : Nat) (arm : Fin K) : 0 <= generatedBudgetAt action sigma2 delta margin omega t arm

Genuine Bernoulli-KL index on one generated prefix.

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

KL score reconstructed from a finite generated pair history.

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

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

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

Round-robin initialization followed by KL-index maximization.

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

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

theorem historyIndex_le_nextArm_of_K_le {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta margin : Real) (defaultAction : Fin K) (t : Nat) (history : History.FinitePairHistory (Fin K) Rat t) (ht : K <= t) (arm : Fin K) : historyIndex sigma2 delta margin defaultAction t history arm <= historyIndex sigma2 delta margin defaultAction t history (historyNextArm hK sigma2 delta margin defaultAction t history)

Pair-history reconstruction for the KL-UCB policy.

def pairHistory {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta margin : 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 := pairHistory hK sigma2 delta margin defaultAction n previousRewardHistory let nextAction := historyNextArm hK sigma2 delta margin defaultAction n previousHistory History.extendPairHistorySucc previousHistory (nextAction, rewardHistory ⟨n + 1, Finset.mem_Iic.mpr le_rfl⟩) def historyState {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta margin : Real) (defaultAction : Fin K) (n : Nat) (rewardHistory : History.FiniteRewardHistory Rat n) : UCB.SelectedPolicySuccessorFiniteHistoryState K

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

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

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

theorem measurable_historyState {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta margin : Real) (defaultAction : Fin K) (n : Nat) : Measurable (historyState hK sigma2 delta margin defaultAction n)

The measurable KL-UCB policy. Its declaration has no terminal horizon.

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

Canonical generated action trace of the KL-UCB policy.

def generatedAction {Omega : Type} {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta margin : 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 generatedAction_succ {Omega : Type} {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta margin : Real) (defaultAction : Fin K) (reward : Omega -> RewardTrace Rat) (omega : Omega) (t : Nat) : generatedAction hK sigma2 delta margin defaultAction reward omega (t + 1) = historyNextArm hK sigma2 delta margin defaultAction t (pairHistory hK sigma2 delta margin defaultAction t (History.finiteRewardHistoryOfTrace (reward omega) t))

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

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

The finite-history score, count, mean, and budget are definitionally the ones on the same generated trajectory.

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

Selected KL index maximality on the actual generated action/reward trace.

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

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

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

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

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

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

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

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

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

A bounded empirical-mean deviation on the actual prefix makes the true interior arm mean feasible for the KL confidence set used by the policy.

theorem armMean_mem_confidenceSet_of_abs_lt_radius {Omega : Type} {K : Nat} (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Rat) (sigma2 : NNReal) (delta margin : Real) (hmargin0 : 0 < margin) (hmarginHalf : margin <= 1 / 2) (armMean : Fin K -> Rat) (omega : Omega) (t : Nat) (arm : Fin K) (hemp : IsBernoulliParameter (UCB.selectedPolicySuccessorEmpiricalMeanAt action reward omega t arm)) (hmean : (armMean arm : Real) ∈ Set.Icc margin (1 - margin)) (hdev : |UCB.selectedPolicySuccessorEmpiricalMeanAt action reward omega t arm - (armMean arm : Real)| < UCB.selectedPolicySuccessorTelescopingRadiusAt action sigma2 delta omega t arm) : (armMean arm : Real) ∈ confidenceSet (UCB.selectedPolicySuccessorEmpiricalMeanAt action reward omega t arm) (ConditionalExpectationReward.successorArmPullCount (action omega) arm (t + 1)) (generatedBudgetAt action sigma2 delta margin omega t arm)

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

theorem armMean_le_generatedIndexAt_of_abs_lt_radius {Omega : Type} {K : Nat} (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Rat) (sigma2 : NNReal) (delta margin : Real) (hmargin0 : 0 < margin) (hmarginHalf : margin <= 1 / 2) (armMean : Fin K -> Rat) (omega : Omega) (t : Nat) (arm : Fin K) (hemp : IsBernoulliParameter (UCB.selectedPolicySuccessorEmpiricalMeanAt action reward omega t arm)) (hmean : (armMean arm : Real) ∈ Set.Icc margin (1 - margin)) (hdev : |UCB.selectedPolicySuccessorEmpiricalMeanAt action reward omega t arm - (armMean arm : Real)| < UCB.selectedPolicySuccessorTelescopingRadiusAt action sigma2 delta omega t arm) : (armMean arm : Real) <= generatedIndexAt action reward sigma2 delta margin omega t arm

On the common generated all-time good event, selection of a positive-gap arm forces its realized KL calibration radius to remain large. This is the single-arm, single-round KL pull-threshold leaf.

theorem margin_mul_gap_div_eight_le_radius_of_selected_of_not_badEvent {Omega : Type} {K : Nat} (hK : 0 < K) (reward : Omega -> RewardTrace Rat) (armMean : Fin K -> Rat) (sigma2 : NNReal) (delta margin : Real) (hmargin0 : 0 < margin) (hmarginHalf : margin <= 1 / 2) (hmean : forall arm : Fin K, (armMean arm : Real) ∈ Set.Icc margin (1 - margin)) (defaultAction best : Fin K) (omega : Omega) (t : Nat) (ht : K <= t) (hemp : forall arm : Fin K, IsBernoulliParameter (UCB.selectedPolicySuccessorEmpiricalMeanAt (generatedAction hK sigma2 delta margin defaultAction reward) reward omega t arm)) (hbest : forall arm : Fin K, (armMean arm : Real) <= (armMean best : Real)) (hgap : 0 < UCB.meanGap (fun arm => (armMean arm : Real)) best (generatedAction hK sigma2 delta margin defaultAction reward omega (t + 1))) (hgood : omega ∉ ConditionalExpectationReward.successorArmEmpiricalMeanFintypeTelescopingAllTimeBadEvent (generatedAction hK sigma2 delta margin defaultAction reward) reward armMean sigma2 delta) : margin * UCB.meanGap (fun arm => (armMean arm : Real)) best (generatedAction hK sigma2 delta margin defaultAction reward omega (t + 1)) / 8 <= UCB.selectedPolicySuccessorTelescopingRadiusAt (generatedAction hK sigma2 delta margin defaultAction reward) sigma2 delta omega t (generatedAction hK sigma2 delta margin defaultAction reward omega (t + 1))

Explicit KL-UCB pull threshold, obtained by inverting the accepted telescoping radius at the effective gap `margin * gap / 4`.

def pullThreshold (K : Nat) (sigma2 : NNReal) (T : Nat) (delta margin gap : Real) : Nat

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

theorem pullCount_le_of_not_badEvent {Omega : Type} {K : Nat} (hK : 0 < K) (reward : Omega -> RewardTrace Rat) (armMean : Fin K -> Rat) (sigma2 : NNReal) (delta margin : Real) (hdelta : 0 < delta) (hmargin0 : 0 < margin) (hmarginHalf : margin <= 1 / 2) (hmean : forall arm : Fin K, (armMean arm : Real) ∈ Set.Icc margin (1 - margin)) (defaultAction best chosen : Fin K) (omega : Omega) (T : Nat) (hbest : forall arm : Fin K, (armMean arm : Real) <= (armMean best : Real)) (hemp : forall t : Nat, forall arm : Fin K, IsBernoulliParameter (UCB.selectedPolicySuccessorEmpiricalMeanAt (generatedAction hK sigma2 delta margin defaultAction reward) reward omega t arm)) (hgap : 0 < UCB.meanGap (fun arm => (armMean arm : Real)) best chosen) (hgood : omega ∉ ConditionalExpectationReward.successorArmEmpiricalMeanFintypeTelescopingAllTimeBadEvent (generatedAction hK sigma2 delta margin defaultAction reward) reward armMean sigma2 delta) : ConditionalExpectationReward.successorArmPullCount (generatedAction hK sigma2 delta margin defaultAction reward omega) chosen (T + 1) <= pullThreshold K sigma2 T delta margin (UCB.meanGap (fun arm => (armMean arm : Real)) best chosen)

The accepted all-time telescoping confidence producer instantiated on the KL-UCB policy. The theorem explicitly transports the sampled pair action to the reward-reconstructed action used by `generatedIndexAt`.

theorem actionRewardHistoryStepKernelFamily_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 margin : 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) ((historyPolicy hK sigma2 delta margin defaultAction i).action (historyState hK sigma2 delta margin 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 := historyPolicy hK sigma2 delta margin defaultAction let state := historyState hK sigma2 delta margin defaultAction let pairContext : (i : Nat) -> ((j : Finset.Iic i) -> Prod (Fin K) Rat) -> Context

Arms-by-times KL-confidence failure event on the exact generated trace.

def generatedKLAllTimeBadEvent {Omega : Type} {K : Nat} (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Rat) (armMean : Fin K -> Rat) (sigma2 : NNReal) (delta margin : Real) : Set Omega

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

theorem generatedKLAllTimeBadEvent_subset_absBadEvent {Omega : Type} {K : Nat} (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Rat) (armMean : Fin K -> Rat) (sigma2 : NNReal) (delta margin : Real) (hmargin0 : 0 < margin) (hmarginHalf : margin <= 1 / 2) (hmean : forall arm : Fin K, (armMean arm : Real) ∈ Set.Icc margin (1 - margin)) (hemp : forall omega t arm, IsBernoulliParameter (UCB.selectedPolicySuccessorEmpiricalMeanAt action reward omega t arm)) : generatedKLAllTimeBadEvent action reward armMean sigma2 delta margin ⊆ ConditionalExpectationReward.successorArmEmpiricalMeanFintypeTelescopingAllTimeBadEvent action reward armMean sigma2 delta

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

theorem measure_generatedKLAllTimeBadEvent_le {Omega : Type} [MeasurableSpace Omega] {K : Nat} (mu : Measure Omega) (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Rat) (armMean : Fin K -> Rat) (sigma2 : NNReal) (delta margin : Real) (hmargin0 : 0 < margin) (hmarginHalf : margin <= 1 / 2) (hmean : forall arm : Fin K, (armMean arm : Real) ∈ Set.Icc margin (1 - margin)) (hemp : ∀ᵐ omega ∂mu, forall t arm, IsBernoulliParameter (UCB.selectedPolicySuccessorEmpiricalMeanAt action reward omega t arm)) (hconfidence : mu (ConditionalExpectationReward.successorArmEmpiricalMeanFintypeTelescopingAllTimeBadEvent action reward armMean sigma2 delta) <= ENNReal.ofReal delta) : mu (generatedKLAllTimeBadEvent action reward armMean sigma2 delta margin) <= ENNReal.ofReal delta

Selected reward sums remain nonnegative under a pathwise `[0,1]` reward contract.

theorem sumRewards_nonneg_of_mem_Icc_zero_one {Action : Type} [DecidableEq Action] (action : ActionTrace Action) (reward : RewardTrace Real) (arm : Action) (n : Nat) (hraw : forall i, i < n -> reward i ∈ Set.Icc (0 : Real) 1) : 0 <= sumRewards action reward arm n

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

theorem sumRewards_le_pullCount_of_mem_Icc_zero_one {Action : Type} [DecidableEq Action] (action : ActionTrace Action) (reward : RewardTrace Real) (arm : Action) (n : Nat) (hraw : forall i, i < n -> reward i ∈ Set.Icc (0 : Real) 1) : sumRewards action reward arm n <= (pullCount action arm n : Real)

Hence every positive-count empirical mean on the canonical successor trace is a Bernoulli parameter.

theorem successorArmEmpiricalMean_isBernoulliParameter_of_rewards_mem_Icc {Action : Type} [DecidableEq Action] (action : ActionTrace Action) (reward : RewardTrace Rat) (arm : Action) (n : Nat) (hcount : 0 < ConditionalExpectationReward.successorArmPullCount action arm n) (hraw : forall i : Nat, (((reward i : Rat) : Real)) ∈ Set.Icc (0 : Real) 1) : IsBernoulliParameter (ConditionalExpectationReward.successorArmEmpiricalMean action reward arm n)

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

theorem generatedEmpiricalMean_isBernoulliParameter_of_rewards_mem_Icc {Omega : Type} {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta margin : Real) (defaultAction : Fin K) (reward : Omega -> RewardTrace Rat) (omega : Omega) (hraw : forall i : Nat, (((reward omega i : Rat) : Real)) ∈ Set.Icc (0 : Real) 1) (t : Nat) (ht : K <= t) (arm : Fin K) : IsBernoulliParameter (UCB.selectedPolicySuccessorEmpiricalMeanAt (generatedAction hK sigma2 delta margin defaultAction reward) reward omega t arm)

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

theorem successorArmEmpiricalMean_isBernoulliParameter_of_rewards_mem_Icc' {Action : Type} [DecidableEq Action] (action : ActionTrace Action) (reward : RewardTrace Rat) (arm : Action) (n : Nat) (hraw : forall i : Nat, (((reward i : Rat) : Real)) ∈ Set.Icc (0 : Real) 1) : IsBernoulliParameter (ConditionalExpectationReward.successorArmEmpiricalMean action reward arm n)

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

theorem generatedEmpiricalMean_isBernoulliParameter_of_rewards_mem_Icc' {Omega : Type} {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta margin : Real) (defaultAction : Fin K) (reward : Omega -> RewardTrace Rat) (omega : Omega) (hraw : forall i : Nat, (((reward omega i : Rat) : Real)) ∈ Set.Icc (0 : Real) 1) (t : Nat) (arm : Fin K) : IsBernoulliParameter (UCB.selectedPolicySuccessorEmpiricalMeanAt (generatedAction hK sigma2 delta margin defaultAction reward) reward omega t arm)

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

theorem measure_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 margin : Real) (hdelta : 0 < delta) (hmargin0 : 0 < margin) (hmarginHalf : margin <= 1 / 2) (hmean : forall arm : Fin K, (armMean arm : Real) ∈ Set.Icc margin (1 - margin)) (hraw : ∀ᵐ omega ∂mu, forall i, (((reward omega i : Rat) : Real)) ∈ Set.Icc (0 : Real) 1) (defaultAction best chosen : Fin K) (T : Nat) (hbest : forall arm : Fin K, (armMean arm : Real) <= (armMean best : Real)) (hgap : 0 < UCB.meanGap (fun arm => (armMean arm : Real)) best chosen) (hconfidence : mu (ConditionalExpectationReward.successorArmEmpiricalMeanFintypeTelescopingAllTimeBadEvent (generatedAction hK sigma2 delta margin defaultAction reward) reward armMean sigma2 delta) <= ENNReal.ofReal delta) : mu {omega | pullThreshold K sigma2 T delta margin (UCB.meanGap (fun arm => (armMean arm : Real)) best chosen) < ConditionalExpectationReward.successorArmPullCount (generatedAction hK sigma2 delta margin defaultAction reward omega) chosen (T + 1)} <= ENNReal.ofReal delta

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

theorem lintegral_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 margin : Real) (hdelta : 0 < delta) (hmargin0 : 0 < margin) (hmarginHalf : margin <= 1 / 2) (hmean : forall arm : Fin K, (armMean arm : Real) ∈ Set.Icc margin (1 - margin)) (hraw : ∀ᵐ omega ∂mu, forall i, (((reward omega i : Rat) : Real)) ∈ Set.Icc (0 : Real) 1) (defaultAction best chosen : Fin K) (T : Nat) (hbest : forall arm : Fin K, (armMean arm : Real) <= (armMean best : Real)) (hgap : 0 < UCB.meanGap (fun arm => (armMean arm : Real)) best chosen) (hconfidence : mu (ConditionalExpectationReward.successorArmEmpiricalMeanFintypeTelescopingAllTimeBadEvent (generatedAction hK sigma2 delta margin defaultAction reward) reward armMean sigma2 delta) <= ENNReal.ofReal delta) : ∫⁻ omega, (ConditionalExpectationReward.successorArmPullCount (generatedAction hK sigma2 delta margin defaultAction reward omega) chosen (T + 1) : ENNReal) ∂mu <= (pullThreshold K sigma2 T delta margin (UCB.meanGap (fun arm => (armMean arm : Real)) best chosen) : ENNReal) + (T : ENNReal) * ENNReal.ofReal delta

Regret-time shift of the canonical generated KL-UCB action.

def generatedRegretAction {Omega : Type} {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta margin : 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 measurable_generatedRegretAction {Omega : Type} [MeasurableSpace Omega] {K : Nat} (hK : 0 < K) (sigma2 : NNReal) (delta margin : Real) (defaultAction : Fin K) (reward : Omega -> RewardTrace Rat) (hreward : forall t : Nat, Measurable (fun omega : Omega => reward omega t)) (t : Nat) : Measurable (fun omega => generatedRegretAction hK sigma2 delta margin defaultAction reward omega t)

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

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

Finite-time expected pseudo-regret of the actual generated KL-UCB policy. The `T * delta` failure-event term is explicit; this theorem makes no asymptotic-optimality or leading-constant claim.

theorem lintegral_ofReal_pseudoRegret_generatedKLUCBBounded_le {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 margin : Real) (hdelta : 0 < delta) (hmargin0 : 0 < margin) (hmarginHalf : margin <= 1 / 2) (hmean : forall arm : Fin K, (model.mean arm : Real) ∈ Set.Icc margin (1 - margin)) (hraw : ∀ᵐ omega ∂mu, forall i, (((reward omega i : Rat) : Real)) ∈ Set.Icc (0 : Real) 1) (defaultAction : Fin K) (T : Nat) (hconfidence : mu (ConditionalExpectationReward.successorArmEmpiricalMeanFintypeTelescopingAllTimeBadEvent (generatedAction model.hK sigma2 delta margin defaultAction reward) reward model.mean sigma2 delta) <= ENNReal.ofReal delta) : ∫⁻ omega, ENNReal.ofReal (((pseudoRegret model (generatedRegretAction model.hK sigma2 delta margin defaultAction reward omega) T : Rat) : Real)) ∂mu <= (Finset.univ : Finset (Fin K)).sum (fun arm => ENNReal.ofReal (((model.gap arm : Rat) : Real)) * ((pullThreshold K sigma2 T delta margin (((model.gap arm : Rat) : Real)) : Nat) : ENNReal) + ENNReal.ofReal (((model.gap arm : Rat) : Real)) * ((T : ENNReal) * ENNReal.ofReal delta))

One good generated sample controls every finite horizon and positive-gap arm for the same KL-UCB policy.

theorem allHorizonPullCount_of_not_badEvent {Omega : Type} {K : Nat} (hK : 0 < K) (reward : Omega -> RewardTrace Rat) (armMean : Fin K -> Rat) (sigma2 : NNReal) (delta margin : Real) (hdelta : 0 < delta) (hmargin0 : 0 < margin) (hmarginHalf : margin <= 1 / 2) (hmean : forall arm : Fin K, (armMean arm : Real) ∈ Set.Icc margin (1 - margin)) (defaultAction best : Fin K) (omega : Omega) (hraw : forall i : Nat, (((reward omega i : Rat) : Real)) ∈ Set.Icc (0 : Real) 1) (hbest : forall arm : Fin K, (armMean arm : Real) <= (armMean best : Real)) (hgood : omega ∉ ConditionalExpectationReward.successorArmEmpiricalMeanFintypeTelescopingAllTimeBadEvent (generatedAction hK sigma2 delta margin defaultAction reward) reward armMean sigma2 delta) : forall T : Nat, forall chosen : Fin K, 0 < UCB.meanGap (fun arm => (armMean arm : Real)) best chosen -> ConditionalExpectationReward.successorArmPullCount (generatedAction hK sigma2 delta margin defaultAction reward omega) chosen (T + 1) <= pullThreshold K sigma2 T delta margin (UCB.meanGap (fun arm => (armMean arm : Real)) best chosen)

Canonical action/reward trajectory measure of the KL-UCB policy.

def actionRewardTrajMeasure {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 margin : Real) (defaultAction : Fin K) : Measure (Nat -> Prod (Fin K) Rat)

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

theorem measure_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 margin : 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) ((historyPolicy hK sigma2 delta margin defaultAction i).action (historyState hK sigma2 delta margin 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 := actionRewardTrajMeasure hK mu0 rewardKernel context hcontext sigma2 delta margin defaultAction let reward : (Nat -> Prod (Fin K) Rat) -> RewardTrace Rat := fun trajectory t => (trajectory t).2 let action := generatedAction hK sigma2 delta margin defaultAction reward mu (ConditionalExpectationReward.successorArmEmpiricalMeanFintypeTelescopingAllTimeBadEvent action reward armMean sigma2 delta) <= ENNReal.ofReal delta

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

theorem measure_generatedKLAllTimeBadEvent_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 margin : Real) (hmargin0 : 0 < margin) (hmarginHalf : margin <= 1 / 2) (harmMargin : forall arm : Fin K, (armMean arm : Real) ∈ Set.Icc margin (1 - margin)) (hcontext : forall n : Nat, Measurable (context n)) (hraw : ∀ᵐ trajectory ∂(actionRewardTrajMeasure hK mu0 rewardKernel context hcontext sigma2 delta margin defaultAction), forall i : Nat, ((((trajectory i).2 : Rat) : Real)) ∈ Set.Icc (0 : Real) 1) (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) ((historyPolicy hK sigma2 delta margin defaultAction i).action (historyState hK sigma2 delta margin 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 := actionRewardTrajMeasure hK mu0 rewardKernel context hcontext sigma2 delta margin defaultAction let reward : (Nat -> Prod (Fin K) Rat) -> RewardTrace Rat := fun trajectory t => (trajectory t).2 let action := generatedAction hK sigma2 delta margin defaultAction reward mu (generatedKLAllTimeBadEvent action reward armMean sigma2 delta margin) <= ENNReal.ofReal delta

Canonical generated-policy KL-UCB regret theorem on the very trajectory measure built from the same measurable KL policy and reward kernel.

theorem lintegral_ofReal_pseudoRegret_generatedKLUCBBounded_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 margin : Real) (T : Nat) (hdelta : 0 < delta) (hmargin0 : 0 < margin) (hmarginHalf : margin <= 1 / 2) (harmMargin : forall arm : Fin K, (model.mean arm : Real) ∈ Set.Icc margin (1 - margin)) (hcontext : forall n : Nat, Measurable (context n)) (hraw : ∀ᵐ trajectory ∂(actionRewardTrajMeasure model.hK mu0 rewardKernel context hcontext sigma2 delta margin defaultAction), forall i : Nat, ((((trajectory i).2 : Rat) : Real)) ∈ Set.Icc (0 : Real) 1) (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) ((historyPolicy model.hK sigma2 delta margin defaultAction i).action (historyState model.hK sigma2 delta margin 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))) : let mu := actionRewardTrajMeasure model.hK mu0 rewardKernel context hcontext sigma2 delta margin defaultAction let reward : (Nat -> Prod (Fin K) Rat) -> RewardTrace Rat := fun trajectory t => (trajectory t).2 let action := generatedRegretAction model.hK sigma2 delta margin 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)) * ((pullThreshold K sigma2 T delta margin (((model.gap arm : Rat) : Real)) : Nat) : ENNReal) + ENNReal.ofReal (((model.gap arm : Rat) : Real)) * ((T : ENNReal) * ENNReal.ofReal delta))

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

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