Legacy topic placeholder · setting
Heavy-tailed bandits
Raw-moment sample-index truncation: the unchanged source-radius4/r^-2 policy now has a compiled corrected expected-regret chain with additive5Delta; the conservative actual-policy expected pseudo-regret chain has independent acceptance with explicit source deltas. A complete finite Lean counterexample rejects the literal printed regret coefficient for valid0/-1 arms at2^50; ten reviewed declarations now have shared registry mappings; recent-source proof dependencies and all-topic evidence remain open. A separately sourced Genalti2024 finite-supremum obstruction, real-process adapter and nonempty sharp slice now extend the reviewed map; no full-paper or topic acceptance follows.
Result contract to fill
A separate record is required for each exact model and guarantee. Compare bounds only when assumptions, feedback, metrics and parameter regimes match.
- Exact setting and model class
- Pending source verification
- Assumptions
- Pending source verification
- Feedback structure
- Pending source verification
- Algorithm / method
- Pending source verification
- Regret or other metric
- Pending source verification
- Expectation / high probability
- Pending source verification
- Horizon, dimension and other parameter dependencies
- Pending source verification
- Upper bound and conditions
- Pending source verification
- Lower bound and conditions
- Pending source verification
- Computation, oracle and relaxation requirements
- Pending source verification
- Paper / theorem / version / verification date
- Pending source verification
- Canonical Lean references and completion boundary
- Pending source verification
Three separate evidence ledgers
- Literature results: Mapped source and repairs reviewed within the disclosed scope; remaining source audits are incomplete.
- Lean mapping: Mapped results independently reviewed with explicit differences; topic acceptance remains incomplete.
- Literature open problems: none asserted. Missing formalization is not an open mathematical problem.
Reviewed heavy-tail results in the shared library
Source confidence and actual policy, corrected expected regret, a separate clipping transfer, and a finite printed-coefficient counterexample. These mapped results do not complete the topic. Separately sourced Genalti2024 fixed-horizon supremum obstruction and actual-law adapter are additional reviewed results.
Mapped results independently reviewed with explicit scope differences; topic incomplete.
Bandits with Heavy Tail · Bubeck, Cesa-Bianchi and Lugosi · 2013
Frozen source provenance
PDF SHA-256: df94efa3708dab85063d6c7a04e0812f264c1c6f13a284017eb2efeed5077ef3
Compiled source snapshot: 597ffe493d8839fe73290c2042aa78addec99a1f. The page-wide banner separately reports this site's current Lean gate.
- The actual source-radius4 policy has an explicitly corrected regret guarantee; the printed coefficient is refuted, not accepted.
- Clipping transfer is an estimator adaptation on one action trace, not a corruption-robust regret theorem.
- The finite counterexample uses a fixed permissible deterministic tie rule; no universal randomized-tie certificate is claimed.
- Recent-source audit and all-topic ICLR evidence remain open; the reviewed mappings do not establish topic completion.
- Reading membership is not a proof dependency; the current page banner separately reports whether Lean was rerun for this build.
- The primary source block above covers the BCL results. Genalti2024 Eq5 is a separate positive-scale fixed-horizon obstruction, not an adaptive learning-rate theorem; source https://proceedings.mlr.press/v247/genalti24a.html, PDF SHA25665eceb2cd402baa8c7f5b60d273a103fbd181cf6803a4b7f0d2f4092742fe5b6.
| Role | Canonical Lean declaration | Source or instance scope |
|---|---|---|
| producer | BanditRLProof.HeavyTail.source_truncated_mean_upper_tail | BCL Lemma1: radius4; closed-event/common-mean generalizations |
| producer | BanditRLProof.HeavyTail.source_truncated_mean_lower_tail | BCL Lemma1: lower-tail sign counterpart |
| algorithm | BanditRLProof.HeavyTail.SourcePolicy.robustAction | BCL Figure1: causal history policy; explicit deterministic ties and initialization |
| producer | BanditRLProof.HeavyTail.SourcePolicy.robustMean_upper_tail_sum | Source schedule: new signed finite budget2 repair |
| producer | BanditRLProof.HeavyTail.SourcePolicy.robustMean_lower_tail_sum | Source schedule: new signed finite budget2 repair |
| endpoint | BanditRLProof.HeavyTail.SourcePolicy.robust_expected_regret | Explicit corrected coefficient for unchanged policy; all natural horizons; not printed constant |
| endpoint | BanditRLProof.HeavyTail.adaptive_corrupted_clipped_mean_tail | Reserved clipping adaptation: same consumed prefix, outer measure; no corrupted-policy regret |
| endpoint | BanditRLProof.HeavyTail.observed_corrupted_clipped_mean_tail | Clipping adaptation on one observed action trace |
| endpoint | BanditRLProof.HeavyTail.SourceCounterexample.literal_printed_bound_false | Finite refutation of BCL printed coefficient; deterministic permitted ties, Dirac0/-1, T=2^50 |
| model | BanditRLProof.HeavyTail.SourceCounterexample.kernel_raw_moment | Admissible raw second moments of finite counterexample |
| endpoint | BanditRLProof.HeavyTail.GenaltiAudit.normalized_sSup_ne_top | Genalti2024 Eq5 obstruction: enlarged trace-law class, u>0, finite T |
| producer | BanditRLProof.HeavyTail.GenaltiAudit.process_value_mem | Genalti2024 Eq1 adapter: actual measurable actions and actual image law |
| canary | BanditRLProof.HeavyTail.GenaltiAudit.normalized_sSup_two_eq | Genalti2024 raw-moment class: K2epsilon1 universal cap sharp across policies |