average and cond

Stream: mathlib4

[Yury G. Kudryashov]

Should we refactor docs#MeasureTheory.average to use docs#ProbabilityTheory.cond ?

[Yury G. Kudryashov]

Or just make ⨍ ... a notation for the integral w.r.t. μ[|s]/μ[|univ]

[Yaël Dillies]

Is there any API about cond μ univ?

[Yaël Dillies]

I have a closely related issue, namely that I need to talk about the average measure on a type. We have docs#MeasureTheory.count, and I want the measure cond count univ. What is the best way to talk about that?

[Yury G. Kudryashov]

I think that we should use count[|univ] and fill in gaps in API if needed.

[Yury G. Kudryashov]

There is docs#ProbabilityTheory.condCount