Legacy topic placeholder · setting
Combinatorial bandits
Triggered combinatorial semi-bandit CUCB: actual causal trajectory, nonlinear monotone smooth rewards, approximation oracle and complete Theorems 1-2 independently reviewed under explicit model and analysis deltas. Topic and all-ten 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.
CUCB: reviewed full source-qualified regret chain
Algorithm 1 and both complete performance theorems under CUCB-CONTRACT, with actual primitive feedback, nonlinear scores, fresh oracle and concrete noisy consumers. Independent blind/source/repair acceptance is bound separately from current build and publication validation.
Mapped results independently reviewed with explicit scope differences; topic incomplete.
Combinatorial Multi-Armed Bandit and Its Extension to Probabilistically Triggered Arms · Wei Chen, Yajun Wang, Yang Yuan and Qinshi Wang · 2016
Frozen source provenance
PDF SHA-256: 6a29fc188cd1490c53864eb4f839e572551c171388fc27ba256a7e61424e856c
Compiled source snapshot: 604e4b7011c51d9a65726051bb531ccf3b105df4. The page-wide banner separately reports this site's current Lean gate.
- Observed marginal compatibility is required: arbitrary outcome-dependent censoring is not covered. Fresh measurable oracle and inverse range on needed positive gaps are explicit.
- Distinct selected subsets, nonempty possible-trigger sets and removal of never-triggerable arms; parameterized duplicate-subset application extensions are outside this contract.
- Normalized analysis-only charging repairs mixed p=1/p<1 thresholds; conditional mixing, weighted counting and zero/small-horizon boundaries are explicit. The learner is unchanged.
- The signed benchmark is H alpha beta OPT minus expected actual reward, not ordinary OPT regret. Both Theorem 2 trigger branches retain exact constants and residuals.
- Finite concavity is separately proved for actual counts, not an actual dependency of the current common-cutoff endpoint proof.
- The primary noisy input-dependent oracle model has R(1)=1/4; the supplementary uniform randomized oracle ignores input and is not a learning-improvement example.
- Reading references are not proof edges. Recent-source complete disposition, ICLR evidence and whole-topic acceptance remain incomplete.
Mathematical contract and proof
Finite distinct feasible subsets act on m bounded base arms. The environment produces a mask, outcomes and a nonnegative integrable total reward. For every action a and arm i, law(observe i and value_i in B)=p_i^a D_i(B). This supports adaptive concentration while permitting dependence among arms. Minimum trigger probabilities are derived from actual laws.
At prefix length n, CUCB uses index one for zero observations, otherwise min(empirical mean + sqrt(3 log(n+1)/(2 count)),1). A fixed measurable approximation-oracle kernel draws the action before fresh environment feedback. One infinite causal trajectory serves every horizon; analysis counters and unknown true gaps do not enter the learner.
Let d(a)=alpha OPT-r(a), Delta=max_a max(0,d(a)), and R(H)=H alpha beta OPT-E sum reward. The actual reward identity gives R(H)=E sum d(A_t)-H alpha(1-beta)OPT. This signed credit cancels the oracle-failure charge after taking expectations.
Write ell_H(d,p)=log(H)c(d,p), with u=f^{-1}(d), c(d,1)=6/u^2 and c(d,p)=max(12/(u^2 p),24/p) for p<1. The repaired analysis charges argmin N_i/c(d,p_i). If that arm exceeds its threshold, all possible arms do. Charge is known after the action but before feedback; integrating the actual action mixture produces the trigger tail, with no extra number-of-actions factor.
Theorem 1 gives R(H)<=sum_i [d_i,min ell_H(d_i,min,p_i)+integral from d_i,min to d_i,max of ell_H(x,p_i) dx]+[1+(2+1{p*<1})pi^2/6]m Delta for H>=1. Empty bad-action families contribute zero. Distinct old integer counters and finite layer-cake integration retain the zero-counter residual. Confidence and trigger failures are derived and summed, not assumed.
For f(u)=gamma u^omega, gamma>0 and 0<omega<=1, Theorem 2 gives 2gamma/(2-omega)(6m log H)^(omega/2)H^(1-omega/2)+(1+pi^2/3)m Delta when p*=1. For p*<1 replace 6 by 12/p*, pi^2/3 by pi^2/2, and add sum_i(24 log H/p_i)Delta. A common cutoff and power-tail integration give both rates; H=1 is handled separately.
The concrete 64-atom model has three noisy arms and two distinct two-arm actions, product rewards, actual minimum trigger probabilities (1/2,1,1/2), and positive first-round regret 1/4. Other actual consumers cover a randomized beta=1/2 oracle, full-observation deterministic triggering and a no-bad-action boundary. Canonical links below expose exact statements and proofs.
| Role | Canonical Lean declaration | Source or instance scope |
|---|---|---|
| model | BanditRLProof.CUCB.FeedbackModel | Section 2: primitive triggered feedback; observed-marginal compatibility made explicit |
| model | BanditRLProof.CUCB.SourceModel | Section 2: monotone smooth reward and approximation oracle; inverse-range clarification |
| algorithm | BanditRLProof.CUCB.cucbTrajectory | Algorithm 1: one causal CUCB trajectory, zero initial counts and initial indices one |
| producer | BanditRLProof.CUCB.SourceModel.chargeData_sufficient | Analysis-counter repair: normalized charge choice handles mixed trigger probabilities |
| producer | BanditRLProof.CUCB.FeedbackModel.nice_event_probability | Proof of confidence control from actual primitive laws |
| producer | BanditRLProof.CUCB.FeedbackModel.charged_observation_tail | Proof of charged-trigger concentration under adaptive action selection |
| producer | BanditRLProof.CUCB.SourceModel.approximationRegret_eq_gap_sum | Original signed approximation regret and actual-reward identity |
| producer | BanditRLProof.CUCB.SourceModel.approximationRegret_le_underSampled_add_source_tail | Oracle failure credit cancellation and source tail constants |
| endpoint | BanditRLProof.CUCB.SourceModel.theorem_one_refined_regret | Theorem 1: refined gap-dependent integral bound, with disclosed analysis repair |
| producer | BanditRLProof.CUCB.SourceModel.polynomial_threshold_integral_probabilistic | Theorem 2: mixed-trigger polynomial envelope integrated on actual gap interval |
| producer | BanditRLProof.CUCB.SourceModel.underChargeCount_power_sum_le | Finite concavity obligation on actual counts; separately proved, not used by cutoff endpoint route |
| endpoint | BanditRLProof.CUCB.SourceModel.theorem_two_deterministic | Theorem 2: p*=1 branch, H>=1 including H=1 |
| endpoint | BanditRLProof.CUCB.SourceModel.theorem_two_probabilistic | Theorem 2: p*<1 branch, H>=1 including H=1 |
| canary | BanditRLProof.CUCB.FiniteExample.source | Constructed 64-atom nonlinear noisy model; not a source-paper example |
| canary | BanditRLProof.CUCB.FiniteExample.noisy_each_arm | Each actual arm law has probability of one strictly between zero and one |
| canary | BanditRLProof.CUCB.FiniteExample.regret_one_positive | Actual learning-trajectory R(1)=1/4 |
| canary | BanditRLProof.CUCB.FiniteExample.refined_regret | Concrete full Theorem 1 instance |
| canary | BanditRLProof.CUCB.FiniteExample.probabilistic_regret | Concrete random-trigger Theorem 2 instance |
| canary | BanditRLProof.CUCB.FiniteExample.randomizedSource | Supplementary uniform action oracle with beta=1/2; ignores input |
| canary | BanditRLProof.CUCB.FiniteExample.randomized_probabilistic_regret | Actual signed-regret theorem for supplementary randomized oracle |
| canary | BanditRLProof.CUCB.FiniteExample.deterministic_regret | Noisy full-observation recovery of Theorem 2 |
| canary | BanditRLProof.CUCB.FiniteExample.no_bad_regret | Alpha=1/3 no-bad-action boundary, all horizons |
| reuse | BanditRLProof.Thompson.uniformActionMeasure | Existing shared finite uniform measure used by the concrete sample law and randomized oracle; not an efficiency experiment |