BanditRLProof.LowerBounds.InstanceDependent

The exact scalar asymptotic quantifier in Definition 16.1: a nonnegative regret sequence is smaller than every positive polynomial order. Regret nonnegativity is kept outside this analytic predicate so callers must expose the model-specific fact explicitly.

def IsConsistentRegret (regret : Nat -> Real) : Prop

Definition 16.1 over an abstract policy/environment regret interface. This preserves the source quantifier order: one policy, every environment in the class, and every positive real exponent.

def IsConsistentPolicyOver {Policy Environment : Type*} (environmentClass : Set Environment) (regret : Policy -> Environment -> Nat -> Real) (policy : Policy) : Prop

A finite-armed product environment whose arm laws have certified finite means. The `mean` field is intentionally tied to the Bochner integral rather than treated as an unrelated parameter: this is the source-level bridge used when an unchanged arm law must imply an unchanged arm mean.

structure FiniteMeanBanditEnvironment (K : Nat) where

The source gap `Delta_i(nu) = muStar(nu) - mu_i(nu)`.

def FiniteMeanBanditEnvironment.gap {K : Nat} (environment : FiniteMeanBanditEnvironment K) (arm : Fin K) : Real

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

theorem FiniteMeanBanditEnvironment.gap_nonneg {K : Nat} (environment : FiniteMeanBanditEnvironment K) (arm : Fin K) : 0 <= environment.gap arm

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

theorem FiniteMeanBanditEnvironment.gap_bestArm {K : Nat} (environment : FiniteMeanBanditEnvironment K) : environment.gap environment.bestArm = 0

The mean increase `lambda` of the single changed arm in Lemma 16.3.

def oneArmMeanIncrease {K : Nat} (original reference : FiniteMeanBanditEnvironment K) (changedArm : Fin K) : Real

The changed environment's advantage over the original optimal mean, `lambda - Delta_i(nu)`, in the exact second branch of Lemma 16.3's minimum.

def oneArmChangedMargin {K : Nat} (original reference : FiniteMeanBanditEnvironment K) (changedArm : Fin K) : Real

Equal arm laws have equal certified finite means.

theorem FiniteMeanBanditEnvironment.mean_eq_of_armLaw_eq {K : Nat} (first second : FiniteMeanBanditEnvironment K) (arm : Fin K) (hlaw : first.armLaw arm = second.armLaw arm) : first.mean arm = second.mean arm

The unstructured product class in Theorem 16.2: each arm law belongs to its specified component class. Finite means are certified by the environment.

def FiniteMeanBanditEnvironment.InUnstructuredClass {K : Nat} (environment : FiniteMeanBanditEnvironment K) (componentClass : Fin K → Set (Measure Real)) : Prop

Replace one arm by a finite-mean probability law whose mean exceeds the old optimum. This constructs the source alternative environment explicitly.

def FiniteMeanBanditEnvironment.withImprovedArm {K : Nat} (environment : FiniteMeanBanditEnvironment K) (changedArm : Fin K) (alternative : Measure Real) [IsProbabilityMeasure alternative] (hintegrable : Integrable id alternative) (hbetter : environment.mean environment.bestArm < ∫ x, x ∂alternative) : FiniteMeanBanditEnvironment K where

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

theorem FiniteMeanBanditEnvironment.withImprovedArm_law {K : Nat} (environment : FiniteMeanBanditEnvironment K) (changedArm : Fin K) (alternative : Measure Real) [IsProbabilityMeasure alternative] (hi : Integrable id alternative) (hb : environment.mean environment.bestArm < ∫ x, x ∂alternative) (arm : Fin K) : (environment.withImprovedArm changedArm alternative hi hb).armLaw arm = if arm = changedArm then alternative else environment.armLaw arm

The replacement arm is uniquely optimal, as required by Lemma 16.3.

theorem FiniteMeanBanditEnvironment.withImprovedArm_unique {K : Nat} (environment : FiniteMeanBanditEnvironment K) (changedArm : Fin K) (alternative : Measure Real) [IsProbabilityMeasure alternative] (hi : Integrable id alternative) (hb : environment.mean environment.bestArm < ∫ x, x ∂alternative) (arm : Fin K) (hne : arm ≠ changedArm) : (environment.withImprovedArm changedArm alternative hi hb).mean arm < (environment.withImprovedArm changedArm alternative hi hb).mean changedArm

Unstructured classes permit exactly the single-component replacement used by the source change-of-measure argument.

theorem FiniteMeanBanditEnvironment.withImprovedArm_mem {K : Nat} (environment : FiniteMeanBanditEnvironment K) (componentClass : Fin K → Set (Measure Real)) (hclass : environment.InUnstructuredClass componentClass) (changedArm : Fin K) (alternative : Measure Real) [IsProbabilityMeasure alternative] (hi : Integrable id alternative) (hb : environment.mean environment.bestArm < ∫ x, x ∂alternative) (halt : alternative ∈ componentClass changedArm) : (environment.withImprovedArm changedArm alternative hi hb).InUnstructuredClass componentClass

The source identity behind Lemma 16.3: `lambda - Delta_i(nu) = mu_i(nu') - muStar(nu)`.

theorem oneArmMeanIncrease_sub_gap_eq_changedMargin {K : Nat} (original reference : FiniteMeanBanditEnvironment K) (changedArm : Fin K) : oneArmMeanIncrease original reference changedArm - original.gap changedArm = oneArmChangedMargin original reference changedArm

Source mean-to-gap producer for a one-arm change. If the changed arm is suboptimal originally, uniquely optimal after the change, and every other arm law is unchanged, then it produces all sign and comparison obligations needed by the exact majority-event consumer for Lemma 16.3.

theorem oneArmMeanChange_produces_gap_contract {K : Nat} (original reference : FiniteMeanBanditEnvironment K) (changedArm : Fin K) (hsuboptimal : original.mean changedArm < original.mean original.bestArm) (hunique : forall arm, arm ≠ changedArm -> reference.mean arm < reference.mean changedArm) (hsame : forall arm, arm ≠ changedArm -> original.armLaw arm = reference.armLaw arm) : 0 < original.gap changedArm /\ 0 < oneArmChangedMargin original reference changedArm /\ (forall arm, arm ≠ changedArm -> oneArmChangedMargin original reference changedArm <= reference.gap arm)

An unrestricted finite vector of unit-variance Gaussian means, together with a certified optimal arm. Unlike the Chapter 15 minimax cube, Chapter 16 uses all mean vectors in `Real^k`.

structure UnitVarianceGaussianBanditEnvironment (K : Nat) where

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

def UnitVarianceGaussianBanditEnvironment.gap {K : Nat} (environment : UnitVarianceGaussianBanditEnvironment K) (arm : Fin K) : Real

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

theorem UnitVarianceGaussianBanditEnvironment.gap_nonneg {K : Nat} (environment : UnitVarianceGaussianBanditEnvironment K) (arm : Fin K) : 0 <= environment.gap arm

The finite-mean product environment induced by arbitrary unit-variance Gaussian arms.

noncomputable def UnitVarianceGaussianBanditEnvironment.toFiniteMean {K : Nat} (environment : UnitVarianceGaussianBanditEnvironment K) : FiniteMeanBanditEnvironment K where

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

theorem UnitVarianceGaussianBanditEnvironment.toFiniteMean_mean {K : Nat} (environment : UnitVarianceGaussianBanditEnvironment K) : environment.toFiniteMean.mean = environment.mean

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

theorem UnitVarianceGaussianBanditEnvironment.toFiniteMean_gap {K : Nat} (environment : UnitVarianceGaussianBanditEnvironment K) : environment.toFiniteMean.gap = environment.gap

Mean vector obtained by increasing exactly one Gaussian arm by `(1 + epsilon) Delta_i`, as in the proof of Theorem 16.4.

def chapter16GaussianChangedMean {K : Nat} (environment : UnitVarianceGaussianBanditEnvironment K) (changedArm : Fin K) (epsilon : Real) (arm : Fin K) : Real

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

theorem chapter16GaussianChangedMean_changed {K : Nat} (environment : UnitVarianceGaussianBanditEnvironment K) (changedArm : Fin K) (epsilon : Real) : chapter16GaussianChangedMean environment changedArm epsilon changedArm = environment.mean changedArm + (1 + epsilon) * environment.gap changedArm

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

theorem chapter16GaussianChangedMean_other {K : Nat} (environment : UnitVarianceGaussianBanditEnvironment K) (changedArm : Fin K) (epsilon : Real) (arm : Fin K) (harm : arm ≠ changedArm) : chapter16GaussianChangedMean environment changedArm epsilon arm = environment.mean arm

The shifted Gaussian arm is uniquely optimal whenever its original gap and `epsilon` are positive.

theorem chapter16GaussianChangedMean_uniqueBest {K : Nat} (environment : UnitVarianceGaussianBanditEnvironment K) (changedArm : Fin K) (epsilon : Real) (hgap : 0 < environment.gap changedArm) (hepsilon : 0 < epsilon) : forall arm, arm ≠ changedArm -> chapter16GaussianChangedMean environment changedArm epsilon arm < chapter16GaussianChangedMean environment changedArm epsilon changedArm

The shifted mean vector, certified with the changed arm as an optimum.

noncomputable def chapter16GaussianChangedEnvironment {K : Nat} (environment : UnitVarianceGaussianBanditEnvironment K) (changedArm : Fin K) (epsilon : Real) (hgap : 0 < environment.gap changedArm) (hepsilon : 0 < epsilon) : UnitVarianceGaussianBanditEnvironment K where

The Gaussian shift stays in the source box `[mu_j, mu_j + 2 Delta_j]` when `epsilon <= 1`.

theorem chapter16GaussianChangedMean_mem_localBox {K : Nat} (environment : UnitVarianceGaussianBanditEnvironment K) (changedArm : Fin K) (epsilon : Real) (hgap : 0 < environment.gap changedArm) (hepsilon : 0 < epsilon) (hepsilon_one : epsilon <= 1) : forall arm, chapter16GaussianChangedMean environment changedArm epsilon arm ∈ Set.Icc (environment.mean arm) (environment.mean arm + 2 * environment.gap arm)

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

theorem chapter16GaussianChangedEnvironment_uniqueBest {K : Nat} (environment : UnitVarianceGaussianBanditEnvironment K) (changedArm : Fin K) (epsilon : Real) (hgap : 0 < environment.gap changedArm) (hepsilon : 0 < epsilon) : forall arm, arm ≠ changedArm -> (chapter16GaussianChangedEnvironment environment changedArm epsilon hgap hepsilon).mean arm < (chapter16GaussianChangedEnvironment environment changedArm epsilon hgap hepsilon).mean changedArm

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

theorem chapter16GaussianChangedEnvironment_sameArmLaw {K : Nat} (environment : UnitVarianceGaussianBanditEnvironment K) (changedArm : Fin K) (epsilon : Real) (hgap : 0 < environment.gap changedArm) (hepsilon : 0 < epsilon) : forall arm, arm ≠ changedArm -> environment.toFiniteMean.armLaw arm = (chapter16GaussianChangedEnvironment environment changedArm epsilon hgap hepsilon).toFiniteMean.armLaw arm

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

theorem chapter16GaussianChangedEnvironment_meanIncrease {K : Nat} (environment : UnitVarianceGaussianBanditEnvironment K) (changedArm : Fin K) (epsilon : Real) (hgap : 0 < environment.gap changedArm) (hepsilon : 0 < epsilon) : oneArmMeanIncrease environment.toFiniteMean (chapter16GaussianChangedEnvironment environment changedArm epsilon hgap hepsilon).toFiniteMean changedArm = (1 + epsilon) * environment.gap changedArm

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

theorem chapter16GaussianChangedEnvironment_changedMargin {K : Nat} (environment : UnitVarianceGaussianBanditEnvironment K) (changedArm : Fin K) (epsilon : Real) (hgap : 0 < environment.gap changedArm) (hepsilon : 0 < epsilon) : oneArmChangedMargin environment.toFiniteMean (chapter16GaussianChangedEnvironment environment changedArm epsilon hgap hepsilon).toFiniteMean changedArm = epsilon * environment.gap changedArm

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

theorem chapter16GaussianChangedEnvironment_armKL {K : Nat} (environment : UnitVarianceGaussianBanditEnvironment K) (changedArm : Fin K) (epsilon : Real) (hgap : 0 < environment.gap changedArm) (hepsilon : 0 < epsilon) : InformationTheory.klDiv (environment.toFiniteMean.armLaw changedArm) ((chapter16GaussianChangedEnvironment environment changedArm epsilon hgap hepsilon).toFiniteMean.armLaw changedArm) = ENNReal.ofReal (((1 + epsilon) * environment.gap changedArm) ^ 2 / 2)

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

theorem chapter16GaussianChangedEnvironment_armKL_toReal {K : Nat} (environment : UnitVarianceGaussianBanditEnvironment K) (changedArm : Fin K) (epsilon : Real) (hgap : 0 < environment.gap changedArm) (hepsilon : 0 < epsilon) : (InformationTheory.klDiv (environment.toFiniteMean.armLaw changedArm) ((chapter16GaussianChangedEnvironment environment changedArm epsilon hgap hepsilon).toFiniteMean.armLaw changedArm)).toReal = ((1 + epsilon) * environment.gap changedArm) ^ 2 / 2

Membership in the local Gaussian class `E(nu)` of Theorem 16.4.

def InChapter16GaussianLocalClass {K : Nat} (base candidate : UnitVarianceGaussianBanditEnvironment K) : Prop

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

theorem inChapter16GaussianLocalClass_self {K : Nat} (environment : UnitVarianceGaussianBanditEnvironment K) : InChapter16GaussianLocalClass environment environment

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

theorem inChapter16GaussianLocalClass_changed {K : Nat} (environment : UnitVarianceGaussianBanditEnvironment K) (changedArm : Fin K) (epsilon : Real) (hgap : 0 < environment.gap changedArm) (hepsilon : 0 < epsilon) (hepsilon_one : epsilon <= 1) : InChapter16GaussianLocalClass environment (chapter16GaussianChangedEnvironment environment changedArm epsilon hgap hepsilon)

The sum of two source-consistent regret sequences is still consistent. This is the closure step used for `R_n(nu) + R_n(nu')` in the proof of Theorem 16.2.

theorem IsConsistentRegret.add {first second : Nat -> Real} (hfirst : IsConsistentRegret first) (hsecond : IsConsistentRegret second) : IsConsistentRegret (fun n => first n + second n)

Two consistent regret sequences are eventually at most `n^p` for every positive exponent `p`. This is a stronger eventual form of the source's auxiliary `C_p n^p` bound and avoids introducing an opaque constant.

theorem IsConsistentRegret.eventually_add_le_rpow {first second : Nat -> Real} (hfirst : IsConsistentRegret first) (hsecond : IsConsistentRegret second) {p : Real} (hp : 0 < p) : ∀ᶠ n : Nat in atTop, first n + second n <= (n : Real) ^ p

Eventually, the logarithmic growth ratio of a positive sum of two consistent regrets is at most every positive exponent. This is the direction-correct analytic leaf used before the source takes a limsup.

theorem IsConsistentRegret.eventually_log_add_div_log_le {first second : Nat -> Real} (hfirst : IsConsistentRegret first) (hsecond : IsConsistentRegret second) (hpositive : ∀ᶠ n : Nat in atTop, 0 < first n + second n) {p : Real} (hp : 0 < p) : ∀ᶠ n : Nat in atTop, Real.log (first n + second n) / Real.log n <= p

Consistency extracts every strict reciprocal-information lower bound from the source logarithmic inequality. This eventual form does not assume that the normalized pull counts converge.

theorem IsConsistentRegret.eventually_pull_div_log_ge {first second pulls : Nat → Real} {c d r : Real} (hfirst : IsConsistentRegret first) (hsecond : IsConsistentRegret second) (hpositive : ∀ᶠ n in atTop, 0 < first n + second n) (hd : 0 < d) (hr : r < 1 / d) (hsource : ∀ᶠ n : Nat in atTop, (c + Real.log n - Real.log (first n + second n)) / d ≤ pulls n) : ∀ᶠ n in atTop, r ≤ pulls n / Real.log n

The finite-positive information branch in extended-real liminf form. The conclusion allows infinite normalized pull growth.

theorem IsConsistentRegret.liminf_pull_div_log_ge {first second pulls : Nat → Real} {c d : Real} (hfirst : IsConsistentRegret first) (hsecond : IsConsistentRegret second) (hpositive : ∀ᶠ n in atTop, 0 < first n + second n) (hd : 0 < d) (hsource : ∀ᶠ n : Nat in atTop, (c + Real.log n - Real.log (first n + second n)) / d ≤ pulls n) : ENNReal.ofReal (1 / d) ≤ liminf (fun n : Nat => ENNReal.ofReal (pulls n / Real.log n)) atTop

The source quantity `d_inf(P, muStar, M) = inf {D(P,P') : P' in M, mean(P') > muStar}`. The value is extended-real, so an empty alternative set has infimum `∞` and support failures remain visible.

def divergenceInfimum {Reward : Type*} [MeasurableSpace Reward] (P : Measure Reward) (muStar : Real) (distributionClass : Set (Measure Reward)) (mean : Measure Reward -> Real) : ENNReal

Any admissible confusing alternative upper-bounds `d_inf`, with KL in the source direction from the original law to the alternative law.

theorem divergenceInfimum_le {Reward : Type*} [MeasurableSpace Reward] {P P' : Measure Reward} {muStar : Real} {distributionClass : Set (Measure Reward)} {mean : Measure Reward -> Real} (hclass : P' ∈ distributionClass) (hbetter : muStar < mean P') : divergenceInfimum P muStar distributionClass mean <= relativeEntropy P P'

Every strict upper bound on `d_inf` admits a confusing alternative below that bound. No minimizer or finite positive infimum is assumed.

theorem divergenceInfimum_exists_alternative_lt {Reward : Type*} [MeasurableSpace Reward] {P : Measure Reward} {muStar : Real} {distributionClass : Set (Measure Reward)} {mean : Measure Reward -> Real} {bound : ENNReal} (hbound : divergenceInfimum P muStar distributionClass mean < bound) : ∃ P', P' ∈ distributionClass ∧ muStar < mean P' ∧ relativeEntropy P P' < bound

Lift a near-infimum arm law to an admissible product environment. The component classes consist of finite-mean probability laws, exactly as in Theorem 16.2; the information cost stays in `ENNReal`.

theorem FiniteMeanBanditEnvironment.exists_confusingEnvironment_lt {K : Nat} (environment : FiniteMeanBanditEnvironment K) (componentClass : Fin K → Set (Measure Real)) (hclass : environment.InUnstructuredClass componentClass) (hfinite : ∀ arm P, P ∈ componentClass arm → IsProbabilityMeasure P ∧ Integrable id P) (changedArm : Fin K) {bound : ENNReal} (hbound : divergenceInfimum (environment.armLaw changedArm) (environment.mean environment.bestArm) (componentClass changedArm) (fun P => ∫ x, x ∂P) < bound) : ∃ reference : FiniteMeanBanditEnvironment K, reference.InUnstructuredClass componentClass ∧ (∀ arm, arm ≠ changedArm → environment.armLaw arm = reference.armLaw arm) ∧ (∀ arm, arm ≠ changedArm → reference.mean arm < reference.mean changedArm) ∧ relativeEntropy (environment.armLaw changedArm) (reference.armLaw changedArm) < bound

The infinite branch includes both an empty alternative class and classes whose every confusing alternative has infinite directed KL.

theorem divergenceInfimum_eq_top_iff {Reward : Type*} [MeasurableSpace Reward] {P : Measure Reward} {muStar : Real} {distributionClass : Set (Measure Reward)} {mean : Measure Reward -> Real} : divergenceInfimum P muStar distributionClass mean = ⊤ ↔ ∀ P', P' ∈ distributionClass → muStar < mean P' → relativeEntropy P P' = ⊤

Parameterized form of `d_inf`, useful when a distribution class is presented by a family of laws rather than an injective set-level mean map.

def parametricDivergenceInfimum {Reward Parameter : Type*} [MeasurableSpace Reward] (law : Parameter -> Measure Reward) (mean : Parameter -> Real) (parameter : Parameter) (muStar : Real) : ENNReal

Candidate inequality for the parameterized `d_inf` surface.

theorem parametricDivergenceInfimum_le {Reward Parameter : Type*} [MeasurableSpace Reward] {law : Parameter -> Measure Reward} {mean : Parameter -> Real} {parameter alternative : Parameter} {muStar : Real} (hbetter : muStar < mean alternative) : parametricDivergenceInfimum law mean parameter muStar <= relativeEntropy (law parameter) (law alternative)

Unit-variance Gaussian specialization of the source `d_inf`.

abbrev unitGaussianDivergenceInfimum (mu muStar : Real) : ENNReal

A Gaussian alternative with mean `muStar + epsilon` is admissible and has the exact arm-level information cost shown here. Taking `epsilon -> 0` is a separate infimum/limit leaf and is not hidden in this theorem.

theorem unitGaussianDivergenceInfimum_le_perturbed (mu muStar epsilon : Real) (hepsilon : 0 < epsilon) : unitGaussianDivergenceInfimum mu muStar <= ENNReal.ofReal (((muStar - mu) + epsilon) ^ 2 / 2)

Every strictly better unit-Gaussian alternative costs at least the boundary value from Table 16.1.

theorem unitGaussianDivergenceInfimum_ge (mu muStar : Real) (hmu : mu < muStar) : ENNReal.ofReal ((muStar - mu) ^ 2 / 2) <= unitGaussianDivergenceInfimum mu muStar

Exact unit-variance Gaussian row of Table 16.1. The strict alternative mean means the boundary law is not itself admissible; the reverse inequality is obtained from positive perturbations tending to zero.

theorem unitGaussianDivergenceInfimum_eq (mu muStar : Real) (hmu : mu < muStar) : unitGaussianDivergenceInfimum mu muStar = ENNReal.ofReal ((muStar - mu) ^ 2 / 2)

Chapter 16's one-arm change-of-measure specialization of Lemma 15.1. When two stationary bandit environments differ only at `changedArm`, the directed relative entropy of their finite histories is exactly the first-environment expected number of pulls of that arm times its arm-law relative entropy. The algorithm is one common, possibly randomized, nonanticipating history policy in both environments.

theorem banditHistoryRelativeEntropy_eq_expectedPulls_mul_of_only_arm_changed {K : Nat} {Reward : Type*} [MeasurableSpace Reward] [MeasurableSpace.CountablyGenerated Reward] (algorithm : Thompson.HistoryAlgorithm (Fin K) Reward) (armLaw referenceArmLaw : Kernel (Fin K) Reward) [IsMarkovKernel armLaw] [IsMarkovKernel referenceArmLaw] (changedArm : Fin K) (lastRound : Nat) (hsame : forall arm, arm ≠ changedArm -> armLaw arm = referenceArmLaw arm) : InformationTheory.klDiv (canonicalBanditHistoryMeasure algorithm armLaw lastRound) (canonicalBanditHistoryMeasure algorithm referenceArmLaw lastRound) = canonicalRealizedExpectedPullCountThrough algorithm armLaw lastRound changedArm * InformationTheory.klDiv (armLaw changedArm) (referenceArmLaw changedArm)

The source majority event `A = {T_i(n) > n/2}` in the repository's inclusive convention, where `lastRound` contains `lastRound + 1` pulls.

def oneArmMajorityPullEvent {K : Nat} {Reward : Type*} (changedArm : Fin K) (lastRound : Nat) : Set (History.FinitePairHistory (Fin K) Reward lastRound)

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

theorem measurableSet_oneArmMajorityPullEvent {K : Nat} {Reward : Type*} [MeasurableSpace Reward] (changedArm : Fin K) (lastRound : Nat) : MeasurableSet (oneArmMajorityPullEvent (Reward := Reward) changedArm lastRound)

Gap-times-pull-count pseudo-regret on one realized finite history. The gap vector is kept explicit so the later Chapter 16 environment layer must identify it with `muStar - mu_i`; no scalar regret hypothesis is hidden here.

noncomputable def finiteHistoryGapPseudoRegret {K : Nat} {Reward : Type*} (gap : Fin K -> Real) (lastRound : Nat) (history : History.FinitePairHistory (Fin K) Reward lastRound) : ENNReal

Expected gap pseudo-regret under the canonical law generated by one possibly randomized history policy and one stationary arm kernel.

noncomputable def canonicalGapExpectedPseudoRegret {K : Nat} {Reward : Type*} [MeasurableSpace Reward] [MeasurableSpace.CountablyGenerated Reward] (algorithm : Thompson.HistoryAlgorithm (Fin K) Reward) (armLaw : Kernel (Fin K) Reward) [IsMarkovKernel armLaw] (gap : Fin K -> Real) (lastRound : Nat) : ENNReal

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

theorem measurable_finiteHistoryGapPseudoRegret {K : Nat} {Reward : Type*} [MeasurableSpace Reward] (gap : Fin K -> Real) (lastRound : Nat) : Measurable (finiteHistoryGapPseudoRegret (Reward := Reward) gap lastRound)

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

theorem finiteHistoryGapPseudoRegret_ne_top {K : Nat} {Reward : Type*} (gap : Fin K -> Real) (lastRound : Nat) (history : History.FinitePairHistory (Fin K) Reward lastRound) : finiteHistoryGapPseudoRegret gap lastRound history ≠ ∞

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

theorem finiteHistoryGapPseudoRegret_toReal {K : Nat} {Reward : Type*} (gap : Fin K -> Real) (lastRound : Nat) (history : History.FinitePairHistory (Fin K) Reward lastRound) (hgap : forall arm, 0 <= gap arm) : (finiteHistoryGapPseudoRegret gap lastRound history).toReal = ∑ arm : Fin K, gap arm * finiteHistoryPullCountReal lastRound history arm

The expected realized pull counts of all arms sum to the inclusive horizon for every Markov arm kernel, not only for the Gaussian Chapter 15 instance.

theorem sum_canonicalRealizedExpectedPullCountThrough_general {K : Nat} {Reward : Type*} [MeasurableSpace Reward] [MeasurableSpace.CountablyGenerated Reward] (algorithm : Thompson.HistoryAlgorithm (Fin K) Reward) (armLaw : Kernel (Fin K) Reward) [IsMarkovKernel armLaw] (lastRound : Nat) : ∑ arm : Fin K, canonicalRealizedExpectedPullCountThrough algorithm armLaw lastRound arm = lastRound + 1

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

theorem canonicalRealizedExpectedPullCountThrough_ne_top {K : Nat} {Reward : Type*} [MeasurableSpace Reward] [MeasurableSpace.CountablyGenerated Reward] (algorithm : Thompson.HistoryAlgorithm (Fin K) Reward) (armLaw : Kernel (Fin K) Reward) [IsMarkovKernel armLaw] (lastRound : Nat) (arm : Fin K) : canonicalRealizedExpectedPullCountThrough algorithm armLaw lastRound arm ≠ ∞

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

theorem canonicalGapExpectedPseudoRegret_eq_sum_expectedPulls {K : Nat} {Reward : Type*} [MeasurableSpace Reward] [MeasurableSpace.CountablyGenerated Reward] (algorithm : Thompson.HistoryAlgorithm (Fin K) Reward) (armLaw : Kernel (Fin K) Reward) [IsMarkovKernel armLaw] (gap : Fin K -> Real) (lastRound : Nat) : canonicalGapExpectedPseudoRegret algorithm armLaw gap lastRound = ∑ arm : Fin K, ENNReal.ofReal (gap arm) * canonicalRealizedExpectedPullCountThrough algorithm armLaw lastRound arm

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

theorem canonicalGapExpectedPseudoRegret_ne_top {K : Nat} {Reward : Type*} [MeasurableSpace Reward] [MeasurableSpace.CountablyGenerated Reward] (algorithm : Thompson.HistoryAlgorithm (Fin K) Reward) (armLaw : Kernel (Fin K) Reward) [IsMarkovKernel armLaw] (gap : Fin K -> Real) (lastRound : Nat) : canonicalGapExpectedPseudoRegret algorithm armLaw gap lastRound ≠ ∞

Real-valued presentation of the finite expected pseudo-regret. Finiteness is proved above rather than assumed by the Chapter 16 consumer.

noncomputable def canonicalGapExpectedPseudoRegretReal {K : Nat} {Reward : Type*} [MeasurableSpace Reward] [MeasurableSpace.CountablyGenerated Reward] (algorithm : Thompson.HistoryAlgorithm (Fin K) Reward) (armLaw : Kernel (Fin K) Reward) [IsMarkovKernel armLaw] (gap : Fin K -> Real) (lastRound : Nat) : Real

Real-valued gap-times-expected-pulls decomposition. This is the precise finite-horizon form used when Theorem 16.4 sums its per-arm lower bounds.

theorem canonicalGapExpectedPseudoRegretReal_eq_sum_expectedPulls {K : Nat} {Reward : Type*} [MeasurableSpace Reward] [MeasurableSpace.CountablyGenerated Reward] (algorithm : Thompson.HistoryAlgorithm (Fin K) Reward) (armLaw : Kernel (Fin K) Reward) [IsMarkovKernel armLaw] (gap : Fin K -> Real) (hgap : forall arm, 0 <= gap arm) (lastRound : Nat) : canonicalGapExpectedPseudoRegretReal algorithm armLaw gap lastRound = ∑ arm : Fin K, gap arm * (canonicalRealizedExpectedPullCountThrough algorithm armLaw lastRound arm).toReal

Expected pseudo-regret of an unrestricted unit-variance Gaussian environment in the Chapter 16 gap-times-pulls convention.

noncomputable def unitVarianceGaussianExpectedPseudoRegret {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (environment : UnitVarianceGaussianBanditEnvironment K) (lastRound : Nat) : Real

On the source majority event, the original environment pays at least half the horizon times the changed arm's positive gap.

theorem oneArmMajority_forces_gapPseudoRegret {K : Nat} {Reward : Type*} (gap : Fin K -> Real) (hgap : forall arm, 0 <= gap arm) (changedArm : Fin K) (hchanged : 0 < gap changedArm) (lastRound : Nat) (history : History.FinitePairHistory (Fin K) Reward lastRound) (hA : history ∈ oneArmMajorityPullEvent (Reward := Reward) changedArm lastRound) : ENNReal.ofReal (((lastRound + 1 : Nat) : Real) * gap changedArm / 2) <= finiteHistoryGapPseudoRegret gap lastRound history

On the complement of the majority event, every non-changed arm charged by at least `changedMargin` forces half-horizon pseudo-regret.

theorem oneArmMajority_compl_forces_gapPseudoRegret {K : Nat} {Reward : Type*} (gap : Fin K -> Real) (hgap : forall arm, 0 <= gap arm) (changedArm : Fin K) (changedMargin : Real) (hmargin : 0 < changedMargin) (hother : forall arm, arm ≠ changedArm -> changedMargin <= gap arm) (lastRound : Nat) (history : History.FinitePairHistory (Fin K) Reward lastRound) (hAc : history ∈ (oneArmMajorityPullEvent (Reward := Reward) changedArm lastRound)ᶜ) : ENNReal.ofReal (((lastRound + 1 : Nat) : Real) * changedMargin / 2) <= finiteHistoryGapPseudoRegret gap lastRound history

Original-environment event probability charged to the actual canonical gap pseudo-regret.

theorem oneArmMajority_probability_charge_le_expectedPseudoRegret {K : Nat} {Reward : Type*} [MeasurableSpace Reward] [MeasurableSpace.CountablyGenerated Reward] (algorithm : Thompson.HistoryAlgorithm (Fin K) Reward) (armLaw : Kernel (Fin K) Reward) [IsMarkovKernel armLaw] (gap : Fin K -> Real) (hgap : forall arm, 0 <= gap arm) (changedArm : Fin K) (hchanged : 0 < gap changedArm) (lastRound : Nat) : ((lastRound + 1 : Nat) : Real) * gap changedArm / 2 * (canonicalBanditHistoryMeasure algorithm armLaw lastRound).real (oneArmMajorityPullEvent (Reward := Reward) changedArm lastRound) <= canonicalGapExpectedPseudoRegretReal algorithm armLaw gap lastRound

Changed-environment complement probability charged to the actual canonical gap pseudo-regret.

theorem oneArmMajority_compl_probability_charge_le_expectedPseudoRegret {K : Nat} {Reward : Type*} [MeasurableSpace Reward] [MeasurableSpace.CountablyGenerated Reward] (algorithm : Thompson.HistoryAlgorithm (Fin K) Reward) (armLaw : Kernel (Fin K) Reward) [IsMarkovKernel armLaw] (gap : Fin K -> Real) (hgap : forall arm, 0 <= gap arm) (changedArm : Fin K) (changedMargin : Real) (hmargin : 0 < changedMargin) (hother : forall arm, arm ≠ changedArm -> changedMargin <= gap arm) (lastRound : Nat) : ((lastRound + 1 : Nat) : Real) * changedMargin / 2 * (canonicalBanditHistoryMeasure algorithm armLaw lastRound).real (oneArmMajorityPullEvent (Reward := Reward) changedArm lastRound)ᶜ <= canonicalGapExpectedPseudoRegretReal algorithm armLaw gap lastRound

Chapter 16's measurable-event information constraint before regret calibration. It instantiates Bretagnolle--Huber on the exact majority event and rewrites the full history KL using the compiled one-arm specialization of Lemma 15.1.

theorem bretagnolleHuberScale_expectedPulls_mul_armKL_le_majorityErrors {K : Nat} {Reward : Type*} [MeasurableSpace Reward] [MeasurableSpace.CountablyGenerated Reward] (algorithm : Thompson.HistoryAlgorithm (Fin K) Reward) (armLaw referenceArmLaw : Kernel (Fin K) Reward) [IsMarkovKernel armLaw] [IsMarkovKernel referenceArmLaw] (changedArm : Fin K) (lastRound : Nat) (hsame : forall arm, arm ≠ changedArm -> armLaw arm = referenceArmLaw arm) : bretagnolleHuberScale (canonicalRealizedExpectedPullCountThrough algorithm armLaw lastRound changedArm * InformationTheory.klDiv (armLaw changedArm) (referenceArmLaw changedArm)) <= (canonicalBanditHistoryMeasure algorithm armLaw lastRound).real (oneArmMajorityPullEvent (Reward := Reward) changedArm lastRound) + (canonicalBanditHistoryMeasure algorithm referenceArmLaw lastRound).real (oneArmMajorityPullEvent (Reward := Reward) changedArm lastRound)ᶜ

Finite-information evaluation of the testing scale used when Chapter 16 passes from extended-real KL to the real logarithmic inequality.

theorem bretagnolleHuberScale_mul_eq_exp {expectedPull armInformation : ENNReal} (hpull : expectedPull ≠ ∞) (hinformation : armInformation ≠ ∞) : bretagnolleHuberScale (expectedPull * armInformation) = (1 / 2 : Real) * Real.exp (-(expectedPull.toReal * armInformation.toReal))

Deterministic assembly of the two majority-event regret charges with the Bretagnolle--Huber testing error.

theorem exp_testing_bound_of_majority_regret_bounds (expectedPull information gap changedMargin horizon originalError changedError originalRegret changedRegret : Real) (hgap : 0 < gap) (hmargin : 0 < changedMargin) (hhorizon : 0 < horizon) (horiginalError : 0 <= originalError) (hchangedError : 0 <= changedError) (htesting : (1 / 2 : Real) * Real.exp (-(expectedPull * information)) <= originalError + changedError) (horiginalRegret : horizon * gap / 2 * originalError <= originalRegret) (hchangedRegret : horizon * changedMargin / 2 * changedError <= changedRegret) : horizon * min gap changedMargin / 4 * Real.exp (-(expectedPull * information)) <= originalRegret + changedRegret

The exact logarithmic rearrangement used in Lemma 16.3. This theorem is only the scalar consumer of the testing inequality; the bandit theorem must still produce `htesting` from the common-policy history law, the majority event, and the two expected pseudo-regrets.

theorem expectedPullCount_ge_log_regret_of_exp_testing_bound (expectedPull information gap changedMargin horizon regretSum : Real) (hinformation : 0 < information) (hgap : 0 < gap) (hmargin : 0 < changedMargin) (hhorizon : 0 < horizon) (htesting : horizon * min gap changedMargin / 4 * Real.exp (-(expectedPull * information)) <= regretSum) : (Real.log (min gap changedMargin / 4) + Real.log horizon - Real.log regretSum) / information <= expectedPull

Chapter 16's finite-time change-of-measure calculation with the actual canonical gap pseudo-regrets produced above. This closes the common-policy, one-arm-KL, majority-event, exact `1/4`, and logarithmic assembly route for explicit nonnegative gap vectors. It is intentionally not named as source Lemma 16.3: a later environment layer must still prove that these vectors are the mean gaps of finite-mean arm laws and discharge the finite-positive-KL branch from that source contract.

theorem expectedPullCount_ge_log_gapPseudoRegret_of_only_arm_changed {K : Nat} {Reward : Type*} [MeasurableSpace Reward] [MeasurableSpace.CountablyGenerated Reward] (algorithm : Thompson.HistoryAlgorithm (Fin K) Reward) (armLaw referenceArmLaw : Kernel (Fin K) Reward) [IsMarkovKernel armLaw] [IsMarkovKernel referenceArmLaw] (originalGap referenceGap : Fin K -> Real) (horiginalGap : forall arm, 0 <= originalGap arm) (hreferenceGap : forall arm, 0 <= referenceGap arm) (changedArm : Fin K) (changedMargin : Real) (hchangedGap : 0 < originalGap changedArm) (hmargin : 0 < changedMargin) (hother : forall arm, arm ≠ changedArm -> changedMargin <= referenceGap arm) (lastRound : Nat) (hsame : forall arm, arm ≠ changedArm -> armLaw arm = referenceArmLaw arm) (hinformation_ne_top : InformationTheory.klDiv (armLaw changedArm) (referenceArmLaw changedArm) ≠ ∞) (hinformation_pos : 0 < (InformationTheory.klDiv (armLaw changedArm) (referenceArmLaw changedArm)).toReal) : (Real.log (min (originalGap changedArm) changedMargin / 4) + Real.log ((lastRound + 1 : Nat) : Real) - Real.log (canonicalGapExpectedPseudoRegretReal algorithm armLaw originalGap lastRound + canonicalGapExpectedPseudoRegretReal algorithm referenceArmLaw referenceGap lastRound)) / (InformationTheory.klDiv (armLaw changedArm) (referenceArmLaw changedArm)).toReal <= (canonicalRealizedExpectedPullCountThrough algorithm armLaw lastRound changedArm).toReal

The two regrets in the one-arm testing construction cannot both vanish when arm KL is finite and both source gaps are positive.

theorem gapPseudoRegret_add_pos_of_only_arm_changed {K : Nat} {Reward : Type*} [MeasurableSpace Reward] [MeasurableSpace.CountablyGenerated Reward] (algorithm : Thompson.HistoryAlgorithm (Fin K) Reward) (armLaw referenceArmLaw : Kernel (Fin K) Reward) [IsMarkovKernel armLaw] [IsMarkovKernel referenceArmLaw] (originalGap referenceGap : Fin K -> Real) (horiginalGap : forall arm, 0 <= originalGap arm) (hreferenceGap : forall arm, 0 <= referenceGap arm) (changedArm : Fin K) (changedMargin : Real) (hchangedGap : 0 < originalGap changedArm) (hmargin : 0 < changedMargin) (hother : forall arm, arm ≠ changedArm -> changedMargin <= referenceGap arm) (lastRound : Nat) (hsame : forall arm, arm ≠ changedArm -> armLaw arm = referenceArmLaw arm) (hinformation_ne_top : InformationTheory.klDiv (armLaw changedArm) (referenceArmLaw changedArm) ≠ ∞) : 0 < canonicalGapExpectedPseudoRegretReal algorithm armLaw originalGap lastRound + canonicalGapExpectedPseudoRegretReal algorithm referenceArmLaw referenceGap lastRound

*Lattimore--Szepesvári, Lemma 16.3.** This is the exact source one-arm change-of-measure inequality for finite-mean product environments. The denominator is presented through `ENNReal.toReal`; when arm KL is infinite this evaluates the source convention `x / ∞ = 0`. The zero-KL case is impossible here because the changed arm has different certified finite means.

theorem expectedPullCount_ge_log_regret_changeOfMeasure {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (original reference : FiniteMeanBanditEnvironment K) (changedArm : Fin K) (hsuboptimal : original.mean changedArm < original.mean original.bestArm) (hunique : forall arm, arm ≠ changedArm -> reference.mean arm < reference.mean changedArm) (hsame : forall arm, arm ≠ changedArm -> original.armLaw arm = reference.armLaw arm) (lastRound : Nat) : (Real.log (min (oneArmMeanIncrease original reference changedArm - original.gap changedArm) (original.gap changedArm) / 4) + Real.log ((lastRound + 1 : Nat) : Real) - Real.log (canonicalGapExpectedPseudoRegretReal algorithm original.armLaw original.gap lastRound + canonicalGapExpectedPseudoRegretReal algorithm reference.armLaw reference.gap lastRound)) / (InformationTheory.klDiv (original.armLaw changedArm) (reference.armLaw changedArm)).toReal <= (canonicalRealizedExpectedPullCountThrough algorithm original.armLaw lastRound changedArm).toReal

Expected regret after exactly `n` pulls, including the empty horizon.

def finiteMeanExpectedRegret {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (environment : FiniteMeanBanditEnvironment K) : Nat → Real | 0 => 0 | n + 1 => canonicalGapExpectedPseudoRegretReal algorithm environment.armLaw environment.gap n /-- Expected pull count after exactly `n` pulls, including the empty horizon. -/ def finiteMeanExpectedPullCount {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (environment : FiniteMeanBanditEnvironment K) (arm : Fin K) : Nat → Real | 0 => 0 | n + 1 => (canonicalRealizedExpectedPullCountThrough algorithm environment.armLaw n arm).toReal theorem finiteMeanExpectedPullCount_nonneg {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (environment : FiniteMeanBanditEnvironment K) (arm : Fin K) (n : Nat) : 0 ≤ finiteMeanExpectedPullCount algorithm environment arm n

Expected pull count after exactly `n` pulls, including the empty horizon.

def finiteMeanExpectedPullCount {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (environment : FiniteMeanBanditEnvironment K) (arm : Fin K) : Nat → Real | 0 => 0 | n + 1 => (canonicalRealizedExpectedPullCountThrough algorithm environment.armLaw n arm).toReal theorem finiteMeanExpectedPullCount_nonneg {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (environment : FiniteMeanBanditEnvironment K) (arm : Fin K) (n : Nat) : 0 ≤ finiteMeanExpectedPullCount algorithm environment arm n

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

theorem finiteMeanExpectedPullCount_nonneg {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (environment : FiniteMeanBanditEnvironment K) (arm : Fin K) (n : Nat) : 0 ≤ finiteMeanExpectedPullCount algorithm environment arm n

Source regret decomposition with the exact number-of-pulls horizon.

theorem finiteMeanExpectedRegret_eq_sum {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (environment : FiniteMeanBanditEnvironment K) (n : Nat) : finiteMeanExpectedRegret algorithm environment n = ∑ arm, environment.gap arm * finiteMeanExpectedPullCount algorithm environment arm n

Extended-real normalization of the source regret decomposition.

theorem finiteMeanNormalizedRegret_eq_sum {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (environment : FiniteMeanBanditEnvironment K) (n : Nat) (hn : 1 < n) : ENNReal.ofReal (finiteMeanExpectedRegret algorithm environment n / Real.log n) = ∑ arm, ENNReal.ofReal (environment.gap arm) * ENNReal.ofReal (finiteMeanExpectedPullCount algorithm environment arm n / Real.log n)

Theorem 16.2's per-alternative information constraint for finite KL. Consistency is imposed on the actual regret sequences of the two environments, and the conclusion uses the original-law pull count.

theorem consistentRegret_liminf_expectedPull_div_log_ge_of_alternative {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (original reference : FiniteMeanBanditEnvironment K) (changedArm : Fin K) (hsuboptimal : original.mean changedArm < original.mean original.bestArm) (hunique : ∀ arm, arm ≠ changedArm → reference.mean arm < reference.mean changedArm) (hsame : ∀ arm, arm ≠ changedArm → original.armLaw arm = reference.armLaw arm) (hfirst : IsConsistentRegret (finiteMeanExpectedRegret algorithm original)) (hsecond : IsConsistentRegret (finiteMeanExpectedRegret algorithm reference)) (hfinite : InformationTheory.klDiv (original.armLaw changedArm) (reference.armLaw changedArm) ≠ ∞) : ENNReal.ofReal (1 / (InformationTheory.klDiv (original.armLaw changedArm) (reference.armLaw changedArm)).toReal) ≤ liminf (fun n : Nat => ENNReal.ofReal (finiteMeanExpectedPullCount algorithm original changedArm n / Real.log n)) atTop

The exact per-arm information constraint supporting Theorem 16.2. The inverse infimum remains extended-real: zero infimum forces infinite liminf, while an empty or all-infinite alternative class contributes zero.

theorem consistentPolicy_liminf_expectedPull_div_log_ge_inv_dInf {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (componentClass : Fin K → Set (Measure Real)) (hfinite : ∀ arm P, P ∈ componentClass arm → IsProbabilityMeasure P ∧ Integrable id P) (hconsistent : IsConsistentPolicyOver {environment : FiniteMeanBanditEnvironment K | environment.InUnstructuredClass componentClass} finiteMeanExpectedRegret algorithm) (original : FiniteMeanBanditEnvironment K) (hclass : original.InUnstructuredClass componentClass) (changedArm : Fin K) (hsuboptimal : original.mean changedArm < original.mean original.bestArm) : (divergenceInfimum (original.armLaw changedArm) (original.mean original.bestArm) (componentClass changedArm) (fun P => ∫ x, x ∂P))⁻¹ ≤ liminf (fun n : Nat => ENNReal.ofReal (finiteMeanExpectedPullCount algorithm original changedArm n / Real.log n)) atTop

*Lattimore--Szepesvári, Theorem 16.2.** The unstructured finite-mean product-class regret lower bound, including zero and infinite information costs. All quotients and the liminf are extended-real.

theorem consistentPolicy_liminf_expectedRegret_div_log_ge {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (componentClass : Fin K → Set (Measure Real)) (hfinite : ∀ arm P, P ∈ componentClass arm → IsProbabilityMeasure P ∧ Integrable id P) (hconsistent : IsConsistentPolicyOver {environment : FiniteMeanBanditEnvironment K | environment.InUnstructuredClass componentClass} finiteMeanExpectedRegret algorithm) (original : FiniteMeanBanditEnvironment K) (hclass : original.InUnstructuredClass componentClass) : (∑ arm : Fin K with 0 < original.gap arm, ENNReal.ofReal (original.gap arm) / divergenceInfimum (original.armLaw arm) (original.mean original.bestArm) (componentClass arm) (fun P => ∫ x, x ∂P)) ≤ liminf (fun n : Nat => ENNReal.ofReal (finiteMeanExpectedRegret algorithm original n / Real.log n)) atTop

Per-arm finite-time Gaussian consequence used in Theorem 16.4, before summing and taking positive parts. Both regret bounds are retained explicitly so the published `2 C n^p` denominator is visible.

theorem gaussianExpectedPullCount_ge_finiteTimeInstanceDependent {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (environment : UnitVarianceGaussianBanditEnvironment K) (changedArm : Fin K) (epsilon C p : Real) (hgap : 0 < environment.gap changedArm) (hepsilon : 0 < epsilon) (hepsilon_one : epsilon <= 1) (_hC : 0 < C) (lastRound : Nat) (hbase : unitVarianceGaussianExpectedPseudoRegret algorithm environment lastRound <= C * (((lastRound + 1 : Nat) : Real) ^ p)) (hchanged : unitVarianceGaussianExpectedPseudoRegret algorithm (chapter16GaussianChangedEnvironment environment changedArm epsilon hgap hepsilon) lastRound <= C * (((lastRound + 1 : Nat) : Real) ^ p)) : (Real.log (epsilon * environment.gap changedArm / 4) + Real.log ((lastRound + 1 : Nat) : Real) - Real.log (2 * C * (((lastRound + 1 : Nat) : Real) ^ p))) / (((1 + epsilon) * environment.gap changedArm) ^ 2 / 2) <= (canonicalRealizedExpectedPullCountThrough algorithm (unitGaussianKernel environment.mean) lastRound changedArm).toReal

Exact logarithmic normalization in the displayed bound (16.5).

theorem chapter16Gaussian_finiteTime_log_identity (epsilon gap C p horizon : Real) (hepsilon : 0 < epsilon) (hgap : 0 < gap) (hC : 0 < C) (hhorizon : 0 < horizon) : Real.log (epsilon * gap / 4) + Real.log horizon - Real.log (2 * C * horizon ^ p) = (1 - p) * Real.log horizon + Real.log (epsilon * gap / (8 * C))

*Lattimore--Szepesvári, Theorem 16.4.** Finite-time instance-dependent lower bound for arbitrary unit-variance Gaussian means. `lastRound + 1` is the source horizon `n`; the supplied set `N` is therefore stated on positive horizon lengths.

theorem gaussianExpectedRegret_ge_finiteTimeInstanceDependent {K : Nat} (algorithm : Thompson.HistoryAlgorithm (Fin K) Real) (environment : UnitVarianceGaussianBanditEnvironment K) (horizons : Set Nat) (hhorizons : horizons.Nonempty) (C p : Real) (hC : 0 < C) (_hp : p ∈ Set.Ioo (0 : Real) 1) (hregret : forall (lastRound : Nat), lastRound + 1 ∈ horizons -> forall candidate : UnitVarianceGaussianBanditEnvironment K, InChapter16GaussianLocalClass environment candidate -> unitVarianceGaussianExpectedPseudoRegret algorithm candidate lastRound <= C * (((lastRound + 1 : Nat) : Real) ^ p)) (epsilon : Real) (hepsilon : epsilon ∈ Set.Ioc (0 : Real) 1) (lastRound : Nat) (hhorizon : lastRound + 1 ∈ horizons) : unitVarianceGaussianExpectedPseudoRegret algorithm environment lastRound >= 2 / (1 + epsilon) ^ 2 * ∑ arm ∈ Finset.univ.filter (fun arm : Fin K => 0 < environment.gap arm), max (((1 - p) * Real.log ((lastRound + 1 : Nat) : Real) + Real.log (epsilon * environment.gap arm / (8 * C))) / environment.gap arm) 0