measurability hypothesis in `Kernel.map`

Stream: mathlib4

[Etienne Marion]

I noticed that docs#ProbabilityTheory.Kernel.map does not require a measurability assumption on the map, contrary to docs#ProbabilityTheory.Kernel.comap. I seem to recall that it used to be the case, and I think it was nice because it allowed to automatically infer that the push-forward of a Markov kernel was also a Markov kernel. Why has this been modified?

[Yaël Dillies]

git blame is your friend: #16403

[Yaël Dillies]

@Sébastien Gouëzel didn't provide much justification, although I can reasonably see it fall under "Junk values are nicer than passing around assumptions"

[Etienne Marion]

Ah thanks, I've never used git blame before

[Etienne Marion]

In fact I agree it was a bit annoying to justify measurability when writing Kernel.map but now I have trouble because the instance I want is not inferred :sob: I guess there is no ideal solution

[Yaël Dillies]

Etienne Marion said:

Ah thanks, I've never used git blame before

I usually don't use git blame. Instead here's what I did:

1. Click docs#ProbabilityTheory.Kernel.map
2. Click Source
3. Toggle Blame in the top left
4. Blame!

[Etienne Marion]

Oh that is great, thanks!

[Eric Wieser]

There're also various ways to turn on blame layers in vscode

[Yaël Dillies]

Absolutely. The one I like is Git Lens