Notation for vectors in euclidean space

Stream: mathlib4

[Eric Wieser]

In #17732, I introduce some notation and a delaborator for (WithLp.equiv 2 _).symm ![x, y, z], which avoids traps around computing the sup norm by accident. I feel strongly that we should have some notation, but not about what symbols it should use.

[Eric Wieser]

/poll What should the notation be?

• (WithLp.equiv 2 _).symm ![x, y, z] is fine already
• ![x, y, z], even though this has the wrong type
• !ₑ[1, 2, 3]
• !₂[1, 2, 3]

[Yakov Pechersky]

How about a prefix or postfix e instead of in the middle?

[Yaël Dillies]

I should mention that I'm about to add the L2 norm as a definition with notation ‖x‖_[2]. Maybe that's enough for most people?

[Eric Wieser]

I don't really have any preference for prefix (ᴱ![x, y, z])/postfix(![x, y, z]ᴱ), but those are good alternatives

[Eric Wieser]

Yaël Dillies said:

I should mention that I'm about to add the L2 norm as a definition with notation ‖x‖_[2].

Making this a new definition rather than just notation strikes me as undesirable; is there a reason that you can't use the WithLp machinery?

[Eric Wieser]

Pinging this thread again since some more options have appeared above, and this way people in later time-zones might spot it.

[Eric Wieser]

One criticism I'd level against ![x, y, z]_p is that the applied ![x, y, z]_2 2 is a little confusing

[Eric Wieser]

Based on the poll above clearly disliking the e subscript, I've changed #17732 to support !₂[1, 2, 3], !₀[x, y, z], and in the elaborator but not the delaborator, !ₚ[1, 2, 3]

[Eric Wieser]

I suppose another path here would be to introduce withLp 2 as a much shorter spelling of (WithLp.equiv 2 _).symm

[Violeta Hernández]

Eric Wieser said:

One criticism I'd level against ![x, y, z]_p is that the applied ![x, y, z]_2 2 is a little confusing

What about !_2[x, y, z] then?

[Violeta Hernández]

(not sure if that's allowed notation)

[Eric Wieser]

Eric Wieser said:

Based on the poll above clearly disliking the e subscript, I've changed #17732 to support !₂[1, 2, 3], !₀[x, y, z], and in the elaborator but not the delaborator, !ₚ[1, 2, 3]

Unfortunately this seems to have run into a lean bug relating to the subscript parser that I can't track down.

[Mario Carneiro]

@Eric Wieser do you have a reproduction?

[Eric Wieser]

Only the one in the PR

[Eric Wieser]

The cause is a missing docs#Lean.enableInitializersExecution before pretty much every call to withImportModules

[Eric Wieser]

This thread on parser aliases seems relevant

[Eric Wieser]

#17732 is now passing CI;.

@Frédéric Dupuis, @Kim Morrison , @Richard Copley, @Luigi Massacci , you all voted only for ![1, 2, 3]_p; are you happy with the !ₚ[1, 2, 3] that the PR provides instead?

[Frédéric Dupuis]

Not really: the idea was to be able to use an arbitrary p, not hardcode a few values.

[Nick Ward]

@Eric Wieser I've hacked together a delaborator in #20719 (here) that is inspired by, but slightly less conservative than, that in #17732. Do you think it's worth the effort to make this shared / usable for !ₚ₊₁[1, 2, 3] and other subscript notations?