# Zulip Chat Archive

## Stream: new members

### Topic: Semidefinite Quadratic Forms

#### Daniel Pusicha (Jan 21 2022 at 14:50):

Okay here comes a question from a person with a not so deep mathematical background and I hope my head is not ripped off for asking.

In order to get warm with Lean (3) and mathlib I want to formalise a proof that seems easy on paper:

- Having a positive definite quadratic form $x^\top P x$ and a positive semidefinite quadratic form $x^\top S x$
- Then the sum $x^\top P x + x^\top S x = x^\top P' x$ yields a positive definite quadratic form $x^\top P' x$.

The proof to that statement should be very simple as

- positive definiteness for $Q$ is defined in mathlib as $\forall x \neq 0, 0 < Q x$ (and $Q x = 0$ for $x=0$ but I think this is omitted as there is
`quadratic_form.map_zero`

which says`⇑Q 0 = 0`

) - (positive) semidefiniteness for $Q$ is not yet defined in mathlib, but I would describe it as $\forall x \neq 0, 0 \leq Q x$ (and $Q x = 0$ for $x=0$ )

$x^\top P x$ | $x^\top S x$ | $x^\top P' x$ | |
---|---|---|---|

$x=0$ | $0$ | $0$ | $0$ |

$x\neq0$ | $>0$ | $\geq 0$ | $>0$ |

**Note:**

- This is a proof for $x \in \mathbb R^n$ but I learned now that there is a more general definition for quadratic forms $Q$ which I don't know too much about but I assume this proof extends to it

So first of all, I would like to contribute the definition for positive semidefinite quadratic forms

```
/-- A positive semi definite quadratic form is greater equal zero on nonzero vectors. -/
def pos_semi_def (Q₂ : quadratic_form R₂ M) : Prop := (∀ x ≠ 0, 0 ≤ Q₂ x)
```

and what I came up with for the proof

```
lemma pos_def_pos_semi_def_add {Q Q' : quadratic_form R₂ M} (hQ : pos_def Q) (hQ' : pos_semi_def Q') : pos_def (Q+Q') :=
begin
unfold pos_def,
unfold pos_def at hQ,
unfold pos_semi_def at hQ',
intro h1,
intro h2,
rw quadratic_form.add_apply,
--library_search,
exact lt_add_of_pos_of_le (hQ h1 h2) (hQ' h1 h2),
end
```

Here is my sketch in the Lean Web Editor. Probably this can be formalised in a more elegant way and maybe this is not even relevant for mathlib so I would love to hear your feedback. For the future I am interested in Lyapunov stability but that is still a long way (for me and for mathlib)

#### Eric Wieser (Jan 21 2022 at 15:22):

I was thinking about this too - but perhaps we can simply spell positive-semidefinite as `0 ≤ Q`

#### Eric Wieser (Jan 21 2022 at 15:23):

With `Q₁ ≤ Q₂`

defined as `⇑Q₁ ≤ ⇑Q₂`

(which is docs#pi.has_le), which makes `0 ≤ Q`

defeq to `∀ x, 0 ≤ ⇑Q x`

#### Eric Wieser (Jan 21 2022 at 15:25):

We could then change docs#quadratic_form.pos_def.nonneg to use that notation

#### Damiano Testa (Jan 21 2022 at 15:26):

You probably do not need to exclude `x = 0`

in your quantification.

#### Eric Wieser (Jan 21 2022 at 15:34):

(I made a small start on something related in branch#eric-wieser/quadratic_form-preorder a while ago - although looking again, I think only two lines of that are salvageable, and it would be easier to write them from scratch!)

#### Daniel Pusicha (Jan 21 2022 at 15:43):

So when I understand you both correctly you suggest

```
/-- A positive semi definite quadratic form is greater equal zero on nonzero vectors. -/
def pos_semi_def (Q₂ : quadratic_form R₂ M) : Prop := ( 0 ≤ Q₂ )
```

suffices because there are further definitions that give the statement implicitly and therefore making a more "lean" code

#### Daniel Pusicha (Jan 21 2022 at 15:45):

So maybe you can give me some advise how I could proceed

#### Eric Wieser (Jan 21 2022 at 15:48):

I would lean towards something like:

```
lemma coe_injective : @function.injective (quadratic_form R M) (M → R) coe_fn :=
λ q₁ q₂ h, by { cases q₁, cases q₂, congr }
/-- An order on quadratic forms inherited from their order as functions.
Note that `0 ≤ Q` means that `Q` is positive semidefinite, but `0 < Q` does not mean `Q` is positive definite. -/
instance : partial_order (quadratic_form R M) :=
partial_order.lift coe_injective
```

#### Eric Wieser (Jan 21 2022 at 15:49):

And then just write `0 ≤ Q`

whenever you want to express "positive semidefinite"

#### Yaël Dillies (Jan 21 2022 at 15:51):

Nope, it's not!`0 < Q`

is always false, right?

#### Eric Wieser (Jan 21 2022 at 15:54):

`0 < Q`

is "positive semidefinite but not zero", right?

Last updated: Dec 20 2023 at 11:08 UTC