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 is → is 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