rename Memℒp to MemLp?

Stream: mathlib4

[Floris van Doorn]

Unicode characters in declaration names are pretty annoying, and I don't see any reason why Memℒp needs to have a unicode character in the name. Shall we just replace the ℒ with a regular L?

Reasons why it is annoying:

• More annoying to type
• docs#MeasureTheory.Memℒp
• No results found here: https://leanprover-community.github.io/mathlib4_docs/404.html#MeasureTheory.Mem%E2%84%92
• The character ℒ / ℒ looks quite different in various fonts (for me, these two occurrences of the same character are displayed very differently)

[Etienne Marion]

I think the reason is that usually ℒp is used to denote the set of functions with integrable power p while Lp is for the quotient set. But I agree this is quite annoying and not very useful.

[Rémy Degenne]

That was the reason, but I agree it's annoying to use and and we should change it.

[Kevin Buzzard]

Do these comments also apply to docs#Memℓp ? (edit: lol at least one of them seems to)

[Yaël Dillies]

I basically never use the docs for anything related to Lp spaces precisely because it's so hard to type

[Floris van Doorn]

Does such a name change require deprecating all lemmas with an ℒ in the name, or is just the definitions sufficient? (I think I know the answer but I don't like it)

[Michael Rothgang]

How difficult would it be to

• make loogle support entering the L well?
• make doc-gen support the same unicode input options?

Deprecating many lemmas is painful, to what extent would this already help?

[Kevin Buzzard]

How difficult would it be to write a script which deprecates all declarations with an ℒ in?

[Yaël Dillies]

The script already exists: scripts/add_deprecations.sh

[Marc Huisinga]

Michael Rothgang said:

How difficult would it be to

• make loogle support entering the L well?
• make doc-gen support the same unicode input options?

Deprecating many lemmas is painful, to what extent would this already help?

Loogle already supports Unicode input.

[Floris van Doorn]

Yaël Dillies said:

The script already exists: scripts/add_deprecations.sh

Oh nice! I didn't know the script, so I did some regex-replace myself. Is the script idempotent? I think I missed a few deprecations.

[Floris van Doorn]

WIP: #22164

[Yaël Dillies]

No, it is not idempotent

[Yury G. Kudryashov]

CC: @Sébastien Gouëzel

[Floris van Doorn]

#22164 builds now, and a speedy review would be appreciated, since it likely rots quickly.

[Michael Rothgang]

Marc Huisinga said:

Michael Rothgang said:

How difficult would it be to make loogle support entering the L well?

Loogle already supports Unicode input.

I know! I guess I have a bug report then, in that I cannot make loogle find results with "Mem𝓛p". Never mind: copy-pasting the name from the docs works. But using \MCL to type a curly L fails, as that is a different unicode L.

[Jireh Loreaux]

The one used in Memℒp is \McL.