Stream: math-comp analysis

Topic: Good topics for first PR?


view this post on Zulip Fernando Chu (Mar 31 2023 at 19:21):

Hello, I've been recently learning more about Coq and SSReflect, and wanted to strengthen my knowledge by contributing to this project. Any topics that would be good for a newbie? I just read the Mathematical Components book and I know basic (undergraduate) analysis.

view this post on Zulip Zachary Stone (Mar 31 2023 at 20:04):

Welcome! I've found this to be a great project for learning more about coq, and formalization in general. There's plenty of undergrad analysis we still don't have, so I'm sure there's a suitable topic for you. Of course asking for help is encouraged (more like required. It's tough stuff for all of us!).

Here are some areas I've been thinking about recently. These are definitely challenges, but hopefully rewarding ones.

view this post on Zulip Fernando Chu (Mar 31 2023 at 20:18):

Definitely the third one seams the easiest haha but I'll try to explore at least a bit of each suggestion, thanks!

view this post on Zulip Zachary Stone (Mar 31 2023 at 20:42):

Agreed. I'll think on this a bit more as well. Others should definitely chime in too, if there's an better candidate.

Good luck! Please do reach out here with any questions. Personally, I'm always happy to talk about math, and eager to hear about first-time experiences with the library.

view this post on Zulip Fernando Chu (Mar 31 2023 at 22:04):

hmmm I think there's some basic facts about (natural) logarithms in exp.v (Definition ln x), in fact I think all the useful ones are already there

view this post on Zulip Fernando Chu (Mar 31 2023 at 22:05):

I think only thing that's missing is its integral, or maybe did you mean something else?

view this post on Zulip Alexander Gryzlov (Mar 31 2023 at 22:22):

There are some recent lecture notes specifically about MC-A: https://www.math.nagoya-u.ac.jp/~garrigue/lecture/2022_affeldt/index.html

view this post on Zulip Fernando Chu (Mar 31 2023 at 23:10):

oh they look great, thanks!

view this post on Zulip Zachary Stone (Apr 01 2023 at 16:36):

I think there's some basic facts about (natural) logarithms

Ah, my bad. I totally forgot that existed. Logs of other bases is certainly a nice generalization. Having the example of ln to work from is probably helpful too.

view this post on Zulip Reynald Affeldt (Apr 03 2023 at 08:24):

What about the continuity of x |-> x * ln x?

view this post on Zulip Reynald Affeldt (Apr 03 2023 at 08:30):

(or more generally properties of ln useful to deal with Shannon's entropy)


Last updated: Jun 22 2024 at 15:01 UTC