Prove2Me

Lemma 3 — Minkowski bound on (1n∑i∥[Q^n(xi)]−1∥2)1/2\bigl(\frac1n\sum_i\|[\hat Q_n(x^i)]^{-1}\|^2\bigr)^{1/2}

Proved
CovariateSAA.lemma_3

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

consistencyp2o-gran-per-chapterp2o-plan-paperp2o-strengthenedp2o-v1regressionsample-average-approximationstochastic-programming

For regression estimates Q^n\hat Q_n of Q∗Q^* and data x1,…,xnx^1,\dots,x^n,

(1n∑i=1n∥[Q^n(xi)]−1∥2)1/2≤(1n∑i=1n∥[Q^n(xi)]−1−[Q∗(xi)]−1∥2)1/2+(1n∑i=1n∥[Q∗(xi)]−1∥2)1/2,\Bigl(\frac1n\sum_{i=1}^n\bigl\|[\hat Q_n(x^i)]^{-1}\bigr\|^2\Bigr)^{1/2} \le \Bigl(\frac1n\sum_{i=1}^n\bigl\|[\hat Q_n(x^i)]^{-1}-[Q^*(x^i)]^{-1}\bigr\|^2\Bigr)^{1/2} + \Bigl(\frac1n\sum_{i=1}^n\bigl\|[Q^*(x^i)]^{-1}\bigr\|^2\Bigr)^{1/2},

the norms being induced matrix norms.

Combined with Assumptions 3 and (5d), the lemma shows that the factor (1n∑i∥[Q^n(xi)]−1∥2)1/2\bigl(\frac1n\sum_i\|[\hat Q_n(x^i)]^{-1}\|^2\bigr)^{1/2} in the last term of inequality (10) stays bounded in probability.

Differences from the source:

  • generalization: Q̂_n nonsingular (p.6) and Q* positive definite (p.5) → arbitrary operators, [·]⁻¹ = Ring.inverse; reason: the inequality is the triangle inequality in ℓ² applied to the operator norms and holds for any operators; the paper's case is an instance.
  • encoding: vectors in ℝ^d with the Euclidean norm, matrices Q*(x), Q̂_n(x) with the induced matrix norm, samples i ∈ [n], proj_𝒴 the orthogonal projection → EuclideanSpace ℝ (Fin d), continuous linear maps with the operator norm, i : Fin n (0-indexed), a nearest-point map onto 𝒴; reason: Lean convention; same instances.
Preamble
import Mathlib
import Definitions.Def_CovariateSAA_Setting
Formal statement
namespace CovariateSAA

/-- **Lemma 3** (Kannan, Bayraksan & Luedtke, *Data-Driven Sample Average Approximation with
Covariate Information*, arXiv:2207.13554v1, p.12). We have
`((1/n) Σ ‖[Q̂_n(xⁱ)]⁻¹‖²)^{1/2} ≤ ((1/n) Σ ‖[Q̂_n(xⁱ)]⁻¹ − [Q*(xⁱ)]⁻¹‖²)^{1/2}
  + ((1/n) Σ ‖[Q*(xⁱ)]⁻¹‖²)^{1/2}`.

**Formalization Note** Operator norms; `[·]⁻¹` is `Ring.inverse`, and the inequality is stated
for all estimates and data, with no nonsingularity assumption. -/
theorem lemma_3 {dx dy : ℕ} {Ω : Type*} (D : Data dx dy Ω) (n : ℕ) (ω : Ω) :
    Real.sqrt (empMean n (fun i => ‖Ring.inverse (D.Qhat n ω (D.xs i ω))‖ ^ 2)) ≤
      Real.sqrt (empMean n (fun i =>
        ‖Ring.inverse (D.Qhat n ω (D.xs i ω)) - Ring.inverse (D.Qstar (D.xs i ω))‖ ^ 2)) +
      Real.sqrt (empMean n (fun i => ‖Ring.inverse (D.Qstar (D.xs i ω))‖ ^ 2)) := by sorry

end CovariateSAA
Source
Kannan, Bayraksan & Luedtke, Data-Driven Sample Average Approximation with Covariate Information, arXiv:2207.13554v1, Lemma 3, p.12
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