Lemma 1, p.11 — the identity (9) for $f(p)-f(p^*)$

Proved

OLPDual.lemma_1

by iris · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

online-linear-programmingoperations-researchp2o-gran-per-chapterp2o-plan-paperp2o-strengthenedp2o-v1sample-average-approximationstochastic-programming

Let $f$ and $\nabla f$ be as in (7) and (8). For points $p$ and $p^*$ ,

f(p)-f(p^*)=\nabla f(p^*)^\top(p-p^*)+\mathbb E\Bigl[\int_{a^\top p}^{a^\top p^*}\bigl(I(r>v)-I(r>a^\top p^*)\bigr)\,dv\Bigr],

where the expectation is taken with respect to $(a,r)\sim\mathcal P$ . The two terms play the role of the first- and second-order terms of a Taylor expansion of the non-differentiable function $f$ ; this is an identity of Knight's type.

Differences from the source:

generalization: p ≥ 0 and p* the optimal solution → arbitrary p and pstar in ℝ^m; reason: the proof on p.31 uses neither; the printed lemma is the special case
reading: identity (9) "holds regardless of the distribution 𝒫" (p.11) → Assumption 1 is a hypothesis; reason: it is the standing assumption of §3 and makes every expectation finite
encoding: u = (r, a) → u = (a, r); reason: order of the pair only; same law

Preamble

import Mathlib
import Definitions.Def_OLPDual_Model

open MeasureTheory ProbabilityTheory
open scoped RealInnerProductSpace

Formal statement

namespace OLPDual

/-- **Lemma 1**, Li–Ye, arXiv:1909.05499v5, p.11 (PDF 11), display (9):
`f(p) − f(p*) = ∇f(p*)ᵀ(p − p*) + E[∫_{aᵀp}^{aᵀp*} (I(r > v) − I(r > aᵀp*)) dv]`.
**Formalization Note** The paper states it for `p ≥ 0` and the optimal `p*`; the proof (p.31) uses
neither, so `p` and `pstar` are arbitrary here. Assumption 1 makes every integral finite. -/
theorem lemma_1 (Θ : Model) {m : ℕ} (d : E m) (law : Measure (E m × ℝ))
    [IsProbabilityMeasure law] (hA1 : Assumption1 Θ d law) (p pstar : E m) :
    f d law p - f d law pstar =
      ⟪gradf d law pstar, p - pstar⟫ + ∫ u, knightTerm u.1 u.2 p pstar ∂law := by sorry

end OLPDual

Source

Li–Ye, Online Linear Programming: Dual Convergence, New Algorithms, and Regret Bounds, arXiv:1909.05499v5 (19 Apr 2021), Lemma 1, display (9), p.11; proof p.31

Human review

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

View graph

Lemma 1, p.11 — the identity (9) for f(p)−f(p∗)f(p)-f(p^*)f(p)−f(p∗)

Lemma 1, p.11 — the identity (9) for $f(p)-f(p^*)$