BanditRLProof.Algorithms.ThompsonStationaryReward

Uniform random table used to represent all stationary reward-kernel draws.

abbrev UnitArmStream (K : Nat)

Independent uniform coordinates indexed by pull number and arm.

noncomputable def uniformUnitArmStreamMeasure (K : Nat) : Measure (UnitArmStream K)

A fixed measurable uniform-randomness representation of a reward kernel.

noncomputable def stationaryRewardSampler {Env : Type u} {K : Nat} [MeasurableSpace Env] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] : (Env × Fin K) -> Set.Icc (0 : Real) 1 -> Real

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

theorem measurable_uncurry_stationaryRewardSampler {Env : Type u} {K : Nat} [MeasurableSpace Env] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] : Measurable (Function.uncurry (stationaryRewardSampler rewardKernel))

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

theorem stationaryRewardSampler_map_volume {Env : Type u} {K : Nat} [MeasurableSpace Env] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (input : Env × Fin K) : Measure.map (stationaryRewardSampler rewardKernel input) volume = rewardKernel input

Turn one environment and one uniform table into its latent reward table.

noncomputable def rewardStreamOfUnitArmStream {Env : Type u} {K : Nat} [MeasurableSpace Env] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] : Env × UnitArmStream K -> UCB.ArmRewardStream K

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

theorem measurable_rewardStreamOfUnitArmStream {Env : Type u} {K : Nat} [MeasurableSpace Env] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] : Measurable (rewardStreamOfUnitArmStream rewardKernel)

The arm-indexed reward kernel obtained by freezing the environment.

noncomputable def stationaryRewardKernelAt {Env : Type u} {K : Nat} [MeasurableSpace Env] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (env : Env) : Kernel (Fin K) Real

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

theorem stationaryRewardKernelAt_apply {Env : Type u} {K : Nat} [MeasurableSpace Env] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (env : Env) (arm : Fin K) : stationaryRewardKernelAt rewardKernel env arm = rewardKernel (env, arm)

Markov kernel that samples an independent latent reward stream at each environment.

noncomputable def stationaryArmStreamKernel {Env : Type u} {K : Nat} [MeasurableSpace Env] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] : Kernel Env (UCB.ArmRewardStream K)

At a fixed environment, the sampled latent table has the canonical product arm-stream law.

theorem stationaryArmStreamKernel_apply {Env : Type u} {K : Nat} [MeasurableSpace Env] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (env : Env) : stationaryArmStreamKernel rewardKernel env = UCB.armStreamMeasure (stationaryRewardKernelAt rewardKernel env)

A stationary reward kernel is a measurable history environment that ignores history.

noncomputable def stationaryMeasurableHistoryEnvironment {Env : Type u} {K : Nat} [MeasurableSpace Env] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] : MeasurableHistoryEnvironment Env (Fin K) Real where

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

theorem stationaryMeasurableHistoryEnvironment_initialFeedback {Env : Type u} {K : Nat} [MeasurableSpace Env] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] : (stationaryMeasurableHistoryEnvironment rewardKernel).initialFeedback = rewardKernel

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

theorem stationaryMeasurableHistoryEnvironment_feedback_apply {Env : Type u} {K : Nat} [MeasurableSpace Env] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (n : Nat) (env : Env) (history : History.FinitePairHistory (Fin K) Real n) (arm : Fin K) : (stationaryMeasurableHistoryEnvironment rewardKernel).feedback n (env, (history, arm)) = rewardKernel (env, arm)

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

theorem stationaryMeasurableHistoryEnvironment_at_initialFeedback_apply {Env : Type u} {K : Nat} [MeasurableSpace Env] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (env : Env) (arm : Fin K) : ((stationaryMeasurableHistoryEnvironment rewardKernel).at env).initialFeedback arm = rewardKernel (env, arm)

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

theorem stationaryMeasurableHistoryEnvironment_at_feedback_apply {Env : Type u} {K : Nat} [MeasurableSpace Env] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (env : Env) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (arm : Fin K) : ((stationaryMeasurableHistoryEnvironment rewardKernel).at env).feedback n (history, arm) = rewardKernel (env, arm)

Initial reward read from coordinate zero of the selected latent arm.

def latentArmStreamInitialReward {Env : Type u} {K : Nat} : ((Env × UCB.ArmRewardStream K) × Fin K) → Real

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

theorem measurable_latentArmStreamInitialReward {Env : Type u} {K : Nat} [MeasurableSpace Env] : Measurable (latentArmStreamInitialReward (Env

Next unused reward coordinate determined by the visible finite history.

noncomputable def latentArmStreamNextReward {Env : Type u} {K : Nat} (n : Nat) : ((Env × UCB.ArmRewardStream K) × (History.FinitePairHistory (Fin K) Real n × Fin K)) → Real

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

theorem measurable_latentArmStreamNextReward {Env : Type u} {K : Nat} [MeasurableSpace Env] (n : Nat) : Measurable (latentArmStreamNextReward (Env

Measurable deterministic feedback environment that exposes a latent reward table through the next-unused-coordinate rule. The first environment component is retained for the Bayesian model but does not affect feedback.

noncomputable def latentArmStreamMeasurableHistoryEnvironment {Env : Type u} {K : Nat} [MeasurableSpace Env] : MeasurableHistoryEnvironment (Env × UCB.ArmRewardStream K) (Fin K) Real where

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

theorem latentArmStreamMeasurableHistoryEnvironment_initialFeedback_apply {Env : Type u} {K : Nat} [MeasurableSpace Env] (env : Env) (stream : UCB.ArmRewardStream K) (arm : Fin K) : (latentArmStreamMeasurableHistoryEnvironment (Env

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

theorem latentArmStreamMeasurableHistoryEnvironment_feedback_apply {Env : Type u} {K : Nat} [MeasurableSpace Env] (n : Nat) (env : Env) (stream : UCB.ArmRewardStream K) (history : History.FinitePairHistory (Fin K) Real n) (arm : Fin K) : (latentArmStreamMeasurableHistoryEnvironment (Env

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

theorem measurable_latentArmStreamNextReward_fixed {Env : Type u} {K : Nat} [MeasurableSpace Env] (n : Nat) (env : Env) (stream : UCB.ArmRewardStream K) : Measurable (fun input : History.FinitePairHistory (Fin K) Real n × Fin K => stream (ETC.realHistoryPullCount n input.1 input.2) input.2)

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

theorem latentArmStreamMeasurableHistoryEnvironment_at_initialFeedback_apply {Env : Type u} {K : Nat} [MeasurableSpace Env] (env : Env) (stream : UCB.ArmRewardStream K) (arm : Fin K) : ((latentArmStreamMeasurableHistoryEnvironment (Env

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

theorem latentArmStreamMeasurableHistoryEnvironment_at_feedback_apply {Env : Type u} {K : Nat} [MeasurableSpace Env] (n : Nat) (env : Env) (stream : UCB.ArmRewardStream K) (history : History.FinitePairHistory (Fin K) Real n) (arm : Fin K) : ((latentArmStreamMeasurableHistoryEnvironment (Env

The initial canonical reward reads coordinate zero of the selected arm.

theorem canonicalLatentArmStreamTrajectory_reward_zero_ae {Env : Type u} {K : Nat} [MeasurableSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (stream : UCB.ArmRewardStream K) : ∀ᵐ trajectory ∂ canonicalMeasurableEnvironmentTrajectoryKernel algorithm (latentArmStreamMeasurableHistoryEnvironment (Env

Every shifted canonical reward reads the selected arm's next unused coordinate.

theorem canonicalLatentArmStreamTrajectory_reward_succ_ae {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (stream : UCB.ArmRewardStream K) (n : Nat) : ∀ᵐ trajectory ∂ canonicalMeasurableEnvironmentTrajectoryKernel algorithm (latentArmStreamMeasurableHistoryEnvironment (Env

The canonical trajectory under deterministic latent-stream feedback has the same reward trace as the pathwise next-unused-coordinate construction.

theorem canonicalLatentArmStreamTrajectory_reward_eq_rewardFromArmStream_ae {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (stream : UCB.ArmRewardStream K) : canonicalHistoryTrajectoryReward =ᵐ[ canonicalMeasurableEnvironmentTrajectoryKernel algorithm (latentArmStreamMeasurableHistoryEnvironment (Env

A next-unused arm-stream reward coordinate is measurable at each time.

theorem measurable_rewardFromArmStream_apply {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (action : Omega -> ActionTrace (Fin K)) (haction : forall t, Measurable (fun omega => action omega t)) (armStream : Omega -> ArmRewardStream K) (hmeasurable : forall i arm, Measurable (fun omega => armStream omega i arm)) (t : Nat) : Measurable (fun omega => rewardFromArmStream action armStream omega t)

Adaptive-count upper tail on any sample space whose latent-stream projection has the canonical stationary product law. The action trace may use additional algorithmic randomness carried by the sample space.

theorem measure_sumRewards_sub_pullCount_mul_ge_le_of_armStream_identDistrib {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (action : Omega -> ActionTrace (Fin K)) (armStream : Omega -> ArmRewardStream K) (hmeasurable : forall i arm, Measurable (fun omega => armStream omega i arm)) (hstreamLaw : IdentDistrib armStream id mu (armStreamMeasure nu)) (arm : Fin K) (mean : Real) (sigma2 : NNReal) (hsubG : HasSubgaussianMGF (fun reward => reward - mean) sigma2 (nu arm)) (n : Nat) (threshold : Nat -> Real) (hthreshold : forall k, k <= n -> 0 <= threshold k) : mu {omega : Omega | threshold (pullCount (action omega) arm n) <= sumRewards (action omega) (rewardFromArmStream action armStream omega) arm n - (pullCount (action omega) arm n : Real) * mean} <= (Finset.range (n + 1)).sum (fun k => ENNReal.ofReal (Real.exp (-(threshold k) ^ 2 / (2 * (k : Real) * (sigma2 : Real)))))

Lower-tail counterpart of the arbitrary-sample latent-stream transport.

theorem measure_pullCount_mul_sub_sumRewards_ge_le_of_armStream_identDistrib {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (action : Omega -> ActionTrace (Fin K)) (armStream : Omega -> ArmRewardStream K) (hmeasurable : forall i arm, Measurable (fun omega => armStream omega i arm)) (hstreamLaw : IdentDistrib armStream id mu (armStreamMeasure nu)) (arm : Fin K) (mean : Real) (sigma2 : NNReal) (hsubG : HasSubgaussianMGF (fun reward => reward - mean) sigma2 (nu arm)) (n : Nat) (threshold : Nat -> Real) (hthreshold : forall k, k <= n -> 0 <= threshold k) : mu {omega : Omega | threshold (pullCount (action omega) arm n) <= (pullCount (action omega) arm n : Real) * mean - sumRewards (action omega) (rewardFromArmStream action armStream omega) arm n} <= (Finset.range (n + 1)).sum (fun k => ENNReal.ofReal (Real.exp (-(threshold k) ^ 2 / (2 * (k : Real) * (sigma2 : Real)))))

Positive-count upper tail under an arbitrary algorithmic-randomness coupling.

theorem measure_pos_and_sumRewards_sub_pullCount_mul_ge_le_of_armStream_identDistrib {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (action : Omega -> ActionTrace (Fin K)) (armStream : Omega -> ArmRewardStream K) (hmeasurable : forall i arm, Measurable (fun omega => armStream omega i arm)) (hstreamLaw : IdentDistrib armStream id mu (armStreamMeasure nu)) (arm : Fin K) (mean : Real) (sigma2 : NNReal) (hsubG : HasSubgaussianMGF (fun reward => reward - mean) sigma2 (nu arm)) (n : Nat) (threshold : Nat -> Real) (hthreshold : forall k, 0 < k -> k <= n -> 0 <= threshold k) : mu {omega : Omega | 0 < pullCount (action omega) arm n ∧ threshold (pullCount (action omega) arm n) <= sumRewards (action omega) (rewardFromArmStream action armStream omega) arm n - (pullCount (action omega) arm n : Real) * mean} <= ((Finset.range (n + 1)).filter (fun k => 0 < k)).sum (fun k => ENNReal.ofReal (Real.exp (-(threshold k) ^ 2 / (2 * (k : Real) * (sigma2 : Real)))))

Positive-count lower tail under an arbitrary algorithmic-randomness coupling.

theorem measure_pos_and_pullCount_mul_sub_sumRewards_ge_le_of_armStream_identDistrib {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (action : Omega -> ActionTrace (Fin K)) (armStream : Omega -> ArmRewardStream K) (hmeasurable : forall i arm, Measurable (fun omega => armStream omega i arm)) (hstreamLaw : IdentDistrib armStream id mu (armStreamMeasure nu)) (arm : Fin K) (mean : Real) (sigma2 : NNReal) (hsubG : HasSubgaussianMGF (fun reward => reward - mean) sigma2 (nu arm)) (n : Nat) (threshold : Nat -> Real) (hthreshold : forall k, 0 < k -> k <= n -> 0 <= threshold k) : mu {omega : Omega | 0 < pullCount (action omega) arm n ∧ threshold (pullCount (action omega) arm n) <= (pullCount (action omega) arm n : Real) * mean - sumRewards (action omega) (rewardFromArmStream action armStream omega) arm n} <= ((Finset.range (n + 1)).filter (fun k => 0 < k)).sum (fun k => ENNReal.ofReal (Real.exp (-(threshold k) ^ 2 / (2 * (k : Real) * (sigma2 : Real)))))

Adaptive-count upper tail for any action trace driven by a canonical latent arm stream. No UCB action rule is used.

theorem measure_sumRewards_sub_pullCount_mul_ge_le_of_canonicalArmStream {K : Nat} (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (action : ArmRewardStream K -> ActionTrace (Fin K)) (arm : Fin K) (mean : Real) (sigma2 : NNReal) (hsubG : HasSubgaussianMGF (fun reward => reward - mean) sigma2 (nu arm)) (n : Nat) (threshold : Nat -> Real) (hthreshold : forall k, k <= n -> 0 <= threshold k) : armStreamMeasure nu {stream : ArmRewardStream K | threshold (pullCount (action stream) arm n) <= sumRewards (action stream) (rewardFromArmStream action id stream) arm n - (pullCount (action stream) arm n : Real) * mean} <= (Finset.range (n + 1)).sum (fun k => ENNReal.ofReal (Real.exp (-(threshold k) ^ 2 / (2 * (k : Real) * (sigma2 : Real)))))

Adaptive-count lower tail for any action trace driven by a canonical latent arm stream. No UCB action rule is used.

theorem measure_pullCount_mul_sub_sumRewards_ge_le_of_canonicalArmStream {K : Nat} (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (action : ArmRewardStream K -> ActionTrace (Fin K)) (arm : Fin K) (mean : Real) (sigma2 : NNReal) (hsubG : HasSubgaussianMGF (fun reward => reward - mean) sigma2 (nu arm)) (n : Nat) (threshold : Nat -> Real) (hthreshold : forall k, k <= n -> 0 <= threshold k) : armStreamMeasure nu {stream : ArmRewardStream K | threshold (pullCount (action stream) arm n) <= (pullCount (action stream) arm n : Real) * mean - sumRewards (action stream) (rewardFromArmStream action id stream) arm n} <= (Finset.range (n + 1)).sum (fun k => ENNReal.ofReal (Real.exp (-(threshold k) ^ 2 / (2 * (k : Real) * (sigma2 : Real)))))

Canonical trajectory kernel after freezing the non-stream environment.

noncomputable def latentArmStreamTrajectoryKernel {Env : Type u} {K : Nat} [MeasurableSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) : Kernel (UCB.ArmRewardStream K) ((n : Nat) -> Fin K × Real)

Joint law of a stationary latent arm stream and its generated trajectory.

noncomputable def latentArmStreamTrajectoryMeasure {Env : Type u} {K : Nat} [MeasurableSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] : Measure (UCB.ArmRewardStream K × ((n : Nat) -> Fin K × Real))

Action trace projected from the trajectory coordinate of the coupling.

def latentArmStreamTrajectoryAction {K : Nat} : (UCB.ArmRewardStream K × ((n : Nat) -> Fin K × Real)) -> ActionTrace (Fin K)

Reward trace projected from the trajectory coordinate of the coupling.

def latentArmStreamTrajectoryReward {K : Nat} : (UCB.ArmRewardStream K × ((n : Nat) -> Fin K × Real)) -> RewardTrace Real

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

theorem measurable_latentArmStreamTrajectoryAction_apply {K : Nat} (t : Nat) : Measurable (fun sample : UCB.ArmRewardStream K × ((n : Nat) -> Fin K × Real) => latentArmStreamTrajectoryAction sample t)

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

theorem measurable_latentArmStreamTrajectoryReward_apply {K : Nat} (t : Nat) : Measurable (fun sample : UCB.ArmRewardStream K × ((n : Nat) -> Fin K × Real) => latentArmStreamTrajectoryReward sample t)

Pull counts remain measurable when the queried arm is sample-dependent.

theorem measurable_pullCount_selectedArm {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (action : Omega -> ActionTrace (Fin K)) (haction : forall t, Measurable (fun omega => action omega t)) (arm : Omega -> Fin K) (harm : Measurable arm) (n : Nat) : Measurable (fun omega => pullCount (action omega) (arm omega) n)

Selected-arm reward sums are measurable for a measurable arm selector.

theorem measurable_sumRewards_selectedArm {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) (haction : forall t, Measurable (fun omega => action omega t)) (hreward : forall t, Measurable (fun omega => reward omega t)) (arm : Omega -> Fin K) (harm : Measurable arm) (n : Nat) : Measurable (fun omega => sumRewards (action omega) (reward omega) (arm omega) n)

The real empirical mean is measurable for a measurable arm selector.

theorem measurable_realEmpiricalMean_selectedArm {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) (haction : forall t, Measurable (fun omega => action omega t)) (hreward : forall t, Measurable (fun omega => reward omega t)) (arm : Omega -> Fin K) (harm : Measurable arm) (n : Nat) : Measurable (fun omega => UCB.realEmpiricalMean (action omega) (reward omega) (arm omega) n)

The stream coordinate of the coupling has exactly the canonical stream law.

theorem identDistrib_fst_latentArmStreamTrajectoryMeasure {Env : Type u} {K : Nat} [MeasurableSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] : IdentDistrib Prod.fst id (latentArmStreamTrajectoryMeasure algorithm env nu) (UCB.armStreamMeasure nu) where

The joint coupling reads its actual rewards from its own latent stream.

theorem latentArmStreamTrajectoryReward_eq_rewardFromArmStream_ae {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] : latentArmStreamTrajectoryReward =ᵐ[ latentArmStreamTrajectoryMeasure algorithm env nu] UCB.rewardFromArmStream latentArmStreamTrajectoryAction Prod.fst

Upper adaptive-count tail for rewards on the coupled Thompson trajectory.

theorem measure_latentArmStreamTrajectory_sumRewards_sub_pullCount_mul_ge_le {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (arm : Fin K) (mean : Real) (sigma2 : NNReal) (hsubG : HasSubgaussianMGF (fun reward => reward - mean) sigma2 (nu arm)) (n : Nat) (threshold : Nat -> Real) (hthreshold : forall k, k <= n -> 0 <= threshold k) : latentArmStreamTrajectoryMeasure algorithm env nu {sample | threshold (pullCount (latentArmStreamTrajectoryAction sample) arm n) <= sumRewards (latentArmStreamTrajectoryAction sample) (latentArmStreamTrajectoryReward sample) arm n - (pullCount (latentArmStreamTrajectoryAction sample) arm n : Real) * mean} <= (Finset.range (n + 1)).sum (fun k => ENNReal.ofReal (Real.exp (-(threshold k) ^ 2 / (2 * (k : Real) * (sigma2 : Real)))))

Lower adaptive-count tail for rewards on the coupled Thompson trajectory.

theorem measure_latentArmStreamTrajectory_pullCount_mul_sub_sumRewards_ge_le {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (arm : Fin K) (mean : Real) (sigma2 : NNReal) (hsubG : HasSubgaussianMGF (fun reward => reward - mean) sigma2 (nu arm)) (n : Nat) (threshold : Nat -> Real) (hthreshold : forall k, k <= n -> 0 <= threshold k) : latentArmStreamTrajectoryMeasure algorithm env nu {sample | threshold (pullCount (latentArmStreamTrajectoryAction sample) arm n) <= (pullCount (latentArmStreamTrajectoryAction sample) arm n : Real) * mean - sumRewards (latentArmStreamTrajectoryAction sample) (latentArmStreamTrajectoryReward sample) arm n} <= (Finset.range (n + 1)).sum (fun k => ENNReal.ofReal (Real.exp (-(threshold k) ^ 2 / (2 * (k : Real) * (sigma2 : Real)))))

Positive-count upper tail for rewards on the coupled trajectory.

theorem measure_latentArmStreamTrajectory_pos_and_sumRewards_sub_pullCount_mul_ge_le {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (arm : Fin K) (mean : Real) (sigma2 : NNReal) (hsubG : HasSubgaussianMGF (fun reward => reward - mean) sigma2 (nu arm)) (n : Nat) (threshold : Nat -> Real) (hthreshold : forall k, 0 < k -> k <= n -> 0 <= threshold k) : latentArmStreamTrajectoryMeasure algorithm env nu {sample | 0 < pullCount (latentArmStreamTrajectoryAction sample) arm n ∧ threshold (pullCount (latentArmStreamTrajectoryAction sample) arm n) <= sumRewards (latentArmStreamTrajectoryAction sample) (latentArmStreamTrajectoryReward sample) arm n - (pullCount (latentArmStreamTrajectoryAction sample) arm n : Real) * mean} <= ((Finset.range (n + 1)).filter (fun k => 0 < k)).sum (fun k => ENNReal.ofReal (Real.exp (-(threshold k) ^ 2 / (2 * (k : Real) * (sigma2 : Real)))))

Positive-count lower tail for rewards on the coupled trajectory.

theorem measure_latentArmStreamTrajectory_pos_and_pullCount_mul_sub_sumRewards_ge_le {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (arm : Fin K) (mean : Real) (sigma2 : NNReal) (hsubG : HasSubgaussianMGF (fun reward => reward - mean) sigma2 (nu arm)) (n : Nat) (threshold : Nat -> Real) (hthreshold : forall k, 0 < k -> k <= n -> 0 <= threshold k) : latentArmStreamTrajectoryMeasure algorithm env nu {sample | 0 < pullCount (latentArmStreamTrajectoryAction sample) arm n ∧ threshold (pullCount (latentArmStreamTrajectoryAction sample) arm n) <= (pullCount (latentArmStreamTrajectoryAction sample) arm n : Real) * mean - sumRewards (latentArmStreamTrajectoryAction sample) (latentArmStreamTrajectoryReward sample) arm n} <= ((Finset.range (n + 1)).filter (fun k => 0 < k)).sum (fun k => ENNReal.ofReal (Real.exp (-(threshold k) ^ 2 / (2 * (k : Real) * (sigma2 : Real)))))

Environment-indexed kernel that samples the stationary latent stream and then runs the actual history algorithm against next-unused deterministic feedback.

noncomputable def stationaryLatentArmStreamTrajectoryKernel {Env : Type u} {K : Nat} [MeasurableSpace Env] [NeZero K] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (algorithm : HistoryAlgorithm (Fin K) Real) : Kernel Env (UCB.ArmRewardStream K × ((n : Nat) -> Fin K × Real))

Its conditional law is exactly the fixed-environment coupling above.

theorem stationaryLatentArmStreamTrajectoryKernel_apply {Env : Type u} {K : Nat} [MeasurableSpace Env] [NeZero K] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) : stationaryLatentArmStreamTrajectoryKernel rewardKernel algorithm env = latentArmStreamTrajectoryMeasure algorithm env (stationaryRewardKernelAt rewardKernel env)

Pointwise upper tail for the actual augmented Thompson trajectory kernel.

theorem stationaryLatentArmStreamTrajectoryKernel_sumRewards_upper_tail {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (algorithm : HistoryAlgorithm (Fin K) Real) (mean : Env -> Fin K -> Real) (sigma2 : NNReal) (hsubG : forall env arm, HasSubgaussianMGF (fun reward => reward - mean env arm) sigma2 (rewardKernel (env, arm))) (env : Env) (arm : Fin K) (n : Nat) (threshold : Nat -> Real) (hthreshold : forall k, k <= n -> 0 <= threshold k) : stationaryLatentArmStreamTrajectoryKernel rewardKernel algorithm env {sample | threshold (pullCount (latentArmStreamTrajectoryAction sample) arm n) <= sumRewards (latentArmStreamTrajectoryAction sample) (latentArmStreamTrajectoryReward sample) arm n - (pullCount (latentArmStreamTrajectoryAction sample) arm n : Real) * mean env arm} <= (Finset.range (n + 1)).sum (fun k => ENNReal.ofReal (Real.exp (-(threshold k) ^ 2 / (2 * (k : Real) * (sigma2 : Real)))))

Pointwise lower tail for the actual augmented Thompson trajectory kernel.

theorem stationaryLatentArmStreamTrajectoryKernel_sumRewards_lower_tail {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (algorithm : HistoryAlgorithm (Fin K) Real) (mean : Env -> Fin K -> Real) (sigma2 : NNReal) (hsubG : forall env arm, HasSubgaussianMGF (fun reward => reward - mean env arm) sigma2 (rewardKernel (env, arm))) (env : Env) (arm : Fin K) (n : Nat) (threshold : Nat -> Real) (hthreshold : forall k, k <= n -> 0 <= threshold k) : stationaryLatentArmStreamTrajectoryKernel rewardKernel algorithm env {sample | threshold (pullCount (latentArmStreamTrajectoryAction sample) arm n) <= (pullCount (latentArmStreamTrajectoryAction sample) arm n : Real) * mean env arm - sumRewards (latentArmStreamTrajectoryAction sample) (latentArmStreamTrajectoryReward sample) arm n} <= (Finset.range (n + 1)).sum (fun k => ENNReal.ofReal (Real.exp (-(threshold k) ^ 2 / (2 * (k : Real) * (sigma2 : Real)))))

Positive-count upper tail for the environment-indexed augmented kernel.

theorem stationaryLatentArmStreamTrajectoryKernel_pos_and_sumRewards_upper_tail {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (algorithm : HistoryAlgorithm (Fin K) Real) (mean : Env -> Fin K -> Real) (sigma2 : NNReal) (hsubG : forall env arm, HasSubgaussianMGF (fun reward => reward - mean env arm) sigma2 (rewardKernel (env, arm))) (env : Env) (arm : Fin K) (n : Nat) (threshold : Nat -> Real) (hthreshold : forall k, 0 < k -> k <= n -> 0 <= threshold k) : stationaryLatentArmStreamTrajectoryKernel rewardKernel algorithm env {sample | 0 < pullCount (latentArmStreamTrajectoryAction sample) arm n ∧ threshold (pullCount (latentArmStreamTrajectoryAction sample) arm n) <= sumRewards (latentArmStreamTrajectoryAction sample) (latentArmStreamTrajectoryReward sample) arm n - (pullCount (latentArmStreamTrajectoryAction sample) arm n : Real) * mean env arm} <= ((Finset.range (n + 1)).filter (fun k => 0 < k)).sum (fun k => ENNReal.ofReal (Real.exp (-(threshold k) ^ 2 / (2 * (k : Real) * (sigma2 : Real)))))

Positive-count lower tail for the environment-indexed augmented kernel.

theorem stationaryLatentArmStreamTrajectoryKernel_pos_and_sumRewards_lower_tail {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (algorithm : HistoryAlgorithm (Fin K) Real) (mean : Env -> Fin K -> Real) (sigma2 : NNReal) (hsubG : forall env arm, HasSubgaussianMGF (fun reward => reward - mean env arm) sigma2 (rewardKernel (env, arm))) (env : Env) (arm : Fin K) (n : Nat) (threshold : Nat -> Real) (hthreshold : forall k, 0 < k -> k <= n -> 0 <= threshold k) : stationaryLatentArmStreamTrajectoryKernel rewardKernel algorithm env {sample | 0 < pullCount (latentArmStreamTrajectoryAction sample) arm n ∧ threshold (pullCount (latentArmStreamTrajectoryAction sample) arm n) <= (pullCount (latentArmStreamTrajectoryAction sample) arm n : Real) * mean env arm - sumRewards (latentArmStreamTrajectoryAction sample) (latentArmStreamTrajectoryReward sample) arm n} <= ((Finset.range (n + 1)).filter (fun k => 0 < k)).sum (fun k => ENNReal.ofReal (Real.exp (-(threshold k) ^ 2 / (2 * (k : Real) * (sigma2 : Real)))))

Environment coordinate of the stationary augmented trajectory sample.

def stationaryLatentArmStreamTrajectoryEnvironment {Env : Type u} {K : Nat} : (Env × (UCB.ArmRewardStream K × ((n : Nat) -> Fin K × Real))) -> Env

Action trace of the stationary augmented trajectory sample.

def stationaryLatentArmStreamTrajectoryAction {Env : Type u} {K : Nat} : (Env × (UCB.ArmRewardStream K × ((n : Nat) -> Fin K × Real))) -> ActionTrace (Fin K)

Reward trace of the stationary augmented trajectory sample.

def stationaryLatentArmStreamTrajectoryReward {Env : Type u} {K : Nat} : (Env × (UCB.ArmRewardStream K × ((n : Nat) -> Fin K × Real))) -> RewardTrace Real

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

theorem measurable_stationaryLatentArmStreamTrajectoryEnvironment {Env : Type u} {K : Nat} [MeasurableSpace Env] : Measurable (stationaryLatentArmStreamTrajectoryEnvironment (Env

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

theorem measurable_stationaryLatentArmStreamTrajectoryAction_apply {Env : Type u} {K : Nat} [MeasurableSpace Env] (t : Nat) : Measurable (fun sample : Env × (UCB.ArmRewardStream K × ((n : Nat) -> Fin K × Real)) => stationaryLatentArmStreamTrajectoryAction sample t)

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

theorem measurable_stationaryLatentArmStreamTrajectoryReward_apply {Env : Type u} {K : Nat} [MeasurableSpace Env] (t : Nat) : Measurable (fun sample : Env × (UCB.ArmRewardStream K × ((n : Nat) -> Fin K × Real)) => stationaryLatentArmStreamTrajectoryReward sample t)

Prior mixture of the stationary latent stream and its actual trajectory.

noncomputable def stationaryLatentArmStreamTrajectoryMeasure {Env : Type u} {K : Nat} [MeasurableSpace Env] [NeZero K] (prior : Measure Env) (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (algorithm : HistoryAlgorithm (Fin K) Real) : Measure (Env × (UCB.ArmRewardStream K × ((n : Nat) -> Fin K × Real)))

Upper fixed-arm adaptive-count tail after mixing the fixed-environment augmented trajectory through the environment prior.

theorem stationaryLatentArmStreamTrajectoryMeasure_sumRewards_upper_tail {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (prior : Measure Env) [IsProbabilityMeasure prior] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (algorithm : HistoryAlgorithm (Fin K) Real) (mean : Env -> Fin K -> Real) (hmeas_mean : Measurable (fun input : Env × Fin K => mean input.1 input.2)) (sigma2 : NNReal) (hsubG : forall env arm, HasSubgaussianMGF (fun reward => reward - mean env arm) sigma2 (rewardKernel (env, arm))) (arm : Fin K) (n : Nat) (threshold : Nat -> Real) (hthreshold : forall k, k <= n -> 0 <= threshold k) : stationaryLatentArmStreamTrajectoryMeasure prior rewardKernel algorithm {sample | threshold (pullCount (stationaryLatentArmStreamTrajectoryAction sample) arm n) <= sumRewards (stationaryLatentArmStreamTrajectoryAction sample) (stationaryLatentArmStreamTrajectoryReward sample) arm n - (pullCount (stationaryLatentArmStreamTrajectoryAction sample) arm n : Real) * mean (stationaryLatentArmStreamTrajectoryEnvironment sample) arm} <= (Finset.range (n + 1)).sum (fun k => ENNReal.ofReal (Real.exp (-(threshold k) ^ 2 / (2 * (k : Real) * (sigma2 : Real)))))

Lower-tail counterpart of the augmented-prior mixture theorem.

theorem stationaryLatentArmStreamTrajectoryMeasure_sumRewards_lower_tail {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (prior : Measure Env) [IsProbabilityMeasure prior] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (algorithm : HistoryAlgorithm (Fin K) Real) (mean : Env -> Fin K -> Real) (hmeas_mean : Measurable (fun input : Env × Fin K => mean input.1 input.2)) (sigma2 : NNReal) (hsubG : forall env arm, HasSubgaussianMGF (fun reward => reward - mean env arm) sigma2 (rewardKernel (env, arm))) (arm : Fin K) (n : Nat) (threshold : Nat -> Real) (hthreshold : forall k, k <= n -> 0 <= threshold k) : stationaryLatentArmStreamTrajectoryMeasure prior rewardKernel algorithm {sample | threshold (pullCount (stationaryLatentArmStreamTrajectoryAction sample) arm n) <= (pullCount (stationaryLatentArmStreamTrajectoryAction sample) arm n : Real) * mean (stationaryLatentArmStreamTrajectoryEnvironment sample) arm - sumRewards (stationaryLatentArmStreamTrajectoryAction sample) (stationaryLatentArmStreamTrajectoryReward sample) arm n} <= (Finset.range (n + 1)).sum (fun k => ENNReal.ofReal (Real.exp (-(threshold k) ^ 2 / (2 * (k : Real) * (sigma2 : Real)))))

Integrate a uniform pointwise kernel event bound through a probability prior.

theorem measure_compProd_le_of_forall_kernel_apply_le {Env : Type u} {Omega : Type v} [MeasurableSpace Env] [MeasurableSpace Omega] (prior : Measure Env) [IsProbabilityMeasure prior] (kernel : Kernel Env Omega) [IsMarkovKernel kernel] (event : Set (Env × Omega)) (hevent : MeasurableSet event) (bound : ENNReal) (hbound : forall env, kernel env (Prod.mk env ⁻¹' event) <= bound) : (prior ⊗ₘ kernel) event <= bound

Positive-count upper tail after mixing through the environment prior.

theorem stationaryLatentArmStreamTrajectoryMeasure_pos_and_sumRewards_upper_tail {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (prior : Measure Env) [IsProbabilityMeasure prior] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (algorithm : HistoryAlgorithm (Fin K) Real) (mean : Env -> Fin K -> Real) (hmeas_mean : Measurable (fun input : Env × Fin K => mean input.1 input.2)) (sigma2 : NNReal) (hsubG : forall env arm, HasSubgaussianMGF (fun reward => reward - mean env arm) sigma2 (rewardKernel (env, arm))) (arm : Fin K) (n : Nat) (threshold : Nat -> Real) (hthreshold : forall k, 0 < k -> k <= n -> 0 <= threshold k) : stationaryLatentArmStreamTrajectoryMeasure prior rewardKernel algorithm {sample | 0 < pullCount (stationaryLatentArmStreamTrajectoryAction sample) arm n ∧ threshold (pullCount (stationaryLatentArmStreamTrajectoryAction sample) arm n) <= sumRewards (stationaryLatentArmStreamTrajectoryAction sample) (stationaryLatentArmStreamTrajectoryReward sample) arm n - (pullCount (stationaryLatentArmStreamTrajectoryAction sample) arm n : Real) * mean (stationaryLatentArmStreamTrajectoryEnvironment sample) arm} <= ((Finset.range (n + 1)).filter (fun k => 0 < k)).sum (fun k => ENNReal.ofReal (Real.exp (-(threshold k) ^ 2 / (2 * (k : Real) * (sigma2 : Real)))))

Positive-count lower tail after mixing through the environment prior.

theorem stationaryLatentArmStreamTrajectoryMeasure_pos_and_sumRewards_lower_tail {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (prior : Measure Env) [IsProbabilityMeasure prior] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (algorithm : HistoryAlgorithm (Fin K) Real) (mean : Env -> Fin K -> Real) (hmeas_mean : Measurable (fun input : Env × Fin K => mean input.1 input.2)) (sigma2 : NNReal) (hsubG : forall env arm, HasSubgaussianMGF (fun reward => reward - mean env arm) sigma2 (rewardKernel (env, arm))) (arm : Fin K) (n : Nat) (threshold : Nat -> Real) (hthreshold : forall k, 0 < k -> k <= n -> 0 <= threshold k) : stationaryLatentArmStreamTrajectoryMeasure prior rewardKernel algorithm {sample | 0 < pullCount (stationaryLatentArmStreamTrajectoryAction sample) arm n ∧ threshold (pullCount (stationaryLatentArmStreamTrajectoryAction sample) arm n) <= (pullCount (stationaryLatentArmStreamTrajectoryAction sample) arm n : Real) * mean (stationaryLatentArmStreamTrajectoryEnvironment sample) arm - sumRewards (stationaryLatentArmStreamTrajectoryAction sample) (stationaryLatentArmStreamTrajectoryReward sample) arm n} <= ((Finset.range (n + 1)).filter (fun k => 0 < k)).sum (fun k => ENNReal.ofReal (Real.exp (-(threshold k) ^ 2 / (2 * (k : Real) * (sigma2 : Real)))))

Pull-count-scaled radius used by the clipped Thompson score.

noncomputable def clippedCountWidthThreshold (sigma2 : NNReal) (delta : Real) (k : Nat) : Real

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

theorem clippedCountWidthThreshold_nonneg (sigma2 : NNReal) (delta : Real) (k : Nat) : 0 <= clippedCountWidthThreshold sigma2 delta k

The clipped-score count threshold has the intended confidence exponent.

theorem clippedCountWidthThreshold_sq_div_eq (sigma2 : NNReal) (delta : Real) (k : Nat) (hsigma2 : sigma2 ≠ 0) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (hk : 0 < k) : (clippedCountWidthThreshold sigma2 delta k) ^ 2 / (2 * (k : Real) * (sigma2 : Real)) = Real.log (1 / delta)

The positive-count clipped-radius exponential sum is exactly `n * delta`.

theorem sum_clippedCountWidthThreshold_tail_eq (sigma2 : NNReal) (delta : Real) (n : Nat) (hsigma2 : sigma2 ≠ 0) (hdelta : 0 < delta) (hdelta_one : delta <= 1) : ((Finset.range (n + 1)).filter (fun k => 0 < k)).sum (fun k => ENNReal.ofReal (Real.exp (-(clippedCountWidthThreshold sigma2 delta k) ^ 2 / (2 * (k : Real) * (sigma2 : Real))))) = (n : ENNReal) * ENNReal.ofReal delta

A finite union of lower prefix deviations pays once per positive pull count.

theorem measure_biUnion_clippedCountWidthThreshold_le_mul_sub_armPrefixSum_le {K : Nat} (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (arm : Fin K) (mean : Real) (sigma2 : NNReal) (hsubG : HasSubgaussianMGF (fun reward => reward - mean) sigma2 (nu arm)) (hsigma2 : sigma2 ≠ 0) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (m : Nat) : UCB.armStreamMeasure nu (⋃ k ∈ Finset.Icc 1 m, {stream : UCB.ArmRewardStream K | clippedCountWidthThreshold sigma2 delta k <= (k : Real) * mean - UCB.armPrefixSum arm k stream}) <= (m : ENNReal) * ENNReal.ofReal delta

A clipped-score lower-confidence failure implies a lower sum deviation.

theorem clippedCountWidthThreshold_le_mul_mean_sub_sumRewards {K : Nat} (action : ActionTrace (Fin K)) (reward : RewardTrace Real) (arm : Fin K) (n : Nat) (mean : Real) (sigma2 : NNReal) (delta : Real) (hcount : 0 < pullCount action arm n) (hindex : UCB.realEmpiricalMean action reward arm n + Real.sqrt (2 * (sigma2 : Real) * Real.log (1 / delta) / (pullCount action arm n : Real)) <= mean) : clippedCountWidthThreshold sigma2 delta (pullCount action arm n) <= (pullCount action arm n : Real) * mean - sumRewards action reward arm n

A clipped-score upper-confidence failure implies an upper sum deviation.

theorem clippedCountWidthThreshold_le_sumRewards_sub_mul_mean {K : Nat} (action : ActionTrace (Fin K)) (reward : RewardTrace Real) (arm : Fin K) (n : Nat) (mean : Real) (sigma2 : NNReal) (delta : Real) (hcount : 0 < pullCount action arm n) (hindex : mean <= UCB.realEmpiricalMean action reward arm n - Real.sqrt (2 * (sigma2 : Real) * Real.log (1 / delta) / (pullCount action arm n : Real))) : clippedCountWidthThreshold sigma2 delta (pullCount action arm n) <= sumRewards action reward arm n - (pullCount action arm n : Real) * mean

Finite-horizon lower-confidence failure for one arm on the coupled trajectory. All times with the same realized pull count reduce to the same latent-stream prefix event, so the bound pays for `1, ..., n - 1` once rather than unioning the fixed-time bounds.

theorem measure_latentArmStreamTrajectory_exists_realEmpiricalMean_add_width_le_mean_le {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (arm : Fin K) (mean : Real) (sigma2 : NNReal) (hsubG : HasSubgaussianMGF (fun reward => reward - mean) sigma2 (nu arm)) (hsigma2 : sigma2 ≠ 0) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (n : Nat) : latentArmStreamTrajectoryMeasure algorithm env nu {sample | ∃ t < n, 0 < pullCount (latentArmStreamTrajectoryAction sample) arm t ∧ UCB.realEmpiricalMean (latentArmStreamTrajectoryAction sample) (latentArmStreamTrajectoryReward sample) arm t + Real.sqrt (2 * (sigma2 : Real) * Real.log (1 / delta) / (pullCount (latentArmStreamTrajectoryAction sample) arm t : Real)) <= mean} <= (n - 1 : Nat) * ENNReal.ofReal delta

Prior-mixed finite-horizon lower-confidence failure for an environment-dependent measurable arm selector.

theorem stationaryLatentArmStreamTrajectoryMeasure_exists_selectedArm_realEmpiricalMean_add_width_le_mean_le {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (prior : Measure Env) [IsProbabilityMeasure prior] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (algorithm : HistoryAlgorithm (Fin K) Real) (mean : Env -> Fin K -> Real) (hmeas_mean : Measurable (fun input : Env × Fin K => mean input.1 input.2)) (sigma2 : NNReal) (hsubG : forall env arm, HasSubgaussianMGF (fun reward => reward - mean env arm) sigma2 (rewardKernel (env, arm))) (hsigma2 : sigma2 ≠ 0) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (selectedArm : Env -> Fin K) (hselectedArm : Measurable selectedArm) (n : Nat) : stationaryLatentArmStreamTrajectoryMeasure prior rewardKernel algorithm {sample | ∃ t < n, 0 < pullCount (stationaryLatentArmStreamTrajectoryAction sample) (selectedArm (stationaryLatentArmStreamTrajectoryEnvironment sample)) t ∧ UCB.realEmpiricalMean (stationaryLatentArmStreamTrajectoryAction sample) (stationaryLatentArmStreamTrajectoryReward sample) (selectedArm (stationaryLatentArmStreamTrajectoryEnvironment sample)) t + Real.sqrt (2 * (sigma2 : Real) * Real.log (1 / delta) / (pullCount (stationaryLatentArmStreamTrajectoryAction sample) (selectedArm (stationaryLatentArmStreamTrajectoryEnvironment sample)) t : Real)) <= mean (stationaryLatentArmStreamTrajectoryEnvironment sample) (selectedArm (stationaryLatentArmStreamTrajectoryEnvironment sample))} <= (n - 1 : Nat) * ENNReal.ofReal delta

Prior-mixed lower-confidence failure bound for the clipped score radius.

theorem stationaryLatentArmStreamTrajectoryMeasure_realEmpiricalMean_add_width_le_mean {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (prior : Measure Env) [IsProbabilityMeasure prior] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (algorithm : HistoryAlgorithm (Fin K) Real) (mean : Env -> Fin K -> Real) (hmeas_mean : Measurable (fun input : Env × Fin K => mean input.1 input.2)) (sigma2 : NNReal) (hsubG : forall env arm, HasSubgaussianMGF (fun reward => reward - mean env arm) sigma2 (rewardKernel (env, arm))) (delta : Real) (arm : Fin K) (n : Nat) : stationaryLatentArmStreamTrajectoryMeasure prior rewardKernel algorithm {sample | 0 < pullCount (stationaryLatentArmStreamTrajectoryAction sample) arm n ∧ UCB.realEmpiricalMean (stationaryLatentArmStreamTrajectoryAction sample) (stationaryLatentArmStreamTrajectoryReward sample) arm n + Real.sqrt (2 * (sigma2 : Real) * Real.log (1 / delta) / (pullCount (stationaryLatentArmStreamTrajectoryAction sample) arm n : Real)) <= mean (stationaryLatentArmStreamTrajectoryEnvironment sample) arm} <= ((Finset.range (n + 1)).filter (fun k => 0 < k)).sum (fun k => ENNReal.ofReal (Real.exp (-(clippedCountWidthThreshold sigma2 delta k) ^ 2 / (2 * (k : Real) * (sigma2 : Real)))))

Prior-mixed upper-confidence failure bound for the clipped score radius.

theorem stationaryLatentArmStreamTrajectoryMeasure_mean_le_realEmpiricalMean_sub_width {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (prior : Measure Env) [IsProbabilityMeasure prior] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (algorithm : HistoryAlgorithm (Fin K) Real) (mean : Env -> Fin K -> Real) (hmeas_mean : Measurable (fun input : Env × Fin K => mean input.1 input.2)) (sigma2 : NNReal) (hsubG : forall env arm, HasSubgaussianMGF (fun reward => reward - mean env arm) sigma2 (rewardKernel (env, arm))) (delta : Real) (arm : Fin K) (n : Nat) : stationaryLatentArmStreamTrajectoryMeasure prior rewardKernel algorithm {sample | 0 < pullCount (stationaryLatentArmStreamTrajectoryAction sample) arm n ∧ mean (stationaryLatentArmStreamTrajectoryEnvironment sample) arm <= UCB.realEmpiricalMean (stationaryLatentArmStreamTrajectoryAction sample) (stationaryLatentArmStreamTrajectoryReward sample) arm n - Real.sqrt (2 * (sigma2 : Real) * Real.log (1 / delta) / (pullCount (stationaryLatentArmStreamTrajectoryAction sample) arm n : Real))} <= ((Finset.range (n + 1)).filter (fun k => 0 < k)).sum (fun k => ENNReal.ofReal (Real.exp (-(clippedCountWidthThreshold sigma2 delta k) ^ 2 / (2 * (k : Real) * (sigma2 : Real)))))

Simplified `n * delta` lower-confidence failure bound.

theorem stationaryLatentArmStreamTrajectoryMeasure_realEmpiricalMean_add_width_le_mean_le_nat_mul_delta {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (prior : Measure Env) [IsProbabilityMeasure prior] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (algorithm : HistoryAlgorithm (Fin K) Real) (mean : Env -> Fin K -> Real) (hmeas_mean : Measurable (fun input : Env × Fin K => mean input.1 input.2)) (sigma2 : NNReal) (hsubG : forall env arm, HasSubgaussianMGF (fun reward => reward - mean env arm) sigma2 (rewardKernel (env, arm))) (hsigma2 : sigma2 ≠ 0) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (arm : Fin K) (n : Nat) : stationaryLatentArmStreamTrajectoryMeasure prior rewardKernel algorithm {sample | 0 < pullCount (stationaryLatentArmStreamTrajectoryAction sample) arm n ∧ UCB.realEmpiricalMean (stationaryLatentArmStreamTrajectoryAction sample) (stationaryLatentArmStreamTrajectoryReward sample) arm n + Real.sqrt (2 * (sigma2 : Real) * Real.log (1 / delta) / (pullCount (stationaryLatentArmStreamTrajectoryAction sample) arm n : Real)) <= mean (stationaryLatentArmStreamTrajectoryEnvironment sample) arm} <= (n : ENNReal) * ENNReal.ofReal delta

Simplified `n * delta` upper-confidence failure bound.

theorem stationaryLatentArmStreamTrajectoryMeasure_mean_le_realEmpiricalMean_sub_width_le_nat_mul_delta {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (prior : Measure Env) [IsProbabilityMeasure prior] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (algorithm : HistoryAlgorithm (Fin K) Real) (mean : Env -> Fin K -> Real) (hmeas_mean : Measurable (fun input : Env × Fin K => mean input.1 input.2)) (sigma2 : NNReal) (hsubG : forall env arm, HasSubgaussianMGF (fun reward => reward - mean env arm) sigma2 (rewardKernel (env, arm))) (hsigma2 : sigma2 ≠ 0) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (arm : Fin K) (n : Nat) : stationaryLatentArmStreamTrajectoryMeasure prior rewardKernel algorithm {sample | 0 < pullCount (stationaryLatentArmStreamTrajectoryAction sample) arm n ∧ mean (stationaryLatentArmStreamTrajectoryEnvironment sample) arm <= UCB.realEmpiricalMean (stationaryLatentArmStreamTrajectoryAction sample) (stationaryLatentArmStreamTrajectoryReward sample) arm n - Real.sqrt (2 * (sigma2 : Real) * Real.log (1 / delta) / (pullCount (stationaryLatentArmStreamTrajectoryAction sample) arm n : Real))} <= (n : ENNReal) * ENNReal.ofReal delta

Bayesian prior augmented with the stationary latent arm stream.

noncomputable def stationaryLatentArmStreamPrior {Env : Type u} {K : Nat} [MeasurableSpace Env] [NeZero K] (prior : Measure Env) (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] : Measure (Env × UCB.ArmRewardStream K)

Canonical trajectory measure in the left-associated sample shape consumed by the Thompson Bayesian-regret decomposition.

noncomputable def stationaryLatentArmStreamCanonicalTrajectoryMeasure {Env : Type u} {K : Nat} [MeasurableSpace Env] [NeZero K] (prior : Measure Env) (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (algorithm : HistoryAlgorithm (Fin K) Real) : Measure ((Env × UCB.ArmRewardStream K) × ((n : Nat) -> Fin K × Real))

The concentration and decomposition sample shapes agree by product associativity.

theorem stationaryLatentArmStreamTrajectoryMeasure_map_prodAssoc_symm {Env : Type u} {K : Nat} [MeasurableSpace Env] [NeZero K] (prior : Measure Env) (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (algorithm : HistoryAlgorithm (Fin K) Real) : (stationaryLatentArmStreamTrajectoryMeasure prior rewardKernel algorithm).map MeasurableEquiv.prodAssoc.symm = stationaryLatentArmStreamCanonicalTrajectoryMeasure prior rewardKernel algorithm

Decomposition-facing lower-confidence failure bound on the canonical augmented trajectory measure.

theorem stationaryLatentArmStreamCanonicalTrajectoryMeasure_realEmpiricalMean_add_width_le_mean_le_nat_mul_delta {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (prior : Measure Env) [IsProbabilityMeasure prior] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (algorithm : HistoryAlgorithm (Fin K) Real) (mean : Env -> Fin K -> Real) (hmeas_mean : Measurable (fun input : Env × Fin K => mean input.1 input.2)) (sigma2 : NNReal) (hsubG : forall env arm, HasSubgaussianMGF (fun reward => reward - mean env arm) sigma2 (rewardKernel (env, arm))) (hsigma2 : sigma2 ≠ 0) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (arm : Fin K) (n : Nat) : stationaryLatentArmStreamCanonicalTrajectoryMeasure prior rewardKernel algorithm {sample : (Env × UCB.ArmRewardStream K) × ((n : Nat) → Fin K × Real) | 0 < pullCount (environmentTrajectoryAction sample) arm n ∧ UCB.realEmpiricalMean (environmentTrajectoryAction sample) (environmentTrajectoryReward sample) arm n + Real.sqrt (2 * (sigma2 : Real) * Real.log (1 / delta) / (pullCount (environmentTrajectoryAction sample) arm n : Real)) <= mean sample.1.1 arm} <= (n : ENNReal) * ENNReal.ofReal delta

Decomposition-facing upper-confidence failure bound on the canonical augmented trajectory measure.

theorem stationaryLatentArmStreamCanonicalTrajectoryMeasure_mean_le_realEmpiricalMean_sub_width_le_nat_mul_delta {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (prior : Measure Env) [IsProbabilityMeasure prior] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (algorithm : HistoryAlgorithm (Fin K) Real) (mean : Env -> Fin K -> Real) (hmeas_mean : Measurable (fun input : Env × Fin K => mean input.1 input.2)) (sigma2 : NNReal) (hsubG : forall env arm, HasSubgaussianMGF (fun reward => reward - mean env arm) sigma2 (rewardKernel (env, arm))) (hsigma2 : sigma2 ≠ 0) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (arm : Fin K) (n : Nat) : stationaryLatentArmStreamCanonicalTrajectoryMeasure prior rewardKernel algorithm {sample : (Env × UCB.ArmRewardStream K) × ((n : Nat) → Fin K × Real) | 0 < pullCount (environmentTrajectoryAction sample) arm n ∧ mean sample.1.1 arm <= UCB.realEmpiricalMean (environmentTrajectoryAction sample) (environmentTrajectoryReward sample) arm n - Real.sqrt (2 * (sigma2 : Real) * Real.log (1 / delta) / (pullCount (environmentTrajectoryAction sample) arm n : Real))} <= (n : ENNReal) * ENNReal.ofReal delta

Decomposition-facing horizon-uniform lower-confidence failure for a measurable environment-dependent arm, with the exact `(n - 1) * delta` cost.

theorem stationaryLatentArmStreamCanonicalTrajectoryMeasure_exists_selectedArm_realEmpiricalMean_add_width_le_mean_le {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (prior : Measure Env) [IsProbabilityMeasure prior] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (algorithm : HistoryAlgorithm (Fin K) Real) (mean : Env -> Fin K -> Real) (hmeas_mean : Measurable (fun input : Env × Fin K => mean input.1 input.2)) (sigma2 : NNReal) (hsubG : forall env arm, HasSubgaussianMGF (fun reward => reward - mean env arm) sigma2 (rewardKernel (env, arm))) (hsigma2 : sigma2 ≠ 0) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (selectedArm : Env -> Fin K) (hselectedArm : Measurable selectedArm) (n : Nat) : stationaryLatentArmStreamCanonicalTrajectoryMeasure prior rewardKernel algorithm {sample : (Env × UCB.ArmRewardStream K) × ((n : Nat) -> Fin K × Real) | ∃ t < n, 0 < pullCount (environmentTrajectoryAction sample) (selectedArm sample.1.1) t ∧ UCB.realEmpiricalMean (environmentTrajectoryAction sample) (environmentTrajectoryReward sample) (selectedArm sample.1.1) t + Real.sqrt (2 * (sigma2 : Real) * Real.log (1 / delta) / (pullCount (environmentTrajectoryAction sample) (selectedArm sample.1.1) t : Real)) <= mean sample.1.1 (selectedArm sample.1.1)} <= (n - 1 : Nat) * ENNReal.ofReal delta

The first pinned-LML Thompson concentration expectation: the finite-horizon best-action mean minus clipped-UCB sum is controlled by the horizon-uniform lower-confidence failure event.

theorem stationaryLatentArmStreamCanonicalTrajectoryMeasure_integral_sum_mean_bestAction_sub_clippedUCB_le {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (prior : Measure Env) [IsProbabilityMeasure prior] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (algorithm : HistoryAlgorithm (Fin K) Real) (bestAction : Env -> Fin K) (hbestAction : Measurable bestAction) (mean : Env -> Fin K -> Real) (hmeas_mean : Measurable (fun input : Env × Fin K => mean input.1 input.2)) (l u : Real) (hlu : l <= u) (hmeanMem : forall env arm, mean env arm ∈ Set.Icc l u) (sigma2 : NNReal) (hsubG : forall env arm, HasSubgaussianMGF (fun reward => reward - mean env arm) sigma2 (rewardKernel (env, arm))) (hsigma2 : sigma2 ≠ 0) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (n : Nat) : integral (stationaryLatentArmStreamCanonicalTrajectoryMeasure prior rewardKernel algorithm) (fun sample => ∑ t ∈ Finset.range n, (mean sample.1.1 (bestAction sample.1.1) - clippedUCB l u (sigma2 : Real) delta (environmentTrajectoryAction sample) (environmentTrajectoryReward sample) (bestAction sample.1.1) t)) <= (u - l) * (n - 1) * n * delta

A finite union of upper prefix deviations pays once per positive pull count.

theorem measure_biUnion_clippedCountWidthThreshold_le_armPrefixSum_sub_mul_le {K : Nat} (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (arm : Fin K) (mean : Real) (sigma2 : NNReal) (hsubG : HasSubgaussianMGF (fun reward => reward - mean) sigma2 (nu arm)) (hsigma2 : sigma2 ≠ 0) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (m : Nat) : UCB.armStreamMeasure nu (⋃ k ∈ Finset.Icc 1 m, {stream : UCB.ArmRewardStream K | clippedCountWidthThreshold sigma2 delta k <= UCB.armPrefixSum arm k stream - (k : Real) * mean}) <= (m : ENNReal) * ENNReal.ofReal delta

Finite-horizon upper-confidence failure for one arm on the coupled trajectory. Times with the same positive pull count collapse to one latent-stream prefix event, preserving the exact `(n - 1) * delta` cost.

theorem measure_latentArmStreamTrajectory_exists_mean_le_realEmpiricalMean_sub_width_le {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (arm : Fin K) (mean : Real) (sigma2 : NNReal) (hsubG : HasSubgaussianMGF (fun reward => reward - mean) sigma2 (nu arm)) (hsigma2 : sigma2 ≠ 0) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (n : Nat) : latentArmStreamTrajectoryMeasure algorithm env nu {sample | ∃ t < n, 0 < pullCount (latentArmStreamTrajectoryAction sample) arm t ∧ mean <= UCB.realEmpiricalMean (latentArmStreamTrajectoryAction sample) (latentArmStreamTrajectoryReward sample) arm t - Real.sqrt (2 * (sigma2 : Real) * Real.log (1 / delta) / (pullCount (latentArmStreamTrajectoryAction sample) arm t : Real))} <= (n - 1 : Nat) * ENNReal.ofReal delta

Finite-arm union of the horizon upper-confidence failures at fixed environment.

theorem measure_latentArmStreamTrajectory_exists_arm_exists_mean_le_realEmpiricalMean_sub_width_le {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (algorithm : HistoryAlgorithm (Fin K) Real) (env : Env) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (mean : Fin K -> Real) (sigma2 : NNReal) (hsubG : forall arm, HasSubgaussianMGF (fun reward => reward - mean arm) sigma2 (nu arm)) (hsigma2 : sigma2 ≠ 0) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (n : Nat) : latentArmStreamTrajectoryMeasure algorithm env nu {sample | ∃ arm : Fin K, ∃ t < n, 0 < pullCount (latentArmStreamTrajectoryAction sample) arm t ∧ mean arm <= UCB.realEmpiricalMean (latentArmStreamTrajectoryAction sample) (latentArmStreamTrajectoryReward sample) arm t - Real.sqrt (2 * (sigma2 : Real) * Real.log (1 / delta) / (pullCount (latentArmStreamTrajectoryAction sample) arm t : Real))} <= (K : ENNReal) * ((n - 1 : Nat) : ENNReal) * ENNReal.ofReal delta

Prior mixing preserves the finite-arm horizon upper-confidence budget.

theorem stationaryLatentArmStreamTrajectoryMeasure_exists_arm_exists_mean_le_realEmpiricalMean_sub_width_le {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (prior : Measure Env) [IsProbabilityMeasure prior] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (algorithm : HistoryAlgorithm (Fin K) Real) (mean : Env -> Fin K -> Real) (hmeas_mean : Measurable (fun input : Env × Fin K => mean input.1 input.2)) (sigma2 : NNReal) (hsubG : forall env arm, HasSubgaussianMGF (fun reward => reward - mean env arm) sigma2 (rewardKernel (env, arm))) (hsigma2 : sigma2 ≠ 0) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (n : Nat) : stationaryLatentArmStreamTrajectoryMeasure prior rewardKernel algorithm {sample | ∃ arm : Fin K, ∃ t < n, 0 < pullCount (stationaryLatentArmStreamTrajectoryAction sample) arm t ∧ mean (stationaryLatentArmStreamTrajectoryEnvironment sample) arm <= UCB.realEmpiricalMean (stationaryLatentArmStreamTrajectoryAction sample) (stationaryLatentArmStreamTrajectoryReward sample) arm t - Real.sqrt (2 * (sigma2 : Real) * Real.log (1 / delta) / (pullCount (stationaryLatentArmStreamTrajectoryAction sample) arm t : Real))} <= (K : ENNReal) * ((n - 1 : Nat) : ENNReal) * ENNReal.ofReal delta

Decomposition-facing finite-arm horizon upper-confidence failure with exact `K * (n - 1) * delta` cost.

theorem stationaryLatentArmStreamCanonicalTrajectoryMeasure_exists_arm_exists_mean_le_realEmpiricalMean_sub_width_le {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (prior : Measure Env) [IsProbabilityMeasure prior] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (algorithm : HistoryAlgorithm (Fin K) Real) (mean : Env -> Fin K -> Real) (hmeas_mean : Measurable (fun input : Env × Fin K => mean input.1 input.2)) (sigma2 : NNReal) (hsubG : forall env arm, HasSubgaussianMGF (fun reward => reward - mean env arm) sigma2 (rewardKernel (env, arm))) (hsigma2 : sigma2 ≠ 0) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (n : Nat) : stationaryLatentArmStreamCanonicalTrajectoryMeasure prior rewardKernel algorithm {sample | ∃ arm : Fin K, ∃ t < n, 0 < pullCount (environmentTrajectoryAction sample) arm t ∧ mean sample.1.1 arm <= UCB.realEmpiricalMean (environmentTrajectoryAction sample) (environmentTrajectoryReward sample) arm t - Real.sqrt (2 * (sigma2 : Real) * Real.log (1 / delta) / (pullCount (environmentTrajectoryAction sample) arm t : Real))} <= (K : ENNReal) * ((n - 1 : Nat) : ENNReal) * ENNReal.ofReal delta

The second pinned-LML Thompson concentration expectation: selected-action clipped-UCB excess is bounded by deterministic pull-count summation plus the finite-arm horizon upper-confidence failure budget.

theorem stationaryLatentArmStreamCanonicalTrajectoryMeasure_integral_sum_clippedUCB_action_sub_mean_le {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [NeZero K] (prior : Measure Env) [IsProbabilityMeasure prior] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (algorithm : HistoryAlgorithm (Fin K) Real) (mean : Env -> Fin K -> Real) (hmeas_mean : Measurable (fun input : Env × Fin K => mean input.1 input.2)) (l u : Real) (hlu : l <= u) (hmeanMem : forall env arm, mean env arm ∈ Set.Icc l u) (sigma2 : NNReal) (hsubG : forall env arm, HasSubgaussianMGF (fun reward => reward - mean env arm) sigma2 (rewardKernel (env, arm))) (hsigma2 : sigma2 ≠ 0) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (n : Nat) : integral (stationaryLatentArmStreamCanonicalTrajectoryMeasure prior rewardKernel algorithm) (fun sample => ∑ t ∈ Finset.range n, (clippedUCB l u (sigma2 : Real) delta (environmentTrajectoryAction sample) (environmentTrajectoryReward sample) (environmentTrajectoryAction sample t) t - mean sample.1.1 (environmentTrajectoryAction sample t))) <= (u - l) * K + 4 * Real.sqrt (2 * (sigma2 : Real) * Real.log (1 / delta) * K * n) + (u - l) * K * (n - 1) * n * delta

Stationary-reward Thompson Bayesian regret with an explicit confidence parameter. This is the decomposition-facing join of the two pinned-LML clipped-UCB expectation bounds. The analytic upper bound is in fact comparator-uniform, but the public Bayesian-regret endpoint deliberately retains `IsOptimalMeanSelector mean bestAction` as an interpretation contract.

theorem stationaryLatentArmStreamCanonicalTrajectoryMeasure_integral_trajectoryBayesMeanRegret_le_of_delta {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [NeZero K] (prior : Measure Env) [IsProbabilityMeasure prior] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (bestAction : Env -> Fin K) (hbestAction : Measurable bestAction) (mean : Env -> Fin K -> Real) (hbest : IsOptimalMeanSelector mean bestAction) (hmeas_mean : Measurable (fun input : Env × Fin K => mean input.1 input.2)) (l u : Real) (hlu : l <= u) (hmeanMem : forall env arm, mean env arm ∈ Set.Icc l u) (sigma2 : NNReal) (hsubG : forall env arm, HasSubgaussianMGF (fun reward => reward - mean env arm) sigma2 (rewardKernel (env, arm))) (hsigma2 : sigma2 ≠ 0) (delta : Real) (hdelta : 0 < delta) (hdelta_one : delta <= 1) (n : Nat) : let augmentedPrior := stationaryLatentArmStreamPrior prior rewardKernel let feedbackEnvironment := latentArmStreamMeasurableHistoryEnvironment (Env

Pinned-LML stationary-reward Thompson Bayesian-regret bound, obtained from the explicit-confidence theorem with `delta = 1 / n ^ 2`. Unlike the comparator-relative decomposition, this endpoint explicitly requires the selector to maximize the declared mean surface pointwise.

theorem stationaryLatentArmStreamCanonicalTrajectoryMeasure_integral_trajectoryBayesMeanRegret_le {Env : Type u} {K : Nat} [MeasurableSpace Env] [StandardBorelSpace Env] [Nonempty Env] [NeZero K] (prior : Measure Env) [IsProbabilityMeasure prior] (rewardKernel : Kernel (Env × Fin K) Real) [IsMarkovKernel rewardKernel] (bestAction : Env -> Fin K) (hbestAction : Measurable bestAction) (mean : Env -> Fin K -> Real) (hbest : IsOptimalMeanSelector mean bestAction) (hmeas_mean : Measurable (fun input : Env × Fin K => mean input.1 input.2)) (l u : Real) (hlu : l <= u) (hmeanMem : forall env arm, mean env arm ∈ Set.Icc l u) (sigma2 : NNReal) (hsubG : forall env arm, HasSubgaussianMGF (fun reward => reward - mean env arm) sigma2 (rewardKernel (env, arm))) (hsigma2 : sigma2 ≠ 0) (n : Nat) : let augmentedPrior := stationaryLatentArmStreamPrior prior rewardKernel let feedbackEnvironment := latentArmStreamMeasurableHistoryEnvironment (Env