# Finsler's lemma

Finsler's lemma is a mathematical result named after Paul Finsler. It states equivalent ways to express the positive definiteness of a quadratic form Q constrained by a linear form L. Since it is equivalent to another lemmas used in optimization and control theory, such as Yakubovich's S-lemma, Finsler's lemma has been given many proofs and has been widely used, particularly in results related to robust optimization and linear matrix inequalities.

## Statement of Finsler's lemma

Let x ∈ R$^n$, and Q ∈ R$^{nxn}$ and L ∈ R$^{nxn}$ be symmetric matrices. The following statements are equivalent:
* $\displaystyle x^{T}Lx=0{\text{ and }}x\neq 0{\text{ implies }}x^{T}Qx<0.$
* $\exists \mu \in \mathbb {R} :Q-\mu L\prec 0.$

## Variants
### Non-Strict Finsler Lemma

When the matrix L is indefinite, replacing strict inequalities with non-strict ones still maintains the equivalence between the statements of Finsler's lemma. However, if L is not indefinite, additional assumptions are necessary to ensure equivalence between the statements.

### Extra equivalences when L is positive semi-definite

In the particular case that L is positive semi-definite, it is possible to decompose it as L = B$^T$B. The following statements, which are also referred as Finsler's lemma in the literature, are equivalent:
* $x^{T}Qx<0{\text{ for all }}x\in \ker(B)\smallsetminus \{0\}$
* $B^{\perp ^{T}}QB^{\perp }\prec 0$
* $\exists \mu \in \mathbb {R} :Q-\mu B^{T}B\prec 0$
* $\exists X\in \mathbb {R} ^{n\times m}:Q+XB+B^{T}X^{T}\prec 0$

### Matrix Finsler's lemma

There is also a variant of Finsler's lemma for quadratic matrix inequalities, known as matrix Finsler's lemma, which states that the following statements are equivalent for symmetric matrices Q and L belonging to R$^{(l+k)x(l+k)}$:
* $\left[{\begin{array}{l}I\\Z\end{array}}\right]^{\top }Q\left[{\begin{array}{l}I\\Z\end{array}}\right]\succeq 0{\text{ for all }}Z\in \mathbb {R} ^{l\times k}{\text{ such that }}\left[{\begin{array}{l}I\\Z\end{array}}\right]^{\top }L\left[{\begin{array}{l}I\\Z\end{array}}\right]=0$
* $\exists \mu \in \mathbb {R} :Q-\mu L\succeq 0$
under the assumption that
$Q={\begin{bmatrix}Q_{11}&Q_{12}\\Q_{12}^{T}&Q_{22}\end{bmatrix}}$ and $L={\begin{bmatrix}L_{11}&L_{12}\\L_{12}^{T}&L_{22}\end{bmatrix}}$
satisfy the following assumptions:
* Q$_{12}$ = 0 and Q$_{22}$ < 0,
* L$_{22}$ < 0, and L$_{11}$ - L$_{12}$L$_{22}$$^+$L$_{12}$ = 0, and
* there exists a matrix G such that Q$_{11}$ + G$^T$Q$_{22}$G > 0 and L$_{22}$G = L$_{12}$$^T$$_.$

## Generalizations
### Projection lemma

The equivalence between the following statements is also common on the literature of linear matrix inequalities, and is known as the Projection Lemma (or also as Elimination Lemma):
* $B^{\perp ^{T}}QB^{\perp }\prec 0{\text{ and }}C^{T\perp T}QC^{T\perp }\prec 0$
* $\exists X\in \mathbb {R} ^{n\times m}:Q+CXB+B^{T}X^{T}C^{T}\prec 0$
This lemma generalizes one of the Finsler's lemma variants by including an extra matrix C and an extra constraint involving this extra matrix.
It is interesting to note that if the strict inequalities are changed to non-strict inequalities, the equivalence does not hold anymore: only the second statement imply the first statement. Nevertheless, it still possible to obtain the equivalence between the statements under extra assumptions.

### Robust version

Finsler's lemma also generalizes for matrices Q and B depending on a parameter s within a set S. In this case, it is natural to ask if the same variable μ (respectively X) can satisfy $Q(s)-\mu B^{T}(s)B(s)\prec 0$ for all $s\in S$ (respectively, $Q(s)+X(s)B(s)+B^{T}(s)X^{T}(s)\prec 0$). If Q and B depends continuously on the parameter s, and S is compact, then this is true. If S is not compact, but Q and B are still continuous matrix-valued functions, then μ and X can be guaranteed to be at least continuous functions.

## Applications
### Data-driven control

The matrix variant of Finsler lemma has been applied to the data-driven control of Lur'e systems and in a data-driven robust linear matrix inequality-based model predictive control scheme.

### S-Variable approach to robust control of linear dynamical systems

Finsler's lemma can be used to give novel linear matrix inequality (LMI) characterizations to stability and control problems. The set of LMIs stemmed from this procedure yields less conservative results when applied to control problems where the system matrices has dependence on a parameter, such as robust control problems and control of linear-parameter varying systems. This approach has recently been called as S-variable approach and the LMIs stemming from this approach are known as SV-LMIs (also known as dilated LMIs).

### Sufficient condition for universal stabilizability of non-linear systems

A nonlinear system has the universal stabilizability property if every forward-complete solution of a system can be globally stabilized. By the use of Finsler's lemma, it is possible to derive a sufficient condition for universal stabilizability in terms of a differential linear matrix inequality.