1. Finite bandits, traces, and regret

Plain-English statement. A finite bandit model packages a rational mean for every arm together with a distinguished best arm and a proof that this arm really has maximal mean.

Intuition

The structure prevents later regret proofs from silently choosing a nonoptimal comparator. The proof field is data, so every downstream gap theorem can reuse it.

Why it is needed

Gaps, pseudo-regret, ETC commit errors, UCB suboptimal pulls, and the stochastic Tsallis endpoints all need the same fixed comparator.

Place in the proof

This is the model root of the deterministic proof DAG.

Proof idea

This is a structure definition rather than a theorem. Its crucial invariant is the maximality field; derived lemmas prove gap nonnegativity and upper bounds.

Lean reading notes

A Lean structure bundles values and proofs. Passing one model value therefore passes both the means and the best-arm certificate without a separate global assumption.

Teaching dependencies

No direct teaching dependency recorded.

structure FiniteBanditModel (K : Nat) where

Plain-English statement. The pull count of arm a before time n is the number of indices t<n at which the action trace selected a.

Intuition

Most bandit analyses eventually ask how often a suboptimal arm was selected. This definition is the common bridge from an adaptive trace to finite combinatorics.

Why it is needed

ETC uses exact exploration counts; UCB controls small-count and large-count selections; regret decompositions weight these counts by gaps.

Place in the proof

It sits immediately above action traces and below almost every finite-arm regret theorem.

Proof idea

The definition is a finite list count. Separate wrapper lemmas expose equivalent Finset sums and measurable random-variable forms when probability enters.

Lean reading notes

Keeping the core definition dependency-light makes elementary count algebra available before importing measure theory.

Teaching dependencies

No direct teaching dependency recorded.

def pullCount [DecidableEq Action] (action : ActionTrace Action) (a : Action) : Nat → Nat | 0 => 0 | t + 1 => pullCount action a t + if action t = a then 1 else 0 @[simp] theorem pullCount_zero [DecidableEq Action] (action : ActionTrace Action) (a : Action) : pullCount action a 0 = 0

Plain-English statement. Cumulative pseudo-regret can be regrouped by arm: every pull of arm a contributes exactly its fixed gap.

Intuition

The left side follows time; the right side follows arms. Algorithm-specific proofs normally bound the right side, one arm at a time.

Why it is needed

It turns a probabilistic control of pull counts into a regret theorem without redoing the deterministic bookkeeping for every algorithm.

Place in the proof

This is the central deterministic join between model gaps and algorithm traces.

Proof idea

Expand pseudo-regret as a finite time sum, insert the indicator of each arm, swap finite sums, and identify the inner indicator sum with pullCount.

Lean reading notes

The proof uses Finset rearrangement and previously compiled wrappers. No measure, independence, or integrability assumption appears.

Teaching dependencies

BanditRLProof.pullCount, BanditRLProof.pseudoRegret, BanditRLProof.FiniteBanditModel

theorem pseudoRegret_eq_finset_sum_gap_mul_pullCount : pseudoRegret model action t = (Finset.univ : Finset (Fin K)).sum (fun a : Fin K => model.gap a * (pullCount action a t : Rat))

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.

Proof idea

The definition uses ENNReal complete-lattice infimum and supremum over subtypes for the explicit policy and environment sets.

Lean reading notes

The definitions retain standard empty-class lattice semantics. Intended bandit consumers must prove their policy and environment classes are nonempty; no boundedness assumption is hidden.

Teaching dependencies

BanditRLProof.LowerBounds.worstCaseExpectedRegret

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

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.

Proof idea

Split the full Fin (m+1) sum into arm zero plus the Fin.succ tail, use nonnegativity to bound the tail by n, then apply Mathlib's finite exists-le-average lemma to m copies of n/m.

Lean reading notes

The source's one-based arms 2 through k are represented by i.succ for i : Fin m. The theorem assumes 0 < m, all expected pulls nonnegative, and the exact total identity; no probability law is hidden.

Teaching dependencies

BanditRLProof.LowerBounds.exists_alternative_le_average, BanditRLProof.LowerBounds.alternativeExpectedPullBudget_le

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 that later history-law and testing inequalities can consume; the Gaussian minimax terminal remains planned for Chapters 14 and 15.

Proof idea

Scale the explicit pull-discrepancy bound by the nonnegative gap, show the two lower expressions sum to at least Delta times n minus the error, and compare their maximum with half their sum.

Lean reading notes

The discrepancy error is a visible Real-valued premise. The declaration proves no absolute continuity, KL bound, testing inequality, or Gaussian construction.

Teaching dependencies

BanditRLProof.LowerBounds.baseEnvironmentRegret, BanditRLProof.LowerBounds.changedEnvironmentRegretLowerBound

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.

Proof idea

Apply the quantitative theorem with error zero and rewrite the directional premise as a nonpositive difference.

Lean reading notes

The cross-environment comparison remains an explicit premise; no statistical law comparison is hidden.

Teaching dependencies

BanditRLProof.LowerBounds.max_base_changed_regretLowerBound_ge_half_sub_error

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. 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.

Proof idea

The declaration is a project-facing exact adapter for Mathlib's klDiv finiteness characterization.

Lean reading notes

The KL direction is P to Q. Mutual absolute continuity is neither assumed nor derived, and the theorem works on a common measurable space.

Teaching dependencies

BanditRLProof.LowerBounds.relativeEntropy

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 of data processing; it is not the full arbitrary-sub-sigma-algebra Exercise 14.10.

Proof idea

Split both measures over A and its complement, identify the restricted Radon–Nikodym derivatives, lower-bound each restricted KL by the corresponding mass-level klFun term, and restore Bernoulli endpoints separately.

Lean reading notes

The parameters are ordered as P(A), Q(A), and the bound uses D(P,Q). Finite KL supplies P absolutely continuous with respect to Q; infinite KL is discharged directly.

Teaching dependencies

BanditRLProof.LowerBounds.relativeEntropy_ne_top_iff, BanditRLProof.LowerBounds.relativeEntropy_restrict_add_compl, BanditRLProof.LowerBounds.bernoulliKLCore_event_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.

Proof idea

For interior q, Jensen bounds likelihood affinity below by exp(-d/2), while a two-term square-root inequality bounds half the squared affinity by the testing error. Endpoint support mismatches use infinite KL explicitly.

Lean reading notes

Both p and q carry closed-unit-interval hypotheses. Cases q=0 and q=1 are proved separately, so no interior assumption leaks into the public theorem.

Teaching dependencies

BanditRLProof.LowerBounds.binaryBretagnolleHuberCore, BanditRLProof.LowerBounds.bretagnolleHuberScale

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.

Proof idea

Split on whether the larger divergence is infinite; otherwise use monotonicity of toReal and the real exponential after negation.

Lean reading notes

The explicit top branch prevents a hidden finiteness assumption in the final source theorem.

Teaching dependencies

BanditRLProof.LowerBounds.bretagnolleHuberScale, BanditRLProof.LowerBounds.bretagnolleHuberScale_nonneg

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.

Proof idea

Apply event data processing, reverse it through the antitone testing scale, invoke the endpoint-complete binary theorem, and rewrite Q(A complement) as one minus Q(A).

Lean reading notes

The theorem assumes only two probability measures on one measurable space and a measurable event. It does not assume finite KL, mutual absolute continuity, a policy, horizon, filtration, or stopping time.

Teaching dependencies

BanditRLProof.LowerBounds.bernoulliRelativeEntropy_event_le, BanditRLProof.LowerBounds.bretagnolleHuberScale_antitone, BanditRLProof.LowerBounds.binaryBretagnolleHuber

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.

Proof idea

Identify the joint Radon–Nikodym derivative fibrewise, integrate its logarithm under the composition product, and preserve the singular branch: positive first-law mass on an infinite-KL fibre makes both sides infinite.

Lean reading notes

The theorem assumes a finite first measure, finite Markov kernels, countably generated target measurable space, and measurability of the pointwise KL function. It does not assume absolute continuity or finite KL.

Teaching dependencies

No direct teaching dependency recorded.

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. Theorem 15.2 and later regret terminals remain separate consumers.

Proof idea

Recursively expose the canonical finite history law as a composition product, apply the same-policy conditional KL identity at each successor, sum over finite actions, and identify policy arm masses with lower integrals of realized pull counts.

Lean reading notes

Finite arms and a countably generated reward space are explicit. The equality uses ENNReal KL and lower-integral expected counts, covers singular or infinite arm KL, and uses the first environment in both the history law and expectation. The local lastRound index denotes lastRound+1 observations.

Teaching dependencies

BanditRLProof.LowerBounds.klDiv_compProd_same_left_eq_lintegral_klDiv_of_measurable, BanditRLProof.LowerBounds.klDiv_historyStep_samePolicy_eq_iterated_lintegral_armKL_general, BanditRLProof.LowerBounds.canonicalRealizedExpectedPullCountThrough_eq_expectedPullCountThrough

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. 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.

Proof idea

Use absolute continuity in both directions through Lebesgue measure, identify both Radon–Nikodym derivatives with Gaussian densities, cancel the positive normalizer, and expand the squares.

Lean reading notes

The almost-everywhere law is the first Gaussian N(mu,1), preserving the source KL direction. No bandit policy or history law appears.

Teaching dependencies

BanditRLProof.LowerBounds.log_gaussianPDFReal_div_gaussianPDFReal_one

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 the compiled Lemma 15.1 history identity; Theorem 15.2 still needs the regret/event terminal.

Proof idea

Prove mutual absolute continuity via Lebesgue measure, establish L1 integrability from the Gaussian first moment, invoke Mathlib's KL integral formula, and normalize the resulting polynomial.

Lean reading notes

The value is symmetric only because both variances are one; the declaration and every downstream contract retain the direction from mu to nu.

Teaching dependencies

BanditRLProof.LowerBounds.llr_gaussianReal_one_ae, BanditRLProof.LowerBounds.integrable_llr_gaussianReal_one

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 from the still-blocked regret/event and constant bridge.

Place in the proof

It is a compiled numeric dependency of Theorem 15.2, not a proof that the history divergence has this upper bound.

Proof idea

Square the nonnegative real square root and normalize the positive field denominators.

Lean reading notes

The parameters are explicit positive real alternative count and horizon values. Natural-cast and bandit-semantic obligations remain with the source terminal.

Teaching dependencies

BanditRLProof.LowerBounds.gaussianMinimaxGap_sq

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. A regret sequence is consistent when it divided by n to the 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.

Proof idea

The declaration directly records a filter limit for each positive real exponent.

Lean reading notes

Regret nonnegativity is deliberately a caller obligation. The base is the natural horizon cast to Real and the exponent is Real.rpow.

Teaching dependencies

No direct teaching dependency recorded.

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.

Proof idea

Add the two normalized limits, bound the ratio by one eventually, take monotone logarithms, rewrite log(n^p)=p log n, and divide by positive log n.

Lean reading notes

The sum must be eventually positive and the proof explicitly restricts to horizons greater than one.

Teaching dependencies

BanditRLProof.LowerBounds.IsConsistentRegret.add, BanditRLProof.LowerBounds.IsConsistentRegret.eventually_add_le_rpow

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.

Proof idea

Define the infimum over a set comprehension and use complete-lattice sInf_le to insert any admissible candidate.

Lean reading notes

The mean functional and distribution class are explicit. The strict comparison and KL direction P to P-prime are visible in the type.

Teaching dependencies

BanditRLProof.LowerBounds.relativeEntropy

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 unit-variance Gaussian arm, changing the mean to mu-star plus a positive epsilon gives an admissible d_inf candidate with its exact squared-distance KL cost.

Intuition

A mean just above the optimal threshold supplies the approaching sequence behind the Gaussian d_inf formula.

Why it is needed

The leaf connects Chapter 16's infimum interface to the compiled Chapter 15 Gaussian KL without pretending the limiting infimum equality is already proved.

Place in the proof

It is the upper-candidate half of Table 16.1's unit-variance Gaussian calculation; the lower bound and epsilon-to-zero extraction remain open.

Proof idea

Insert the alternative parameter mu-star plus epsilon, apply the exact Gaussian KL theorem, and normalize the squared displacement.

Lean reading notes

The premise epsilon>0 discharges strict mean improvement. The output stays ENNReal and retains the original-to-alternative orientation.

Teaching dependencies

BanditRLProof.LowerBounds.parametricDivergenceInfimum_le, BanditRLProof.LowerBounds.klDiv_gaussianReal_one

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

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.

Proof idea

Apply Mathlib's probability-measure first-moment theorem to the integrable function x maps to one minus F_x(u), then chain the assumed lower bound on its integral.

Lean reading notes

The source suppresses regularity; Lean exposes integrability of the CDF-tail function as a premise. The theorem does not construct the CDF or reward-matrix law.

Teaching dependencies

No direct teaching dependency recorded.

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.

Proof idea

Use Mathlib's lower bound on the real measure of a set difference and finish with linear arithmetic.

Lean reading notes

No measurable-set premise is needed because the measure interface is an outer measure on all sets; finiteness is explicit.

Teaching dependencies

No direct teaching dependency recorded.

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

It does not prove Eq. (17.8), Claim 17.6, Claim 17.7, or Theorem 17.4.

Proof idea

Subtract the half-horizon and quarter-horizon count bounds, multiply by a nonnegative gap, and compose with the explicit source comparison.

Lean reading notes

Counts are natural numbers cast to Real. The nonnegative gap and Eq. (17.8) lower comparison are explicit assumptions.

Teaching dependencies

BanditRLProof.LowerBounds.adversarialRegretLowerExpression_ge_quarter

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