Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)
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

Gt:=∑s=1tAsAsT,St:=∑s=1tAsηs(0≤t≤n).

Give each finite real matrix space its entrywise Euclidean topology and corresponding Borel sigma-algebra. Then Vt, bt, Gt, St, and Dt:=det⁡(Vt) are Ft+1-measurable matrix, vector, or real random elements, and the ridge estimate θ^t=Vt−1bt is an Ft+1-measurable Rd-valued random element for every 0≤t≤n.

Facts & Assumptions

Given: The finite-dimensional bandit model's measurable feature vectors, reward noises, and rewards through the finite horizon.

[F1]

Finite-dimensional linear contextual bandit model: As is Fs-measurable, ηs is Fs+1-measurable, Xs=⟨θ∗,As⟩+ηs, and Vt, bt, and θ^t have the displayed formulas.

[F2]
[F3]

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.

[F4]

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.

[F5]

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.

[F6]

Deleted-row-and-column minors, cofactors, the cofactor matrix and the adjugate over a commutative ring: each entry of adj⁡(V) is a signed deleted-row-and-column determinant; for size 1, the empty minor has determinant 1.

[F8]

The ridge information matrix is positive definite and invertible: each Vt is invertible and Dt:=det⁡(Vt)≥λd>0.

[F9]

A continuous map has Borel preimages of Borel sets: a continuous real function has Borel preimages of Borel sets.

[F10]

Rectangular matrix multiplication and the identity matrix In, including zero-sized shapes: each coordinate of a matrix-vector product is a finite sum of products of entries.

Proof

1.1givenF1F2F4

For s≤t, each coordinate of As is Fs-measurable and each coordinate of ηs is Fs+1-measurable; the filtration gives Fs,Fs+1⊆Ft+1. The reward equation and [F4] make Xs measurable at Ft+1. Applying [F4] coordinatewise to the finite sums and products defining Gt, St, Vt, and bt proves that each coordinate is Ft+1-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 t=0 all four are constant.

2.1step 1.1F3F5F8

The determinant Dt is Ft+1-measurable by step 1.1, [F4], and the polynomial formula [F5]. By [F8] its range lies in J=[λd,∞). It is also measurable as a map into J: for every relatively open set J∩U, with U⊆R open, Dt−1(J∩U)=Dt−1(U) because Dt takes values in J.

3.1step 2.1F3F4F5F6F7F8F9

The reciprocal r:J→R, r(x)=1/x, is continuous since λd>0, hence Borel measurable by [F9]. The definition of measurability in [F3] then makes Dt−1=r∘Dt measurable. By [F5]–[F6], every entry of adj⁡(Vt) is measurable; for d=1 it is the constant 1. Since Vt is invertible, [F7] gives adj⁡(Vt)=DtVt−1, so Vt−1=Dt−1adj⁡(Vt) has measurable entries by [F4].

4.1step 1.1step 3.1F2F4F10∎

By [F10], every coordinate of θ^t=Vt−1bt 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 θ^t a measurable random element. At t=0, θ^0=0 is constant. Thus every stated vector and matrix is an Ft+1-measurable random element.

Depends on

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