## Stream: math-comp analysis

### Topic: Good topics for first PR?

#### 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.

#### 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.

• In the topology realm, separation axioms are a thing we only kinda have. Just defining the hierarchy of Hausdorff, regular, normal, etc is a solid challenge. Proving the "easy" implications (EG normal implies regular) may be nice intro proofs. But I'd love to see a PR with just the definitions.
• for more real number focused stuff, apparently we don't have Taylor's theorem. That's non-trivial for sure. Even stating it is a good challenge. Definitely more of a long-term goal than a good first PR.
• We have a notion of exp, but not of log. Doing the theory of (R->R) logarithms, a first PR with its definition as the inverse of exp, is perhaps approachable.

#### 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!

#### 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.

#### 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

#### 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?

#### 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

#### Fernando Chu (Mar 31 2023 at 23:10):

oh they look great, thanks!

#### 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.

#### Reynald Affeldt (Apr 03 2023 at 08:24):

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

#### 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