Zulip Chat Archive

Stream: new members

Topic: Billy Miao's Introduction and a question about Gram-Schmidt

Jiale Miao (Mar 18 2022 at 17:50):

Hello. I am currently an undergraduate maths student at Imperial College London. I formalised Gram-Schmidt Orthogonalization which seems not in mathlib yet and Professor Kevin Buzzard have looked at my code. I am wondering whether this topic is appropriate for mathlib. @Kevin Buzzard

Johan Commelin (Mar 18 2022 at 17:54):

Welcome! Do you have a link to your code?

Johan Commelin (Mar 18 2022 at 17:55):

These classical matrix algorithms definitely belong in mathlib

Kevin Buzzard (Mar 18 2022 at 18:02):

It's here https://github.com/Biiiilly/Gram_Schmidt_Ortho and we can work on it more before a PR is coming. Billy is a 1st year UG who's been following my course and is now venturing off doing his own stuff. He originally did it for R^n but he's now trying a general inner product space.

Kevin Buzzard (Mar 18 2022 at 18:04):

I am particularly fond of the use of 37 in the construction.

Adam Topaz (Mar 18 2022 at 18:09):

Yeah, that $37$ is commonly overlooked in all informal linear algebra texts.

Kevin Buzzard (Mar 18 2022 at 18:15):

The trick was to avoid the issue that even though we're doing ∑ i in finset.range(k+1), in the definition of GS (k+1), the equation compiler cannot immediately see that i < k+1 so it won't let you use GS i.

In fact @Billy Miao I see now that the base case and the inductive step are the same -- this is really a definition by strong induction. You can do

/-- Gram-Schmidt Process -/
def GS (f : ℕ → E): ℕ → E
| n := f n - ∑ i in finset.range n,
  if h1 : i < n then proj 𝕜 E (GS i) (f n) else f 37

Jiale Miao (Mar 18 2022 at 18:17):

oh yes, that's much better now

Jiale Miao (Mar 18 2022 at 18:22):

I guess I could keep the lemma GS_k_1 since I am gonna use it in the final proof

Eric Wieser (Mar 18 2022 at 19:31):

Presumably getting the full QR decomposition isn't a difficult step from here?

Eric Wieser (Mar 18 2022 at 19:33):

Does summing over fin n avoid the 37?

Kevin Buzzard (Mar 18 2022 at 19:39):

probably you would have to explicitly put i.2 into the local context? (I think it uses assumption to check)

Yaël Dillies (Mar 18 2022 at 23:35):

You will need docs#finset.attach

Eric Wieser (Mar 18 2022 at 23:57):

But ∑ i in (finset.range n).attach is ∑ i : fin n definitionally, isn't it?

Yaël Dillies (Mar 19 2022 at 00:22):

Don't think so (univ : finset {x // x < n} vs univ : finset {x // x ∈ finset.range n}) but I see your point about summing over fin n.

Jiale Miao (Mar 21 2022 at 11:32):

Hello, I want to make a pull request to mathlib. Could somebody give me the permission to push a branch? My username is Biiiilly

Eric Wieser (Mar 21 2022 at 13:19):

Invite sent!

Jiale Miao (Mar 21 2022 at 14:49):

Thank you! Got it

Last updated: Dec 20 2023 at 11:08 UTC