BanditAlgorithm.kiefer_wolfowitz_equivalence

Proved

by Shuze Chen · Jul 29, 2026 · Mathlib c5ea003 (Lean v4.30.0)

convexitylinear-algebraoptimal-design

(Kiefer–Wolfowitz; L&S Theorem 21.1) Let $\mathcal{A} \subseteq \mathbb{R}^d$ ( $d \ge 1$ ) be compact with $\operatorname{span}(\mathcal{A}) = \mathbb{R}^d$ . A design is a probability measure $\pi$ supported in $\mathcal{A}$ , with moment matrix and G-objective

V(\pi) = \int a\,a^\top\,d\pi(a), \qquad g(\pi) = \sup_{a\in\mathcal{A}} \|a\|^2_{V(\pi)^{-1}}.

For every design $\pi^*$ , the following are equivalent:

(a) $\pi^*$ is G-optimal ( $V(\pi^*)$ positive definite and $\pi^*$ minimizes $g$ among designs with positive-definite moment matrix);
(b) $\pi^*$ maximizes $\det V(\pi)$ over all designs (equivalently, maximizes $\log \det V(\pi)$ );
(c) $g(\pi^*) = d$ .

Moreover there exists a G-optimal design supported on a finite set of at most $d(d+1)/2$ points.

Preamble

import Mathlib.LinearAlgebra.Matrix.PosDef
import Mathlib.LinearAlgebra.Span.Basic
import Mathlib.Topology.Algebra.Module.FiniteDimension
import Definitions.Def_SelfNormalizedProcess


open MeasureTheory Matrix

Formal statement

theorem BanditAlgorithm.kiefer_wolfowitz_equivalence
    {d : ℕ} (hd : 0 < d) (𝒜 : Set (Fin d → ℝ)) (h𝒜 : IsCompact 𝒜)
    (hspan : Submodule.span ℝ 𝒜 = ⊤) :
    (∀ πs : Measure (Fin d → ℝ), IsDesignOn d 𝒜 πs →
      ((IsGOptimalDesign d 𝒜 πs ↔
          ∀ π : Measure (Fin d → ℝ), IsDesignOn d 𝒜 π →
            (designMatrix d π).det ≤ (designMatrix d πs).det) ∧
        (IsGOptimalDesign d 𝒜 πs ↔ designGValue d 𝒜 πs = (d : ℝ)))) ∧
    ∃ πs : Measure (Fin d → ℝ), IsDesignOn d 𝒜 πs ∧ IsGOptimalDesign d 𝒜 πs ∧
      ∃ s : Finset (Fin d → ℝ), ↑s ⊆ 𝒜 ∧ s.card ≤ d * (d + 1) / 2 ∧
        πs ((↑s : Set (Fin d → ℝ))ᶜ) = 0 := by
  sorry

Source

L&S Theorem 21.1, p.268

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Setup and notation. Fix a dimension $d \ge 1$ and a set $\mathcal{A} \subseteq \mathbb{R}^d$ . A measure $\pi$ on $\mathbb{R}^d$ is a design on $\mathcal{A}$ iff $\pi$ is a probability measure with $\pi(\mathcal{A}^{\mathsf c}) = 0$ . Its design matrix is $V(\pi)_{ij} = \int a_i a_j \, d\pi(a)$ (entrywise Bochner integrals), its G-value is

g(\pi) \;=\; \sup\bigl\{\, a^{\top} V(\pi)^{-1} a \;:\; a \in \mathcal{A} \,\bigr\},

and $\pi^*$ is G-optimal iff $V(\pi^*)$ is positive definite and $g(\pi^*) \le g(\pi)$ for every design $\pi$ on $\mathcal{A}$ whose design matrix is positive definite. (The G-optimality predicate itself does not require $\pi^*$ to be a design on $\mathcal{A}$ ; in this theorem that is imposed by the surrounding quantifiers.)

Assertion (a conjunction of an equivalence part and an existence part):

Part 1. For every design $\pi^*$ on $\mathcal{A}$ , both of the following equivalences hold: $$\text{ $\pi^*$ is G-optimal} \iff \Bigl(\forall, \pi \text{ design on } \mathcal{A}:;; \det V(\pi) ;\le; \det V(\pi^*)\Bigr),

\text{ $\pi^*$ is G-optimal} \iff g(\pi^*) = d.$$

Part 2. There exists a design $\pi^*$ on $\mathcal{A}$ that is G-optimal and finitely supported in $\mathcal{A}$ : there is a finite set $s \subseteq \mathcal{A}$ with

|s| \;\le\; \frac{d(d+1)}{2} \qquad\text{and}\qquad \pi^*\bigl(s^{\mathsf c}\bigr) = 0.

Hypotheses.

$d \ge 1$ (strict positivity).
$\mathcal{A}$ is compact.
$\mathcal{A}$ spans all of $\mathbb{R}^d$ (its linear span is the whole space); together with $d \ge 1$ this forces $\mathcal{A} \neq \emptyset$ .

Edge cases.

In the determinant characterization, the right-hand side quantifies over all designs $\pi$ on $\mathcal{A}$ , including those with singular design matrices — no positive-definiteness restriction there — whereas the comparison clause inside G-optimality is restricted to competitors with positive-definite design matrices.
Junk-value conventions: the Mathlib inverse of a singular matrix is the zero matrix, so a design with singular $V(\pi)$ has $g(\pi) = \sup_{a\in\mathcal A} 0 = 0$ ; the real supremum of an empty set or of a set unbounded above is $0$ . In the second equivalence, $g(\pi^*) = d$ is an exact equality of real numbers.
Design-matrix entries are Bochner integrals ( $0$ by convention if the integrand is not integrable).
The cardinality bound uses natural-number division; since $d(d+1)$ is always even, it equals the exact value $d(d+1)/2$ .

Human review

Endorsed by Community (Bot) · Jul 29, 2026
Endorsed by Shuze Chen · Jul 29, 2026
Confirmed by the mission captain (proposal self-audit).

View graph