Double-check local notations in `hoelder.v`

[affeldt-aist]

https://github.com/math-comp/analysis/blob/c5ea0abfda9c1ec4f223ea2e013de20fbf23135f/theories/hoelder.v#L370

Lemmas relying on this specialization should be future proof for when the restriction on the argument of the norm is lifted, i.e., when this becomes Local Notation "'N_ p [ f ]" := (Lnorm mu p f), in particular eminkowski might be a misnommer.

@CohenCyril @proux01 @hoheinzollern @t6s