Zulip Chat Archive

Stream: general

Topic: Paper on change of variables


Sebastien Gouezel (Jul 23 2022 at 12:53):

I have written a paper on the change of variables formula, that I am supposed to hand over tomorrow. If anyone wants to have a look, comments are most welcome! samplepaper.pdf

Heather Macbeth (Jul 23 2022 at 13:08):

This is very nice both as a write-up of the work and as an exposition of mathlib philosophy. It is already very polished! (Given the subject of the article, there's a pun there ...) The only small suggestion I have is that the standard English name for the "local inverse theorem" is the "inverse function theorem".

Heather Macbeth (Jul 23 2022 at 13:10):

(Oh, and a couple of bibliography entries have bad capitalization.)

Eric Wieser (Jul 23 2022 at 13:45):

I think f ’’ s is a typo for f '' s, but perhaps that's out of your control

Eric Rodriguez (Jul 23 2022 at 15:13):

maybe I'm being nitpicky, but if you have to explain typeclass arguments I think it's definitely worth explaining that even though ℝ × ℝ is "clearly" ℝ² they're nowhere near defeq and the system won't be happy with you saying such a thing, and the proof will be awkward

Eric Rodriguez (Jul 23 2022 at 15:14):

I'm guessing the Gaussian integral is also in Isabelle/HOL, right? how do they get round this issue?

Ruben Van de Velde (Jul 23 2022 at 15:38):

I think"lines of codes" is typically "lines of code"

Johan Commelin (Jul 23 2022 at 16:43):

I just started reading. Typo on page 1:

is that isis that it

Johan Commelin (Jul 23 2022 at 17:08):

Page 8, assumptions that should be checked by the user: do you mean provided by the user?

Johan Commelin (Jul 23 2022 at 17:09):

Aah, ok. I think I understand what you mean. So ignore :this:

Johan Commelin (Jul 23 2022 at 17:26):

Page 14, one should therefore another distance. I think this sentence is a word.

David Wärn (Jul 23 2022 at 17:58):

Page 3, at every x ∈ s then. The then looks out of place to me? But maybe you want some word to separate the maths parts, so I don't know what to write...

Alex J. Best (Jul 23 2022 at 20:39):

"bazaar -> bizarre"

Patrick Massot (Jul 23 2022 at 21:26):

I'm pretty sure he means bazaar. It's referring to https://en.wikipedia.org/wiki/The_Cathedral_and_the_Bazaar

Alex J. Best (Jul 23 2022 at 22:11):

Ok wow today I learned thanks, this is what I get for skim reading :see_no_evil:

Jireh Loreaux (Jul 24 2022 at 06:17):

Page 11, "prominent most" -> "most prominent"

Sebastien Gouezel (Jul 24 2022 at 07:04):

Thanks a lot to all of you, I have implemented all your suggestions!

Rob Lewis (Jul 25 2022 at 18:29):

Heather Macbeth said:

This is very nice both as a write-up of the work and as an exposition of mathlib philosophy.

:+1: this was a really great read!


Last updated: Dec 20 2023 at 11:08 UTC