rayleigh_sandwich

The Rayleigh sandwich, formalized — TARGET 4 (enabler) of the LeanPunov stream

Seal

Rung rung-1 · Status sealed · #print axioms for all four public theorems is [propext, Classical.choice, Quot.sound] — no sorryAx (recorded in The machine seal; rung-1 run wf_69fe2268-589, final build 2641 jobs, on the stream note (~/Code/tasks/streams/leanpunov.md)). No interface hypotheses; discharges L2’s assumed QuadSandwich via quadSandwich_matrix — see interfaces.
Links: module index · interface ledger · related lyapunov_comparison, block_lyapunov, stiffness_residual, com_lasalle · sources giordano2019coordinated, khalil1996nonlinear (no wiki page yet) · pin pin_rayleigh.py

Sealed theorems

le_dotProduct_mulVec

Lower bound: $c_1\le {\lambda }_i$ for all $i$ gives $c_1{\mathbf{x}}^{\top }\mathbf{x}\le {\mathbf{x}}^{\top }\mathbf{Kx}$.

dotProduct_mulVec_le

Upper bound: ${\lambda }_i\le c_2$ for all $i$ gives ${\mathbf{x}}^{\top }\mathbf{Kx}\le c_2{\mathbf{x}}^{\top }\mathbf{x}$.

rayleigh_sandwich

The tightest form: ${\lambda }_{\min }{\mathbf{x}}^{\top }\mathbf{x}\le {\mathbf{x}}^{\top }\mathbf{Kx}\le {\lambda }_{\max }{\mathbf{x}}^{\top }\mathbf{x}$ (Rayleigh–Ritz).

quadSandwich_matrix

The QuadSandwich producer on EuclideanSpace ℝ n — L2’s assumed hypothesis, delivered.

Why this theorem, and why now

The Lyapunov layer (L2, (~/Code/vault/lean/Lyapunov.lean)) proves that a Lyapunov function obeying a decrease inequality decays exponentially, and packages the state-level conclusion — lyapunov_norm_sq_exp_decay — behind one hypothesis it does not itself discharge:

$$\text{QuadSandwich}V{c}_1{c}_2:=\forall y,c_1\Vert y{\Vert }^2\le V(y)\le c_2\Vert y{\Vert }^2$$

Every quadratic Lyapunov function in the thesis is of the form $V(\mathbf{y})={\mathbf{y}}^{\top }\mathbf{Ky}$ with $\mathbf{K}$ a symmetric positive-definite inertia or stiffness matrix (the framing paper giordano2019coordinated eq 37 is exactly this, with $\mathbf{K}=\mathrm{diag}(\breve{\mathbf{M}},\breve{\mathbf{K}})$). The statement that such a $V$ is sandwiched between $c_1\Vert \mathbf{y}{\Vert }^2$ and $c_2\Vert \mathbf{y}{\Vert }^2$ is the Rayleigh–Ritz theorem: the quadratic form is trapped between its extreme eigenvalues times the squared norm. This file proves it and hands QuadSandwich back as a ready instance, so the L2 state-level bound is no longer conditional on an unproven hypothesis. It is an enabler: downstream targets consume le_dotProduct_mulVec / dotProduct_mulVec_le by name to bound whatever quadratic form their subsystem produces.

The precise statements

Work over $\mathbb{R}$ with a finite index type $n$; let $\mathbf{K}$ be a real matrix with K.IsHermitian (i.e. symmetric — positive-definiteness is not needed for the sandwich itself, only to guarantee $c_1>0$). Write ${\mathbf{x}}^{\top }\mathbf{Kx}$ as x ⬝ᵥ K *ᵥ x and ${\mathbf{x}}^{\top }\mathbf{x}=\Vert \mathbf{x}{\Vert }^2$ as x ⬝ᵥ x. Let ${\lambda }_i$ be Mathlib’s hK.eigenvalues.

Lower bound (le_dotProduct_mulVec). If $c_1\le {\lambda }_i$ for all $i$, then $c_1{\mathbf{x}}^{\top }\mathbf{x}\le {\mathbf{x}}^{\top }\mathbf{Kx}$.

Upper bound (dotProduct_mulVec_le). If ${\lambda }_i\le c_2$ for all $i$, then ${\mathbf{x}}^{\top }\mathbf{Kx}\le c_2{\mathbf{x}}^{\top }\mathbf{x}$.

Sandwich, tightest form (rayleigh_sandwich, requires $n$ nonempty).
${\lambda }_{\min }{\mathbf{x}}^{\top }\mathbf{x}\le {\mathbf{x}}^{\top }\mathbf{Kx}\le {\lambda }_{\max }{\mathbf{x}}^{\top }\mathbf{x}$
with ${\lambda }_{\min }=\text{univ.inf’}\lambda$, ${\lambda }_{\max }=\text{univ.sup’}\lambda$ the least and greatest eigenvalues.

QuadSandwich producer (quadSandwich_matrix). For any uniform bounds $c_1\le {\lambda }_i\le c_2$, the map $\mathbf{y}\mapsto {\mathbf{y}}^{\top }\mathbf{Ky}$ on EuclideanSpace ℝ n satisfies QuadSandwich (· K ·) c₁ c₂ — the L2 hypothesis, delivered.

The general uniform-bound form is deliberately primary. QuadSandwich needs some pair $(c_1,c_2)$, not necessarily the tightest; keeping the constants free lets a caller plug in whatever bounds its subsystem supplies (e.g. the mass-matrix bounds $\underline{m},\overline{m}$ that stay valid over a whole trajectory), and dodges the empty-index junk value of ${\lambda }_{\min }/{\lambda }_{\max }$. rayleigh_sandwich recovers the textbook ${\lambda }_{\min }\dots {\lambda }_{\max }$ statement as the instantiation $c_1={\lambda }_{\min }$, $c_2={\lambda }_{\max }$.

Source and provenance

The Rayleigh–Ritz variational characterisation of the extreme eigenvalues is standard: Horn & Johnson, Matrix Analysis (2nd ed.), Theorem 4.2.2, and the same bound appears at lemma level in Khalil, Nonlinear Systems as the quadratic bound ${\lambda }_{\min }(P)\Vert x{\Vert }^2\le x^{\top }Px\le {\lambda }_{\max }(P)\Vert x{\Vert }^2$ used throughout its Lyapunov chapter. No coined terminology is introduced.

Scratch work — where the bound comes from

A real symmetric matrix is orthogonally diagonalizable: $\mathbf{K}=\mathbf{U}\mathrm{diag}(\lambda ){\mathbf{U}}^{\top }$ with $\mathbf{U}$ orthogonal ($\mathbf{U}{\mathbf{U}}^{\top }=\mathbf{I}$). Change variables $\mathbf{w}={\mathbf{U}}^{\top }\mathbf{x}$. Then

$${\mathbf{x}}^{\top }\mathbf{Kx}={\mathbf{x}}^{\top }\mathbf{U}\mathrm{diag}(\lambda ){\mathbf{U}}^{\top }\mathbf{x}={\mathbf{w}}^{\top }\mathrm{diag}(\lambda )\mathbf{w}=\sum _i{\lambda }_i{w}_i^2,{\mathbf{x}}^{\top }\mathbf{x}={\mathbf{x}}^{\top }(\mathbf{U}{\mathbf{U}}^{\top })\mathbf{x}={\mathbf{w}}^{\top }\mathbf{w}=\sum _i{w}_i^2.$$

Since each $w_i^2\ge 0$ and $c_1\le {\lambda }_i\le c_2$, comparing the two sums termwise gives $c_1\sum w_i^2\le \sum {\lambda }_i{w}_i^2\le c_2\sum w_i^2$, which is the sandwich. The whole theorem is a diagonalization followed by a termwise scalar inequality; the geometry enters only through $\mathbf{U}{\mathbf{U}}^{\top }=\mathbf{I}$, which preserves the norm.

(All three algebraic facts — the change-of-variables identity, the two sum decompositions, and the sandwich — are SymPy-pinned in (~/Code/vault/lean/pin_rayleigh.py): the identity symbolically for arbitrary $3\times 3$ matrices, the sandwich numerically over 2000 random $5\times 5$ SPD matrices.)

Proof (teacher-verifiable), and how the Lean mirrors it

The Lean proof factors through three private lemmas, matching the scratch work exactly:

1. quad_conj — the load-bearing algebra. For any square real matrices $\mathbf{U},\mathbf{M}$,
   ${\mathbf{x}}^{\top }(\mathbf{UM}{\mathbf{U}}^{\top })\mathbf{x}=({\mathbf{U}}^{\top }\mathbf{x}{)}^{\top }\mathbf{M}({\mathbf{U}}^{\top }\mathbf{x}).$
   This is a pure ring identity — no orthogonality — proved by rewriting matrix–vector associativity (mulVec_mulVec), the dot–matrix–vector adjunction (dotProduct_mulVec), and ${\mathbf{x}}^{\top }\mathbf{U}=({\mathbf{U}}^{\top }\mathbf{x}{)}^{\top }$ (mulVec_transpose). Isolating it this way makes the orthogonality do exactly one job (step 3) and nothing more.

2. spectral_conj — the diagonalization. Mathlib’s IsHermitian.spectral_theorem states $\mathbf{K}=\text{conjStarAlgAut}\mathbf{U}\mathrm{diag}(\iota \circ \lambda )$ with $\iota =$ RCLike.ofReal and $\mathbf{U}=$ hK.eigenvectorUnitary. Peeling the wrappers over $\mathbb{R}$ — Unitary.conjStarAlgAut_apply ($\text{conjStarAlgAut}\mathbf{U}\mathbf{M}=\mathbf{UM}(\star \mathbf{U})$), RCLike.ofReal_real_eq_id ($\iota =\mathrm{id}$ on $\mathbb{R}$), and the trivial-star fact $\star \mathbf{U}={\mathbf{U}}^{\top }$ (Matrix.star_eq_conjTranspose then conjTranspose_eq_transpose_of_trivial, since $\star =\mathrm{id}$ on $\mathbb{R}$) — gives the clean $\mathbf{K}=\mathbf{U}\mathrm{diag}(\lambda ){\mathbf{U}}^{\top }$.

3. rayleigh_sums — the two decompositions ${\mathbf{x}}^{\top }\mathbf{Kx}={\sum }_i{\lambda }_i{w}_i^2$ and ${\mathbf{x}}^{\top }\mathbf{x}={\sum }_i{w}_i^2$, with $\mathbf{w}={\mathbf{U}}^{\top }\mathbf{x}$. The first applies spectral_conj (on the left of the goal only, via conv_lhs, since hK mentions K and a naïve rewrite would fail the motive check) then quad_conj with $\mathbf{M}=\mathrm{diag}(\lambda )$ and mulVec_diagonal. The second uses quad_conj with $\mathbf{M}=\mathbf{I}$ together with orthogonality $\mathbf{UI}{\mathbf{U}}^{\top }=\mathbf{U}{\mathbf{U}}^{\top }=\mathbf{I}$ (Unitary.coe_mul_star_self) — this is the only place orthogonality is used.

The public bounds then rewrite through rayleigh_sums, distribute the constant (Finset.mul_sum), and compare termwise with Finset.sum_le_sum and mul_le_mul_of_nonneg_right … (sq_nonneg _). rayleigh_sandwich instantiates $c_1,c_2$ at Finset.inf'_le / Finset.le_sup'. The QuadSandwich producer bridges the norm once: real_inner_self_eq_norm_sq and EuclideanSpace.inner_eq_star_dotProduct give $\Vert \mathbf{y}{\Vert }^2={\mathbf{y}}^{\top }\mathbf{y}$ (star_trivial kills the conjugation over $\mathbb{R}$), after which the two bounds apply directly.

What is interfaced (nothing) and what is assumed

No interface hypotheses, no sorry. Unlike the L3/L4a topology lemmas, this target has zero named applier-side scaffolding — the eigenvalue bounds $c_1\le {\lambda }_i\le c_2$ are the mathematical content of the hypothesis, not un-formalized machinery. quadSandwich_matrix fixes the Lyapunov function to the concrete matrix quadratic form $\mathbf{y}\mapsto {\mathbf{y}}^{\top }\mathbf{Ky}$ on EuclideanSpace ℝ n; a caller wanting a different (e.g. affine-shifted) $V$ re-instantiates, but the sandwich engine is complete.

Two honest notes for the reviewer:

• The norm in QuadSandwich is the Euclidean norm; the producer is stated on EuclideanSpace ℝ n (not the plain n → ℝ, whose default Pi norm is the sup norm). The core bounds le_dotProduct_mulVec / dotProduct_mulVec_le are stated norm-free on n → ℝ in terms of x ⬝ᵥ x, so they compose with either norm convention.
• Positive-definiteness is stronger than needed: symmetry (IsHermitian) alone gives the sandwich. Matrix.PosDef.isHermitian supplies the hypothesis, and Matrix.PosDef.eigenvalues_pos then licenses a strictly positive $c_1$ when the caller wants the definite lower bound the Lyapunov argument ultimately relies on.

Mathlib stones used

Matrix.IsHermitian.spectral_theorem, .eigenvalues, .eigenvectorUnitary; Unitary.conjStarAlgAut_apply, Unitary.coe_mul_star_self; Matrix.star_eq_conjTranspose, Matrix.conjTranspose_eq_transpose_of_trivial; RCLike.ofReal_real_eq_id; Matrix.mulVec_mulVec, dotProduct_mulVec, mulVec_transpose, mulVec_diagonal, one_mulVec; Finset.mul_sum, Finset.sum_le_sum, Finset.inf'_le, Finset.le_sup', Finset.univ_nonempty; EuclideanSpace.inner_eq_star_dotProduct, real_inner_self_eq_norm_sq, star_trivial.

The machine seal

Rayleigh.lean in this directory holds quad_conj, spectral_conj, rayleigh_sums (private) and the four public results. #print axioms for all four public theorems is [propext, Classical.choice, Quot.sound] — no sorryAx. The build copy lives at ~/lean/leanpunov/Leanpunov/Rayleigh.lean; this directory’s copy is the tracked source of truth, imported into Leanpunov.lean after L4a.

Cost feel. One L2-scale push: ~130 lines, one SymPy pin, four fix cycles (all name/mechanics — Unitary.-qualified conjStarAlgAut_apply, the conv_lhs motive dodge, two redundant closers where simp already discharged the goal). Well inside the stall budget; no wall hit.