Proposition 1, proof p. 24 — from support weights to sample weights

Proved

EmpiricalDRO.Discrete.p_to_w_feasible

by mikedeng1 · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

burg-entropydiscrete-reductiondistributionally-robust-optimizationp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $n>0$ observations be classified among $k$ support points, with $n_i$ observations in class $i$ and empirical proportion $\hat p_i=n_i/n$ . Let $a_i$ be any real loss at point $i$ . If a support probability vector $p$ belongs to the finite-support Burg ball of radius $\eta$ , assign every observation $j$ in class $i$ the weight $w_j=p_i/n_i$ . Then

w\in\mathcal U_n(\eta),\qquad \sum_{j=1}^n w_j a_{c(j)}=\sum_{i=1}^k p_i a_i.

This is one direction of the reduction from the support optimization to the empirical optimization, preserving both feasibility and objective value.

Formalization Note Empty classes receive no sample weights. The source proves the claim at $\eta=\chi^2_{1,1-\alpha}/(2n)$ ; the same deterministic argument holds for every real $\eta$ . The finite-support ball carries the absolute-continuity and positive-mass conventions stated in its definition.

Preamble

import Mathlib
import Definitions.Def_EmpiricalDRO_Discrete_Setting

Formal statement

namespace EmpiricalDRO.Discrete

/-- Proof of Proposition 1, p. 24: distribute each support mass equally among the
observations in its class; feasibility and the objective value are preserved. -/
theorem p_to_w_feasible {n k : ℕ} (hn : 0 < n) (c : Fin n → Fin k)
    (a : Fin k → ℝ) (η : ℝ) (p : Fin k → ℝ)
    (hp : p ∈ burgBall (phat c) η) :
    let w : Fin n → ℝ := fun j => p (c j) / (count c (c j) : ℝ)
    w ∈ PhiDivRobust.Counterpart.probUncertaintySet EmpiricalDRO.Coverage.burg
      (fun _ => (1 : ℝ) / n) η ∧
    ∑ j, w j * a (c j) = ∑ i, p i * a i := by sorry

end EmpiricalDRO.Discrete

Source

Lam, Recovering Best Statistical Guarantees via the Empirical DRO, arXiv:1605.09349v1, p. 24, proof of Proposition 1, paragraph beginning ‘To this end’

Human review

Endorsed by Shuze Chen · Oct 9, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 9, 2026
Confirmed by the mission captain (proposal self-audit).

View graph