1. Finite bandits, traces, and regret

Plain-English statement. Minimax expected regret is the infimum, over an explicit policy class, of each policy's supremum expected regret over an explicit environment class.

Intuition

A lower-bound theorem must defeat every admissible policy on at least one admissible environment; the two nested order operations make that quantifier order visible.

Why it is needed

Chapter 13 states its Gaussian theorem in minimax form, so later information-theoretic leaves need a stable semantic endpoint rather than an informal phrase.

Place in the proof

This is the order-theoretic root of the Part IV lower-bound spine and is separate from any Gaussian or KL construction.

noncomputable def minimaxExpectedRegret {Policy : Type u} {Environment : Type v} (regret : Policy -> Environment -> ENNReal) (policyClass : Set Policy) (environmentClass : Set Environment) : ENNReal

Plain-English statement. A policy is minimax optimal only if it belongs to the chosen policy class and its worst-case regret over the chosen environment class attains that class's minimax value.

Intuition

The same policy can be minimax optimal for one horizon or environment class and fail to be optimal for another.

Why it is needed

This compiles the explicit Chapter 13 warning that minimax optimality is not a property of a policy alone.

Place in the proof

It refines the minimax value surface without asserting that an arbitrary infimum has a minimizing policy.

def IsMinimaxOptimal {Policy : Type u} {Environment : Type v} (regret : Policy -> Environment -> ENNReal) (policyClass : Set Policy) (environmentClass : Set Environment) (policy : Policy) : Prop

Plain-English statement. For the two Gaussian observation laws with means zero and Delta and variance one over n, the midpoint decision's worst-case error probability is at most exp(-n Delta squared over eight).

Intuition

A larger sample size or a wider separation makes the two Gaussian hypotheses exponentially easier to distinguish.

Why it is needed

It adds a real two-hypothesis probability theorem for the opening of Section 13.1 while leaving the sharper source display auditable.

Place in the proof

This is a symmetric Chernoff companion, distinct from the separately compiled exact two-sided Mills-ratio Eq. (13.1).

theorem gaussianSampleMeanThresholdRisk_le_exp (sampleSize : Nat) (gap : Real) (hgap : 0 < gap) : gaussianSampleMeanThresholdRisk sampleSize gap ≤ Real.exp (-(sampleSize : Real) * gap ^ 2 / 8)

Plain-English statement. In an m-plus-one-arm problem with arm zero distinguished, nonnegative expected pulls summing exactly to the horizon imply that some alternative arm is pulled no more than the alternative average n divided by m.

Intuition

The policy has only n pulls to distribute; after reserving the base arm, not every alternative can exceed the average alternative budget.

Why it is needed

Chapter 13 changes the source distribution of a lightly explored arm, making that change difficult for the policy to detect.

Place in the proof

It is the finite averaging leaf between the exact pull-count identity and the future two-history change-of-measure theorem.

theorem exists_leastExploredAlternative {m : Nat} (hm : 0 < m) (expectedPulls : Fin (m + 1) -> Real) (horizon : Nat) (hnonneg : ∀ arm, 0 ≤ expectedPulls arm) (htotal : ∑ arm : Fin (m + 1), expectedPulls arm = (horizon : Real)) : ∃ i : Fin m, expectedPulls i.succ ≤ (horizon : Real) / (m : Real)

Plain-English statement. If the base-environment expected base-arm pulls exceed the changed-environment expectation by at most an explicit error, then one of the two Chapter 13 regret expressions is at least Delta times n minus that error, divided by two.

Intuition

The base environment punishes too few base-arm pulls and the changed environment punishes too many; an information theorem may lose a quantitative error without erasing the deterministic lower-bound structure.

Why it is needed

This matches the source's approximate cross-law comparison without turning approximation into equality or an unjustified direction.

Place in the proof

It is the Chapter 13 algebra interface consumed by the compiled Chapter 14–15 history-law and testing route; the resulting Gaussian minimax endpoint gives the source-order statement with c=1/54.

theorem max_base_changed_regretLowerBound_ge_half_sub_error (horizon : Nat) (gap baseFirstExpectedPulls changedFirstExpectedPulls error : Real) (hgap : 0 ≤ gap) (hpullDifference : baseFirstExpectedPulls - changedFirstExpectedPulls ≤ error) : gap * ((horizon : Real) - error) / 2 ≤ max (baseEnvironmentRegret horizon gap baseFirstExpectedPulls) (changedEnvironmentRegretLowerBound gap changedFirstExpectedPulls)

Plain-English statement. If the changed-environment expected base-arm pulls are at least the base-environment expectation, then one Chapter 13 regret expression is at least Delta times n over two.

Intuition

This is the zero-error directional endpoint of the quantitative discrepancy theorem.

Why it is needed

It preserves a convenient special case while keeping the more realistic error-bearing bridge canonical.

Place in the proof

It is a corollary, not a change-of-measure theorem and not Theorem 13.1.

theorem max_base_changed_regretLowerBound_ge_half (horizon : Nat) (gap baseFirstExpectedPulls changedFirstExpectedPulls : Real) (hgap : 0 ≤ gap) (htransport : baseFirstExpectedPulls ≤ changedFirstExpectedPulls) : gap * (horizon : Real) / 2 ≤ max (baseEnvironmentRegret horizon gap baseFirstExpectedPulls) (changedEnvironmentRegretLowerBound gap changedFirstExpectedPulls)

Plain-English statement. Every finite binary prefix code with nonempty codewords satisfies the Kraft inequality.

Intuition

Prefix freedom makes codeword boundaries recoverable in concatenated messages, so the codebook cannot occupy more than all leaves of a binary tree.

Why it is needed

This is the first compiled coding-theory bridge in Chapter 14 and the structural lower-bound ingredient behind entropy versus expected length.

Place in the proof

This declaration is only the prefix-code-to-Kraft leaf. Separate Chapter 14 modules now compile recursive Huffman optimality, the one-bit entropy sandwich, and exact-real arithmetic source coding; their model boundaries remain explicit in the textbook spine.

theorem kraft_inequality [Fintype Symbol] [DecidableEq Symbol] (code : BinaryPrefixCode Symbol) : ∑ word ∈ code.codebook, (1 / 2 : Real) ^ word.length ≤ 1

Plain-English statement. Finite base-two entropy equals natural entropy divided by the natural logarithm of two.

Intuition

Bits and nats measure the same information with different logarithmic units.

Why it is needed

The exact conversion closes the definition-level content of Eqs. (14.2)–(14.3) without implying an optimal coding theorem.

Place in the proof

The entropy definitions and nonnegativity compile; the optimal expected-length comparison remains open.

theorem discreteEntropyBaseTwo_eq_div_log_two (support : Finset Symbol) (probability : Symbol → Real) : discreteEntropyBaseTwo support probability = discreteEntropy support probability / Real.log 2

Plain-English statement. Restricting two finite measures to any smaller sigma-algebra cannot increase their relative entropy.

Intuition

Forgetting measurable distinctions replaces the likelihood ratio by its conditional expectation, and convexity says this loses information.

Why it is needed

This closes Exercise 14.10 in its full sub-sigma-algebra form rather than only for the binary sigma-algebra generated by one event.

Place in the proof

It is a general finite-measure theorem; the existing event DPI remains a useful Bernoulli specialization for Bretagnolle–Huber.

theorem relativeEntropy_trim_le {α : Type*} {m m₀ : MeasurableSpace α} {P Q : @Measure α m₀} [IsFiniteMeasure P] [IsFiniteMeasure Q] (hm : m ≤ m₀) : @relativeEntropy α m (P.trim hm) (Q.trim hm) ≤ @relativeEntropy α m₀ P Q

Plain-English statement. Measure relative entropy is finite exactly when P is absolutely continuous with respect to Q and the P-log-likelihood ratio is integrable.

Intuition

The theorem makes the regular finite branch and singular or non-integrable branch visible instead of hiding them behind a real-valued KL convention.

Why it is needed

Every Chapter 14 conversion from extended-real KL to a real analytic inequality must justify that conversion without silently assuming support compatibility.

Place in the proof

This is the regularity gate between Mathlib's measure KL and the event-level data-processing proof.

theorem relativeEntropy_ne_top_iff {α : Type*} [MeasurableSpace α] {P Q : Measure α} : relativeEntropy P Q ≠ ∞ ↔ P ≪ Q ∧ Integrable (llr P Q) P

Plain-English statement. Replacing a full observation by the one-bit answer to whether it lies in a measurable event cannot increase relative entropy.

Intuition

Any decision based only on event membership discards information, so its two-point KL cost is no larger than the full-law cost.

Why it is needed

This is the exact bridge from measure-level information to the binary testing inequality used by finite-arm lower bounds.

Place in the proof

It is the compiled event specialization used by testing; the full arbitrary-sub-sigma-algebra Exercise 14.10 now compiles separately as relativeEntropy_trim_le.

theorem bernoulliRelativeEntropy_event_le {α : Type*} [MeasurableSpace α] {P Q : Measure α} [IsProbabilityMeasure P] [IsProbabilityMeasure Q] {A : Set α} (hA : MeasurableSet A) : bernoulliRelativeEntropy (P.real A) (Q.real A) ≤ relativeEntropy P Q

Plain-English statement. For Bernoulli probabilities p and q, the sum p plus one minus q dominates the extended-real Bretagnolle–Huber testing scale.

Intuition

Two binary laws with small relative entropy cannot simultaneously make both directional testing errors tiny.

Why it is needed

The binary theorem isolates the analytic affinity and endpoint work from the measure-theoretic event reduction.

Place in the proof

It sits between event data processing and the final measure-level Chapter 14 theorem.

theorem binaryBretagnolleHuber {p q : Real} (hp : KLUCB.IsBernoulliParameter p) (hq : KLUCB.IsBernoulliParameter q) : bretagnolleHuberScale (bernoulliRelativeEntropy p q) ≤ p + (1 - q)

Plain-English statement. The real testing scale one-half exponential negative KL decreases as its extended-real information argument increases.

Intuition

More divergence permits a weaker lower bound on testing error, while infinite divergence gives the zero scale.

Why it is needed

Antitonicity is the order-theoretic adapter that turns event data processing into the correctly oriented testing bound.

Place in the proof

It connects the binary theorem to the full-measure theorem without converting infinity through ENNReal.toReal.

theorem bretagnolleHuberScale_antitone {d D : ENNReal} (h : d ≤ D) : bretagnolleHuberScale D ≤ bretagnolleHuberScale d

Plain-English statement. For probability measures P and Q and a measurable event A, the P probability of A plus the Q probability of its complement is bounded below by one half exponential negative D(P,Q), with zero on the infinite-KL branch.

Intuition

A low-information change of law forces at least one of the two directional testing errors to remain appreciable.

Why it is needed

This is the Chapter 14 testing terminal that Chapter 15 can apply to same-policy bandit-history laws after their divergence has been constructed and bounded.

Place in the proof

It is the exact compiled counterpart of Lattimore–Szepesvári Theorem 14.2, not an adaptive-history theorem by itself.

theorem bretagnolleHuber {α : Type*} [MeasurableSpace α] {P Q : Measure α} [IsProbabilityMeasure P] [IsProbabilityMeasure Q] {A : Set α} (hA : MeasurableSet A) : bretagnolleHuberScale (relativeEntropy P Q) ≤ P.real A + Q.real Aᶜ

Plain-English statement. When two one-step joint laws share the same first marginal, their relative entropy is the first-law integral of the pointwise relative entropy between their conditional kernels.

Intuition

The shared past contributes no information; only the next conditional observation separates the two laws, and its cost is averaged over histories actually seen under the first law.

Why it is needed

This closes the conditional-kernel chain-rule gap that previously prevented arm-level KL costs from being accumulated along an adaptive bandit history.

Place in the proof

It is the measure-theoretic engine of Chapter 15 Lemma 15.1, before specializing the conditional kernels to one randomized policy and finite arms.

theorem klDiv_compProd_same_left_eq_lintegral_klDiv_of_measurable {Base Target : Type*} [MeasurableSpace Base] [MeasurableSpace Target] [MeasurableSpace.CountablyGenerated Target] (mu : Measure Base) [IsFiniteMeasure mu] (kappa eta : Kernel Base Target) [IsMarkovKernel kappa] [IsMarkovKernel eta] (hmeasurable : Measurable (fun base => InformationTheory.klDiv (kappa base) (eta base))) : InformationTheory.klDiv (mu ⊗ₘ kappa) (mu ⊗ₘ eta) = ∫⁻ base, InformationTheory.klDiv (kappa base) (eta base) ∂mu

Plain-English statement. For one common randomized policy in two finite-arm environments, the directed KL between their canonical finite history laws equals the sum of first-environment expected pull counts times the directed KL of each arm law.

Intuition

At every round the same policy cancels from the likelihood ratio; an arm pays information only when the policy selects it, so repeated conditional costs regroup into expected pull counts.

Why it is needed

This is the compiled Chapter 15 change-of-environment identity used by minimax, instance-dependent, and high-probability lower-bound routes.

Place in the proof

It is the local source-facing counterpart of Lattimore–Szepesvári Lemma 15.1. The compiled Theorem 15.2 consumes it; later Chapter 16–17 terminals remain separate.

theorem banditHistoryRelativeEntropy_eq_expectedPulls_sum {K : Nat} {Reward : Type v} [MeasurableSpace Reward] [MeasurableSpace.CountablyGenerated Reward] (algorithm : Thompson.HistoryAlgorithm (Fin K) Reward) (armLaw referenceArmLaw : Kernel (Fin K) Reward) [IsMarkovKernel armLaw] [IsMarkovKernel referenceArmLaw] (lastRound : Nat) : InformationTheory.klDiv (canonicalBanditHistoryMeasure algorithm armLaw lastRound) (canonicalBanditHistoryMeasure algorithm referenceArmLaw lastRound) = ∑ arm : Fin K, canonicalRealizedExpectedPullCountThrough algorithm armLaw lastRound arm * InformationTheory.klDiv (armLaw arm) (referenceArmLaw arm)

Plain-English statement. A measurable observation of two finite measures cannot have more relative entropy than the original laws.

Intuition

Coarsening the available information can only make two laws harder to distinguish.

Why it is needed

This is the reusable data-processing half of Chapter 15 Exercise 15.7 and also turns Lemma 15.1 into bounds for deterministic-history statistics.

Place in the proof

It is a generic finite-measure theorem and a dependency of the stopping-time exercise, not the stopped-history inequality itself.

theorem klDiv_map_le {Source Target : Type*} [MeasurableSpace Source] [MeasurableSpace Target] (mu nu : Measure Source) [IsFiniteMeasure mu] [IsFiniteMeasure nu] (observe : Source -> Target) (hobserve : Measurable observe) : InformationTheory.klDiv (mu.map observe) (nu.map observe) <= InformationTheory.klDiv mu nu

Plain-English statement. Under the first unit-variance Gaussian law, the log Radon–Nikodym derivative toward a second unit-variance Gaussian is an affine function of the observation.

Intuition

Equal Gaussian variances cancel their normalizing constants, leaving a difference of two quadratic exponents that simplifies to an affine log likelihood ratio.

Why it is needed

This is the regular analytic leaf needed before Chapter 15 can compute the KL cost of changing one Gaussian arm.

Place in the proof

It is an arm-level dependency, not the adaptive-history likelihood-ratio decomposition of Lemma 15.1.

theorem llr_gaussianReal_one_ae (mu nu : Real) : llr (unitGaussianArm mu) (unitGaussianArm nu) =ᵐ[unitGaussianArm mu] fun x => (mu - nu) * x + (nu ^ 2 - mu ^ 2) / 2

Plain-English statement. The relative entropy from a unit-variance Gaussian with mean mu to one with mean nu is one half the squared mean difference.

Intuition

Integrating the affine log likelihood ratio under N(mu,1) replaces the observation by its mean mu and leaves the squared mean displacement.

Why it is needed

Theorem 15.2 changes one arm from mean zero to 2 Delta, so this leaf supplies its exact information cost 2 Delta squared.

Place in the proof

It is the compiled Gaussian arm-KL dependency consumed by Lemma 15.1 and the now-compiled Theorem 15.2 history/event assembly.

theorem klDiv_gaussianReal_one (mu nu : Real) : InformationTheory.klDiv (unitGaussianArm mu) (unitGaussianArm nu) = ENNReal.ofReal ((mu - nu) ^ 2 / 2)

Plain-English statement. The Chapter 15 gap choice makes the Gaussian information exponent exactly one half.

Intuition

Choosing the gap to balance the number of alternatives against the horizon keeps the changed history laws at constant information distance after applying Lemma 15.1.

Why it is needed

This isolates the source's tuning algebra before the compiled history-KL and event-testing assembly.

Place in the proof

It is a numeric dependency consumed by the compiled Theorem 15.2, while its statement alone does not bound history divergence.

theorem gaussianMinimaxGap_informationExponent_eq_half {alternativeCount horizon : Real} (halternatives : 0 < alternativeCount) (hhorizon : 0 < horizon) : 2 * horizon * gaussianMinimaxGap alternativeCount horizon ^ 2 / alternativeCount = 1 / 2

Plain-English statement. For every randomized finite-history policy, k greater than one, and n at least k minus one, some k-armed unit-variance Gaussian bandit with means in the unit cube has expected pseudo-regret at least one twenty-seventh times the square root of (k minus one) times n.

Intuition

A policy cannot explore every alternative often under the base instance. Raising one lightly sampled arm creates a competing environment that stays close in history KL, so the policy must incur substantial regret in at least one of the two worlds.

Why it is needed

This is the first complete source-facing textbook minimax theorem in the Part IV spine: it joins reusable probability, history-law, Gaussian, event, and lattice layers into the exact external endpoint.

Place in the proof

It is the compiled counterpart of Lattimore–Szepesvári Theorem 15.2 and implies the coarser Chapter 13 order statement with c=1/54. It does not promote the Bernoulli notes, exercises, or Chapter 16–17 terminals.

theorem finiteArmedGaussianMinimaxLowerBound {k horizon : Nat} (hk : 1 < k) (hkhorizon : k - 1 ≤ horizon) (algorithm : Thompson.HistoryAlgorithm (Fin k) Real) : ∃ environment : UnitGaussianBanditEnvironment k, ENNReal.ofReal ((1 / 27 : Real) * Real.sqrt (((k - 1 : Nat) : Real) * (horizon : Real))) ≤ gaussianExpectedPseudoRegret algorithm environment (horizon - 1)

Plain-English statement. A regret sequence is consistent when its ratio to n to the power p converges to zero for every positive real exponent p.

Intuition

Consistency excludes a policy that pays polynomial regret on the instance, while still allowing logarithmic and other subpolynomial behavior.

Why it is needed

Definition 16.1 quantifies over every environment and every positive real exponent; the scalar predicate freezes the inner analytic contract exactly.

Place in the proof

It is a generic dependency interface, not proof that a concrete bandit policy is consistent over a concrete class.

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

Plain-English statement. The logarithmic growth ratio of a positive sum of two consistent regret sequences is eventually at most every positive exponent.

Intuition

Two subpolynomial regrets remain subpolynomial, so their logarithm grows more slowly than any positive multiple of log n.

Why it is needed

This is the direction-correct analytic step used in the source proof before taking the limsup that feeds Theorem 16.2's pull-count liminf.

Place in the proof

It stops before the limsup/liminf and before any bandit history law; those endpoints remain separate obligations.

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

Plain-English statement. The Chapter 16 information cost is the extended-real infimum of original-to-alternative KL over laws in the class whose mean is strictly above the target mean.

Intuition

The easiest law that would make the arm optimal determines how much information a policy must collect to rule out that confusion.

Why it is needed

Keeping the infimum in ENNReal preserves empty alternative sets, support mismatch, zero cost, and infinite cost instead of hiding them behind real defaults.

Place in the proof

This is the exact source-shaped definition. Turning it into expected pulls and regret still requires the blocked history change-of-measure bridge.

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

Plain-English statement. For a suboptimal unit-variance Gaussian arm, the Chapter 16 information infimum is exactly one half of the squared gap to the optimal mean.

Intuition

Every strictly better Gaussian alternative is at least the boundary distance away, while alternatives just above the boundary approach that cost.

Why it is needed

This closes the unit-Gaussian row of Table 16.1 instead of recording only one perturbed candidate.

Place in the proof

It is an exact distribution-level dependency of the now-compiled per-arm information constraint and Theorem 16.2 regret terminal.

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

Plain-English statement. When only one arm law changes, the original-law expected pulls times that arm's KL controls the sum of the two majority-event errors under one common randomized policy.

Intuition

If the policy almost never pulls the changed arm, the two history laws remain hard to distinguish, so the majority decision must fail in at least one environment.

Why it is needed

This is the exact one-arm event-information layer reused by Lemma 16.3 and the asymptotic route.

Place in the proof

The history KL and event inequality compile and now feed two canonical gap-pseudo-regret event charges; the finite arm-law mean-to-gap identification and source Lemma 16.3 terminal also compile.

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)ᶜ

Plain-English statement. For two finite-arm history laws that differ only at one arm, the compiled majority-event charges turn the directed arm KL into the exact logarithmic lower bound on the original-law expected pull count for explicit nonnegative gap vectors.

Intuition

The policy cannot simultaneously avoid the changed arm, keep both expected gap regrets small, and distinguish the two environments. The two event errors are each paid for by an actual gap-times-pull-count expectation.

Why it is needed

This closes the common-policy information, exact half-horizon charges, factor-one-quarter assembly, and logarithmic algebra that sit immediately below Lemma 16.3.

Place in the proof

It is the compiled conditional consumer below the now-compiled finite-mean source Lemma 16.3 terminal.

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

Plain-English statement. For finite-mean product bandits that differ at exactly one arm, the original-law expected pull count satisfies the exact Lemma 16.3 logarithmic lower bound.

Intuition

The finite-mean bridge turns equality of every unchanged law into equality of its mean, so unique optimality after the change supplies exactly the alternative gap needed by the event test.

Why it is needed

This is the first compiled source terminal in Chapter 16's finite-time route and preserves the source minimum, KL direction, original-law pulls, and arbitrary randomized policy.

Place in the proof

Lemma 16.3 and Theorem 16.2 compile, connected by exact horizon indexing and extended-real liminf aggregation.

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

Plain-English statement. Under the local C n^p envelope, every unit-variance Gaussian instance satisfies the exact finite-time positive-part lower bound of Theorem 16.4.

Intuition

Raise each suboptimal mean by (1+epsilon) times its gap, use Lemma 16.3 arm by arm, and keep only the nonnegative part before summing.

Why it is needed

The theorem closes the exact local Gaussian finite-time endpoint, including its horizon set, 8C logarithm, factor 2/(1+epsilon)^2, and positive-part placement.

Place in the proof

Theorem 16.4 compiles for unrestricted real Gaussian means. The general unstructured-class Theorem 16.2 also compiles.

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

Plain-English statement. If the average random-regret tail over a probability law on instances is at least delta, then one deterministic instance has tail probability at least delta.

Intuition

An average cannot exceed every point, so randomizing the hard reward matrix can be converted back into one fixed adversarial sequence.

Why it is needed

This is the exact first-moment content of Claim 17.5, which closes the final probabilistic-method step in the source's adversarial route.

Place in the proof

Claim 17.5 is compiled, but the clipped-normal law and the average-tail lower bound that feed it remain blocked.

theorem exists_cdfTail_ge_of_integral_ge {Instance : Type*} [MeasurableSpace Instance] (Q : Measure Instance) [IsProbabilityMeasure Q] (cdf : Instance -> Real -> Real) (threshold delta : Real) (hIntegrable : Integrable (fun x => 1 - cdf x threshold) Q) (hAverage : delta <= ∫ x, 1 - cdf x threshold ∂Q) : exists x, delta <= 1 - cdf x threshold

Plain-English statement. An event with probability at least twice delta still has probability at least delta after removing a bad event of probability at most delta.

Intuition

The pull-small event can lose all rounds with excessive clipping and still retain the confidence level needed by Theorem 17.4.

Why it is needed

This isolates the exact probability bookkeeping between Claims 17.6 and 17.7 without pretending either claim is available.

Place in the proof

It is a generic outer-measure leaf between the two blocked construction-specific claims.

theorem measureReal_diff_ge_delta {Omega : Type*} [MeasurableSpace Omega] (P : Measure Omega) [IsFiniteMeasure P] (pullSmall clippingBad : Set Omega) (delta : Real) (hPullSmall : 2 * delta <= P.real pullSmall) (hClippingBad : P.real clippingBad <= delta) : delta <= P.real (pullSmall \ clippingBad)

Plain-English statement. If Eq. (17.8) holds, pulling the hard arm at most half the time and clipping at most a quarter of rounds forces random regret at least gap times horizon over four.

Intuition

After removing the hard-arm pulls and boundary-clipped rounds, at least one quarter of the horizon still contributes the gap.

Why it is needed

This compiles the deterministic end of the source argument while leaving the construction-specific pathwise comparison visible as a premise.

Place in the proof

This conditional lemma does not itself prove Eq. (17.8), but the same module now separately compiles construction-level Eq. (17.8). It does not prove Claim 17.6, Claim 17.7, or Theorem 17.4.

theorem randomRegret_ge_quarter_of_clippingDecomposition (horizon pullCount clippingCount : Nat) (gap randomRegret : Real) (hGap : 0 <= gap) (hPull : (pullCount : Real) <= (horizon : Real) / 2) (hClipping : (clippingCount : Real) <= (horizon : Real) / 4) (hSource : adversarialRegretLowerExpression horizon pullCount clippingCount gap <= randomRegret) : gap * ((horizon : Real) / 4) <= randomRegret