Holder vs Hoelder

Stream: mathlib4

[Kim Morrison]

rss-bot said:

chore: rename Holder to Hoelder (mathlib4#16870)

As indicated by https://en.wikipedia.org/wiki/Germanic_umlaut#Substitution, Hölder should be transcribed to Hoelder in ASCII.

Authored-by: YaelDillies (commit)

Seriously? This is not a good idea. The wikipedia page certainly doesn't say "should", and even if it did that wouldn't matter. This is contrary to usual usage in the English mathematical literature.

[Kim Morrison]

But fine, I guess we can make life hard for people out of orthographic pedantry. :woman_shrugging:

[Kim Morrison]

https://books.google.com/ngrams/graph?content=Hoelder+inequality%2CHolder+inequality&year_start=1800&year_end=2022&corpus=en&smoothing=3

:high_five::microphone:

[Matthew Ballard]

We have docs#KaehlerDifferential so signals from the library point this way. (Personally I just assumed this was the policy from this data point and take no opinion.)

If we want consistency, we need a policy. (Even worse in my opinion...)

[Mauricio Collares]

If Google n-gram is the arbiter, then Mathlib should use Hölder in theorem names :) runs

[Kim Morrison]

(No further comment, I'd prefer to let people do whatever they want to do than have a policy discussion about ũmłāůțš.)

[Kim Morrison]

To be honest it's mostly the prescriptivism of claiming that the Wikipedia page says "should" that upset me here. :-)

[Kim Morrison]

Woah, this also had no deprecations. :-) Who approved this anyway. :-)

[Sébastien Gouëzel]

Can we just revert? It will make things much harder to find, and more ugly. My german is good enough that I know the correct spelling and the correct transliteration, but still JordanHoelderLattice looks so much worth than JordanHolderLattice.

[Kevin Buzzard]

Consistency would be nice and we went for Kaehler, but I don't have an opinion (other than consistency would be nice).

[Rémy Degenne]

The lack of deprecations is really not great. Let's revert, reopen the PR, then discuss?
And let's not merge #16947 too quickly.

[Rémy Degenne]

tagging @Bhavik Mehta who just bors merged it

[Bhavik Mehta]

Oh sorry, I had no idea about this discussion

[Bhavik Mehta]

I was under the impression this was a positive change and consistent with existing mathlib usage, and so should be merged. Sorry if I misunderstood!

[Kim Morrison]

Rémy Degenne said:

The lack of deprecations is really not great. Let's revert, reopen the PR, then discuss?
And let's not merge #16947 too quickly.

#16955 chore: revert holder -> hoelder

[Violeta Hernández]

Mauricio Collares said:

If Google n-gram is the arbiter, then Mathlib should use Hölder in theorem names :smile: runs

I'm not opposed to this! If we're freely using Unicode everywhere else, why not extend that to the names of actual people?

[Violeta Hernández]

This is coming from someone with a non-ASCII last name :smile:

[Ruben Van de Velde]

We'll take that into account when we formalize Hernández's theorem :innocent:

[Mario Carneiro]

Violeta Hernández said:

Mauricio Collares said:

If Google n-gram is the arbiter, then Mathlib should use Hölder in theorem names :) runs

I'm not opposed to this! If we're freely using Unicode everywhere else, why not extend that to the names of actual people?

We generally avoid non-ascii in theorem labels specifically, because labels are typed in a lot of places where we don't have as much control to ensure that the unicode input experience is good (like search bars)

[Yaël Dillies]

rss-bot said:

chore: revert holder -> hoelder (mathlib4#16955)

Per https://leanprover.zulipchat.com/#narrow/stream/116290-rss/topic/Recent.20Commits.20to.20mathlib4.3Amaster/near/471490433

Authored-by: semorrison (commit)

I discover this PR only now. If you are going to revert someone's PR, maybe let them know?

[Ruben Van de Velde]

Previous discussion that lead to the revert at https://leanprover.zulipchat.com/#narrow/stream/116290-rss/topic/Recent.20Commits.20to.20mathlib4.3Amaster/near/471484401

[Kexing Ying]

I personally prefer Holder over Hoelder

[Moritz Firsching]

Kim Morrison said:

https://books.google.com/ngrams/graph?content=Hoelder+inequality%2CHolder+inequality&year_start=1800&year_end=2022&corpus=en&smoothing=3

:high_five::microphone:

https://books.google.com/ngrams/graph?content=Hoelder+inequality%2CHolder+inequality%2C+H%C3%B6lder+inequality&year_start=1800&year_end=2022&corpus=en&smoothing=3

[Michael Stoll]

According to Wikipedia, it should really be Rogers' Inequality...

[Ruben Van de Velde]

@Michael Stoll though note that the changes were not about Hölder's inequality, but other work

[Eric Wieser]

Maybe the one takeaway here is that discussions should never happen in #rss ?

[Ruben Van de Velde]

Perhaps one of them, yeah

[Notification Bot]

A message was moved here from #rss > Recent Commits to mathlib4:master by Eric Wieser.

[Notification Bot]

6 messages were moved here from #mathlib4 > Holder should be Hoelder by Ruben Van de Velde.

[Eric Wieser]

Eric Wieser said:

Maybe the one takeaway here is that discussions should never happen in #rss ?

I've gone ahead and moved all the messages I could find here

[Yury G. Kudryashov]

Note that the original renaming PR didn't add deprecated aliases.

[Yury G. Kudryashov]

If you decide to do the renaming (I don't care about spelling), please add the aliases.

[Eric Wieser]

Maybe we could add a @[transliterate] tag which adds oe aliases for the umlaut spellings?

[Ruben Van de Velde]

Do we only want to do this for German names or also for, say, Japanese ones?

[Ruben Van de Velde]

(Do we have anything named after Chebyshev?)

[Yury G. Kudryashov]

Then we start adding different transliteration versions of Cyrillic names...

[Yury G. Kudryashov]

https://en.wikipedia.org/wiki/Alexandroff_extension docs#OnePoint and docs#AlexandrovDiscrete are both named after https://en.wikipedia.org/wiki/Pavel_Alexandrov

[Yury G. Kudryashov]

We have docs#Polynomial.Chebyshev.T

[Andrew Yang]

For the record, as the original author of KaehlerDifferential in mathlib, I have no preference towards Kaehler or Kahler (or maybe Kahler over Kaehler) and this was kind of a random choice.
In fact I called it derivation_module initially and some reviewer suggested the current name.

[Yaël Dillies]

Yury G. Kudryashov said:

Note that the original renaming PR didn't add deprecated aliases.

I think what happened here is that I wanted to do the aliasing after it was decided the PR was a good idea, and somehow it got merged without me having done it

[Yaël Dillies]

For the special case of transliteration from German, there's a clear rule (Germany has rules) so why not follow it?

[Notification Bot]

5 messages were moved from this topic to #mathlib4 > Concepts named after Nazis etc by Yury G. Kudryashov.

[Notification Bot]

A message was moved here from #mathlib4 > Concepts named after Nazis etc by Yury G. Kudryashov.

[Andrew Yang]

I have no preference towards Kaehler or Kahler (or maybe Kahler over Kaehler)

I personally think that language is prescriptive; the right transliteration is the one that could be understood. In this case, both are correct. If we absolutely need to pick a "more correct one", then it would be the one used more often by (mathematical) literature.

[Moritz Firsching]

What about doc comments: Is the general idea here to use the original spelling for languages, which use extension of latin scripts or the same spelling that is used in the source code?
https://github.com/leanprover-community/mathlib4/blob/dacf74d6a54b0e776c97c90f3a1b9e8ef61f596e/Mathlib/RingTheory/WittVector/Teichmuller.lean#L9-L16
does both: in the title we have

# Teichmüller lifts

but a few lines below it reads:

- `WittVector.teichmuller`: the Teichmuller map.

(I was looking up this name while reading #mathlib4 > Concepts named after Nazis etc )

[Violeta Hernández]

Independently of what we do, I think whenever we choose a transliteration, we should be consistent with it. Anyone doing a Ctrl+F for whatever reason shouldn't have to deal with Alexandroff vs Alexandrov

[Violeta Hernández]

In principle I think it'd be really cool to just write the names with Unicode and all in the docstrings, but on the other hand if we ever formalize Green-Tao writing 陶哲軒 might not really be very clear to most of us...

[Violeta Hernández]

Or even, writing Чебышёв for Chebyshev

[Jon Eugster]

Andrew Yang said:

I have no preference towards Kaehler or Kahler (or maybe Kahler over Kaehler)

In this case, both are correct.

I would argue this statement is false. Arguably one of these is the "correct option" (namely ae) and one is the "american" option (namely just dropping all weird looking symbols as if they don't bear meaning) :wink:

Nevertheless, it might still be a valid choice to go for the "incorrect" option, for example because it might be less confusing for some people :)

[Alex Meiburg]

For one example where I have good anecdata, "Schrödinger" is overwhelmingly transliterated as "Schrodinger", not "Schroedinger". Even the many Germans I know spell it Schrodinger when writing in English. One can argue that there is a distinction between the person and the things that bear his name: when confined to the lower 127, prefer "Erwin Schroedinger" for the name, but "Schrodinger operator" and "Schrodinger's cat"; the "Schr[o/oe/ö]dinger–HJW theorem" is a bit of an edge case.

[Andrew Yang]

Jon Eugster said:

Arguably one of these is the "correct option" (namely ae) and one is the "american" option

I might not have made myself clear but this is exactly the statement I'm arguing against. Both are correct in the sense that both are used and understood by a substantial amount of people without friction. (Unless americans are not humans, that is...)

[Eric Wieser]

Perhaps tangential, but the convention is often to take the american spelling of things in software (e.g. "color" in pretty much any language, or Lean's initialize keyword). Though sometime the convention is to stick with a historic typo because it's too late to change (HTTP referer [sic]), so...

[Johan Commelin]

An @[hoöoelderify] attribute could create all the aliases for us.

[Johan Commelin]

Note that I didn't call it hoöoelderize, because it could be hoöoelderise as well :grinning:

[Mario Carneiro]

@[hoöoelderisze]?