Semidefinite Quadratic Forms

Stream: new members

[Daniel Pusicha]

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]

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

[Eric Wieser]

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]

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

[Damiano Testa]

You probably do not need to exclude x = 0 in your quantification.

[Eric Wieser]

(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]

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]

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

[Eric Wieser]

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]

And then just write 0 ≤ Q whenever you want to express "positive semidefinite"

[Yaël Dillies]

0 < Q is always false, right? Nope, it's not!

[Eric Wieser]

0 < Q is "positive semidefinite but not zero", right?