BanditRLProof.Algorithms.UCBArmStreamFiniteArmRewardLaws

A finite family of Real reward laws, viewed as an arm-indexed kernel.

noncomputable def finiteArmRealRewardKernel {K : Nat} (armLaw : Fin K -> Measure Real) : Kernel (Fin K) Real

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

theorem finiteArmRealRewardKernel_apply {K : Nat} (armLaw : Fin K -> Measure Real) (arm : Fin K) : finiteArmRealRewardKernel armLaw arm = armLaw arm

Pointwise probability laws make the finite-arm kernel Markov.

theorem finiteArmRealRewardKernel_isMarkov {K : Nat} (armLaw : Fin K -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) : IsMarkovKernel (finiteArmRealRewardKernel armLaw) where

Expected regret of the canonical one-policy arm-stream process built from direct finite-arm sub-Gaussian laws. The common tuning proxy is the padded finite maximum of the genuine armwise proxies.

noncomputable def armStreamFiniteArmSubgaussianExpectedRegret {K : Nat} (hK : 0 < K) (armLaw : Fin K -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (varianceProxy : Fin K -> NNReal) (n : Nat) : Real

Direct finite-arm sub-Gaussian laws satisfy the fixed logarithmic envelope.

theorem armStreamFiniteArmSubgaussianExpectedRegret_nonneg_and_le {K : Nat} (hK : 0 < K) (armLaw : Fin K -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (varianceProxy : Fin K -> NNReal) (hsubG : forall arm, HasSubgaussianMGF (fun reward : Real => reward - integral (armLaw arm) id) (varianceProxy arm) (armLaw arm)) (n : Nat) : let nu := finiteArmRealRewardKernel armLaw let sigma2 := Concentration.finiteArmPositiveVarianceProxy varianceProxy 0 <= armStreamFiniteArmSubgaussianExpectedRegret hK armLaw hprob varianceProxy n /\ armStreamFiniteArmSubgaussianExpectedRegret hK armLaw hprob varianceProxy n <= armStreamAsymptoticModelCoefficient nu sigma2 * (1 + Real.log ((n + 1 : Nat) : Real))

Direct finite-arm sub-Gaussian expected regret normalized by `n + 1`.

noncomputable def armStreamFiniteArmSubgaussianExpectedAverageRegret {K : Nat} (hK : 0 < K) (armLaw : Fin K -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (varianceProxy : Fin K -> NNReal) (n : Nat) : Real

Direct stationary finite-arm sub-Gaussian laws instantiate one fixed canonical arm-stream policy with vanishing expected average regret.

theorem armStreamFiniteArmSubgaussianExpectedAverageRegret_tendsto_zero {K : Nat} (hK : 0 < K) (armLaw : Fin K -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (varianceProxy : Fin K -> NNReal) (hsubG : forall arm, HasSubgaussianMGF (fun reward : Real => reward - integral (armLaw arm) id) (varianceProxy arm) (armLaw arm)) : Tendsto (armStreamFiniteArmSubgaussianExpectedAverageRegret hK armLaw hprob varianceProxy) atTop (nhds 0)

Expected regret of the one-policy process for common-bounded arm laws.

noncomputable def armStreamBoundedFiniteArmExpectedRegret {K : Nat} (hK : 0 < K) (armLaw : Fin K -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (n : Nat) : Real

Common-bounded finite-arm laws satisfy the fixed logarithmic envelope.

theorem armStreamBoundedFiniteArmExpectedRegret_nonneg_and_le {K : Nat} (hK : 0 < K) (armLaw : Fin K -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (hbound : forall arm, Filter.Eventually (fun reward : Real => Set.Icc lo hi reward) (ae (armLaw arm))) (n : Nat) : let nu := finiteArmRealRewardKernel armLaw let sigma2 := Concentration.finiteArmPositiveVarianceProxy (fun _ : Fin K => Concentration.intervalVarianceProxy lo hi) 0 <= armStreamBoundedFiniteArmExpectedRegret hK armLaw hprob lo hi n /\ armStreamBoundedFiniteArmExpectedRegret hK armLaw hprob lo hi n <= armStreamAsymptoticModelCoefficient nu sigma2 * (1 + Real.log ((n + 1 : Nat) : Real))

Expected common-bounded one-policy regret normalized by `n + 1`.

noncomputable def armStreamBoundedFiniteArmExpectedAverageRegret {K : Nat} (hK : 0 < K) (armLaw : Fin K -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (n : Nat) : Real

Stationary finite-arm Real reward laws bounded almost surely in one common interval induce one fixed canonical UCB process with vanishing expected average regret. The positive padded tuning proxy removes any `lo < hi` premise.

theorem armStreamBoundedFiniteArmExpectedAverageRegret_tendsto_zero {K : Nat} (hK : 0 < K) (armLaw : Fin K -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Real) (hbound : forall arm, Filter.Eventually (fun reward : Real => Set.Icc lo hi reward) (ae (armLaw arm))) : Tendsto (armStreamBoundedFiniteArmExpectedAverageRegret hK armLaw hprob lo hi) atTop (nhds 0)

Expected regret of the one-policy process for armwise-bounded laws.

noncomputable def armStreamArmwiseBoundedFiniteArmExpectedRegret {K : Nat} (hK : 0 < K) (armLaw : Fin K -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Fin K -> Real) (n : Nat) : Real

Armwise-bounded finite-arm laws satisfy the fixed logarithmic envelope.

theorem armStreamArmwiseBoundedFiniteArmExpectedRegret_nonneg_and_le {K : Nat} (hK : 0 < K) (armLaw : Fin K -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Fin K -> Real) (hbound : forall arm, Filter.Eventually (fun reward : Real => Set.Icc (lo arm) (hi arm) reward) (ae (armLaw arm))) (n : Nat) : let nu := finiteArmRealRewardKernel armLaw let sigma2 := Concentration.finiteArmPositiveVarianceProxy (fun arm => Concentration.intervalVarianceProxy (lo arm) (hi arm)) 0 <= armStreamArmwiseBoundedFiniteArmExpectedRegret hK armLaw hprob lo hi n /\ armStreamArmwiseBoundedFiniteArmExpectedRegret hK armLaw hprob lo hi n <= armStreamAsymptoticModelCoefficient nu sigma2 * (1 + Real.log ((n + 1 : Nat) : Real))

Expected armwise-bounded one-policy regret normalized by `n + 1`.

noncomputable def armStreamArmwiseBoundedFiniteArmExpectedAverageRegret {K : Nat} (hK : 0 < K) (armLaw : Fin K -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Fin K -> Real) (n : Nat) : Real

Stationary finite-arm Real reward laws with arm-dependent almost-sure interval bounds induce one fixed canonical UCB process with vanishing expected average regret. Positive padding removes every pointwise interval-order premise.

theorem armStreamArmwiseBoundedFiniteArmExpectedAverageRegret_tendsto_zero {K : Nat} (hK : 0 < K) (armLaw : Fin K -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Fin K -> Real) (hbound : forall arm, Filter.Eventually (fun reward : Real => Set.Icc (lo arm) (hi arm) reward) (ae (armLaw arm))) : Tendsto (armStreamArmwiseBoundedFiniteArmExpectedAverageRegret hK armLaw hprob lo hi) atTop (nhds 0)