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.
The ridge estimates and self-normalized sums are measurable
Statement
In the finite-dimensional linear contextual bandit model, put
Give each finite real matrix space its entrywise Euclidean topology and corresponding Borel sigma-algebra. Then , , , , and are -measurable matrix, vector, or real random elements, and the ridge estimate is an -measurable -valued random element for every .
Statement references
Finite-dimensional linear contextual bandit model: the model's features, rewards, filtration, and ridge notation.
The ridge information matrix is positive definite and invertible: is invertible and .
Jiří Lebl, Basic Analysis II, Proposition 8.2.7 and Propositions 8.2.8–8.2.9
Tor Lattimore and Csaba Szepesvári, Bandit Algorithms, §19.2
Facts & Assumptions
Given: The finite-dimensional bandit model's measurable feature vectors, reward noises, and rewards through the finite horizon.
Finite-dimensional linear contextual bandit model: is -measurable, is -measurable, , and , , and have the displayed formulas.
The vector space of by matrices over a field, with entrywise operations and Finite rectangular matrices over a commutative ring, their entries, rows and columns: a matrix is the finite function of its real entries; the entrywise Euclidean coordinates identify with .
A measurable function between measurable spaces and The Borel sigma-algebra of a topological space: a map is measurable when preimages of Borel sets are measurable, and the Borel sigma-algebra is generated by open sets.
Arithmetic and lattice operations preserve measurability whenever they are defined: finite pointwise sums and products of real-valued measurable functions are measurable whenever the operations are defined.
For every fixed finite size at least one, the determinant of a real square matrix is a polynomial in its matrix entries: for each fixed finite matrix size, determinant is a finite polynomial in the entries.
Deleted-row-and-column minors, cofactors, the cofactor matrix and the adjugate over a commutative ring: each entry of is a signed deleted-row-and-column determinant; for size , the empty minor has determinant .
The ridge information matrix is positive definite and invertible: each is invertible and .
A continuous map has Borel preimages of Borel sets: a continuous real function has Borel preimages of Borel sets.
Rectangular matrix multiplication and the identity matrix , including zero-sized shapes: each coordinate of a matrix-vector product is a finite sum of products of entries.
Proof
For , each coordinate of is -measurable and each coordinate of is -measurable; the filtration gives . The reward equation and [F4] make measurable at . Applying [F4] coordinatewise to the finite sums and products defining , , , and proves that each coordinate is -measurable. The Borel sigma-algebra of a finite-dimensional Euclidean vector or matrix space is generated by its coordinate projections: rational open boxes form a countable basis. Thus these maps are measurable random elements. At all four are constant.
The determinant is -measurable by step 1.1, [F4], and the polynomial formula [F5]. By [F8] its range lies in . It is also measurable as a map into : for every relatively open set , with open, because takes values in .
The reciprocal , , is continuous since , hence Borel measurable by [F9]. The definition of measurability in [F3] then makes measurable. By [F5]–[F6], every entry of is measurable; for it is the constant . Since is invertible, [F7] gives , so has measurable entries by [F4].
By [F10], every coordinate of is a finite sum of products of measurable entries from steps 1.1 and 3.1; [F4] makes each coordinate measurable. The coordinate-Borel fact in step 1.1 then makes a measurable random element. At , is constant. Thus every stated vector and matrix is an -measurable random element.
Depends on
- For every fixed finite size at least one, the determinant of a real square matrix is a polynomial in its matrix entries
- The Borel sigma-algebra of a topological space
- Finite-dimensional linear contextual bandit model
- Finite rectangular matrices over a commutative ring, their entries, rows and columns
- Deleted-row-and-column minors, cofactors, the cofactor matrix and the adjugate over a commutative ring
- Rectangular matrix multiplication and the identity matrix $I_n$, including zero-sized shapes
- The vector space $M_{m \times n}(F) := F^{\,m \times n}$ of $m$ by $n$ matrices over a field, with entrywise operations
- A measurable function between measurable spaces
- Every field is a commutative ring with $1 \ne 0$; it is an integral domain, and it is a commutative division ring
- The ridge information matrix is positive definite and invertible
- For every positive-sized square matrix over a commutative ring, $A\operatorname{adj}(A)=\operatorname{adj}(A)A=\det(A)I$
- Arithmetic and lattice operations preserve measurability whenever they are defined
- A continuous map has Borel preimages of Borel sets
- The reals form a field
Used by
Dependency tree · two levels
72 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
- Jiří Lebl, Basic Analysis II: Introduction to Real Analysis, Volume II (standard reference, not scraped)
- Tor Lattimore and Csaba Szepesvári, Bandit Algorithms (standard reference, not scraped)