Part IV — Lower Bounds for Bandits with Finitely Many Arms

Chapter 16: Instance-Dependent Lower Bounds

Definition 16.1, Theorem 16.2, Lemma 16.3, and Theorem 16.4 compile with the source quantifiers, information branches, constants, and positive-part placement.

CompiledPrinted pp. 177–184PDF pp. 215–223

Source map

Bandit Algorithms, Tor Lattimore and Csaba Szepesvári, Cambridge University Press (2020), DOI 10.1017/9781108571401.

Chapter DOI. 10.1017/9781108571401.021 · CUP chapter page

Chapter opening (CUP p. 177 / author-online p. 206 / PDF p. 215)
§16.1 Asymptotic Bounds (CUP pp. 177–179 / author-online pp. 207–208 / PDF pp. 216–217; Definition 16.1 and Theorem 16.2)
§16.2 Finite-Time Bounds (CUP p. 180 / author-online pp. 209–210 / PDF pp. 218–219; Lemma 16.3 and Theorem 16.4)
§16.3 Notes (CUP p. 181 / author-online p. 210 / PDF p. 219)
§16.4 Bibliographic Remarks (CUP p. 181 / author-online p. 211 / PDF p. 220)
§16.5 Exercises (CUP pp. 181–184 / author-online pp. 211–214 / PDF pp. 220–223)

Open Chapter 16 at PDF p. 215

Learning goals

Read consistency with its exact quantifier order: every environment and every real exponent p greater than zero.
Keep d_inf extended-real, the confusing alternative strictly better, and KL directed from the original arm law to the alternative.
Trace how consistency controls log(R_n(nu)+R_n(nu-prime))/log(n) before the liminf extraction.
Separate Theorem 16.2's asymptotic product-class result from Lemma 16.3 and Theorem 16.4's finite-time Gaussian route.

Necessary definitions and statements

Policy consistency (Definition 16.1)

Compiled

Policy consistency (Definition 16.1). Formula renderer unavailable; readable fallback: One policy is consistent over the class when its regret is smaller than every positive polynomial order on every environment.\[\forall \nu\in\mathcal E\;\forall p>0:\quad \lim_{n\to\infty}\frac{R_n(\pi,\nu)}{n^p}=0.\]

Distribution-class information cost

Compiled

Distribution-class information cost. Formula renderer unavailable; readable fallback: The information cost is the least original-to-alternative KL among laws in the class whose mean is strictly above the target mean.\[d_{\inf}(P,\mu^*,\mathcal M)=\inf\{D(P\Vert P'):\;P'\in\mathcal M,\;\mu(P')>\mu^*\}.\]

Per-arm asymptotic information constraint

Compiled

Per-arm asymptotic information constraint. Formula renderer unavailable; readable fallback: A consistent policy must sample each suboptimal arm at a logarithmic rate set by the cheapest confusing alternative.\[\liminf_{n\to\infty}\frac{\mathbb E_{\nu,\pi}[T_i(n)]}{\log n}\ge\frac{1}{d_{\inf}(P_i,\mu^*,\mathcal M_i)}.\]

Finite-time Gaussian lower-bound shape

Compiled

Finite-time Gaussian lower-bound shape. Formula renderer unavailable; readable fallback: Under the local C times n to the p regret envelope, the Gaussian lower bound sums the positive part of one explicit logarithmic term per suboptimal arm.\[R_n(\pi,\nu)\ge\frac{2}{(1+\varepsilon)^2}\sum_{i:\Delta_i>0}\left(\frac{(1-p)\log n+\log(\varepsilon\Delta_i/(8C))}{\Delta_i}\right)^+.\]

proof pseudocode

Instance-dependent lower-bound proof flow

Freeze consistency
Require R_n(pi,nu)/n^p to converge to zero for every environment in the class and every real p>0.
Choose a confusing alternative
Change one suboptimal arm to a law in its component class whose mean is strictly above the original optimal mean and whose original-to-alternative KL approaches d_inf.
Lift arm KL to history KL
Use the compiled one-arm specialization of the one-common-policy Lemma 15.1 identity to obtain the original-law realized expected pull-count cost.
Charge both event errors
The compiled finite-mean environment producer identifies the original gap and changed optimality margin, closing the exact Lemma 16.3 inequality under the same canonical history laws.
Extract the rate
Use consistency to bound each alternative cost, aggregate inverse costs with the extended-real inverse-infimum identity, and apply finite-count Fatou to obtain Theorem 16.2.
Specialize finite time
The compiled Theorem 16.4 shifts a Gaussian mean by Delta_i(1+epsilon), proves local-class membership and exact KL, and retains the positive part and factor 2/(1+epsilon)^2.

Key source theorem and boundary

Source theorem · faithful restatement

Definition 16.1, Theorem 16.2, Lemma 16.3, and Theorem 16.4

Original chapter ↗Compiled

Chapter 16 turns one-arm change of measure into asymptotic and finite-time instance-dependent regret obstructions.

Definition 16.1, Theorem 16.2, Lemma 16.3, and Theorem 16.4. Formula renderer unavailable; readable fallback: A consistent policy pays the source d_inf logarithmic constant on every unstructured instance; under the finite-time local Gaussian envelope, an explicit positive-part lower bound holds at every selected horizon.\[\liminf_{n\to\infty}\frac{R_n(\pi,\nu)}{\log n}\ge\sum_{i:\Delta_i>0}\frac{\Delta_i}{d_{\inf}(P_i,\mu^*,\mathcal M_i)},\qquad R_n(\pi,\nu)\ge\frac{2}{(1+\varepsilon)^2}\sum_{i:\Delta_i>0}\left(\frac{(1-p)\log n+\log(\varepsilon\Delta_i/(8C))}{\Delta_i}\right)^+.\]

Lean boundary. The finite-mean source-environment bridge, exact Lemma 16.3, and exact unit-variance Gaussian Theorem 16.4 compile on top of the earlier information and event-regret layers. The unstructured-class Theorem 16.2 also compiles, including empty, zero, finite, and infinite information branches.

Lean correspondence

Only declarations that exist in the current index and pass the verified build may render as compiled.

Lean declaration	Status	Role and exact type
`BanditRLProof.LowerBounds.IsConsistentRegret`	Compiled	Exact scalar every-positive-real-power consistency predicate. Exact compact Lean statement `def IsConsistentRegret (regret : Nat -> Real) : Prop`
`BanditRLProof.LowerBounds.IsConsistentPolicyOver`	Compiled	Generic environment-class wrapper preserving the source quantifier order. Exact compact Lean statement `def IsConsistentPolicyOver {Policy Environment : Type*} (environmentClass : Set Environment) (regret : Policy -> Environment -> Nat -> Real) (policy : Policy) : Prop`
`BanditRLProof.LowerBounds.IsConsistentRegret.add`	Compiled	Closure for the two-environment regret sum used by Theorem 16.2. Exact compact Lean statement `theorem IsConsistentRegret.add {first second : Nat -> Real} (hfirst : IsConsistentRegret first) (hsecond : IsConsistentRegret second) : IsConsistentRegret (fun n => first n + second n)`
`BanditRLProof.LowerBounds.IsConsistentRegret.eventually_add_le_rpow`	Compiled	Every positive polynomial eventually dominates the regret sum. Exact compact Lean statement `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`
`BanditRLProof.LowerBounds.IsConsistentRegret.eventually_log_add_div_log_le`	Compiled	Direction-correct eventual logarithmic growth bound before the limsup step. Exact compact Lean statement `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`
`BanditRLProof.LowerBounds.divergenceInfimum`	Compiled	Extended-real distribution-class d_inf with strict mean improvement. Exact compact Lean statement `def divergenceInfimum {Reward : Type*} [MeasurableSpace Reward] (P : Measure Reward) (muStar : Real) (distributionClass : Set (Measure Reward)) (mean : Measure Reward -> Real) : ENNReal`
`BanditRLProof.LowerBounds.divergenceInfimum_le`	Compiled	Any confusing alternative upper-bounds d_inf in the original-to-alternative KL direction. Exact compact Lean statement `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'`
`BanditRLProof.LowerBounds.parametricDivergenceInfimum`	Compiled	Family-indexed form for parametric law classes. Exact compact Lean statement `def parametricDivergenceInfimum {Reward Parameter : Type*} [MeasurableSpace Reward] (law : Parameter -> Measure Reward) (mean : Parameter -> Real) (parameter : Parameter) (muStar : Real) : ENNReal`
`BanditRLProof.LowerBounds.parametricDivergenceInfimum_le`	Compiled	Strictly better parameter candidate inequality. Exact compact Lean statement `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)`
`BanditRLProof.LowerBounds.unitGaussianDivergenceInfimum`	Compiled	Unit-variance Gaussian parametric d_inf interface. Exact compact Lean statement `abbrev unitGaussianDivergenceInfimum (mu muStar : Real) : ENNReal`
`BanditRLProof.LowerBounds.unitGaussianDivergenceInfimum_le_perturbed`	Compiled	Exact cost of the candidate mean muStar+epsilon. Exact compact Lean statement `theorem unitGaussianDivergenceInfimum_le_perturbed (mu muStar epsilon : Real) (hepsilon : 0 < epsilon) : unitGaussianDivergenceInfimum mu muStar <= ENNReal.ofReal (((muStar - mu) + epsilon) ^ 2 / 2)`
`BanditRLProof.LowerBounds.unitGaussianDivergenceInfimum_eq`	Compiled	Exact unit-variance Gaussian Table 16.1 d_inf formula on the strict suboptimal branch. Exact compact Lean statement `theorem unitGaussianDivergenceInfimum_eq (mu muStar : Real) (hmu : mu < muStar) : unitGaussianDivergenceInfimum mu muStar = ENNReal.ofReal ((muStar - mu) ^ 2 / 2)`
`BanditRLProof.LowerBounds.banditHistoryRelativeEntropy_eq_expectedPulls_mul_of_only_arm_changed`	Compiled	One-arm specialization of Lemma 15.1 with original-law expected pulls. Exact compact Lean statement 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)
`BanditRLProof.LowerBounds.oneArmMajorityPullEvent`	Compiled	Exact source majority event under the inclusive lastRound convention. Exact compact Lean statement `def oneArmMajorityPullEvent {K : Nat} {Reward : Type*} (changedArm : Fin K) (lastRound : Nat) : Set (History.FinitePairHistory (Fin K) Reward lastRound)`
`BanditRLProof.LowerBounds.bretagnolleHuberScale_expectedPulls_mul_armKL_le_majorityErrors`	Compiled	Bretagnolle–Huber information constraint for the two majority-event errors. Exact compact Lean statement 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)ᶜ
`BanditRLProof.LowerBounds.finiteHistoryGapPseudoRegret`	Compiled	Realized finite-history pseudo-regret as an explicit finite sum of gap times pull count. Exact compact Lean statement `noncomputable def finiteHistoryGapPseudoRegret {K : Nat} {Reward : Type*} (gap : Fin K -> Real) (lastRound : Nat) (history : History.FinitePairHistory (Fin K) Reward lastRound) : ENNReal`
`BanditRLProof.LowerBounds.canonicalGapExpectedPseudoRegret_eq_sum_expectedPulls`	Compiled	Canonical expected pseudo-regret regrouped as gap times first-law expected pulls for every arm. Exact compact Lean statement `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`
`BanditRLProof.LowerBounds.oneArmMajority_probability_charge_le_expectedPseudoRegret`	Compiled	Original-law majority-event probability charged by the positive gap of the changed arm. Exact compact Lean statement 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
`BanditRLProof.LowerBounds.oneArmMajority_compl_probability_charge_le_expectedPseudoRegret`	Compiled	Changed-law complementary event charged by the minimum gap of every non-changed arm. Exact compact Lean statement 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
`BanditRLProof.LowerBounds.expectedPullCount_ge_log_gapPseudoRegret_of_only_arm_changed`	Compiled	Exact factor-one-quarter finite-KL logarithmic consumer for explicit nonnegative gap vectors. Exact compact Lean statement 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
`BanditRLProof.LowerBounds.expectedPullCount_ge_log_regret_of_exp_testing_bound`	Compiled	Scalar logarithmic rearrangement used after the source regret/error producers. Exact compact Lean statement `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`
`BanditRLProof.LowerBounds.FiniteMeanBanditEnvironment`	Compiled	Finite arm laws with means certified by Bochner integrals and a certified optimal arm. Exact compact Lean statement `structure FiniteMeanBanditEnvironment (K : Nat) where`
`BanditRLProof.LowerBounds.oneArmMeanChange_produces_gap_contract`	Compiled	Source mean-to-gap producer for one changed arm and a uniquely optimal alternative. Exact compact Lean statement 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)
`BanditRLProof.LowerBounds.expectedPullCount_ge_log_regret_changeOfMeasure`	Compiled	Exact Lemma 16.3 with original-law pulls, directed KL, and the source minimum. Exact compact Lean statement 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
`BanditRLProof.LowerBounds.UnitVarianceGaussianBanditEnvironment`	Compiled	Unrestricted real mean vectors for the source unit-variance Gaussian class. Exact compact Lean statement `structure UnitVarianceGaussianBanditEnvironment (K : Nat) where`
`BanditRLProof.LowerBounds.gaussianExpectedRegret_ge_finiteTimeInstanceDependent`	Compiled	Exact Theorem 16.4 with local class, horizon set, positive parts, and published constants. Exact compact Lean statement 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
`BanditRLProof.LowerBounds.consistentPolicy_liminf_expectedRegret_div_log_ge`	Compiled	Exact Theorem 16.2 over finite-mean unstructured classes, with extended-real d_inf and finite-sum liminf. Exact compact Lean statement 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
`BanditRLProof.LowerBounds.consistentPolicy_liminf_expectedPull_div_log_ge_inv_dInf`	Compiled	Exact per-arm information constraint with all extended-real inverse-infimum branches. Exact compact Lean statement 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

Dependency graph

ch14Chapter 14 event testingCompiled

ch15-gaussianChapter 15 unit-Gaussian arm KLCompiled

consistencyDefinition 16.1 consistency and log growthCompiled

dinfextended-real d_inf and candidate inequalitiesCompiled

gaussian-dinfexact Gaussian d_inf equalityCompiled

historyone-arm history KL and majority-event informationCompiled

scalarfinite-KL and scalar log assemblyCompiled

event-regretcanonical gap pseudo-regret and both event-error chargesCompiled

mean-gapfinite arm-law means to source gap vectorsCompiled

asymptoticTheorem 16.2 liminf regret terminalCompiled

finiteLemma 16.3 and Theorem 16.4Compiled

Reading path

Read Definition 16.1 and verify the order forall environment, forall real p>0.
Read d_inf and Theorem 16.2 with strict alternative mean, original-to-alternative KL, and an unstructured product class.
Trace the source event A={T_i(n)>n/2}, the two regret laws, and the compiled subpolynomial log-growth adapter.
Read Lemma 16.3 before Theorem 16.4 and preserve the unit-Gaussian local class, selected horizon set, constants, and positive part.
Inspect the finite-mean producer and all three source terminals; trace exact n-pull horizons, inverse-infimum aggregation, and finite-count Fatou in Theorem 16.2.

Strict status and remaining gaps

None recorded.