Space before semicolon linter incompatible with variance

Stream: mathlib4

[Yaël Dillies]

Yesterday I PRed a few results about the variance Var[X ; μ] in #28248. Yesterday is also the day I learned that we had a linter for spaces before a semicolon: ; :neutral: What should I do?

[Etienne Marion]

Personnally I have been writing Var[X; mu].

[Yaël Dillies]

But isn't ; supposed to be an infix?

[Damiano Testa]

Not having been educated in France, I find spaces before punctuation very jarring.

[Etienne Marion]

Looking at the variance file, it’s all written without a space, and the notation is defined without a space too.

[Yaël Dillies]

But isn't it supposed to mimic the $X \sim μ$ notation?

[Yaël Dillies]

You don't write $X\!\!\sim μ$, I presume.

[Etienne Marion]

Indeed I don't write that, but that's not how I interpret the notation. To me $X \sim \mu$ means $X$ has law $\mu$ under some probability measure on the domain of $X$, while in Var[X; μ], μ is the measure on the domain of $X$, not its law. So it's more like "the variance of $X$ with respect to the measure $\mu$", which I would write I think $\mathrm{Var}_{\mu}[X]$.

[Yaël Dillies]

If it's the fact that we're using punctuation as an infix that's jarring, maybe we should find a different symbol?

[Kim Morrison]

Var[X; mu] seems not-at-all jarring to me?

[Yaël Dillies]

Yes, but in PFR there's suddenly dk[κ ; μ # η ; ν] and then it's not clear dk[κ; μ # η; ν] is the right choice

[Yaël Dillies]

Sorry, I didn't imagine this would be at all polemical

[Sébastien Gouëzel]

I don't think dk[κ; μ # η; ν]is a problem either.