Legacy topic placeholder · setting
Lipschitz bandits
Source-repaired HOO on a general dissimilarity covering tree: actual causal rewards, dimension-derived all-horizon expected regret, and an arbitrary reward-family interface. Independently reviewed; full topic and ICLR evidence remain incomplete.
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.
HOO: reviewed source-repaired full rate and reward-family interface
Reviewed full HOO chain and reward-family prototype snapshot; production port preserves proof bodies. For each real exponent above the actual dimension, the fixed causal algorithm and one infinite reward law give a positive gamma independent of horizon for all N>=1. Current build validation is reported separately.
Mapped results independently reviewed with explicit scope differences; topic incomplete.
X-Armed Bandits · S. Bubeck, R. Munos, G. Stoltz and C. Szepesvari · 2011
Frozen source provenance
PDF SHA-256: dcbbc42ae1ddc5a21153594a542d593d85b4f18913d9776a16221e2e31be68ef
Compiled source snapshot: 18d30b25e878894ffecf883d3c02d7ebaaa4af03. The page-wide banner separately reports this site's current Lean gate.
- General asymmetric dissimilarity, contained-ball packing and no attained optimum/compactness premise.
- Root initialization, chronological indexing, log(max(N,2)) and extended logzero repairs explicit; representatives and left ties are source-permitted fixed choices.
- Arbitrary arm-indexed probability reward family needs no global-law measurability; countable representative-node kernel preserves actual trajectory.
- Cantor model has infinite arms and non-Dirac distinct-mean rewards, proved dimension<=2; d=3 rate is conservative, not exact dimension or sharpness.
- Reading references are not dependency edges. Recent comparison acceptance and all-topic ICLR evidence remain open; topic incomplete.
Mathematical contract and proof
A1 supplies a measurable binary covering, geometric diameter bounds and pairwise disjoint contained balls; A2 is weak Lipschitz smoothness for a general possibly asymmetric dissimilarity. Rewards are stationary probability laws M_x on [0,1] with mean f(x). The best value is sup f; attainment and compactness are not assumed.
For each real d strictly above the actual (4 nu1/nu2)-near-optimality dimension, there exists gamma>0, independent of N, such that expected actual and pseudo-regret are equal and at most gamma N^((d+1)/(d+2)) log(max(N,2))^(1/(d+2)) for every N>=1. This is an expected-regret statement, not a pathwise bound.
The proof first derives adaptive concentration from the true reward trajectory, then bounds poor-region visits. A1/A2 and the limsup dimension yield a horizon-independent bound on near-optimal node counts. The actual three-way tree partition bounds shallow, near-optimal and poor-branch regret. A geometric sum and an integer depth choice give the displayed rate. Bounded integrability and the actual conditional reward law identify realized and pseudo-regret expectations.
For arbitrary arm-indexed laws define Q(v)=M_(a_v), where a_v is the fixed representative of binary-word node v. The node space is countable, so Q is a measurable Markov kernel without global measurability of x -> M_x. Internally giving X the full sigma algebra lets the existing theorem apply, while preserving all regions, geometry, representatives, dimension and actions. Reducing definitions returns precisely the trajectory driven by Q. For an existing global kernel, the node-law equality is proved by reflexivity.
The family adapter reuses the existing pseudo-regret theorem, actual/pseudo expectation identity and actual-regret theorem. Its public-root canary uses the infinite binary-arm model with non-Dirac rewards and distinct means; dimension<=2 is proved, and d=3 yields the conservative N^(4/5) log(max(N,2))^(1/5) rate. Exact statements and proofs are available through the canonical declaration links below.
| Role | Canonical Lean declaration | Source or instance scope |
|---|---|---|
| model | BanditRLProof.HOO.RegularCovering | A1/A2, Algorithm1, Definitions4-5 and actual countable reward construction |
| algorithm | BanditRLProof.HOO.action | A1/A2, Algorithm1, Definitions4-5 and actual countable reward construction |
| algorithm | BanditRLProof.HOO.trajectory | A1/A2, Algorithm1, Definitions4-5 and actual countable reward construction |
| producer | BanditRLProof.HOO.RegularCovering.nearOptimalNodes_power_bound | A1/A2, Algorithm1, Definitions4-5 and actual countable reward construction |
| endpoint | BanditRLProof.HOO.RegularCovering.expected_pseudoRegret_rate_family | Theorem6 repaired rate / actual expected reward identity |
| endpoint | BanditRLProof.HOO.RegularCovering.expected_actual_eq_pseudoRegret_family | Theorem6 repaired rate / actual expected reward identity |
| endpoint | BanditRLProof.HOO.RegularCovering.expected_actualRegret_rate_family | Theorem6 repaired rate / actual expected reward identity |
| algorithm | BanditRLProof.HOO.Covering.familyNodeLaw | A1/A2, Algorithm1, Definitions4-5 and actual countable reward construction |
| endpoint | BanditRLProof.HOO.CantorModel.expected_actual_rate | Theorem6 repaired rate / actual expected reward identity |