Orthogonality in mathlib

Stream: maths

[Ricardo Prado Cunha]

I am interested in contributing to mathlib and, out of the trivial targets, orthogonality seems the most tenable to me. Are there any past or current attempts at formalizing this or similar that I should be aware of before trying to do it myself?
Also this is a bit unrelated but why does mathlib prefer to use different branches on the main repository rather than forks?

[Jireh Loreaux]

Re: branches instead of forks: because we want to run our CI automatically and it's easier to work with branches than forks for this.

[Yury G. Kudryashov]

We already have docs#Submodule.IsOrtho

[Yury G. Kudryashov]

And docs#Submodule.orthogonal

[Jireh Loreaux]

Yury, that's for inner product spaces.

[Yury G. Kudryashov]

And the goal here is to talk about orthogonality in the space and the dual space?

[Jireh Loreaux]

I think this is about annihilators, but maybe I'm misunderstanding

[Ricardo Prado Cunha]

The link says that it's about annihilators of a subset of V as a subset of the dual space of V.

[Yury G. Kudryashov]

What about copying the docs#convolution design pattern and define orthogonality w.r.t. a (semi)linear operator?

[Jireh Loreaux]

oof, that seems like a nice approach, but maybe a big refactor. Probably not the kind of thing for a new contributor. But maybe I'm overestimating the pain.

[Anatole Dedecker]

Well for sure we could define that for any pairing (i.e bilinear/sesquilinear form) and then apply it to docs#Module.dualPairing

[Anatole Dedecker]

Wait isn't all of this just docs#Submodule.dualAnnihilator ?

[Anatole Dedecker]

Yeah we've had that since !3#6078...

[Jireh Loreaux]

Lol, so I guess we just need to link it to the undergrad list?

[Ricardo Prado Cunha]

Oh yeah that's definitely it. I wonder why it's still in the TODO list? It seems like we also already have stuff like the orthogonal of the bottom and top subspaces, etc. as desired in the wiki. Is it just outdated?

[Jireh Loreaux]

Busy now, but if no one gets to it in an hour or two I'll make a PR to update the list.

[Anatole Dedecker]

Ricardo Prado Cunha said:

Oh yeah that's definitely it. I wonder why it's still in the TODO list? It seems like we also already have stuff like the orthogonal of the bottom and top subspaces, etc. as desired in the wiki. Is it just outdated?

It is just outdated... Sorry for that!

[Johan Commelin]

If only we could have formally verified todo lists (-;

[Anatole Dedecker]

Tbh we are starting to lack interesting low hanging fruits for first contributions. That means we're doing a good job of course, but I also feel bad for newcomers since it's becoming harder and harder to get something interesting into Mathlib without going into more advanced maths...

[Yury G. Kudryashov]

Sometimes I notice a hole in the API and open a mathlib4 issue instead of patching it.

[Yury G. Kudryashov]

Should we copy labels like t-* and good-first-issue to mathlib4?

[Yury G. Kudryashov]

Examples: #5539, #5462 (needs good math background), #5379, #5395

[Anatole Dedecker]

Ha, that first one might be a good first project indeed

[Ricardo Prado Cunha]

Anatole Dedecker said:

Tbh we are starting to lack interesting low hanging fruits for first contributions. That means we're doing a good job of course, but I also feel bad for newcomers since it's becoming harder and harder to get something interesting into Mathlib without going into more advanced maths...

yeah I'm going to start looking into something else to do. as a rising second-year undergrad even a lot of the trivial problems aren't really accessible to me yet, so I might have to defer contributions for a few semesters.

[Jireh Loreaux]

@Ricardo Prado Cunha you should see the issue #5539 Yury linked above. That's a good option for you, and along similar lines.

[Scott Morrison]

I'm pretty skeptical that we are running out of things undergraduates can do. We might have a labelling / categorising / brainstorming problem...

[Yury G. Kudryashov]

I bet we miss quite a few definitions/theorems about basic combinatorics and geometry.

[Yaël Dillies]

Yes, if you are interested in combinatorics I have many low hanging fruits for you.

[Yury G. Kudryashov]

Can you create a bunch of github issues?

[Chris Hughes]

Scott Morrison said:

I'm pretty skeptical that we are running out of things undergraduates can do. We might have a labelling / categorising / brainstorming problem...

I agree. There's a huge amount of maths around, we should never have a shortage of it for a long time. It just might not be the maths our current contributors are most interested in.

[Yury G. Kudryashov]

While we have material doable by an undergraduate student, I'm not so sure that we have lots of material doable by a 1st year undergraduate. E.g., even to talk about Euclidean geometry, one has to learn about docs#InnerProductSpace.