DefinitionDefinition: Literature-sourcedProof: 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.

Matrix multiplicative-weights game and update

Definition

For $n \geq 1$ , a round count $T \geq 1$ , and Hermitian losses $M_{1}, \dots, M_{T} \in C^{n \times n}$ with $- I ⪯ M_{t} ⪯ I$ , choose $0 < η \leq 1$ . Define $S_{0} = 0$ , $S_{t} = \sum_{s = 1}^{t} M_{s}$ , $W_{t} = e^{- η S_{t - 1}}$ , and $ρ_{t} = W_{t} / tr (W_{t})$ . The round cost is $tr (M_{t} ρ_{t})$ . The exponential is the finite-dimensional Hermitian spectral functional calculus. Loss matrices, access to them, and the classical or quantum work to construct them are input costs.

Facts & Assumptions

Given: Finite Hermitian loss matrices $M_{1}, \dots, M_{T}$ , a real parameter $0 < η \leq 1$ , and the trace as the diagonal sum.

[F1]

Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely: a finite-dimensional normal operator has an orthonormal eigenbasis.

[F2]

Adjoints satisfy $(S + T)^{*} = S^{*} + T^{*}$ , $(λ T)^{*} = \overline{λ} T^{*}$ , $(S T)^{*} = T^{*} S^{*}$ , and $T^{* *} = T$ and Self-adjoint and normal endomorphisms of a finite-dimensional real or complex inner product space: adjoints distribute over finite sums, and self-adjoint operators are normal.

[F3]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ : $⟨ S x, y ⟩ = ⟨ x, S^{*} y ⟩$ .

[F4]

Real and complex inner-product spaces and their induced length: the inner product is conjugate-symmetric.

[F5]

The spectral functional calculus f(T) for a normal endomorphism: for a normal $S = \sum_{k} λ_{k} P_{k}$ , $f (S) = \sum_{k} f (λ_{k}) P_{k}$ .

[F6]

The real exponential function and the number $e$ by a power series and The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ : $\exp$ is defined on $R$ and $\exp (x) > 0$ for every real $x$ .

[F7]

The trace $tr (A)$ as the sum of the diagonal entries: trace is the sum of diagonal entries.

[F8]

Non-negative and positive operators and Density operator: nonnegative means self-adjoint with nonnegative quadratic form; positive definite means strictly positive quadratic form on nonzero vectors; a density operator is nonnegative with trace one.

[F9]

Trace of a product of Hermitian matrices is real: the trace of a product of Hermitian matrices is real.

Verification

technique · direct

1.1givenF1F2F3F4F5F6F7algebra

Each $S_{t - 1}$ is Hermitian by [F2] and hence normal, so [F1] gives an orthonormal eigenbasis $S_{t - 1} e_{k} = λ_{k} e_{k}$ . For each unit $e_{k}$ , [F3] and [F4] give $λ_{k} = ⟨ S_{t - 1} e_{k}, e_{k} ⟩ = ⟨ e_{k}, S_{t - 1} e_{k} ⟩ = \overline{λ_{k}}$ , so $λ_{k} \in R$ . By [F5] and [F6], the eigenvalues $\exp (- η λ_{k})$ of $W_{t}$ are positive; hence $W_{t}$ is positive definite and [F7] gives $tr (W_{t}) = \sum_{k} \exp (- η λ_{k}) > 0$ . Therefore $ρ_{t}$ is defined.

2.1givenF7F8F9step 1.1algebra∎

Scaling the positive operator $W_{t}$ by its positive trace gives $ρ_{t} ⪰ 0$ , and the diagonal-sum definition of trace gives $tr (ρ_{t}) = tr (W_{t}) / tr (W_{t}) = 1$ . Thus each update is a density matrix by [F8]. Since $M_{t}$ and $ρ_{t}$ are Hermitian, their product has real trace by [F9], so the round cost is a well-defined real number.

Depends on

Used by

Dependency tree · two levels

44 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

https://arxiv.org/pdf/1705.01843v4 (standard reference, not scraped)