BanditRLProof.Algorithms.UCBArmStreamTail

Every time/arm coordinate has its prescribed stationary kernel law.

theorem armStreamMeasure_map_coord {K : Nat} (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (i : Nat) (arm : Fin K) : Measure.map (fun stream : ArmRewardStream K => stream i arm) (armStreamMeasure nu) = nu arm

Centered coordinates of one fixed arm are independent across time.

theorem iIndepFun_armStreamMeasure_coord_sub {K : Nat} (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (arm : Fin K) (mean : Real) : iIndepFun (fun i (stream : ArmRewardStream K) => stream i arm - mean) (armStreamMeasure nu)

Lower-tail centered coordinates are also independent across time.

theorem iIndepFun_armStreamMeasure_sub_coord {K : Nat} (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (arm : Fin K) (mean : Real) : iIndepFun (fun i (stream : ArmRewardStream K) => mean - stream i arm) (armStreamMeasure nu)

A fixed arm's centered one-coordinate MGF transports to stream space.

theorem hasSubgaussianMGF_armStreamMeasure_coord_sub {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)) (i : Nat) : HasSubgaussianMGF (fun stream : ArmRewardStream K => stream i arm - mean) sigma2 (armStreamMeasure nu)

The corresponding lower-tail coordinate has the same variance proxy.

theorem hasSubgaussianMGF_armStreamMeasure_sub_coord {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)) (i : Nat) : HasSubgaussianMGF (fun stream : ArmRewardStream K => mean - stream i arm) sigma2 (armStreamMeasure nu)

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

theorem sum_coord_sub_eq_armPrefixSum_sub {K : Nat} (stream : ArmRewardStream K) (arm : Fin K) (mean : Real) (k : Nat) : (Finset.range k).sum (fun i => stream i arm - mean) = armPrefixSum arm k stream - (k : Real) * mean

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

theorem sum_sub_coord_eq_mul_sub_armPrefixSum {K : Nat} (stream : ArmRewardStream K) (arm : Fin K) (mean : Real) (k : Nat) : (Finset.range k).sum (fun i => mean - stream i arm) = (k : Real) * mean - armPrefixSum arm k stream

ENNReal upper tail for one fixed arm prefix.

theorem measure_armPrefixSum_sub_mul_ge_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)) (k : Nat) {eps : Real} (heps : 0 <= eps) : armStreamMeasure nu {stream : ArmRewardStream K | eps <= armPrefixSum arm k stream - (k : Real) * mean} <= ENNReal.ofReal (Real.exp (-eps ^ 2 / (2 * (k : Real) * (sigma2 : Real))))

ENNReal lower tail for one fixed arm prefix.

theorem measure_mul_sub_armPrefixSum_ge_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)) (k : Nat) {eps : Real} (heps : 0 <= eps) : armStreamMeasure nu {stream : ArmRewardStream K | eps <= (k : Real) * mean - armPrefixSum arm k stream} <= ENNReal.ofReal (Real.exp (-eps ^ 2 / (2 * (k : Real) * (sigma2 : Real))))

Empirical mean of the first `k` latent rewards of one fixed arm.

noncomputable def armPrefixEmpiricalMean {K : Nat} (arm : Fin K) (k : Nat) (stream : ArmRewardStream K) : Real

Two-sided fixed-sample confidence radius for one arm with per-reward proxy variance `sigma2`.

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

Two-sided `delta` confidence theorem for the empirical mean of exactly `k` latent rewards of one arm under the stationary product arm-stream law. The theorem derives positivity of the total proxy variance from `0 < k` and `sigma2 ≠ 0`; callers do not supply a separate aggregate-variance contract.

theorem measure_armPrefixAverageConfidenceRadius_le_abs_empiricalMean_sub {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)) (k : Nat) (hk : 0 < k) (hsigma2 : sigma2 ≠ 0) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : armStreamMeasure nu {stream : ArmRewardStream K | armPrefixAverageConfidenceRadius sigma2 k delta <= |armPrefixEmpiricalMean arm k stream - mean|} <= ENNReal.ofReal delta

Pair event used to peel an upper selected-reward deviation by pull count.

def upperDeviationPairs (mean : Real) (threshold : Nat -> Real) : Set (Nat × Real)

Pair event used to peel a lower selected-reward deviation by pull count.

def lowerDeviationPairs (mean : Real) (threshold : Nat -> Real) : Set (Nat × Real)

Positive-count upper deviation pair event used by UCB index tails.

def positiveUpperDeviationPairs (mean : Real) (threshold : Nat -> Real) : Set (Nat × Real)

Positive-count lower deviation pair event used by UCB index tails.

def positiveLowerDeviationPairs (mean : Real) (threshold : Nat -> Real) : Set (Nat × Real)

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

theorem mem_fst_image_upperDeviationPairs (mean : Real) (threshold : Nat -> Real) (k : Nat) : k ∈ Prod.fst '' upperDeviationPairs mean threshold

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

theorem mem_fst_image_lowerDeviationPairs (mean : Real) (threshold : Nat -> Real) (k : Nat) : k ∈ Prod.fst '' lowerDeviationPairs mean threshold

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

theorem mem_fst_image_positiveUpperDeviationPairs_iff (mean : Real) (threshold : Nat -> Real) (k : Nat) : k ∈ Prod.fst '' positiveUpperDeviationPairs mean threshold ↔ 0 < k

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

theorem mem_fst_image_positiveLowerDeviationPairs_iff (mean : Real) (threshold : Nat -> Real) (k : Nat) : k ∈ Prod.fst '' positiveLowerDeviationPairs mean threshold ↔ 0 < k

Adaptive-count upper selected-reward tail for the recursive UCB process. The threshold may depend on the realized pull count. Peeling turns the event into a finite sum over all fixed counts `k <= n`, and each term is discharged by the stationary fixed-arm sub-Gaussian prefix tail.

theorem measure_sumRewards_sub_pullCount_mul_ge_le {K : Nat} (hK : 0 < K) (c : Real) (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) : armStreamMeasure nu {stream : ArmRewardStream K | threshold (pullCount (armStreamAction hK c stream) arm n) <= sumRewards (armStreamAction hK c stream) (armStreamReward hK c stream) arm n - (pullCount (armStreamAction hK c 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 selected-reward tail for the recursive UCB process.

theorem measure_pullCount_mul_sub_sumRewards_ge_le {K : Nat} (hK : 0 < K) (c : Real) (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) : armStreamMeasure nu {stream : ArmRewardStream K | threshold (pullCount (armStreamAction hK c stream) arm n) <= (pullCount (armStreamAction hK c stream) arm n : Real) * mean - sumRewards (armStreamAction hK c stream) (armStreamReward hK c stream) arm n} <= (Finset.range (n + 1)).sum (fun k => ENNReal.ofReal (Real.exp (-(threshold k) ^ 2 / (2 * (k : Real) * (sigma2 : Real)))))

Positive-pull-count adaptive upper tail, with the zero-count fiber removed.

theorem measure_pos_and_sumRewards_sub_pullCount_mul_ge_le {K : Nat} (hK : 0 < K) (c : Real) (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) : armStreamMeasure nu {stream : ArmRewardStream K | 0 < pullCount (armStreamAction hK c stream) arm n ∧ threshold (pullCount (armStreamAction hK c stream) arm n) <= sumRewards (armStreamAction hK c stream) (armStreamReward hK c stream) arm n - (pullCount (armStreamAction hK c stream) 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-pull-count adaptive lower tail, with the zero-count fiber removed.

theorem measure_pos_and_pullCount_mul_sub_sumRewards_ge_le {K : Nat} (hK : 0 < K) (c : Real) (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) : armStreamMeasure nu {stream : ArmRewardStream K | 0 < pullCount (armStreamAction hK c stream) arm n ∧ threshold (pullCount (armStreamAction hK c stream) arm n) <= (pullCount (armStreamAction hK c stream) arm n : Real) * mean - sumRewards (armStreamAction hK c stream) (armStreamReward hK c stream) 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 confidence width used in the fixed-count tail fibers.

noncomputable def countWidthThreshold (c : Real) (sigma2 : NNReal) (n k : Nat) : Real

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

theorem countWidthThreshold_nonneg (c : Real) (sigma2 : NNReal) (n k : Nat) : 0 <= countWidthThreshold c sigma2 n k

Lower index failure implies the corresponding count-scaled lower sum deviation.

theorem countWidthThreshold_le_mul_mean_sub_sumRewards_of_empiricalMean_add_width_le {K : Nat} (action : ActionTrace (Fin K)) (reward : RewardTrace Real) (arm : Fin K) (n : Nat) (mean c : Real) (sigma2 : NNReal) (hcount : 0 < pullCount action arm n) (hindex : realEmpiricalMean action reward arm n + realWidth action (c * (sigma2 : Real)) arm n <= mean) : countWidthThreshold c sigma2 n (pullCount action arm n) <= (pullCount action arm n : Real) * mean - sumRewards action reward arm n

Upper index failure implies the corresponding count-scaled upper sum deviation.

theorem countWidthThreshold_le_sumRewards_sub_mul_mean_of_mean_le_empiricalMean_sub_width {K : Nat} (action : ActionTrace (Fin K)) (reward : RewardTrace Real) (arm : Fin K) (n : Nat) (mean c : Real) (sigma2 : NNReal) (hcount : 0 < pullCount action arm n) (hindex : mean <= realEmpiricalMean action reward arm n - realWidth action (c * (sigma2 : Real)) arm n) : countWidthThreshold c sigma2 n (pullCount action arm n) <= sumRewards action reward arm n - (pullCount action arm n : Real) * mean

LML-shaped lower UCB-index tail for the actual recursive arm-stream process, before simplifying the finite fixed-count exponential sum.

theorem measure_realEmpiricalMean_add_realWidth_le_mean {K : Nat} (hK : 0 < K) (c : Real) (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) : armStreamMeasure nu {stream : ArmRewardStream K | 0 < pullCount (armStreamAction hK (c * (sigma2 : Real)) stream) arm n ∧ realEmpiricalMean (armStreamAction hK (c * (sigma2 : Real)) stream) (armStreamReward hK (c * (sigma2 : Real)) stream) arm n + realWidth (armStreamAction hK (c * (sigma2 : Real)) stream) (c * (sigma2 : Real)) arm n <= mean} <= ((Finset.range (n + 1)).filter (fun k => 0 < k)).sum (fun k => ENNReal.ofReal (Real.exp (-(countWidthThreshold c sigma2 n k) ^ 2 / (2 * (k : Real) * (sigma2 : Real)))))

LML-shaped upper UCB-index tail for the actual recursive arm-stream process, before simplifying the finite fixed-count exponential sum.

theorem measure_mean_le_realEmpiricalMean_sub_realWidth {K : Nat} (hK : 0 < K) (c : Real) (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) : armStreamMeasure nu {stream : ArmRewardStream K | 0 < pullCount (armStreamAction hK (c * (sigma2 : Real)) stream) arm n ∧ mean <= realEmpiricalMean (armStreamAction hK (c * (sigma2 : Real)) stream) (armStreamReward hK (c * (sigma2 : Real)) stream) arm n - realWidth (armStreamAction hK (c * (sigma2 : Real)) stream) (c * (sigma2 : Real)) arm n} <= ((Finset.range (n + 1)).filter (fun k => 0 < k)).sum (fun k => ENNReal.ofReal (Real.exp (-(countWidthThreshold c sigma2 n k) ^ 2 / (2 * (k : Real) * (sigma2 : Real)))))

Every positive fixed-count fiber has the same logarithmic exponent.

theorem countWidthThreshold_sq_div_eq (c : Real) (sigma2 : NNReal) (n k : Nat) (hc : 0 <= c) (hsigma2 : sigma2 ≠ 0) (hk : 0 < k) : (countWidthThreshold c sigma2 n k) ^ 2 / (2 * (k : Real) * (sigma2 : Real)) = c * Real.log ((n + 1 : Nat) : Real)

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

theorem positiveCountFilter_eq_Icc (n : Nat) : (Finset.range (n + 1)).filter (fun k => 0 < k) = Finset.Icc 1 n

The fixed-count exponential sum collapses to `n` identical terms.

theorem sum_countWidthThreshold_tail_eq (c : Real) (sigma2 : NNReal) (n : Nat) (hc : 0 <= c) (hsigma2 : sigma2 ≠ 0) : ((Finset.range (n + 1)).filter (fun k => 0 < k)).sum (fun k => ENNReal.ofReal (Real.exp (-(countWidthThreshold c sigma2 n k) ^ 2 / (2 * (k : Real) * (sigma2 : Real))))) = (n : ENNReal) * ENNReal.ofReal (Real.exp (-c * Real.log ((n + 1 : Nat) : Real)))

Convert the peeled logarithmic tail into the inverse-power form used by LML.

theorem natCast_mul_exp_neg_log_le_inv_rpow_sub_one (c : Real) (n : Nat) : (n : ENNReal) * ENNReal.ofReal (Real.exp (-c * Real.log ((n + 1 : Nat) : Real))) <= (1 : ENNReal) / (((n + 1 : Nat) : ENNReal) ^ (c - 1))

Simplified logarithmic lower-index tail for the recursive UCB process.

theorem measure_realEmpiricalMean_add_realWidth_le_mean_log_bound {K : Nat} (hK : 0 < K) (c : Real) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (arm : Fin K) (mean : Real) (sigma2 : NNReal) (hsubG : HasSubgaussianMGF (fun reward => reward - mean) sigma2 (nu arm)) (hc : 0 <= c) (hsigma2 : sigma2 ≠ 0) (n : Nat) : armStreamMeasure nu {stream : ArmRewardStream K | 0 < pullCount (armStreamAction hK (c * (sigma2 : Real)) stream) arm n ∧ realEmpiricalMean (armStreamAction hK (c * (sigma2 : Real)) stream) (armStreamReward hK (c * (sigma2 : Real)) stream) arm n + realWidth (armStreamAction hK (c * (sigma2 : Real)) stream) (c * (sigma2 : Real)) arm n <= mean} <= (n : ENNReal) * ENNReal.ofReal (Real.exp (-c * Real.log ((n + 1 : Nat) : Real)))

Simplified logarithmic upper-index tail for the recursive UCB process.

theorem measure_mean_le_realEmpiricalMean_sub_realWidth_log_bound {K : Nat} (hK : 0 < K) (c : Real) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (arm : Fin K) (mean : Real) (sigma2 : NNReal) (hsubG : HasSubgaussianMGF (fun reward => reward - mean) sigma2 (nu arm)) (hc : 0 <= c) (hsigma2 : sigma2 ≠ 0) (n : Nat) : armStreamMeasure nu {stream : ArmRewardStream K | 0 < pullCount (armStreamAction hK (c * (sigma2 : Real)) stream) arm n ∧ mean <= realEmpiricalMean (armStreamAction hK (c * (sigma2 : Real)) stream) (armStreamReward hK (c * (sigma2 : Real)) stream) arm n - realWidth (armStreamAction hK (c * (sigma2 : Real)) stream) (c * (sigma2 : Real)) arm n} <= (n : ENNReal) * ENNReal.ofReal (Real.exp (-c * Real.log ((n + 1 : Nat) : Real)))

LML-shaped inverse-power lower-index tail for the recursive UCB process.

theorem measure_realEmpiricalMean_add_realWidth_le_mean_rpow_bound {K : Nat} (hK : 0 < K) (c : Real) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (arm : Fin K) (mean : Real) (sigma2 : NNReal) (hsubG : HasSubgaussianMGF (fun reward => reward - mean) sigma2 (nu arm)) (hc : 0 <= c) (hsigma2 : sigma2 ≠ 0) (n : Nat) : armStreamMeasure nu {stream : ArmRewardStream K | 0 < pullCount (armStreamAction hK (c * (sigma2 : Real)) stream) arm n /\ realEmpiricalMean (armStreamAction hK (c * (sigma2 : Real)) stream) (armStreamReward hK (c * (sigma2 : Real)) stream) arm n + realWidth (armStreamAction hK (c * (sigma2 : Real)) stream) (c * (sigma2 : Real)) arm n <= mean} <= (1 : ENNReal) / (((n + 1 : Nat) : ENNReal) ^ (c - 1))

LML-shaped inverse-power upper-index tail for the recursive UCB process.

theorem measure_mean_le_realEmpiricalMean_sub_realWidth_rpow_bound {K : Nat} (hK : 0 < K) (c : Real) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (arm : Fin K) (mean : Real) (sigma2 : NNReal) (hsubG : HasSubgaussianMGF (fun reward => reward - mean) sigma2 (nu arm)) (hc : 0 <= c) (hsigma2 : sigma2 ≠ 0) (n : Nat) : armStreamMeasure nu {stream : ArmRewardStream K | 0 < pullCount (armStreamAction hK (c * (sigma2 : Real)) stream) arm n /\ mean <= realEmpiricalMean (armStreamAction hK (c * (sigma2 : Real)) stream) (armStreamReward hK (c * (sigma2 : Real)) stream) arm n - realWidth (armStreamAction hK (c * (sigma2 : Real)) stream) (c * (sigma2 : Real)) arm n} <= (1 : ENNReal) / (((n + 1 : Nat) : ENNReal) ^ (c - 1))