Teaching chapter 03 of 10 · Canonical route compiled

3. Explore-Then-Commit

Round-robin exploration, empirical means, measurable commit choices, wrong-commit tails, and expected-regret assemblies under bounded or sub-Gaussian arm laws.

How to read the status. It describes this page's canonical local Lean route, not completion of the cited textbook chapter or every extension listed below.

Orientation

Who should read this. The shortest end-to-end stochastic-bandit route in the repository.

Learning goals

Decompose regret into deterministic exploration cost and wrong-commit probability.
Follow empirical-mean concentration into a concrete Real expected-regret bound.
Distinguish compiled local endpoints from the still-partial upstream-compatible port.

Textbook crosswalk

Read the mathematics before the Lean interface

The Book Map is a curated formalization curriculum anchored in Bandit Algorithms, not a chapter-for-chapter reproduction of one book. Visible page labels use the numbered pages of its free online edition; source buttons use the PDF viewer's physical page index, which includes front matter and can therefore be larger. Companion papers cover algorithm-specific results.

Primary spine · free online edition

Bandit Algorithms

Tor Lattimore and Csaba Szepesvári

Location: Ch. 6
Pages: online pp. 91–96

Open at the cited pages

algorithm · ordered flow

Explore-Then-Commit

Read top to bottom: each step supplies the state or proof fact used by the next one.

Explore
Pull every arm m times, usually in round-robin order.
Estimate
Compute each arm's empirical mean from its exploration samples.
Commit
Choose an empirical maximizer using a documented tie rule.
Exploit
Pull that chosen arm for every remaining round.

Algorithm · explicit conventions

Textbook Explore-Then-Commit

This version makes the exploration budget, commit time, empirical means, and tie convention explicit before the regret theorem is read.

Empirical winner after exploration. Formula renderer unavailable; readable fallback: Average the first m samples of each arm and commit to the least-encoded arm with the largest empirical mean.\[\widehat\mu_a=\frac1m\sum_{s=1}^{m}X_{a,s},\qquad \widehat a=\min\operatorname*{arg\,max}_{a\in[k]}\widehat\mu_a.\]

input: k arms, horizon n, exploration count m with 1 ≤ m ≤ n/k
for s = 1,…,m: for a = 1,…,k: pull arm a and record X_{a,s}
compute μ̂_a = (1/m) sum_s X_{a,s} for every arm a
set a_hat to the least-encoded empirical-mean maximizer
for every remaining round: pull a_hat and record its reward

Source/Lean boundary. The textbook permits any fixed empirical-mean tie rule. BanditRLlib's canonical generated ETC route fixes round-robin exploration and an explicit first-occurrence/least-encoded commit rule, then proves measurability and expected regret under its bounded or sub-Gaussian arm-law contracts.

Worked example · follow one decision

Follow one two-arm explore–then–commit run

Take two arms, horizon n = 12, and m = 3 exploration pulls per arm. The six exploration rewards below are deliberately small enough to compute by hand.

Explore both arms equally
Round-robin exploration gives each arm three observations before any commitment is made.
Worked example step 1. Formula renderer unavailable; readable fallback: Arm 1 produces rewards 1, 0, 1; arm 2 produces rewards 0, 1, 0 during exploration.\[X_{1,1:3}=(1,0,1),\qquad X_{2,1:3}=(0,1,0).\]
Compare the empirical means
Arm 1 has the larger empirical mean, so the documented least-encoded tie rule is not needed in this run.
Worked example step 2. Formula renderer unavailable; readable fallback: The empirical means are two thirds for arm 1 and one third for arm 2, so the committed arm is arm 1.\[\widehat\mu_1=\frac23,\qquad \widehat\mu_2=\frac13,\qquad \widehat a=1.\]
Commit for the remaining rounds
After six exploration pulls, the policy uses arm 1 for the final six rounds. If the true means are 0.6 and 0.4, the exploration of arm 2 has already paid three gap units; a wrong commit would instead repeat that gap throughout exploitation.
Worked example step 3. Formula renderer unavailable; readable fallback: Six rounds remain; with a gap of 0.2, the three exploratory pulls of arm 2 contribute expected pseudo-regret 0.6.\[n-km=6,\qquad \Delta_2=0.2,\qquad m\Delta_2=0.6.\]

Takeaway. ETC makes one irreversible decision. Increasing m raises the certain exploration cost but makes the empirical winner more reliable, which is exactly the two-term tradeoff in the theorem card.

Scope. The displayed rewards are one illustrative history, not a simulation result. The regret sentence uses hypothetical true means only to explain gap accounting; the source theorem and exact Lean declarations below control the probabilistic assumptions.

Source theorem · faithful restatement

Theorem 6.1 (ETC regret bound)

Original at online pp. 92–93 ↗

The theorem exposes the central ETC tradeoff: more exploration costs regret now but reduces the probability of committing to a wrong arm.

Model: A finite k-armed stochastic bandit whose centered arm rewards are 1-sub-Gaussian.
Assumptions: The exploration length satisfies 1 ≤ m ≤ n/k; each arm is explored m times and empirical-mean ties are broken by a fixed rule.
Algorithm parameters: Horizon n, arm count k, exploration count m, and gaps Δ_i.
Regret notion: Expected frequentist regret R_n of Explore-Then-Commit.
Guarantee: Exploration cost plus the remaining horizon weighted by exponentially small wrong-commit probabilities.

Source mathematical statement. Formula renderer unavailable; readable fallback: ETC regret is bounded by the exploration cost plus the remaining horizon times exponentially small wrong-commit probabilities.\[R_n\le m\sum_i\Delta_i+(n-mk)\sum_i\Delta_i\exp\!\left(-\frac{m\Delta_i^2}{4}\right).\]

BanditRLlib relationship. The local canonical route constructs a measurable generated ETC law and states explicit tie semantics before deriving bounded and sub-Gaussian expected-regret endpoints.

The mathematical content is restated in this site's notation; wording is ours. See online pp. 92–93 in the linked source for the original statement and full assumptions.

Natural-language and Lean side by side

The mathematical readings are explanatory summaries. The exact generated Lean statement and its source link remain authoritative for hypotheses, types, constants, and indexing.

Mathematics ↔ Lean

Deterministic tie-breaking for the commit arm

Lean declarationBanditRLProof.ETC.argmaxCommitOracle_encode_le_of_score_le

Compiled

Plain-English statement. The canonical Rat ETC commit oracle selects the least encoded arm among all arms tying its maximal score.

Mathematical reading. Formula renderer unavailable; readable fallback: The canonical Rat ETC commit oracle selects the least encoded arm among all arms tying its maximal score.\[s(\hat a)\le s(a)\Longrightarrow \operatorname{encode}(\hat a)\le\operatorname{encode}(a).\]

Intuition: The strict-update fold scans arms in canonical order: a strictly better score replaces the current arm, while an equal score leaves the earlier arm in place.
Why it is needed: The generated ETC policy needs deterministic, explicit tie behavior; maximality alone does not identify which maximizing action is selected.
Place in the proof: This deterministic leaf closes the tie-semantics edge between the concrete Rat commit oracle and the canonical measurable generated ETC route.

Proof and Lean reading notes

Proof idea: Identify the fold with Mathlib's first-occurrence List.argmax, compare the selected arm's list index with any tying maximizer using index_of_argmax, and rewrite finRange indices as encodings.
Lean reading notes: The only substantive assumptions are finite Rat scores and 0<K. No measure, independence, MGF, or unique-maximum assumption is introduced.
Teaching dependencies: BanditRLProof.ETC.argmaxCommitOracle

Exact Lean statement

theorem argmaxCommitOracle_encode_le_of_score_le {K : Nat} (hK : 0 < K) (scores : Fin K -> Rat) (a : Fin K) (hscore : scores ((ETC.argmaxCommitOracle hK).choose scores) <= scores a) : Encodable.encode ((ETC.argmaxCommitOracle hK).choose scores) <= Encodable.encode a

Open in the declaration catalog Open source at line 136

Mathematics ↔ Lean

Expected regret of generated Explore-Then-Commit

Lean declarationBanditRLProof.ETC.integral_real_pseudoRegret_explorationArgmaxGeneratedAction_le_canonicalSubGaussianArmPerArmIntegralRegretBoundReal

Compiled

Plain-English statement. For the generated Explore-Then-Commit policy under finite-arm sub-Gaussian reward laws, expected Real pseudo-regret is bounded by the canonical per-arm exploration-plus-commit expression.

Mathematical reading. Formula renderer unavailable; readable fallback: For the generated Explore-Then-Commit policy under finite-arm sub-Gaussian reward laws, expected Real pseudo-regret is bounded by the canonical per-arm exploration-plus-commit expression.\(\mathbb E\bar R_T\le R_{\mathrm{explore}}+\sum_{a\ne a^\star}(T-mK)\Delta_a\,p_a^{\mathrm{tail}}.\)

Intuition: Exploration pays a deterministic cost; exploitation pays only when empirical noise makes the commit oracle choose the wrong arm.
Why it is needed: This is a concrete end-to-end local ETC theorem rather than only a tail lemma or theorem card.
Place in the proof: Together with the generated-law, round-robin, least-tie, and named wrong-commit declarations in the public canary, it closes the scoped local ETC chapter; direct imported-LML identity remains separate.

Proof and Lean reading notes

Proof idea: Prove empirical-mean measurability, reduce a wrong commit to a pairwise deviation event, apply the sub-Gaussian tail contract, and integrate the deterministic regret split.
Lean reading notes: The Real integral is explicit. The bound and every arm-law regularity hypothesis are visible in the Lean statement; no LML theorem card is used as a proof term.
Teaching dependencies: BanditRLProof.pseudoRegret_eq_finset_sum_gap_mul_pullCount

Exact Lean statement

theorem integral_real_pseudoRegret_explorationArgmaxGeneratedAction_le_canonicalSubGaussianArmPerArmIntegralRegretBoundReal {K : Nat} {Context : Type} [MeasurableSpace Context] (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (sigma2 : NNReal) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (hsubG : forall arm, ProbabilityTheory.HasSubgaussianMGF (fun reward : Rat => ((reward : Rat) : Real) - (((model.mean arm : Rat) : Real))) sigma2 (armLaw arm)) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (hexplorationPulls_pos : 0 < spec.explorationPulls) (r : Nat) : let defaultAction := ETC.exploreArm spec 0 let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context := Context) armLaw hprob let policy := fun t => ETC.explorationArgmaxHistoryPolicy spec model t let state := fun t history => ETC.explorationArgmaxHistoryState t history let stepKernel := RewardKernel.historyStepKernelFamily rewardKernel policy context state hcontext (fun t => ETC.measurable_explorationArgmaxHistoryState t) let trajMeasure := ProbabilityTheory.Kernel.trajMeasure (X := fun _ : Nat => Rat) (armLaw defaultAction) stepKernel integral trajMeasure (fun trajectory : RewardTrace Rat => (((pseudoRegret model (ETC.explorationArgmaxGeneratedAction spec model trajectory) (spec.explorationPulls * K + r) : Rat) : Real))) <= ETC.canonicalSubGaussianArmPerArmIntegralRegretBoundReal spec model r sigma2

Open in the declaration catalog Open source at line 1980

Maintainer contract

Open the canonical completion definition and blockers

Complete when a canonical measurable generated ETC law, commit and tie semantics, wrong-commit concentration, and expected-regret endpoint compile under one documented local toolchain, and every claimed upstream compatibility surface is verified exactly.

Remaining blockers

No remaining blocker inside the canonical local ETC scope: the public Book Map canary certifies the generated law, round-robin exploration, Rat first-occurrence/least-encoded tie rule, named wrong-commit concentration, and bounded/sub-Gaussian expected-regret endpoints. Pinned LML material remains theorem-card-only and outside this completion claim.

Chapter implementation status

The compact summary keeps the reading route visible. Open it for source-linked declarations and exact remaining gaps.

Open 3 implementation records3 compiled · 0 partial · 0 blocked · 0 planned

Milestone	Status	Lean declaration	Remaining gap
Canonical sub-Gaussian ETC expected regret	Compiled	`BanditRLProof.ETC.integral_real_pseudoRegret_explorationArgmaxGeneratedAction_le_canonicalSubGaussianArmPerArmIntegralRegretBoundReal`	—
Canonical Rat ETC least-encoded tie rule	Compiled	`BanditRLProof.ETC.argmaxCommitOracle_argmax_finRangeBanditRLProof.ETC.argmaxCommitOracle_encode_le_of_score_le`	—
Local ETC endpoint aligned with the LML theorem card	Compiled	`BanditRLProof.ETC.integral_real_pseudoRegret_explorationArgmaxGeneratedAction_le_canonicalSubGaussianArmPerArmIntegralRegretBoundReal`	Direct imported-LML symbol and toolchain identity remains cross-toolchain work.

Open boundaries

Direct LML symbol integration remains optional cross-toolchain work even though the local canonical chapter route compiles.
The website never upgrades a theorem card into a local proof certificate.

All Lean modules in this chapter

Open the complete module list (37 modules)

Module	Declarations	Project imports	Status
`BanditRLProof.Algorithms.ETC`	8	1	Compiled
`BanditRLProof.Algorithms.ETCArgmaxOracle`	10	1	Compiled
`BanditRLProof.Algorithms.ETCBoundedRewardInfinitePiSource`	7	3	Compiled
`BanditRLProof.Algorithms.ETCBoundedRewardSource`	17	3	Compiled
`BanditRLProof.Algorithms.ETCBoundedRewardSubGaussian`	8	2	Compiled
`BanditRLProof.Algorithms.ETCCenteredDiffCanonicalTail`	3	1	Compiled
`BanditRLProof.Algorithms.ETCCenteredDiffRewardIndependence`	1	1	Compiled
`BanditRLProof.Algorithms.ETCCenteredDiffRewardSubGaussian`	3	2	Compiled
`BanditRLProof.Algorithms.ETCCenteredDiffSubGaussianWitnesses`	2	1	Compiled
`BanditRLProof.Algorithms.ETCCondSubGaussianWitnesses`	24	4	Compiled
`BanditRLProof.Algorithms.ETCCountLemmas`	4	2	Compiled
`BanditRLProof.Algorithms.ETCEmpiricalMean`	6	3	Compiled
`BanditRLProof.Algorithms.ETCEmpiricalMeanMeasurability`	4	3	Compiled
`BanditRLProof.Algorithms.ETCExactSubGaussianTail`	5	2	Compiled
`BanditRLProof.Algorithms.ETCExpectedPullCount`	4	2	Compiled
`BanditRLProof.Algorithms.ETCExpectedRegretAssembly`	4	2	Compiled
`BanditRLProof.Algorithms.ETCFiniteArmRewardLaw`	51	5	Compiled
`BanditRLProof.Algorithms.ETCGeneratedHistoryPolicy`	8	3	Compiled
`BanditRLProof.Algorithms.ETCInfinitePiExpectedRegretAssembly`	27	3	Compiled
`BanditRLProof.Algorithms.ETCMeasurability`	19	2	Compiled
`BanditRLProof.Algorithms.ETCPairwiseCenteredSubGaussianTail`	1	3	Compiled
`BanditRLProof.Algorithms.ETCPairwiseSubGaussianTail`	1	2	Compiled
`BanditRLProof.Algorithms.ETCPairwiseTailContract`	3	2	Compiled
`BanditRLProof.Algorithms.ETCRatArmLawRealKernel`	8	2	Compiled
`BanditRLProof.Algorithms.ETCRealArgmaxTie`	14	1	Compiled
`BanditRLProof.Algorithms.ETCRealEmpiricalMean`	15	2	Compiled
`BanditRLProof.Algorithms.ETCRealHistoryScore`	10	1	Compiled
`BanditRLProof.Algorithms.ETCRealInfinitePiTail`	17	4	Compiled
`BanditRLProof.Algorithms.ETCRealLMLCompat`	2	1	Compiled
`BanditRLProof.Algorithms.ETCRealPrefixLawTransport`	23	2	Compiled
`BanditRLProof.Algorithms.ETCRealSourceAdapter`	1	1	Compiled
`BanditRLProof.Algorithms.ETCRegretLemmas`	8	2	Compiled
`BanditRLProof.Algorithms.ETCSumRewardsDiff`	6	2	Compiled
`BanditRLProof.Algorithms.ETCTrace`	4	2	Compiled
`BanditRLProof.Algorithms.ETCTraceCountLemmas`	9	3	Compiled
`BanditRLProof.Algorithms.ETCWrongCommitCanonicalTail`	1	1	Compiled
`BanditRLProof.Algorithms.ETCWrongCommitRegretAssembly`	1	1	Compiled