!4#4465 `lp`

Stream: mathlib4

[Jireh Loreaux]

This is the port of the file containing docs#lp, and this file is named lp_space in mathlib3. What should the name be in mathlib4? LpSpace seems wrong semantically but lpSpace bucks the file naming conventions.

[Jireh Loreaux]

On a separate note: lp has both a CoeOut instance and CoeFun instance. This is consistent with Lean 3, but it strikes me as potentially problematic. Is my suspicion warranted?

[Kevin Buzzard]

(unrelated: now is your chance to write a better docstring for whatever lp ends up being called :-) )

[Eric Wieser]

ℓpSpace?

[Kevin Buzzard]

This really is a small l, to distinguish it from the Lp spaces, so maybe you just have to stick with small l and hang the naming conventions? To do anything else would be making things very ambiguous and weird.

[Heather Macbeth]

Really, we shouldn't rename docs#lp without also renaming docs#pi_Lp and docs#measure_theory.Lp. There is no rhyme or reason to the current naming.

[Jireh Loreaux]

To be clear, I'm not talking about renaming the declaration, only the file name.

[Eric Wieser]

Do we have a summary anywhere of what the difference between these is?

[Heather Macbeth]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Lp.20space/near/265243122

[Jireh Loreaux]

/poll what should be the name of the file analysis/normed_space/lp_space in mathlib4?
lpSpace.lean
LpSpace.lean

[Mauricio Collares]

Eric Wieser said:

ℓpSpace?

EllpSpace :flag_spain:

[Ruben Van de Velde]

LittleLSpace

[Jireh Loreaux]

Is my intuition correct that the L (and hence the l) is for Lebesgue? I don't know the history of the mathematical notation.