Prove2Me

Proposition 4.16 (Petersen's lemma), p. 17 — robust strict and non-strict LMIs over F⊤F⩽FˉF^\top F\leqslant\bar F iff C+λEE⊤+λ−1G⊤FˉG<0C+\lambda EE^\top+\lambda^{-1}G^\top\bar FG<0 (⩽0\leqslant0) for some λ>0\lambda>0

Proved
QuadMatIneq.Petersen.proposition_4_16

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

linear-matrix-inequalityp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1petersen-lemmarobust-controls-lemma

Let C∈Rn×nC\in\mathbb R^{n\times n}, E∈Rn×pE\in\mathbb R^{n\times p}, Fˉ∈Rq×q\bar F\in\mathbb R^{q\times q} and G∈Rq×nG\in\mathbb R^{q\times n} with C=C⊤C=C^\top and Fˉ⩾0\bar F\geqslant0, and define the uncertainty set

F:={F∈Rp×q∣F⊤F⩽Fˉ}.\mathcal F:=\{F\in\mathbb R^{p\times q}\mid F^\top F\leqslant\bar F\}.

(a) The following are equivalent:

  • (4.15a) C+EFG+G⊤F⊤E⊤<0C+EFG+G^\top F^\top E^\top<0 for all F∈FF\in\mathcal F;
  • (4.15b) there exists λ>0\lambda>0 such that C+λEE⊤+λ−1G⊤FˉG<0C+\lambda EE^\top+\lambda^{-1}G^\top\bar FG<0.

(b) Suppose that E≠0E\neq0, Fˉ>0\bar F>0 and G≠0G\neq0. Then the following are equivalent:

  • (4.16a) C+EFG+G⊤F⊤E⊤⩽0C+EFG+G^\top F^\top E^\top\leqslant0 for all F∈FF\in\mathcal F;
  • (4.16b) there exists λ>0\lambda>0 such that C+λEE⊤+λ−1G⊤FˉG⩽0C+\lambda EE^\top+\lambda^{-1}G^\top\bar FG\leqslant0.

In display form, part (a) reads

(∀F∈F: C+EFG+G⊤F⊤E⊤<0)  ⟺  ∃ λ>0: C+λEE⊤+λ−1G⊤FˉG<0.\big(\forall F\in\mathcal F:\ C+EFG+G^\top F^\top E^\top<0\big)\iff\exists\,\lambda>0:\ C+\lambda EE^\top+\lambda^{-1}G^\top\bar FG<0 .

Petersen's lemma removes the uncertainty FF from a robust linear matrix inequality at the price of one scalar multiplier λ\lambda; it is a standard tool in robust and data-driven control. The paper recovers both forms from its matrix S-lemmas.

Formalization Note X<0X<0 is (−X).PosDef and X⩽0X\leqslant0 is (−X).PosSemidef, both including symmetry; F⊤F⩽FˉF^\top F\leqslant\bar F is (F̄ − FᵀF).PosSemidef. The multiplier is called lam, required positive, so λ−1\lambda^{-1} is the true inverse. The hypotheses E≠0E\neq0, Fˉ>0\bar F>0, G≠0G\neq0 are attached to part (b) only, as on the page.

Preamble
import Mathlib
import Definitions.Def_QuadMatIneq_Petersen_QMI
import Definitions.Def_QuadMatIneq_Petersen_Setup
Formal statement
namespace QuadMatIneq.Petersen
open Matrix
theorem proposition_4_16 {n p q : ℕ} (C : Matrix (Fin n) (Fin n) ℝ)
    (E : Matrix (Fin n) (Fin p) ℝ) (Fbar : Matrix (Fin q) (Fin q) ℝ)
    (G : Matrix (Fin q) (Fin n) ℝ) (hC : C.IsHermitian) (hFbar : Fbar.PosSemidef) :
    ((∀ F ∈ (uncSet Fbar : Set (Matrix (Fin p) (Fin q) ℝ)),
        (-(C + E * F * G + Gᵀ * Fᵀ * Eᵀ)).PosDef) ↔
      ∃ lam : ℝ, 0 < lam ∧ (-(C + lam • (E * Eᵀ) + lam⁻¹ • (Gᵀ * Fbar * G))).PosDef) ∧
    (E ≠ 0 → Fbar.PosDef → G ≠ 0 →
      ((∀ F ∈ (uncSet Fbar : Set (Matrix (Fin p) (Fin q) ℝ)),
          (-(C + E * F * G + Gᵀ * Fᵀ * Eᵀ)).PosSemidef) ↔
        ∃ lam : ℝ, 0 < lam ∧
          (-(C + lam • (E * Eᵀ) + lam⁻¹ • (Gᵀ * Fbar * G))).PosSemidef)) := by sorry
end QuadMatIneq.Petersen
Source
van Waarde–Camlibel–Eising–Trentelman, arXiv:2203.12959v3, Proposition 4.16 (Petersen's lemma), p. 17
Human review

  • Endorsed by Shuze Chen · Oct 10, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 10, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph