Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck pass
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

An action set whose linear-mean range exceeds one

Example

Consider one round with dimension d=1, regularization λ=1, feature bound L=2, parameter bound m2=1, and deterministic parameter θ∗=1. Let the context be constant and let the two available actions have scalar features 0 and 2. Use zero reward noise. Both candidate features satisfy the model's bound, but their true means are 0 and 2, so the linear-mean range is 2.

Example references

Finite-dimensional linear contextual bandit model: all candidate features must have norm at most L and the conditional noise MGF must be bounded by eq2/2.

LinUCB has a log-determinant high-probability pseudo-regret bound: the regret guarantee additionally assumes the true-mean range within each available action set is at most 1.

Tor Lattimore and Csaba Szepesvári, Bandit Algorithms, §19.3, Theorem 19.2

Abbasi-Yadkori, Pál, and Szepesvári, Theorem 13

Facts & Assumptions

Given: The one-round finite-dimensional linear contextual bandit instance in the Example.

[F1]

Finite-dimensional linear contextual bandit model: each candidate feature has Euclidean norm at most L, rewards are ⟨θ∗,At⟩+ηt, and the conditional noise MGF bound is eq2/2.

[F2]

LinUCB has a log-determinant high-probability pseudo-regret bound: its stated guarantee requires sup⁡a,b∈At⟨θ∗,a−b⟩≤1.

Verification

1.1givenF1algebra

The candidate features are 0 and 2, so both have absolute value at most L=2. The parameter satisfies ∣θ∗∣=1=m2, and zero noise has conditional MGF E[eqη1∣F1]=1≤eq2/2 for every real q. Thus the instance satisfies the model hypotheses.

2.1givenF1F2step 1.1algebra∎

The true means are θ∗⋅0=0 and θ∗⋅2=2. Consequently sup⁡a,b∈{0,2}θ∗(a−b)=2>1, so the additional range premise of [F2] fails. This example therefore lies outside that theorem's stated guarantee and does not refute its conclusion under its hypotheses.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

24 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources