Stream: new members

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,
--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):

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

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